Improve proof quality

theories/Core/Semantic/Evaluation/Lemmas.v

@@ -14,66 +14,63 @@ Section functional_eval.
     clear functional_eval_exp_prop functional_eval_natrec_prop functional_eval_app_prop functional_eval_sub_prop.
 
   Lemma functional_eval_exp : forall M p m1 (Heval1 : {{ ⟦ M ⟧ p ↘ m1 }}), functional_eval_exp_prop M p m1 Heval1.
-  Proof using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_exp_mut_ind
       with (P0 := functional_eval_natrec_prop)
            (P1 := functional_eval_app_prop)
            (P2 := functional_eval_sub_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion_clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 
   Lemma functional_eval_natrec : forall A MZ MS m p r1 (Heval1 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}), functional_eval_natrec_prop A MZ MS m p r1 Heval1.
-  Proof using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_natrec_mut_ind
       with (P := functional_eval_exp_prop)
            (P1 := functional_eval_app_prop)
            (P2 := functional_eval_sub_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 
   Lemma functional_eval_app : forall m n r1 (Heval1 : {{ $| m & n |↘ r1 }}), functional_eval_app_prop m n r1 Heval1.
-  Proof using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_app_mut_ind
       with (P := functional_eval_exp_prop)
            (P0 := functional_eval_natrec_prop)
            (P2 := functional_eval_sub_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 
   Lemma functional_eval_sub : forall σ p p1 (Heval1 : {{ ⟦ σ ⟧s p ↘ p1 }}), functional_eval_sub_prop σ p p1 Heval1.
-  Proof using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_sub_mut_ind
       with (P := functional_eval_exp_prop)
            (P0 := functional_eval_natrec_prop)
            (P1 := functional_eval_app_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 End functional_eval.
 
 #[export]
 Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub : mcltt.
 
 Ltac functional_eval_rewrite_clear1 :=
+  let tactic_error o1 o2 := fail 3 "functional_eval equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
-      clean replace m2 with m1 by mauto; clear H2
+      clean replace m2 with m1 by first [solve [mauto] | tactic_error m2 m1]; clear H2
   | H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
-      clean replace r2 with r1 by mauto; clear H2
+      clean replace r2 with r1 by first [solve [mauto] | tactic_error r2 r1]; clear H2
   | H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
-      clean replace r2 with r1 by mauto; clear H2
+      clean replace r2 with r1 by first [solve [mauto] | tactic_error r2 r1]; clear H2
   | H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
-      clean replace p2 with p1 by mauto; clear H2
+      clean replace p2 with p1 by first [solve [mauto] | tactic_error p2 p1]; clear H2
   end.
 Ltac functional_eval_rewrite_clear := repeat functional_eval_rewrite_clear1.

theories/Core/Semantic/PER/Definitions.v

@@ -210,6 +210,7 @@ Ltac per_univ_elem_econstructor :=
 (** Context/Environment PER *)
 
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
+Arguments rel_typ _ _ _ _ _ _ /.
 
 Definition per_total : relation env := fun p p' => True.