Clean up proofs

9 files changed, 170 insertions, 149 deletions

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 6f602fc..da046f3 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -74,8 +74,6 @@ Ltac solve_by_inverts n :=
 
 Ltac solve_by_invert := solve_by_inverts 1.
 
-Ltac invert x := inversion x; subst; clear x.
-
 Ltac destruct_match :=
   match goal with
   | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:?
@@ -86,10 +84,10 @@ Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try cong
 
 Ltac nicify_hypotheses :=
   repeat match goal with
-         | [ H : ex _ |- _ ] => invert H
-         | [ H : Some _ = Some _ |- _ ] => invert H
+         | [ H : ex _ |- _ ] => inv H
+         | [ H : Some _ = Some _ |- _ ] => inv H
          | [ H : ?x = ?x |- _ ] => clear H
-         | [ H : _ /\ _ |- _ ] => invert H
+         | [ H : _ /\ _ |- _ ] => inv H
          end.
 
 Ltac nicify_goals :=
@@ -169,7 +167,7 @@ Ltac substpp :=
   repeat match goal with
          | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] =>
            let EQ := fresh "EQ" in
-           learn H1 as EQ; rewrite H2 in EQ; invert EQ
+           learn H1 as EQ; rewrite H2 in EQ; inv EQ
          | _ => idtac
          end.
 
@@ -251,3 +249,24 @@ Lemma forall_ptree_true:
 Proof.
   apply ptree_forall.
 Qed.
