Simplifications to proof

3 files changed, 15 insertions, 18 deletions

diff --git a/src/verilog/Test.v b/src/verilog/Test.v
index 5fd6d07..9e13bf6 100644
--- a/src/verilog/Test.v
+++ b/src/verilog/Test.v
@@ -95,20 +95,14 @@ Lemma manual_simulation :
        (State test_output_module (add_assoclist 7%positive (32'h"3") empty_assoclist)
               empty_assoclist test_fextclk 2 (32'h"3")).
 Proof.
-  apply step_module with (assoc1 := empty_assoclist)
-                         (nbassoc := (add_assoclist 7%positive (32'h"3") empty_assoclist)); auto.
-  apply mis_stepp_Cons with (s1 := State test_output_module empty_assoclist (add_assoclist 7%positive (32'h"3") empty_assoclist) test_fextclk 1%nat (32'h"1")).
+  eapply step_module; auto.
+  eapply mis_stepp_Cons; auto.
   apply mi_stepp_Valways_ff.
-  apply stmnt_runp_Vcond_true with (f := test_fextclk 1%nat)
-                                   (assoc := empty_assoclist)
-                                   (vc := 1'h"1"); auto.
+  eapply stmnt_runp_Vcond_true; auto.
   apply get_state_fext_assoc.
-  apply erun_Vbinop with (lv := 1'h"1")
-                         (rv := 1'h"1")
-                         (oper := veq)
-                         (EQ := EQ_trivial (1'h"1")); auto.
-  apply erun_Vinputvar; auto.
-  apply erun_Vlit.
+  eapply erun_Vbinop; auto.
+  apply erun_Vinputvar; simpl. auto.
+  apply erun_Vlit. simpl. unfold ZToValue. simpl. instantiate (1 := eq_refl (vsize (1'h"1"))). auto.
   eapply stmnt_runp_Vnonblock. simpl. auto.
   apply erun_Vlit.
   auto.
@@ -135,6 +129,5 @@ Proof.
   eapply mis_stepp_Cons.
   apply mi_stepp_Vdecl.
   apply mis_stepp_Nil.
-  Unshelve.
-  exact 0%nat.
+  auto. Unshelve. exact 0%nat.
 Qed.
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 39d1832..61f2652 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -101,8 +101,6 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 
 (** ** Arithmetic operations *)
 
-Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined.
-
 Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
 intros; subst; assumption. Defined.
 
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 756dc12..399bff7 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -281,6 +281,7 @@ Inductive expr_runp : fext -> assoclist -> expr -> value -> Prop :=
       expr_runp fext assoc fs vf ->
       valueToBool vc = false ->
       expr_runp fext assoc (Vternary c ts fs) vf.
+Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
   : res A :=
@@ -412,11 +413,12 @@ Inductive state_fext_assoc : state -> fext * assoclist -> Prop :=
 | get_state_fext_assoc :
   forall c assoc nbassoc f cycle pc,
   state_fext_assoc (State c assoc nbassoc f cycle pc) (f cycle, assoc).
+Hint Constructors state_fext_assoc : verilog.
 
 Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
-| stmnt_run_Vskip:
+| stmnt_runp_Vskip:
     forall s, stmnt_runp s Vskip s
-| stmnt_run_Vseq:
+| stmnt_runp_Vseq:
     forall st1 st2 s0 s1 s2,
     stmnt_runp s0 st1 s1 ->
     stmnt_runp s1 st2 s2 ->
@@ -473,6 +475,7 @@ Inductive stmnt_runp: state -> stmnt -> state -> Prop :=
     stmnt_runp (State c assoc nbassoc f cycle pc)
                (Vnonblock lhs rhs)
                (State c assoc nbassoc' f cycle pc).
+Hint Constructors stmnt_runp : verilog.
 
 (*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
   let run := fun st ls =>
@@ -503,6 +506,7 @@ Inductive mi_stepp : state -> module_item -> state -> Prop :=
 | mi_stepp_Vdecl :
     forall s lhs rhs,
     mi_stepp s (Vdecl lhs rhs) s.
+Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : state -> list module_item -> state -> Prop :=
 | mis_stepp_Cons :
@@ -513,6 +517,7 @@ Inductive mis_stepp : state -> list module_item -> state -> Prop :=
 | mis_stepp_Nil :
     forall s,
     mis_stepp s nil s.
+Hint Constructors mis_stepp : verilog.
 
 Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist :=
   PositiveMap.add r v assoc.
@@ -614,6 +619,7 @@ Inductive step : state -> state -> Prop :=
     assoc!(fst m.(mod_return)) = Some result ->
     step (State m assoc empty_assoclist f cycle stvar)
          (Finishstate result).
+Hint Constructors step : verilog.
 
 (*Inductive initial_state (m: module): state -> Prop :=
 | initial_state_intro: