Demonstrates state with multiple variables and hidden state.

rocq-demo/rocq_hdl.v

@@ -77,3 +77,95 @@ Module simple_register.
     apply induct1.
   Qed.
 End simple_register.
+
+(*  The same circuit as above, but with an additional output register.
+    The output is asserted to be always false, but no such restriction
+    is made on the inner register, a "hidden" state. It creates a
+    difficulty for induction: there are unreacheable valid states that
+    leads to invalid states. A two step induction solves the problem. *)
+Module hidden_state.
+  (*  Demonstrate state with several (two) variables. *)
+  Record S :=
+  { a: bool
+  ; b: bool
+  }.
+  (*  Both registers start at zero (false). *)
+  Definition initial (s: S) :=
+    a s = false /\ b s = false.
+  (*  Just b is constrained to be zero (false) *)
+  Definition assert (s: S) :=
+    b s = false.
+  (*  "a" keeps its previous value, "b" copies "a". *)
+  Definition t (s1 s2 : S) :=
+    a s2 = a s1 /\ b s2 = a s1.
+  (*  Base case in one step. *)
+  Theorem base1:
+    forall s0,
+    initial s0 -> assert s0.
+  Proof.
+    unfold initial, assert.
+    intros s0 [_ H].
+    apply H.
+  Qed.
+  (*  Try proving the inductive case in one step. *)
+  Theorem induct1:
+    forall s0 s1,
+    assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold t, assert.
+    intros s0 s1 A T.
+    destruct T as [_ Tb].
+    transitivity (a s0). apply Tb.
+  Abort.
+  (*  Ops, we reach a dead-end. Maybe it's not provable after all?
+      Try proving its negation by finding a counter-example. *)
+  Theorem not_induct1:
+    not (forall s0 s1,
+    assert s0 -> t s0 s1 -> assert s1).
+  Proof.
+    unfold not, assert, t.
+    intros H.
+    specialize H with (s0 := {|a := true; b := false|}).
+    simpl in H.
+    specialize H with (s1 := {|a := true; b := true|}).
+    simpl in H.
+    discriminate H. reflexivity. auto.
+  Qed.
+  (*  Indeed, a valid state where "a" is one (true) leads to
+      an invalid state. Try one more step. *)
+  Theorem base2:
+    forall s0 s1,
+    initial s0 -> assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    intros s0 s1 [Ia _] _ [_ Tb].
+    unfold assert.
+    transitivity (a s0). apply Tb.
+    apply Ia.
+  Qed.
+  Theorem induct2:
+    forall s0 s1 s2,
+    assert s0 -> t s0 s1 -> assert s1 -> t s1 s2 -> assert s2.
+  Proof.
+    intros s0 s1 s2 A0 [T0a T0b] A1 [T1a T1b].
+    unfold assert in *.
+    transitivity (a s1). apply T1b.
+    transitivity (a s0). apply T0a.
+    transitivity (b s1). symmetry. apply T0b.
+    apply A1.
+  Qed.
+  (* Success! Two steps indeed work. *)
+
+  (* Example: all states reacheable in two steps are valid *)
+  Example two_steps_valid:
+    forall s0 s1 s2,
+    initial s0 -> t s0 s1 -> t s1 s2 -> assert s2.
+  Proof.
+    intros s0 s1 s2.
+    intros Hi T01.
+    apply induct2 with (s0 := s0).
+    - apply base1. apply Hi.
+    - apply T01.
+    - apply base2 with (s0 := s0).
+      apply Hi. apply base1. apply Hi. apply T01.
+  Qed.
+End hidden_state.