Coq library work for proofs:

* rename state fields to avoid clash with regstate type
* use rewriting to automate some proofs

1 files changed, 130 insertions, 109 deletions

diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index 54cf45cc..c07016dc 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -1,19 +1,22 @@
 Require Import Sail2_values Sail2_prompt_monad Sail2_prompt Sail2_state_monad Sail2_state Sail2_state Sail2_state_lifting.
 Require Import Sail2_state_monad_lemmas.
 
+Local Open Scope equiv_scope.
+
 (* Monad lifting *)
 
-Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} {s} :
-  liftState r (bind m f) s = bindS (liftState r m) (fun x => liftState r (f x)) s.
-revert s. induction m; simpl.
-all: try (intros; unfold seqS; rewrite bindS_assoc; auto using bindS_ext_cong).
-all: try auto.
-* intro s.
-  rewrite bindS_returnS_left.
-  reflexivity.
+Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} :
+  liftState r (bind m f) === bindS (liftState r m) (fun x => liftState r (f x)).
+induction m; simpl; autorewrite with state; auto using bindS_cong.
 Qed.
 Hint Rewrite liftState_bind : liftState.
 
+(* TODO: I want a general tactic for this, but abstracting the hint db out
+   appears to break.
+   This does beta reduction when no rules apply to try and allow more rules to apply
+   (e.g., the application of f to x in the above lemma may introduce a beta redex). *)
+Ltac rewrite_liftState := rewrite_strat topdown (choice (progress try hints liftState) progress eval cbn beta).
+
 Lemma liftState_return Regval Regs A E {r : Sail2_values.register_accessors Regs Regval} {a :A} :
   liftState (E:=E) r (returnm a) = returnS a.
 reflexivity.
@@ -30,7 +33,7 @@ Lemma Value_liftState_Run:
 
 lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
 *)
-Lemma liftState_if_distrib {Regs Regval A E r x y} {c : bool} :
+Lemma liftState_if_distrib Regs Regval A E {r x y} {c : bool} :
   @liftState Regs Regval A E r (if c then x else y) = if c then liftState r x else liftState r y.
 destruct c; reflexivity.
 Qed.
@@ -98,52 +101,51 @@ Lemma liftState_maybe_fail Regs Regval A E r msg x :
   @liftState Regs Regval A E r (maybe_fail msg x) = maybe_failS msg x.
 destruct x; reflexivity.
 Qed.
-Lemma liftState_and_boolM Regs Regval E r x y s :
-  @liftState Regs Regval _ E r (and_boolM x y) s = and_boolS (liftState r x) (liftState r y) s.
+Lemma liftState_and_boolM Regs Regval E r x y :
+  @liftState Regs Regval _ E r (and_boolM x y) === and_boolS (liftState r x) (liftState r y).
 unfold and_boolM, and_boolS.
 rewrite liftState_bind.
-apply bindS_ext_cong; auto.
+apply bindS_cong; auto.
 intros. rewrite liftState_if_distrib.
 reflexivity.
 Qed.
-Lemma liftState_and_boolMP Regs Regval E P Q R r x y s H :
-  @liftState Regs Regval _ E r (@and_boolMP _ _ P Q R x y H) s = and_boolSP (liftState r x) (liftState r y) s.
+Lemma liftState_and_boolMP Regs Regval E P Q R r x y H :
+  @liftState Regs Regval _ E r (@and_boolMP _ _ P Q R x y H) === and_boolSP (liftState r x) (liftState r y).
 unfold and_boolMP, and_boolSP.
 rewrite liftState_bind.
-simpl.
-apply bindS_ext_cong; auto.
-intros [[|] [A]] s' ?.
+apply bindS_cong; auto.
+intros [[|] [A]].
 * rewrite liftState_bind;
   simpl;
-  apply bindS_ext_cong; auto;
-  intros [a' A'] s'' ?;
+  apply bindS_cong; auto;
+  intros [a' A'];
   rewrite liftState_return;
   reflexivity.
 * rewrite liftState_return.
   reflexivity.
 Qed.
 
-Lemma liftState_or_boolM Regs Regval E r x y s :
-  @liftState Regs Regval _ E r (or_boolM x y) s = or_boolS (liftState r x) (liftState r y) s.
+Lemma liftState_or_boolM Regs Regval E r x y :
+  @liftState Regs Regval _ E r (or_boolM x y) === or_boolS (liftState r x) (liftState r y).
 unfold or_boolM, or_boolS.
 rewrite liftState_bind.
