Optimizing proofs

theories/Core/Semantic/PER/CoreTactics.v

@@ -46,8 +46,7 @@ Ltac destruct_rel_typ :=
 
 Ltac basic_invert_per_univ_elem H :=
   progress simp per_univ_elem in H;
-  inversion H;
-  subst;
+  dependent destruction H;
   try rewrite <- per_univ_elem_equation_1 in *.
 
 Ltac basic_per_univ_elem_econstructor :=

theories/Core/Semantic/PER/Lemmas.v

@@ -446,10 +446,10 @@ Lemma per_univ_elem_trans : forall i R a1 a2,
           R m1 m2 ->
           R m2 m3 ->
           R m1 m3).
-Proof with (basic_per_univ_elem_econstructor; mautosolve).
+Proof with (basic_per_univ_elem_econstructor; mautosolve 4).
   induction 1 using per_univ_elem_ind;
     [> split;
-     [ intros * HT2; basic_invert_per_univ_elem HT2; clear HT2
+     [ intros * HT2; basic_invert_per_univ_elem HT2
      | intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto.
   - (* univ case *)
     subst.

theories/Core/Soundness/FunctionCases.v

@@ -364,7 +364,7 @@ Proof.
   assert {{ Γ ⊩ A : Type@(max i j) }} by mauto 3.
   assert {{ ⊩ Γ, A }} by mauto 2.
   assert (i <= max i j) by lia.
-  assert {{ Γ, A ⊢ Type@i ⊆ Type@(max i j) }} by mauto 3.
+  assert {{ Γ, A ⊢ Type@i ⊆ Type@(max i j) }} by mauto 4.
   assert {{ Γ, A ⊩ B : Type@(max i j) }} by mauto 3.
   mauto 2 using glu_rel_exp_app_helper.
 Qed.

theories/Core/Soundness/LogicalRelation/CoreLemmas.v

@@ -59,7 +59,7 @@ Lemma glu_nat_resp_exp_eq : forall Γ M a,
     {{ Γ ⊢ M ≈ M' : ℕ }} ->
     glu_nat Γ M' a.
 Proof.
-  induction 1; intros; mauto.
+  induction 1; intros; mauto 4.
   econstructor; trivial.
   intros.
   transitivity {{{ M[σ] }}}; mauto.
@@ -82,11 +82,11 @@ Lemma glu_nat_readback : forall Γ M a,
       {{ Δ ⊢ M[σ] ≈ M' : ℕ }}.
 Proof.
   induction 1; intros; progressive_inversion; gen_presups.
-  - transitivity {{{ zero[σ] }}}; mauto.
-  - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto.
+  - transitivity {{{ zero[σ] }}}; mauto 4.
+  - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto 4.
     transitivity {{{ (succ M')[σ] }}}; mauto 3.
     transitivity {{{ succ M'[σ] }}}; mauto 4.
-  - mauto.
+  - mauto 4.
 Qed.
 
 #[global]
@@ -270,7 +270,7 @@ Lemma glu_univ_elem_per_elem : forall i P El a,
 Proof.
   simpl.
   induction 1 using glu_univ_elem_ind; intros;
-    try do 2 match_by_head1 per_univ_elem invert_per_univ_elem;
+    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H);
     simpl_glu_rel;
     try fold (per_univ j m m);
     mauto 4.

theories/Core/Soundness/LogicalRelation/CoreTactics.v

@@ -5,8 +5,7 @@ From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 
 Ltac basic_invert_glu_univ_elem H :=
   progress simp glu_univ_elem in H;
-  inversion H;
-  subst;
+  dependent destruction H;
   try rewrite <- glu_univ_elem_equation_1 in *.
 
 Ltac basic_glu_univ_elem_econstructor :=

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -405,6 +405,7 @@ Proof.
     assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
     eapply wf_subtyp_refl'.
     mauto 4.
+  - bulky_rewrite.
   - bulky_rewrite.
     mauto 3.
   - destruct_by_head pi_glu_typ_pred.
@@ -916,7 +917,7 @@ Qed.
 Ltac invert_glu_ctx_env H :=
   (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
    destruct H as [? [? []]])
-  + (inversion H; subst).
+  + dependent destruction H.
 
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->

theories/Core/Soundness/SubstitutionCases.v

@@ -59,7 +59,7 @@ Proof.
   intros * [SbΓA].
   match_by_head1 glu_ctx_env invert_glu_ctx_env.
   handle_functional_glu_ctx_env.
-  do 2 eexists; repeat split; mauto.
+  do 2 eexists; repeat split; [econstructor | |]; try reflexivity; mauto.
   intros.
   destruct_by_head cons_glu_sub_pred.
   econstructor; mauto.

theories/LibTactics.v

@@ -229,22 +229,16 @@ Tactic Notation "mautosolve" int_or_var(pow) := mautosolve_impl pow.
 (* Improve type class resolution *)
 
 #[export]
-  Hint Extern 1 => eassumption : typeclass_instances.
-
-Ltac predicate_resolve :=
-  lazymatch goal with
-  | |- @Reflexive _ (@predicate_equivalence _) =>
-      simple apply @Equivalence_Reflexive
-  | |- @Symmetric _ (@predicate_equivalence _) =>
-      simple apply @Equivalence_Symmetric
-  | |- @Transitive _ (@predicate_equivalence _) =>
-      simple apply @Equivalence_Transitive
-  | |- @Transitive _ (@predicate_implication _) =>
-      simple apply @PreOrder_Transitive
-  end.
+Hint Extern 1 => eassumption : typeclass_instances.
 
 #[export]
-Hint Extern 1 => predicate_resolve : typeclass_instances.
+Hint Extern 1 (@Reflexive _ (@predicate_equivalence _)) => simple apply @Equivalence_Reflexive : typeclass_instances.
+#[export]
+Hint Extern 1 (@Symmetric _ (@predicate_equivalence _)) => simple apply @Equivalence_Symmetric : typeclass_instances.
+#[export]
+Hint Extern 1 (@Transitive _ (@predicate_equivalence _)) => simple apply @Equivalence_Transitive : typeclass_instances.
+#[export]
+Hint Extern 1 (@Transitive _ (@predicate_implication _)) => simple apply @PreOrder_Transitive : typeclass_instances.
 
 
 (* intuition tactic default setting *)