+
+Ltac decomp_logicals h :=
+  idtac;match type of h with
+  | @ex _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_logicals h1
+  | @sig _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_logicals h1
+  | @sig2 _ (fun x => _) (fun _ => _) => let x' := fresh x in
+                                         let h1 := fresh in
+                                         let h2 := fresh in
+                                         destruct h as [x' h1 h2];
+                                         decomp_logicals h1;
+                                         decomp_logicals h2
+  | @sigT _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_logicals h1
+  | @sigT2 _ (fun x => _) (fun _ => _) => let x' := fresh x in
+                                          let h1 := fresh in
+                                          let h2 := fresh in
+                                          destruct h as [x' h1 h2]; decomp_logicals h1; decomp_logicals h2
+  | and _ _ => let h1 := fresh in let h2 := fresh in destruct h as [h1 h2]; decomp_logicals h1; decomp_logicals h2
+  | iff _ _ => let h1 := fresh in let h2 := fresh in destruct h as [h1 h2]; decomp_logicals h1; decomp_logicals h2
+  | or _ _ => let h' := fresh in destruct h as [h' | h']; [decomp_logicals h' | decomp_logicals h' ]
+  | _ => idtac
+  end.
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 07a9649..5ce7c0a 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -1463,6 +1463,11 @@ Proof.
   rewrite RTree.gso; auto.
 Qed.
 
+Lemma forest_reg_pred:
+  forall (f : forest) w dst dst',
+    (f #r dst <- w) #p dst' = f #p dst'.
+Proof. auto. Qed.
+
 Lemma forest_reg_gss:
   forall (f : forest) w dst,
     (f #r dst <- w) #r dst = w.
@@ -1482,6 +1487,11 @@ Proof.
   rewrite PTree.gso; auto.
 Qed.
 
+Lemma forest_pred_reg:
+  forall (f : forest) w dst dst',
+    (f #p dst <- w) #r dst' = f #r dst'.
+Proof. auto. Qed.
+
 Lemma forest_pred_gss:
   forall (f : forest) w dst,
     (f #p dst <- w) #p dst = w.
diff --git a/src/hls/Array.v b/src/hls/Array.v
index de74611..8b7d262 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -76,7 +76,7 @@ Lemma array_set_wf {A : Type} :
 Proof.
   induction l; intros; destruct i; auto.
 
-  invert H; crush.
+  inv H; crush.
 Qed.
 
 Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
@@ -272,10 +272,10 @@ Proof.
 
   (* This is actually a degenerate case, not an unprovable goal. *)
   pose proof (in_app_or (list_repeat' [] a n) ([a])).
-  apply H0 in H. invert H.
+  apply H0 in H. inv H.
 
   - eapply IHn in X; eassumption.
-  - invert H1; contradiction.
+  - inv H1; contradiction.
 Qed.
 
 Lemma list_repeat_head_tail {A : Type} : forall n (a : A),
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index c2ed9e3..7c9a898 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -71,24 +71,6 @@ Fixpoint replicate {A} (n: nat) (l: A) :=
   | S n => l :: replicate n l
   end.
 
-Definition merge''' {A: Type} (x y: option (@Predicate.pred_op A)) :=
-  match x, y with
-  | Some p1, Some p2 => Some (Pand p1 p2)
-  | Some p, None | None, Some p => Some p
-  | None, None => None
-  end.
-
-Definition merge'' {A: Type} x :=
-  match x with
-  | ((a, e), (b, el)) => (@merge''' A a b, Econs e el)
-  end.
-
-Definition map_pred_op {A B P: Type} (pf: option (@Predicate.pred_op P) * (A -> B))
-           (pa: option (@Predicate.pred_op P) * A): option (@Predicate.pred_op P) * B :=
-  match pa, pf with
-  | (p, a), (p', f) => (merge''' p p', f a)
-  end.
-
 Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
   NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
          (NE.non_empty_prod p1 p2).
@@ -96,33 +78,35 @@ Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
 Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A)
   : predicated B := NE.map (fun x => (fst x, f (snd x))) p.
 
-(*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
-Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
+Definition cons_pred_expr (pel: pred_expr) (tpel: predicated expression_list) :=
   predicated_map (uncurry Econs) (predicated_prod pel tpel).
 
-Fixpoint merge (pel: list pred_expr): predicated expression_list :=
+Fixpoint merge_old (pel: list pred_expr): predicated expression_list :=
   match pel with
   | nil => NE.singleton (T, Enil)
-  | a :: b => merge' a (merge b)
+  | a :: b => cons_pred_expr a (merge_old b)
+  end.
+
+Definition merge (pel: list pred_expr): predicated expression_list :=
+  match NE.of_list pel with
+  | Some npel =>
+    NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) npel
+  | None => NE.singleton (T, Enil)
   end.
 
-Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A)
+Definition seq_app {A B} (pf: predicated (A -> B)) (pa: predicated A)
   : predicated B :=
   predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa).
 
-Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A)
+Definition flap {A B} (pf: predicated (A -> B)) (pa: A)
   : predicated B :=
   NE.map (fun x => (fst x, (snd x) pa)) pf.
 
-Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A)
+Definition flap2 {A B C} (pf: predicated (A -> B -> C)) (pa: A)
            (pb: B): predicated C :=
   NE.map (fun x => (fst x, (snd x) pa pb)) pf.
 
-Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D))
-           (pa: A) (pb: B) (pc: C): predicated D :=
-  NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
-
-Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
+Definition predicated_of_opt {A: Type} (p: option pred_op) (a: A) :=
   match p with
   | Some p' => NE.singleton (p', a)
   | None => NE.singleton (T, a)
@@ -131,24 +115,12 @@ Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
 #[local] Open Scope non_empty_scope.
 #[local] Open Scope pred_op.
 
-Fixpoint NEfold_left {A B} (f: A -> B -> A) (l: NE.non_empty B) (a: A) : A :=
-  match l with
-  | NE.singleton a' => f a a'
-  | a' ::| b => NEfold_left f b (f a a')
-  end.
-
-Fixpoint NEapp {A} (l m: NE.non_empty A) :=
-  match l with
-  | NE.singleton a => a ::| m
-  | a ::| b => a ::| NEapp b m
-  end.
-
 Definition app_predicated' {A: Type} (a b: predicated A) :=