-apply bindS_ext_cong; auto.
+apply bindS_cong; auto.
 intros. rewrite liftState_if_distrib.
 reflexivity.
 Qed.
-Lemma liftState_or_boolMP Regs Regval E P Q R r x y s H :
-  @liftState Regs Regval _ E r (@or_boolMP _ _ P Q R x y H) s = or_boolSP (liftState r x) (liftState r y) s.
+Lemma liftState_or_boolMP Regs Regval E P Q R r x y H :
+  @liftState Regs Regval _ E r (@or_boolMP _ _ P Q R x y H) === or_boolSP (liftState r x) (liftState r y).
 unfold or_boolMP, or_boolSP.
 rewrite liftState_bind.
 simpl.
-apply bindS_ext_cong; auto.
-intros [[|] [A]] s' ?.
+apply bindS_cong; auto.
+intros [[|] [A]].
 * rewrite liftState_return.
   reflexivity.
 * rewrite liftState_bind;
   simpl;
-  apply bindS_ext_cong; auto;
-  intros [a' A'] s'' ?;
+  apply bindS_cong; auto;
+  intros [a' A'];
   rewrite liftState_return;
   reflexivity.
 Qed.
@@ -154,18 +156,15 @@ Hint Rewrite liftState_throw liftState_assert liftState_exit liftState_exclResul
              liftState_or_boolM liftState_or_boolMP
            : liftState.
 
-Lemma liftState_try_catch Regs Regval A E1 E2 r m h s :
-  @liftState Regs Regval A E2 r (try_catch (E1 := E1) m h) s = try_catchS (liftState r m) (fun e => liftState r (h e)) s.
-revert s.
-induction m; intros; simpl;
-try solve
+Lemma liftState_try_catch Regs Regval A E1 E2 r m h :
+  @liftState Regs Regval A E2 r (try_catch (E1 := E1) m h) === try_catchS (liftState r m) (fun e => liftState r (h e)).
+induction m; intros; simpl; autorewrite with state;
+solve
 [ auto
-| unfold seqS;
-  erewrite try_catchS_bindS_no_throw; intros;
+| erewrite try_catchS_bindS_no_throw; intros;
   only 2,3: (autorewrite with ignore_throw; reflexivity);
-  apply bindS_ext_cong; auto
+  apply bindS_cong; auto
 ].
-rewrite try_catchS_throwS. reflexivity.
 Qed.
 Hint Rewrite liftState_try_catch : liftState.
 
@@ -175,25 +174,26 @@ reflexivity.
 Qed.
 Hint Rewrite liftState_early_return : liftState.
 
-Lemma liftState_catch_early_return (*[liftState_simp]:*) Regs Regval A E r m s :
-  liftState (Regs := Regs) r (@catch_early_return Regval A E m) s = catch_early_returnS (liftState r m) s.
+Lemma liftState_catch_early_return (*[liftState_simp]:*) Regs Regval A E r m :
+  liftState (Regs := Regs) r (@catch_early_return Regval A E m) === catch_early_returnS (liftState r m).
 unfold catch_early_return, catch_early_returnS.
-autorewrite with liftState.
+rewrite_liftState.
 apply try_catchS_cong; auto.
 intros [a | e] s'; auto.
 Qed.
 Hint Rewrite liftState_catch_early_return : liftState.
 
-Lemma liftState_liftR Regs Regval A R E r m s :
-  liftState (Regs := Regs) r (@liftR Regval A R E m) s = liftRS (liftState r m) s.
-unfold liftR, liftRS. autorewrite with liftState.
-apply try_catchS_cong; auto.
+Lemma liftState_liftR Regs Regval A R E r m :
+  liftState (Regs := Regs) r (@liftR Regval A R E m) === liftRS (liftState r m).
+unfold liftR, liftRS.
+rewrite_liftState.
+reflexivity.
 Qed.
 Hint Rewrite liftState_liftR : liftState.
 
