Optimize completeness proofs (#102)

Beluga-lang · Jun 6, 2024 · ea9682c · ea9682c
1 parent 0371a75
commit ea9682c
Show file tree

Hide file tree

Showing 9 changed files with 304 additions and 266 deletions.
diff --git a/theories/Core/Completeness/ContextCases.v b/theories/Core/Completeness/ContextCases.v
@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.UniverseCases System.
 Import Domain_Notations.
 
 Proposition valid_ctx_empty :
@@ -20,8 +20,8 @@ Lemma rel_ctx_extend : forall {Γ Γ' A A' i},
 Proof with intuition.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓΓ'] [env_relΓ].
-  pose (env_relΓ0 := env_relΓ).
+  intros * [env_relΓΓ'] [env_relΓ]%rel_exp_of_typ_inversion.
+  pose env_relΓ.
   destruct_conjs.
   handle_per_ctx_env_irrel.
   eexists.
@@ -32,14 +32,11 @@ Proof with intuition.
                           R m m').
     intros.
     (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-    destruct_by_head rel_typ.
-    invert_rel_typ_body.
-    destruct_by_head rel_exp.
-    destruct_conjs.
+    destruct_by_head per_univ.
     econstructor; eauto.
     apply -> per_univ_elem_morphism_iff; eauto.
     split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
-    eapply H10.
+    eapply H7.
     mauto.
   - apply Equivalence_Reflexive.
 Qed.

diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
@@ -1,14 +1,35 @@
 From Coq Require Import Morphisms_Relations Relation_Definitions RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases System.
+From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.TermStructureCases Completeness.UniverseCases System.
 Import Domain_Notations.
 
+Lemma rel_exp_of_pi_inversion : forall {Γ M M' A B},
+    {{ Γ ⊨ M ≈ M' : Π A B }} ->
+    exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
+    forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+    exists in_rel out_rel,
+      rel_typ i A p A p' in_rel /\
+        (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_typ i B d{{{ p ↦ c }}} B d{{{ p' ↦ c' }}} (out_rel c c' equiv_c_c')) /\
+        rel_exp M p M' p'
+          (fun f f' : domain => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app f c f' c' (out_rel c c' equiv_c_c')).
+Proof.
+  intros * [env_relΓ].
+  destruct_conjs.
+  eexists_rel_exp.
+  intros.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  do 2 eexists; repeat split; mauto.
+Qed.
+
 #[local]
 Ltac extract_output_info_with p c p' c' env_rel :=
   let Hequiv := fresh "equiv" in
-  (assert (Hequiv : {{ Dom p ↦ c ≈ p' ↦ c' ∈ env_rel }}) by (apply_relation_equivalence; eexists; eauto);
+  (assert (Hequiv : {{ Dom p ↦ c ≈ p' ↦ c' ∈ env_rel }}) by (apply_relation_equivalence; mauto 4);
    apply_relation_equivalence;
-   (on_all_hyp: fun H => destruct (H _ _ Hequiv) as [? []]);
+   (on_all_hyp: fun H => destruct (H _ _ Hequiv));
+   destruct_conjs;
    destruct_by_head rel_typ;
    destruct_by_head rel_exp).
 
@@ -43,29 +64,21 @@ Lemma rel_exp_pi_cong : forall {i Γ A A' B B'},
 Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓ] [env_relΓA].
+  intros * [env_relΓ]%rel_exp_of_typ_inversion [env_relΓA]%rel_exp_of_typ_inversion.
   destruct_conjs.
-  pose (env_relΓA0 := env_relΓA).
+  pose env_relΓA.
   match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
-  eexists_rel_exp.
+  eexists_rel_exp_of_typ.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
-  destruct_conjs.
+  destruct_by_head per_univ.
   handle_per_univ_elem_irrel.
-  eexists (per_univ _).
-  split; econstructor; mauto.
+  econstructor; mauto.
   eexists.
   per_univ_elem_econstructor; eauto.
   - intros.
-    eapply rel_exp_pi_core; eauto; try reflexivity.
-    clear dependent c.
-    clear dependent c'.
-    intros.
-    extract_output_info_with p c p' c' env_relΓA.
-    invert_rel_typ_body...
+    eapply rel_exp_pi_core; eauto.
+    reflexivity.
   - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
     apply Equivalence_Reflexive.
 Qed.
@@ -81,35 +94,28 @@ Lemma rel_exp_pi_sub : forall {i Γ σ Δ A B},
 Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓ] [env_relΔ] [env_relΔA].
+  intros * [env_relΓ] [env_relΔ]%rel_exp_of_typ_inversion [env_relΔA]%rel_exp_of_typ_inversion.
   destruct_conjs.
-  pose (env_relΔ0 := env_relΔ).
-  pose (env_relΔA0 := env_relΔA).
+  pose env_relΔ.
+  pose env_relΔA.
   match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
-  eexists_rel_exp.
+  eexists_rel_exp_of_typ.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  assert {{ Dom o' ≈ o' ∈ env_relΔ }} by (etransitivity; [symmetry|]; eassumption).
+  assert {{ Dom o' ≈ o' ∈ env_relΔ }} by (etransitivity; [symmetry |]; eassumption).
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
-  destruct_conjs.
+  destruct_by_head per_univ.
   handle_per_univ_elem_irrel.
-  eexists.
-  split; econstructor; mauto.
+  econstructor; mauto.
   eexists.
   per_univ_elem_econstructor; eauto.
   - intros.
     eapply rel_exp_pi_core; eauto; try reflexivity.
     clear dependent c.
     clear dependent c'.
     intros.
-    extract_output_info_with o c o' c' env_relΔA.
-    invert_rel_typ_body.
-    destruct_conjs.
-    econstructor...
+    extract_output_info_with o c o' c' env_relΔA...
   - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
     apply Equivalence_Reflexive.
 Qed.
@@ -124,17 +130,15 @@ Lemma rel_exp_fn_cong : forall {i Γ A A' B M M'},
 Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓ] [env_relΓA].
+  intros * [env_relΓ]%rel_exp_of_typ_inversion [env_relΓA].
   destruct_conjs.
-  pose (env_relΓA0 := env_relΓA).
+  pose env_relΓA.
   match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
+  destruct_by_head per_univ.
   functional_eval_rewrite_clear.
   eexists.
   split; econstructor; mauto.
@@ -170,15 +174,15 @@ Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓ [? [env_relΔ]]] [env_relΔA].
   destruct_conjs.
-  pose (env_relΔA0 := env_relΔA).
+  pose env_relΔA.
   match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
   eexists.
-  split; econstructor; mauto.
+  split; econstructor; mauto 4.
   - per_univ_elem_econstructor; [eapply per_univ_elem_cumu_max_left | |]; eauto.
     + intros.
       eapply rel_exp_pi_core; eauto; try reflexivity.
@@ -209,21 +213,19 @@ Lemma rel_exp_app_cong : forall {Γ M M' A B N N'},
 Proof with intuition.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓ] [].
+  intros * [env_relΓ]%rel_exp_of_pi_inversion [].
   destruct_conjs.
-  pose (env_relΓ0 := env_relΓ).
+  pose env_relΓ.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
-  assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eauto).
+  assert (equiv_p'_p' : env_relΓ p' p') by (etransitivity; [symmetry |]; eassumption).
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  rename x2 into in_rel.
   destruct_by_head rel_typ.
-  handle_per_univ_elem_irrel.
-  invert_rel_typ_body.
   destruct_by_head rel_exp.
-  functional_eval_rewrite_clear.
-  rename x into in_rel.
-  assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eauto).
+  handle_per_univ_elem_irrel.
+  assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eassumption).
   assert (in_rel m1 m'2) by intuition.
   (on_all_hyp: destruct_rel_by_assumption in_rel).
   handle_per_univ_elem_irrel.
@@ -242,19 +244,19 @@ Lemma rel_exp_app_sub : forall {Γ σ Δ M A B N},
 Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓ] [env_relΔ] [].
