Update some proofs (#77)

Beluga-lang · May 10, 2024 · eef8e48 · eef8e48
1 parent c0f3bed
commit eef8e48
Show file tree

Hide file tree

Showing 7 changed files with 339 additions and 446 deletions.
diff --git a/theories/Core/Semantic/Evaluation/Lemmas.v b/theories/Core/Semantic/Evaluation/Lemmas.v
@@ -14,7 +14,7 @@ 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 with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_exp_mut_ind
       with (P0 := functional_eval_natrec_prop)
@@ -25,7 +25,7 @@ Section functional_eval.
   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 with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_natrec_mut_ind
       with (P := functional_eval_exp_prop)
@@ -36,7 +36,7 @@ Section functional_eval.
   Qed.
 
   Lemma functional_eval_app : forall m n r1 (Heval1 : {{ $| m & n |↘ r1 }}), functional_eval_app_prop m n r1 Heval1.
-  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_app_mut_ind
       with (P := functional_eval_exp_prop)
@@ -47,7 +47,7 @@ Section functional_eval.
   Qed.
 
   Lemma functional_eval_sub : forall σ p p1 (Heval1 : {{ ⟦ σ ⟧s p ↘ p1 }}), functional_eval_sub_prop σ p p1 Heval1.
-  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_sub_mut_ind
       with (P := functional_eval_exp_prop)

diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
@@ -68,7 +68,8 @@ Lemma per_bot_then_per_top : forall m m' a a' b b' c c',
     {{ Dom ⇓ (⇑ a b) ⇑ c m ≈ ⇓ (⇑ a' b') ⇑ c' m' ∈ per_top }}.
 Proof.
   intros * H s.
-  specialize (H s) as [? []].
+  pose proof H s.
+  destruct_conjs.
   eexists; split; constructor; eassumption.
 Qed.
 
@@ -104,7 +105,7 @@ Hint Resolve per_top_typ_trans : mcltt.
 Lemma per_nat_sym : forall m n,
     {{ Dom m ≈ n ∈ per_nat }} ->
     {{ Dom n ≈ m ∈ per_nat }}.
-Proof with solve [eauto using per_bot_sym].
+Proof with mautosolve.
   induction 1; econstructor...
 Qed.
 
@@ -115,7 +116,7 @@ Lemma per_nat_trans : forall m n l,
     {{ Dom m ≈ n ∈ per_nat }} ->
     {{ Dom n ≈ l ∈ per_nat }} ->
     {{ Dom m ≈ l ∈ per_nat }}.
-Proof with solve [eauto using per_bot_trans].
+Proof with mautosolve.
   intros * H. gen l.
   induction H; inversion_clear 1; econstructor...
 Qed.
@@ -126,7 +127,7 @@ Hint Resolve per_nat_trans : mcltt.
 Lemma per_ne_sym : forall m n,
     {{ Dom m ≈ n ∈ per_ne }} ->
     {{ Dom n ≈ m ∈ per_ne }}.
-Proof with solve [eauto using per_bot_sym].
+Proof with mautosolve.
   intros * [].
   econstructor...
 Qed.
@@ -138,7 +139,7 @@ Lemma per_ne_trans : forall m n l,
     {{ Dom m ≈ n ∈ per_ne }} ->
     {{ Dom n ≈ l ∈ per_ne }} ->
     {{ Dom m ≈ l ∈ per_ne }}.
-Proof with solve [eauto using per_bot_trans].
+Proof with mautosolve.
   intros * [].
   inversion_clear 1.
   econstructor...
@@ -151,13 +152,13 @@ Lemma per_univ_elem_right_irrel : forall i i' A B R B' R',
     per_univ_elem i A B R ->
     per_univ_elem i' A B' R' ->
     R = R'.
-Proof with solve [eauto].
+Proof with mautosolve.
   intros * Horig.
   remember A as A' in |- *.
   gen A' B' R'.
   induction Horig using per_univ_elem_ind; intros * Heq Hright;
     subst; invert_per_univ_elem Hright; unfold per_univ;
-    try congruence.
+    trivial.
   specialize (IHHorig _ _ _ eq_refl equiv_a_a').
   subst.
   extensionality f.
@@ -186,7 +187,7 @@ Lemma per_univ_elem_sym : forall i A B R,
       (forall a b,
           {{ Dom a ≈ b ∈ R }} ->
           {{ Dom b ≈ a ∈ R }}).
-Proof with solve [try econstructor; eauto using per_bot_sym, per_nat_sym, per_ne_sym].
+Proof with (try econstructor; mautosolve).
   induction 1 using per_univ_elem_ind; subst.
   - split.
     + apply per_univ_elem_core_univ'...
@@ -219,22 +220,20 @@ Corollary per_univ_sym : forall i A B R,
     per_univ_elem i A B R ->
     per_univ_elem i B A R.
 Proof.
-  intros.
-  apply per_univ_elem_sym.
-  assumption.
+  intros * ?%per_univ_elem_sym.
+  firstorder.
 Qed.
 
 Corollary per_elem_sym : forall i A B a b R,
     per_univ_elem i A B R ->
     R a b ->
     R b a.
 Proof.
-  intros * ?.
-  eapply per_univ_elem_sym.
-  eassumption.
+  intros * ?%per_univ_elem_sym.
+  firstorder.
 Qed.
 
-Lemma per_univ_elem_left_irrel : forall i i' A B R A' R',
+Corollary per_univ_elem_left_irrel : forall i i' A B R A' R',
     per_univ_elem i A B R ->
     per_univ_elem i' A' B R' ->
     R = R'.
@@ -243,7 +242,7 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel : forall i i' A B R B' R',
+Corollary per_univ_elem_cross_irrel : forall i i' A B R B' R',
     per_univ_elem i A B R ->
     per_univ_elem i' B' A R' ->
     R = R'.
@@ -284,7 +283,7 @@ Lemma per_univ_elem_trans : forall i A1 A2 R,
           R a1 a2 ->
           R a2 a3 ->
           R a1 a3).
-Proof with solve [eauto using per_bot_trans | econstructor; eauto].
+Proof with ((econstructor + per_univ_elem_econstructor); mautosolve).
   induction 1 using per_univ_elem_ind;
     [> split;
      [ intros * HT2; invert_per_univ_elem HT2; clear HT2
@@ -309,17 +308,16 @@ Proof with solve [eauto using per_bot_trans | econstructor; eauto].
     destruct_rel_mod_eval.
     destruct_rel_mod_app.
     per_univ_elem_irrel_rewrite...
-  - per_univ_elem_econstructor...
+  - idtac...
 Qed.
 
 Corollary per_univ_trans : forall i j A1 A2 A3 R,
     per_univ_elem i A1 A2 R ->
     per_univ_elem j A2 A3 R ->
     per_univ_elem i A1 A3 R.
 Proof.
-  intros * ?.
-  apply per_univ_elem_trans.
-  assumption.
+  intros * ?%per_univ_elem_trans.
+  firstorder.
 Qed.
 
 Corollary per_elem_trans : forall i A1 A2 a1 a2 a3 R,
@@ -328,9 +326,8 @@ Corollary per_elem_trans : forall i A1 A2 a1 a2 a3 R,
     R a2 a3 ->
     R a1 a3.
 Proof.
-  intros * ?.
-  eapply per_univ_elem_trans.
-  eassumption.
+  intros * ?% per_univ_elem_trans.
+  firstorder.
 Qed.
 
 Lemma per_univ_elem_cumu : forall {i a0 a1 R},
@@ -399,22 +396,20 @@ Corollary per_ctx_sym : forall Γ Δ R,
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }}.
 Proof.
-  intros.
-  apply per_ctx_env_sym.
-  assumption.
+  intros * ?%per_ctx_env_sym.
+  firstorder.
 Qed.
 
 Corollary per_env_sym : forall Γ Δ R o p,
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ Dom o ≈ p ∈ R }} ->
     {{ Dom p ≈ o ∈ R }}.
 Proof.