-Lemma liftState_try_catchR Regs Regval A R E1 E2 r m h s :
-  liftState (Regs := Regs) r (@try_catchR Regval A R E1 E2 m h) s = try_catchRS (liftState r m) (fun x => liftState r (h x)) s.
-unfold try_catchR, try_catchRS. autorewrite with liftState.
+Lemma liftState_try_catchR Regs Regval A R E1 E2 r m h :
+  liftState (Regs := Regs) r (@try_catchR Regval A R E1 E2 m h) === try_catchRS (liftState r m) (fun x => liftState r (h x)).
+unfold try_catchR, try_catchRS. rewrite_liftState.
 apply try_catchS_cong; auto.
 intros [r' | e] s'; auto.
 Qed.
@@ -204,25 +204,25 @@ Lemma liftState_bool_of_bitU_nondet Regs Regval :
   by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
 Hint Rewrite liftState_bool_of_bitU_nondet : liftState.
 *)
-Lemma liftState_read_memt Regs Regval A B E H rk a sz r s :
-  liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) s = read_memtS rk a sz s.
+Lemma liftState_read_memt Regs Regval A B E H rk a sz r :
+  liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) === read_memtS rk a sz.
 unfold read_memt, read_memt_bytes, read_memtS, maybe_failS. simpl.
-apply bindS_ext_cong; auto.
-intros [byte bit] s' valIn.
+apply bindS_cong; auto.
+intros [byte bit].
 destruct (option_map _); auto.
 Qed.
 Hint Rewrite liftState_read_memt : liftState.
 
-Lemma liftState_read_mem Regs Regval A B E H rk asz a sz r s :
-  liftState (Regs := Regs) r (@read_mem Regval A B E H rk asz a sz) s = read_memS rk a sz s.
+Lemma liftState_read_mem Regs Regval A B E H rk asz a sz r :
+  liftState (Regs := Regs) r (@read_mem Regval A B E H rk asz a sz) === read_memS rk a sz.
 unfold read_mem, read_memS, read_memtS. simpl.
 unfold read_mem_bytesS, read_memt_bytesS.
 repeat rewrite bindS_assoc.
-apply bindS_ext_cong; auto.
-intros [ bytes | ] s' valIn; auto. simpl.
-apply bindS_ext_cong; auto.
-intros [byte bit] s'' valIn'.
-rewrite bindS_returnS_left. autorewrite with liftState.
+apply bindS_cong; auto.
+intros [ bytes | ]; auto. simpl.
+apply bindS_cong; auto.
+intros [byte bit].
+rewrite bindS_returnS_left. rewrite_liftState.
 destruct (option_map _); auto.
 Qed.
 Hint Rewrite liftState_read_mem : liftState.
@@ -253,15 +253,15 @@ Lemma bindS_rw_left Regs A B E m1 m2 (f : A -> monadS Regs B E) s :
 intro H. unfold bindS. rewrite H. reflexivity.
 Qed. 
 