-  let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in
-  NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b.
+  let negation := ¬ (NE.fold_left (fun a b => a ∨ (fst b)) b ⟂) in
+  NE.app (NE.map (fun x => (negation ∧ fst x, snd x)) a) b.
 
 Definition app_predicated {A: Type} (p': pred_op) (a b: predicated A) :=
-  NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a)
+  NE.app (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a)
         (NE.map (fun x => (p' ∧ fst x, snd x)) b).
 
 Definition prune_predicated {A: Type} (a: predicated A) :=
@@ -215,15 +187,15 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
            prune_predicated
              (app_predicated (dfltp p ∧ pred)
                              (f #r (Reg r))
-                             (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f))));
+                             (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))));
       Some (pred, f #r (Reg r) <- pruned)
   | RBload p chunk addr rl r =>
       do pruned <-
            prune_predicated
              (app_predicated (dfltp p ∧ pred)
                              (f #r (Reg r))
-                             (map_predicated
-                                (map_predicated (pred_ret (Eload chunk addr))
+                             (seq_app
+                                (seq_app (pred_ret (Eload chunk addr))
                                                 (merge (list_translation rl f)))
                                 (f #r Mem)));
       Some (pred, f #r (Reg r) <- pruned)
@@ -232,16 +204,16 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
            prune_predicated
              (app_predicated (dfltp p ∧ pred)
                              (f #r Mem)
-                             (map_predicated
-                                (map_predicated
-                                   (predicated_apply2 (map_predicated (pred_ret Estore)
+                             (seq_app
+                                (seq_app
+                                   (flap2 (seq_app (pred_ret Estore)
                                                                       (f #r (Reg r))) chunk addr)
                                    (merge (list_translation rl f))) (f #r Mem)));
       Some (pred, f #r Mem <- pruned)
   | RBsetpred p' c args p =>
       let new_pred :=
         (from_pred_op f.(forest_preds) (dfltp p' ∧ pred)
-         → from_predicated true f.(forest_preds) (map_predicated (pred_ret (PEsetpred c))
+         → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c))
                                                   (merge (list_translation args f))))
       in
       do _ <- is_initial_pred f p;
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 05467ed..3f8aeae 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -44,6 +44,8 @@ Import OptionExtra.
 #[local] Opaque simplify.
 #[local] Opaque deep_simplify.
 
+Ltac destr := destruct_match; try discriminate; [].
+
 (*|
 ==============
 RTLPargenproof
@@ -475,11 +477,25 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
 
   Lemma sem_update_instr :
     forall f i' i'' a sp p i p' f',
-      sem (mk_ctx i sp ge) f (i', None) ->
       step_instr ge sp (Iexec i') a (Iexec i'') ->
+      sem (mk_ctx i sp ge) f (i', None) ->
       update (p, f) a = Some (p', f') ->
+      eval_predf (is_ps i') p = true ->
       sem (mk_ctx i sp ge) f' (i'', None).
-  Proof. Admitted.
+  Proof.
+    inversion 1; subst; clear H; intros SEM UPD EVAL_PRED.
+    - inv UPD; auto.
+    - inversion UPD as [PRUNE]. unfold Option.bind in PRUNE.
+      destr. inversion_clear PRUNE.
+      rename H3 into EVAL_OP. rename H5 into TRUTHY.
+      rename Heqo into PRUNE.
+      inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
+      cbn [is_ps] in *. constructor.
+      + admit.
+      + constructor; intros. inv PRED. rewrite forest_reg_pred. auto.
+      + rewrite forest_reg_gso; auto; discriminate.
+      + auto.
+    -
 
   Lemma truthy_dflt :
     forall ps p,
@@ -495,6 +511,16 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     rewrite eval_predf_Pand. now rewrite H.
   Qed.
 
+  Lemma Pand_true_right :
+    forall ps a b,
+      eval_predf ps b = false ->
+      eval_predf ps (a ∧ b) = false.
+  Proof.
+    intros.
+    rewrite eval_predf_Pand. rewrite H.
+    eauto with bool.
+  Qed.
+
   Lemma eval_predf_simplify :
     forall ps x,
       eval_predf ps (simplify x) = eval_predf ps x.
@@ -516,8 +542,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     { rewrite eval_predf_negate. now rewrite negb_false_iff. }
     apply Pand_true_left with (b := p') in H0.
     rewrite <- eval_predf_simplify in H0. split; auto.
-    unfold "<-e".
-    destruct i''.
+    unfold "<-e". destruct i''.
     inv H. constructor; auto. admit. admit. simplify.
   Admitted.
 
@@ -567,8 +592,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       sem (mk_ctx i sp ge) f' (i', cf).
   Proof. Admitted.
 
-  Ltac destr := destruct_match; try discriminate; [].
-
   Lemma eval_predf_update_true :
     forall i i' curr_p next_p f f_next instr sp,
       update (curr_p, f) instr = Some (next_p, f_next) ->
@@ -732,8 +755,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
         exists R2, Smallstep.plus GiblePar.step tge R1 t R2 /\ match_states S2 R2.
   Proof.
     induction 1; repeat semantics_simpl.
-    {
-      exploit schedule_oracle_correct; eauto. constructor; eauto. simplify.
+    { exploit schedule_oracle_correct; eauto. constructor; eauto. simplify.
       destruct x0.
       pose proof H2 as X. eapply match_states_stepBB in X; eauto.
       exploit step_cf_correct; eauto. simplify.
@@ -771,9 +793,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   Lemma transl_final_states:
     forall S R r,
       match_states S R -> GibleSeq.final_state S r -> GiblePar.final_state R r.
-  Proof.
-    intros. inv H0. inv H. inv STACKS. constructor.
-  Qed.
+  Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed.
 
   Theorem transf_program_correct:
     Smallstep.forward_simulation (GibleSeq.semantics prog) (GiblePar.semantics tprog).
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 793eb5d..4bb001b 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -143,7 +143,7 @@ Proof.
     exists x. exists (a :: x0). exists x1. simplify; auto.
     econstructor; eauto.
   -  inv H3.
-     exists p. exists nil. exists bb. crush.
+     exists p. exists (@nil instr). exists bb. crush.
      constructor.
 Qed.
 
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index bf1ef1c..1089356 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -248,9 +248,9 @@ Proof.
   discriminate.
 
   destruct l2 eqn:EQl2. crush.
-  simpl in H. invert H.
+  simpl in H. inv H.
   destruct n; simpl in *.
-  invert H0. simpl. reflexivity.
+  inv H0. simpl. reflexivity.
   eauto.
 Qed.
 
@@ -277,9 +277,9 @@ Proof.
   induction l1; intros; crush; auto.
 
   destruct l2 eqn:EQl2. crush.
-  simpl in H. invert H.
+  simpl in H. inv H.
   destruct n; simpl in *.
-  invert H0. simpl. reflexivity.
+  inv H0. simpl. reflexivity.
   eauto.
 Qed.
 
@@ -1068,7 +1068,7 @@ rs assoc``.
       destruct (Pos.eq_dec s d) as [EQ|EQ];
       [> rewrite EQ | rewrite Registers.Regmap.gso; auto]
 
-    | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H
+    | [ H : opt_val_value_lessdef _ _ |- _ ] => inv H
     | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |]
     | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H
     end.
@@ -1102,7 +1102,7 @@ rs assoc``.
     econstructor.
     econstructor.
 
-    all: invert MARR; big_tac. Abort.
+    all: inv MARR; big_tac. Abort.
 
 (*    inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia.
 
@@ -1172,7 +1172,7 @@ rs assoc``.
            | [ _ : context[if ?x then _ else _] |- _ ] =>
              let EQ := fresh "EQ" in
              destruct x eqn:EQ; simpl in *
-           | [ H : ret _ _ = _  |- _ ] => invert H
+           | [ H : ret _ _ = _  |- _ ] => inv H
            | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
            end.
 
@@ -1270,7 +1270,7 @@ rs assoc``.
     inv_state. inv_arr_access.
 
     + (** Preamble *)
-      invert MARR. inv CONST. crush.
+      inv MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1284,14 +1284,14 @@ rs assoc``.
       subst.
 
       pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
+      inv MASSOC'.
       pose proof (H0 r0).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       apply H0 in HPler0.
-      invert HPler0; try congruence.
+      inv HPler0; try congruence.
       rewrite EQr0 in H11.
-      invert H11.
+      inv H11.
 
       unfold check_address_parameter_signed in *;
       unfold check_address_parameter_unsigned in *; crush.
@@ -1393,7 +1393,7 @@ rs assoc``.
         by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
       unfold Ple in HPle. lia.
     + (** Preamble *)
-      invert MARR. inv CONST. crush.
+      inv MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1410,7 +1410,7 @@ rs assoc``.
       clear RSBPr1.
 
       pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
+      inv MASSOC'.
       pose proof (H0 r0).
       pose proof (H0 r1).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
@@ -1419,10 +1419,10 @@ rs assoc``.
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
       apply H8 in HPler0.
       apply H11 in HPler1.
-      invert HPler0; invert HPler1; try congruence.
+      inv HPler0; inv HPler1; try congruence.
       rewrite EQr0 in H13.
       rewrite EQr1 in H14.
-      invert H13. invert H14.
+      inv H13. inv H14.
       clear H0. clear H8. clear H11.
 
       unfold check_address_parameter_signed in *;
@@ -1524,7 +1524,7 @@ rs assoc``.
         by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
       unfold Ple in HPle. lia.
 
-    + invert MARR. inv CONST. crush.
+    + inv MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1652,7 +1652,7 @@ rs assoc``.
     inv_state. inv_arr_access.
 
     + (** Preamble *)
-      invert MARR. inv CONST. crush.
+      inv MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1666,14 +1666,14 @@ rs assoc``.
       subst.
 
       pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
+      inv MASSOC'.
       pose proof (H0 r0).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       apply H8 in HPler0.
-      invert HPler0; try congruence.
+      inv HPler0; try congruence.
       rewrite EQr0 in H11.
-      invert H11.
+      inv H11.
       clear H0. clear H8.
 
       unfold check_address_parameter_unsigned in *;
@@ -1799,7 +1799,7 @@ rs assoc``.
       assert (HPle : Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
       apply H11 in HPle.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert HPle; eauto.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv HPle; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
@@ -1897,7 +1897,7 @@ rs assoc``.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           invert H11.
+           inv H11.
            apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
            rewrite ZLib.div_mul_undo in H14; try lia.
            split; try lia.
@@ -1919,7 +1919,7 @@ rs assoc``.
       crush.
       exploit (BOUNDS ptr); try lia. intros. crush.
       exploit (BOUNDS ptr v); try lia. intros.
-      invert H11.
+      inv H11.
       match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
       assert (Mem.valid_access m AST.Mint32 sp'
                                (Integers.Ptrofs.unsigned
@@ -1931,7 +1931,7 @@ rs assoc``.
                                          (Integers.Ptrofs.unsigned
                                             (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
                                                                  (Integers.Ptrofs.repr ptr))) v).
-      apply X in H11. invert H11. congruence.
+      apply X in H11. inv H11. congruence.
 
       constructor; simplify. unfold Verilog.merge_regs. unfold_merge.
       rewrite AssocMap.gso.
@@ -1941,7 +1941,7 @@ rs assoc``.
       assumption. lia.
 
     + (** Preamble *)
-      invert MARR. inv CONST. crush.
+      inv MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -1958,7 +1958,7 @@ rs assoc``.
       clear RSBPr1.
 
       pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
+      inv MASSOC'.
       pose proof (H0 r0).
       pose proof (H0 r1).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
@@ -1967,10 +1967,10 @@ rs assoc``.
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
       apply H8 in HPler0.
       apply H11 in HPler1.
-      invert HPler0; invert HPler1; try congruence.
+      inv HPler0; inv HPler1; try congruence.
       rewrite EQr0 in H13.
       rewrite EQr1 in H14.
-      invert H13. invert H14.
+      inv H13. inv H14.
       clear H0. clear H8. clear H11.
 
       unfold check_address_parameter_signed in *;
@@ -2100,7 +2100,7 @@ rs assoc``.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
       apply H14 in H15.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H15; eauto.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H15; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
@@ -2198,7 +2198,7 @@ rs assoc``.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           invert H14.
+           inv H14.
            apply Zmult_lt_compat_r with (p := 4) in H16; try lia.
            rewrite ZLib.div_mul_undo in H16; try lia.
            split; try lia.
@@ -2232,14 +2232,14 @@ rs assoc``.
                                          (Integers.Ptrofs.unsigned
                                             (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
                                                                  (Integers.Ptrofs.repr ptr))) v).
-      apply X in H14. invert H14. congruence.
+      apply X in H14. inv H14. congruence.
 
       constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
       assumption. lia.
       unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
       assumption. lia.
 
-    + invert MARR. inv CONST. crush.
+    + inv MARR. inv CONST. crush.
 
       unfold Op.eval_addressing in H0.
       destruct (Archi.ptr64) eqn:ARCHI; crush.
@@ -2366,7 +2366,7 @@ rs assoc``.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
       apply H0 in H8.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H8; eauto.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
@@ -2455,7 +2455,7 @@ rs assoc``.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           invert H0.
+           inv H0.
            apply Zmult_lt_compat_r with (p := 4) in H11; try lia.
            rewrite ZLib.div_mul_undo in H11; try lia.
            split; try lia.
@@ -2476,7 +2476,7 @@ rs assoc``.
       crush.
       exploit (BOUNDS ptr); try lia. intros. crush.
       exploit (BOUNDS ptr v); try lia. intros.
-      invert H0.
+      inv H0.
       match goal with | |- ?x = _ => destruct x eqn:?EQ end; try reflexivity.
       assert (Mem.valid_access m AST.Mint32 sp'
                                (Integers.Ptrofs.unsigned
@@ -2488,7 +2488,7 @@ rs assoc``.
                                          (Integers.Ptrofs.unsigned
                                             (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
                                                                  (Integers.Ptrofs.repr ptr))) v).
-      apply X in H0. invert H0. congruence.
+      apply X in H0. inv H0. congruence.
 
       constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
       assumption. lia.
@@ -2733,12 +2733,12 @@ rs assoc``.
     split.
 
     unfold Mem.alloc in H.
-    invert H.
+    inv H.
     crush.
     unfold Mem.load.
     intros.
     match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
-    invert v0. unfold Mem.range_perm in H4.
+    inv v0. unfold Mem.range_perm in H4.
     unfold Mem.perm in H4. crush.
     unfold Mem.perm_order' in H4.
     small_tac.
@@ -2749,12 +2749,12 @@ rs assoc``.
     apply proj_sumbool_true in H10. lia.
 
     unfold Mem.alloc in H.
-    invert H.
+    inv H.
     crush.
     unfold Mem.store.
     intros.
     match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
-    invert v0. unfold Mem.range_perm in H4.
+    inv v0. unfold Mem.range_perm in H4.
     unfold Mem.perm in H4. crush.
     unfold Mem.perm_order' in H4.
     small_tac.
@@ -2853,7 +2853,7 @@ rs assoc``.
       Smallstep.final_state (RTL.semantics prog) s1 r ->
       Smallstep.final_state (HTL.semantics tprog) s2 r.
   Proof.
-    intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity.
+    intros. inv H0. inv H. inv H4. inv MF. constructor. reflexivity.
   Qed.
   #[local] Hint Resolve transl_final_states : htlproof.
 
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index e13db00..2d8cfac 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -673,7 +673,7 @@ Section CORRECTNESS.
         /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i').
   Proof using.
     induction x0; simplify.
-    - inv H1. inv H. exists nil. exists b'0.
+    - inv H1. inv H. exists (@nil instr). exists b'0.
       split; [|constructor]. rewrite app_nil_l.
       replace (RBexit x cf :: b'0) with ((RBexit x cf :: nil) ++ b'0) by auto.
       f_equal. simplify. destruct cf; auto.
@@ -761,7 +761,7 @@ Section CORRECTNESS.
         /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i').
   Proof using.
     induction x0; simplify.
-    - inv H1. inv H. exists nil. exists b'0.
+    - inv H1. inv H. exists (@nil instr). exists b'0.
       split; [|constructor]. rewrite app_nil_l.
       f_equal. simplify. apply wf_transition_block_opt_prop in H0. rewrite H0.
       rewrite Pos.eqb_refl. auto.
@@ -809,7 +809,7 @@ Section CORRECTNESS.
         econstructor; eauto. constructor; auto.
       + exploit exec_if_conv2; eauto; simplify.
         exploit step_cf_eq; eauto; simplify.
-        apply sim_plus. exists None. exists x4.
+        apply sim_plus. exists (@None (list instr)). exists x4.
         split. apply plus_one. econstructor; eauto.
         apply append. exists (mki rs' pr' m'). split; auto.
         apply step_list_2_eq; auto.
@@ -838,7 +838,7 @@ Section CORRECTNESS.
     rewrite IS_B in H0; simplify.
     exploit step_cf_eq; eauto; simplify.
     apply sim_plus.
-    exists None. exists x.
+    exists (@None (list instr)). exists x.
     split; auto.
     unfold sem_extrap in *.
     inv SIM.
@@ -861,14 +861,14 @@ Section CORRECTNESS.
     - eauto using match_some_correct.
     - eauto using match_none_correct.
     - apply sim_plus. remember (transf_function l f) as tf. symmetry in Heqtf. func_info.
-      exists None. eexists. split.
+      exists (@None (list instr)). eexists. split.
       apply plus_one. constructor; eauto. rewrite <- H1. eassumption.
       rewrite <- H4. rewrite <- H2. econstructor; auto.
-    - apply sim_plus. exists None. eexists. split.
+    - apply sim_plus. exists (@None (list instr)). eexists. split.
       apply plus_one. constructor; eauto.
       constructor; auto.
    - apply sim_plus. remember (transf_function None f) as tf. symmetry in Heqtf. func_info.
-      exists None. inv STK. inv H7. eexists. split. apply plus_one. constructor.
+      exists (@None (list instr)). inv STK. inv H7. eexists. split. apply plus_one. constructor.
       econstructor; auto.
   Qed.
 
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 72140cd..56d7332 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -691,14 +691,14 @@ Proof.
   induction e; intros;
 
   repeat (try match goal with
-              | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H
-              | [ H : expr_runp _ _ _ (Vrange _ _ _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => inv H
+              | [ H : expr_runp _ _ _ (Vrange _ _ _) _ |- _ ] => inv H
 
               | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _,
                   H2 : expr_runp _ _ _ ?e _ |- _ ] =>
@@ -720,7 +720,7 @@ Proof.
   induction 1; intros;
 
   repeat (try match goal with
-              | [ H : location_is _ _ _ _ _ |- _ ] => invert H
+              | [ H : location_is _ _ _ _ _ |- _ ] => inv H
               | [ H1 : expr_runp _ ?asr ?asa ?e _,
                   H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
                 learn (expr_runp_determinate H1 H2)
@@ -736,13 +736,13 @@ Lemma stmnt_runp_determinate :
   induction 1; intros;
 
   repeat (try match goal with
-             | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil  _) _ _ |- _ ] => invert H
+             | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => inv H
+             | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => inv H
+             | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => inv H
+             | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => inv H
+             | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => inv H
+             | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => inv H
+             | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil  _) _ _ |- _ ] => inv H
 
              | [ H1 : expr_runp _ ?asr ?asa ?e _,
                  H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
@@ -766,7 +766,7 @@ Lemma mi_stepp_determinate :
   mi_stepp f asr0 asa0 m asr1' asa1' ->
   asr1' = asr1 /\ asa1' = asa1.
 Proof.
-  intros. destruct m; invert H; invert H0;
+  intros. destruct m; inv H; inv H0;
 
   repeat (try match goal with
               | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _,
@@ -782,7 +782,7 @@ Lemma mi_stepp_negedge_determinate :
   mi_stepp_negedge f asr0 asa0 m asr1' asa1' ->
   asr1' = asr1 /\ asa1' = asa1.
 Proof.
-  intros. destruct m; invert H; invert H0;
+  intros. destruct m; inv H; inv H0;
 
   repeat (try match goal with
               | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _,
@@ -801,8 +801,8 @@ Proof.
   induction 1; intros;
 
   repeat (try match goal with
-              | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H
-              | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H
+              | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => inv H
+              | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => inv H
 
               | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _,
                   H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
@@ -824,8 +824,8 @@ Proof.
   induction 1; intros;
 
   repeat (try match goal with
-              | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => invert H
-              | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H
+              | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => inv H
+              | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => inv H
 
               | [ H1 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _,
                   H2 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
@@ -841,15 +841,15 @@ Lemma semantics_determinate :
   forall (p: program), Smallstep.determinate (semantics p).
 Proof.
   intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
-  - invert H; invert H0; constructor. (* Traces are always empty *)
-  - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
+  - inv H; inv H0; constructor. (* Traces are always empty *)
+  - inv H; inv H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
     pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4.
     pose proof (mis_stepp_negedge_determinate H6 H17).
     crush.
-  - constructor. invert H; crush.
-  - invert H; invert H0; unfold ge0, ge1 in *; crush.
-  - red; simplify; intro; invert H0; invert H; crush.
-  - invert H; invert H0; crush.
+  - constructor. inv H; crush.
+  - inv H; inv H0; unfold ge0, ge1 in *; crush.
+  - red; simplify; intro; inv H0; inv H; crush.
+  - inv H; inv H0; crush.
 Qed.
 
 Local Open Scope positive.