+  intros * [env_relΓ] [env_relΔ]%rel_exp_of_pi_inversion [].
   destruct_conjs.
-  pose (env_relΓ0 := env_relΓ).
-  pose (env_relΔ0 := env_relΔ).
+  pose env_relΓ.
+  pose env_relΔ.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
+  rename x0 into in_rel.
   destruct_by_head rel_typ.
-  invert_rel_typ_body.
+  handle_per_univ_elem_irrel.
   destruct_by_head rel_exp.
-  rename x into in_rel.
   (on_all_hyp_rev: destruct_rel_by_assumption in_rel).
   eexists.
   split; econstructor...
@@ -272,7 +274,7 @@ Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓA] [env_relΓ].
   destruct_conjs.
-  pose (env_relΓA0 := env_relΓA).
+  pose env_relΓA.
   match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_rel_exp.
@@ -297,19 +299,21 @@ Lemma rel_exp_pi_eta : forall {Γ M A B},
 Proof with mautosolve.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
-  intros * [env_relΓ].
+  intros * [env_relΓ]%rel_exp_of_pi_inversion.
   destruct_conjs.
-  pose (env_relΓ0 := env_relΓ).
+  pose env_relΓ.
   eexists_rel_exp.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  rename x into in_rel.
   destruct_by_head rel_typ.
-  invert_rel_typ_body.
   destruct_by_head rel_exp.
   eexists.
   split; econstructor; mauto.
-  intros ? **.
-  (on_all_hyp: destruct_rel_by_assumption in_rel)...
+  - per_univ_elem_econstructor; mauto.
+    apply Equivalence_Reflexive.
+  - intros ? **.
+    (on_all_hyp: destruct_rel_by_assumption in_rel)...
 Qed.
 
 #[export]

diff --git a/theories/Core/Completeness/LogicalRelation/Lemmas.v b/theories/Core/Completeness/LogicalRelation/Lemmas.v
@@ -1,6 +1,6 @@
-From Coq Require Import Morphisms Morphisms_Relations RelationClasses.
+From Coq Require Import Morphisms Morphisms_Relations RelationClasses Relation_Definitions.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core.Completeness Require Import LogicalRelation.Definitions.
+From Mcltt.Core.Completeness Require Import LogicalRelation.Definitions LogicalRelation.Tactics.
 Import Domain_Notations.
 
 Add Parametric Morphism M p M' p' : (rel_exp M p M' p')

diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -14,13 +14,16 @@ Ltac eexists_rel_sub :=
   eexists;
   eexists; [eassumption |].
 
-Ltac invert_rel_typ_body :=
+Ltac simplify_evals :=
   functional_eval_rewrite_clear;
   clear_dups;
   repeat (match_by_head eval_exp ltac:(fun H => directed inversion H; subst; clear H)
           || match_by_head eval_sub ltac:(fun H => directed inversion H; subst; clear H));
   functional_eval_rewrite_clear;
-  clear_dups;
+  clear_dups.
+
+Ltac invert_rel_typ_body :=
+  simplify_evals;
   match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H); subst;
   clear_dups;
   clear_refl_eqs;