-Lemma liftState_read_reg_readS Regs Regval A E reg get_regval' set_regval' s :
+Lemma liftState_read_reg_readS Regs Regval A E reg get_regval' set_regval' :
   (forall s, map_bind reg.(of_regval) (get_regval' reg.(name) s) = Some (reg.(read_from) s)) ->
-  liftState (Regs := Regs) (get_regval', set_regval') (@read_reg _ Regval A E reg) s = readS (fun x => reg.(read_from) (regstate x)) s.
+  liftState (Regs := Regs) (get_regval', set_regval') (@read_reg _ Regval A E reg) === readS (fun x => reg.(read_from) (ss_regstate x)).
 intros.
-unfold read_reg. simpl. unfold readS.
+unfold read_reg. simpl. unfold readS. intro s.
 erewrite bindS_rw_left. 2: {
   apply bindS_returnS_left.
 }
-specialize (H (regstate s)).
+specialize (H (ss_regstate s)).
 destruct (get_regval' _ _) as [v | ]; only 2: discriminate H.
 rewrite bindS_returnS_left.
 simpl in *.
@@ -269,15 +269,15 @@ rewrite H.
 reflexivity.
 Qed.
 
-Lemma liftState_write_reg_updateS Regs Regval A E get_regval' set_regval' reg (v : A) s :
+Lemma liftState_write_reg_updateS Regs Regval A E get_regval' set_regval' reg (v : A) :
   (forall s, set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)) ->
-  liftState (Regs := Regs) (Regval := Regval) (E := E) (get_regval', set_regval') (write_reg reg v) s = updateS (fun s => {| regstate := (write_to reg v s.(regstate)); memstate := s.(memstate); tagstate := s.(tagstate) |}) s.
-intros.
+  liftState (Regs := Regs) (Regval := Regval) (E := E) (get_regval', set_regval') (write_reg reg v) === updateS (fun s => {| ss_regstate := (write_to reg v s.(ss_regstate)); ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |}).
+intros. intro s.
 unfold write_reg. simpl. unfold readS, seqS.
 erewrite bindS_rw_left. 2: {
   apply bindS_returnS_left.
 }
-specialize (H (regstate s)).
+specialize (H (ss_regstate s)).
 destruct (set_regval' _ _) as [v' | ]; only 2: discriminate H.
 injection H as H1.
 unfold updateS.
@@ -299,42 +299,59 @@ lemma liftState_iter[liftState_simp]:
   "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs"
   by (auto simp: iter_def iterS_def liftState_simp)
 *)
-Lemma liftState_foreachM Regs Regval A Vars E (xs : list A) (vars : Vars) (body : A -> Vars -> monad Regval Vars E) r s :
-  liftState (Regs := Regs) r (foreachM xs vars body) s = foreachS xs vars (fun x vars => liftState r (body x vars)) s.
-revert vars s.
+Lemma liftState_foreachM Regs Regval A Vars E (xs : list A) (vars : Vars) (body : A -> Vars -> monad Regval Vars E) r :
+  liftState (Regs := Regs) r (foreachM xs vars body) === foreachS xs vars (fun x vars => liftState r (body x vars)).
+revert vars.
 induction xs as [ | h t].
 * reflexivity.
-* intros vars s. simpl.
-  autorewrite with liftState.
-  apply bindS_ext_cong; auto.
+* intros vars. simpl.
+  rewrite_liftState.
+  apply bindS_cong; auto.
 Qed.
 Hint Rewrite liftState_foreachM : liftState.
 
-Lemma foreachS_cong {A RV Vars E} xs vars f f' s :
-  (forall a vars s, f a vars s = f' a vars s) ->
-  @foreachS A RV Vars E xs vars f s = foreachS xs vars f' s.
+Lemma foreachS_cong {A RV Vars E} xs vars f f' :
+  (forall a vars, f a vars === f' a vars) ->
+  @foreachS A RV Vars E xs vars f === foreachS xs vars f'.
 intro H.
-revert s vars.
+revert vars.
 induction xs.
 * reflexivity.
 * intros. simpl.
-  apply bindS_ext_cong; auto.
+  rewrite H.
+  apply bindS_cong; auto.
 Qed.
 
-Lemma liftState_genlistM Regs Regval A E r f n s :
-  liftState (Regs := Regs) r (@genlistM A Regval E f n) s = genlistS (fun x => liftState r (f x)) n s.
-unfold genlistM, genlistS.
-autorewrite with liftState.
+Add Parametric Morphism {Regs A Vars E : Type} : (@foreachS A Regs Vars E)
+  with signature eq ==> eq ==> equiv ==> equiv as foreachS_morphism.
 apply foreachS_cong.
-intros; autorewrite with liftState.
-apply bindS_ext_cong; auto.
+Qed.
+
+(*Tactic Notation "sail_rewrite" ident(hintdb) := rewrite_strat topdown (choice (hints hintdb) progress eval cbn beta).
+Ltac sail_rewrite hintdb := rewrite_strat topdown (choice (hints hintdb) progress eval cbn beta).*)
+
+Lemma liftState_genlistM Regs Regval A E r f n :
+  liftState (Regs := Regs) r (@genlistM A Regval E f n) === genlistS (fun x => liftState r (f x)) n.
+unfold genlistM, genlistS.
+rewrite_liftState.
+reflexivity.
 Qed.
 Hint Rewrite liftState_genlistM : liftState.
 
-Lemma liftState_choose_bools Regs Regval E descr n r s :
-  liftState (Regs := Regs) r (@choose_bools Regval E descr n) s = choose_boolsS n s.
+Add Parametric Morphism {A RV E : Type} : (@genlistS A RV E)
+  with signature equiv ==> eq ==> equiv as genlistS_morphism.
+intros f g EQ n.
+unfold genlistS.
+apply foreachS_cong.
+intros m vars.
+rewrite EQ.
+reflexivity.
+Qed.
+
+Lemma liftState_choose_bools Regs Regval E descr n r :
+  liftState (Regs := Regs) r (@choose_bools Regval E descr n) === choose_boolsS n.
 unfold choose_bools, choose_boolsS.
-autorewrite with liftState.
+rewrite_liftState.
 reflexivity.
 Qed.
 Hint Rewrite liftState_choose_bools : liftState.
@@ -347,16 +364,14 @@ Lemma liftState_bools_of_bits_nondet[liftState_simp]:
 Hint Rewrite liftState_choose_bools : liftState.
 *)
 
-Lemma liftState_internal_pick Regs Regval A E r (xs : list A) s :
-  liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) s = internal_pickS xs s.
+Lemma liftState_internal_pick Regs Regval A E r (xs : list A) :
+  liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) === internal_pickS xs.
 unfold internal_pick, internal_pickS.
 unfold choose.
-autorewrite with liftState.
-apply bindS_ext_cong.
-* autorewrite with liftState.
-  reflexivity.
-* intros.
-  destruct (nth_error _ _); auto.
+rewrite_liftState.
+apply bindS_cong; auto.
+intros.
+destruct (nth_error _ _); auto.
 Qed.
 Hint Rewrite liftState_internal_pick : liftState.
 
@@ -372,8 +387,9 @@ rewrite app_nil_r.
 reflexivity.
 Qed.
 
-Lemma liftRS_bindS Regs A B R E (m : monadS Regs A E) (f : A -> monadS Regs B E) s :
-  @liftRS B R Regs E (bindS m f) s = bindS (liftRS m) (fun x => liftRS (f x)) s.
+Lemma liftRS_bindS Regs A B R E (m : monadS Regs A E) (f : A -> monadS Regs B E) :
+  @liftRS B R Regs E (bindS m f) === bindS (liftRS m) (fun x => liftRS (f x)).
+intro s.
 unfold liftRS, try_catchS, bindS, throwS, returnS.
 induction (m s) as [ | [[a | [msg | e]] t]].
 * reflexivity.
@@ -480,20 +496,24 @@ Local Opaque _limit_reduces.
 Ltac gen_reduces :=
   match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end.
 
-Lemma liftState_whileM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s :
-  liftState (Regs := RV) r (whileMT vars measure cond body) s = whileST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
+(* TODO: rewrite_liftState is performing really badly here.  We could add liftState_if_distrib
+   to the hint db, but then it starts failing in a way that causes the whole rewriting to fail. *)
+
+Lemma liftState_whileM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) :
+  liftState (Regs := RV) r (whileMT vars measure cond body) === whileST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)).
 unfold whileMT, whileST.
 generalize (measure vars) as limit. intro.
-revert vars s.
+revert vars.
 destruct (Z.le_decidable 0 limit).
 * generalize (Zwf_guarded limit) as acc.
   apply Wf_Z.natlike_ind with (x := limit).
   + intros [acc] *; simpl.
-    autorewrite with liftState.
-    apply bindS_ext_cong; auto.
-    intros. rewrite liftState_if_distrib.
-    destruct a; autorewrite with liftState; auto.
-    apply bindS_ext_cong; auto.
+    match goal with |- context [Build_ArithFact _ ?prf] => generalize prf; intros ?Proof end.
+    rewrite_liftState.
+    setoid_rewrite liftState_if_distrib.
+    apply bindS_cong; auto.
+    destruct a; rewrite_liftState; auto.
+    apply bindS_cong; auto.
     intros. destruct (_limit_reduces _). simpl.
     reflexivity.
   + clear limit H.
@@ -553,16 +573,17 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
   qed auto
 qed*)
 
-Lemma liftState_untilM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s :
-  liftState (Regs := RV) r (untilMT vars measure cond body) s = untilST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
+Lemma liftState_untilM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) :
+  liftState (Regs := RV) r (untilMT vars measure cond body) === untilST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)).
 unfold untilMT, untilST.
 generalize (measure vars) as limit. intro.
-revert vars s.
+revert vars.
 destruct (Z.le_decidable 0 limit).
 * generalize (Zwf_guarded limit) as acc.
   apply Wf_Z.natlike_ind with (x := limit).
-  + intros [acc] *; simpl.
-    autorewrite with liftState.
+  + intros [acc] * s; simpl.
+(* TODO    rewrite_liftState.*)
+autorewrite with liftState.
     apply bindS_ext_cong; auto.
     intros. autorewrite with liftState.
     apply bindS_ext_cong; auto.