-  intros * ?.
-  eapply per_ctx_env_sym.
-  eassumption.
+  intros * ?%per_ctx_env_sym.
+  firstorder.
 Qed.
 
-Lemma per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
+Corollary per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ' ≈ Δ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
@@ -423,7 +418,7 @@ Proof.
   eauto using per_ctx_env_right_irrel.
 Qed.
 
-Lemma per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
+Corollary per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Δ' ≈ Γ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
@@ -474,16 +469,14 @@ Proof with solve [eauto using per_univ_trans].
   - rename tail_rel0 into tail_rel.
     econstructor; eauto.
     + eapply IHper_ctx_env...
-    + simpl in *.
-      intros.
+    + intros.
       assert (tail_rel p p) by (etransitivity; [| symmetry]; eauto).
-      destruct_rel_mod_eval.
+      (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
       per_univ_elem_irrel_rewrite.
       econstructor...
   - assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by mauto.
     eexists.
-    simpl in *.
-    destruct_rel_mod_eval.
+    (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
     per_univ_elem_irrel_rewrite.
     eapply per_elem_trans...
 Qed.
@@ -493,9 +486,8 @@ Corollary per_ctx_trans : forall Γ1 Γ2 Γ3 R,
     {{ DF Γ2 ≈ Γ3 ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ1 ≈ Γ3 ∈ per_ctx_env ↘ R }}.
 Proof.
-  intros * ?.
-  apply per_ctx_env_trans.
-  assumption.
+  intros * ?% per_ctx_env_trans.
+  firstorder.
 Qed.
 
 Corollary per_env_trans : forall Γ1 Γ2 R p1 p2 p3,
@@ -504,7 +496,6 @@ Corollary per_env_trans : forall Γ1 Γ2 R p1 p2 p3,
     {{ Dom p2 ≈ p3 ∈ R }} ->
     {{ Dom p1 ≈ p3 ∈ R }}.
 Proof.
-  intros * ?.
-  eapply per_ctx_env_trans.
-  eassumption.
+  intros * ?% per_ctx_env_trans.
+  firstorder.
 Qed.
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
@@ -7,11 +7,10 @@ Import Domain_Notations.
 Lemma per_nat_then_per_top : forall {n m},
     {{ Dom n ≈ m ∈ per_nat }} ->
     {{ Dom ⇓ ℕ n ≈ ⇓ ℕ m ∈ per_top }}.
-Proof with solve [eexists; firstorder (econstructor; eauto)].
-  induction 1; simpl in *; intros s.
-  - idtac...
-  - specialize (IHper_nat s) as [? []]...
-  - specialize (H s) as [? []]...
+Proof with solve [destruct_conjs; eexists; repeat econstructor; eauto].
+  induction 1; simpl in *; intros s;
+    try specialize (IHper_nat s);
+    try specialize (H s)...
 Qed.
 
 #[export]
@@ -23,13 +22,14 @@ Lemma realize_per_univ_elem_gen : forall {i a a' R},
     /\ (forall {c c'}, {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }})
     /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
 Proof with (solve [try (try (eexists; split); econstructor); mauto]).
-  intros * H; simpl in H.
+  intros * H. simpl in H.
   induction H using per_univ_elem_ind; repeat split; intros.
   - subst...
   - eexists.
     per_univ_elem_econstructor...
-  - destruct H2.
-    specialize (H1 _ _ _ H2) as [? []].
+  - destruct_by_head per_univ.
+    specialize (H1 _ _ _ H2).
+    destruct_conjs.
     intro s.
     specialize (H1 s) as [? []]...
   - idtac...
@@ -41,17 +41,17 @@ Proof with (solve [try (try (eexists; split); econstructor); mauto]).
     destruct_rel_mod_eval.
     specialize (H10 (S s)) as [? []].
     specialize (H3 s) as [? []]...
-  - rewrite H2; clear H2.
+  - (on_all_hyp: fun H => rewrite H in *; clear H).
     intros c0 c0' equiv_c0_c0'.
-    destruct_all.
+    destruct_conjs.
     destruct_rel_mod_eval.
     econstructor; try solve [econstructor; eauto].
     enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by eauto.
     intro s.
     specialize (H3 s) as [? []].
     specialize (H5 _ _ equiv_c0_c0' s) as [? []]...
-  - rewrite H2 in *; clear H2.
-    destruct_all.
+  - (on_all_hyp: fun H => rewrite H in *; clear H).
+    destruct_conjs.
     intro s.
     assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
     destruct_rel_mod_eval.
@@ -72,8 +72,7 @@ Corollary per_univ_then_per_top_typ : forall {i a a' R},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom a ≈ a' ∈ per_top_typ }}.
 Proof.
-  intros.
-  eapply realize_per_univ_elem_gen; eauto.
+  intros * ?%realize_per_univ_elem_gen; firstorder.
 Qed.
 
 #[export]
@@ -83,8 +82,7 @@ Corollary per_bot_then_per_elem : forall {i a a' R c c'},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }}.
 Proof.
-  intros.
-  eapply realize_per_univ_elem_gen; eauto.
+  intros * ?%realize_per_univ_elem_gen; firstorder.
 Qed.
 
 (** We cannot add [per_bot_then_per_elem] as a hint
@@ -95,8 +93,7 @@ Corollary per_elem_then_per_top : forall {i a a' R b b'},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}.
 Proof.
-  intros.
-  eapply realize_per_univ_elem_gen; eauto.
+  intros * ?%realize_per_univ_elem_gen; firstorder.
 Qed.
 
 #[export]