Gluing Cumulativity (#150)

* Update some others * Prove gluing cumulativity * Replace instances Co-authored-by: Jason Hu <[email protected]> * Move extern hints to LibTactics --------- Co-authored-by: Jason Hu <[email protected]>
Beluga-lang · Aug 1, 2024 · 07c74cc · 07c74cc
1 parent 946b8c4
commit 07c74cc
Show file tree

Hide file tree

Showing 8 changed files with 254 additions and 101 deletions.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
@@ -598,7 +598,7 @@ Proof.
 Qed.
 
 Ltac invert_per_univ_elem H :=
-  (unshelve eapply (per_univ_elem_pi_clean_inversion _) in H; [| eassumption | |]; destruct H as [? []])
+  (unshelve eapply (per_univ_elem_pi_clean_inversion _) in H; shelve_unifiable; [eassumption |]; destruct H as [? []])
   + basic_invert_per_univ_elem H.
 
 Lemma per_univ_elem_cumu : forall i a0 a1 R,

diff --git a/theories/Core/Soundness/Cumulativity.v b/theories/Core/Soundness/Cumulativity.v
@@ -0,0 +1,165 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import Realizability.
+From Mcltt.Core.Soundness Require Export LogicalRelation.
+Import Domain_Notations.
+
+Section glu_univ_elem_cumulativity.
+  #[local]
+  Lemma glu_univ_elem_cumulativity_ge : forall {i j a P P' El El'},
+      i <= j ->
+      {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+      {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+      (forall Γ A, {{ Γ ⊢ A ® P }} -> {{ Γ ⊢ A ® P' }}) /\
+        (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ El }} -> {{ Γ ⊢ M : A ® m ∈ El' }}) /\
+        (forall Γ A M m, {{ Γ ⊢ A ® P }} -> {{ Γ ⊢ M : A ® m ∈ El' }} -> {{ Γ ⊢ M : A ® m ∈ El }}).
+  Proof.
+    simpl.
+    intros * Hge Hglu Hglu'. gen El' P' j.
+    induction Hglu using glu_univ_elem_ind; repeat split; intros;
+      try assert {{ DF a ≈ a ∈ per_univ_elem j ↘ in_rel }} by mauto;
+      invert_glu_univ_elem Hglu';
+      handle_functional_glu_univ_elem;
+      simpl in *;
+      try solve [repeat split; intros; destruct_conjs; mauto 3 | intuition; mauto 4].
+
+    - rename x into IP'.
+      rename x0 into IEl'.
+      rename x1 into OP'.
+      rename x2 into OEl'.
+      destruct_by_head pi_glu_typ_pred.
+      econstructor; intros; mauto 4.
+      + assert {{ Δ ⊢ IT[σ] ® IP }} by mauto.
+        assert (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by (eapply proj1; mauto).
+        mauto.
+      + rename a0 into c.
+        rename equiv_a into equiv_c.
+        match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+        apply_relation_equivalence.
+        destruct_rel_mod_eval.
+        handle_per_univ_elem_irrel.
+        assert (forall Γ A, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ A ® OP' c equiv_c }}) by (eapply proj1; mauto).
+        enough {{ Δ ⊢ OT[σ,,m] ® OP c equiv_c }} by mauto.
+        enough {{ Δ ⊢ m : IT[σ] ® c ∈ IEl }} by mauto.
+        eapply IHHglu; mauto.
+    - rename x into IP'.
+      rename x0 into IEl'.
+      rename x1 into OP'.
+      rename x2 into OEl'.
+      destruct_by_head pi_glu_exp_pred.
+      handle_per_univ_elem_irrel.
+      econstructor; intros; mauto 4.
+      + assert (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by (eapply proj1; mauto).
+        mauto.
+      + rename b into c.
+        rename equiv_b into equiv_c.
+        match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+        handle_per_univ_elem_irrel.
+        destruct_rel_mod_eval.
+        destruct_rel_mod_app.
+        handle_per_univ_elem_irrel.
+        eexists; split; mauto.
+        assert (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }}) by (eapply proj1, proj2; mauto).
+        enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl c equiv_c }} by mauto.
+        assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl }} by (eapply IHHglu; mauto).
+        assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ac ∈ OEl c equiv_c }}) by mauto.
+        destruct_conjs.
+        functional_eval_rewrite_clear.
+        mauto.
+    - rename x into IP'.
+      rename x0 into IEl'.
+      rename x1 into OP'.
+      rename x2 into OEl'.
+      destruct_by_head pi_glu_typ_pred.
+      destruct_by_head pi_glu_exp_pred.
+      handle_per_univ_elem_irrel.
+      econstructor; intros; mauto.
+      rename b into c.
+      rename equiv_b into equiv_c.
+      match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+      handle_per_univ_elem_irrel.
+      destruct_rel_mod_eval.
+      destruct_rel_mod_app.
+      handle_per_univ_elem_irrel.
+      rename a1 into b.
+      eexists; split; mauto.
+      assert (forall Γ A M m, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }}) by (eapply proj2, proj2; eauto 3).
+      assert {{ Δ ⊢ OT[σ,,m'] ® OP c equiv_c }} by mauto.
+      enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl' c equiv_c }} by mauto.
+      assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl' }} by (eapply IHHglu; mauto).
+      assert {{ Δ ⊢ IT[σ] ≈ IT0[σ] : Type@j }} as HITeq.
+      {
+        assert {{ Δ ⊢ IT[σ] ® glu_typ_top i a }} as [] by mauto 3.
+        assert {{ Δ ⊢ IT0[σ] ® glu_typ_top j a }} as [] by mauto 3.
+        match_by_head per_top_typ ltac:(fun H => destruct (H (length Δ)) as [? []]).
+        clear_dups.
+        functional_read_rewrite_clear.
+        assert {{ Δ ⊢ IT[σ][Id] ≈ x1 : Type@i }} by mauto 4.
+        assert {{ Δ ⊢ IT[σ] ≈ x1 : Type@i }} by mauto 4.
+        assert {{ Δ ⊢ IT[σ] ≈ x1 : Type@j }} by mauto 4.
+        assert {{ Δ ⊢ IT0[σ][Id] ≈ x1 : Type@j }} by mauto 4.
+        enough {{ Δ ⊢ IT0[σ] ≈ x1 : Type@j }}; mautosolve 4.
+      }
+      assert {{ Δ ⊢ m' : IT0[σ] ® c ∈ IEl' }} by (rewrite <- HITeq; mauto).
+      assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT0[σ,,m'] ® ac ∈ OEl' c equiv_c }}) by mauto.
+      destruct_conjs.
+      functional_eval_rewrite_clear.
+      enough {{ Δ ⊢ OT[σ,,m'] ≈ OT0[σ,,m'] : Type@j }} by (rewrite glu_univ_elem_elem_morphism_iff1; mauto).
+      assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto.
+      assert {{ DG b ∈ glu_univ_elem j ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
+      assert {{ Δ ⊢ OT0[σ,,m'] ® OP' c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
+      assert {{ Δ ⊢ OT[σ,,m'] ® glu_typ_top i b }} as [] by mauto 3.
+      assert {{ Δ ⊢ OT0[σ,,m'] ® glu_typ_top j b }} as [] by mauto 3.
+      match_by_head per_top_typ ltac:(fun H => destruct (H (length Δ)) as [? []]).
+      clear_dups.
+      functional_read_rewrite_clear.
+      assert {{ Δ ⊢ OT[σ,,m'][Id] ≈ x1 : Type@i }} by mauto 4.
+      assert {{ Δ ⊢ OT[σ,,m'] ≈ x1 : Type@i }} by mauto 4.
+      assert {{ Δ ⊢ OT[σ,,m'] ≈ x1 : Type@j }} by mauto 4.
+      assert {{ Δ ⊢ OT0[σ,,m'][Id] ≈ x1 : Type@j }} by mauto 4.
+      enough {{ Δ ⊢ OT0[σ,,m'] ≈ x1 : Type@j }}; mautosolve 4.
+    - destruct_by_head neut_glu_exp_pred.
+      econstructor; mauto.
+      destruct_by_head neut_glu_typ_pred.
+      econstructor; mauto.
+    - destruct_by_head neut_glu_exp_pred.
+      econstructor; mauto.
+  Qed.
+End glu_univ_elem_cumulativity.
+
+Corollary glu_univ_elem_typ_cumu_ge :  forall {i j a P P' El El' Γ A},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A ® P' }}.
+Proof.
+  intros.
+  eapply glu_univ_elem_cumulativity_ge; mauto.
+Qed.
+
+Corollary glu_univ_elem_exp_cumu_ge :  forall {i j a P P' El El' Γ A M m},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }}.
+Proof.
+  intros * ? ? ?. gen m M A Γ.
+  eapply glu_univ_elem_cumulativity_ge; mauto.
+Qed.
+
+Corollary glu_univ_elem_exp_lower :  forall {i j a P P' El El' Γ A M m},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }}.
+Proof.
+  intros * ? ? ?. gen m M A Γ.
+  eapply glu_univ_elem_cumulativity_ge; mauto.
+Qed.
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -14,7 +14,7 @@ Notation "'glu_typ_pred_args'" := (Tcons ctx (Tcons typ Tnil)).
 Notation "'glu_typ_pred'" := (predicate glu_typ_pred_args).
 Notation "'glu_typ_pred_equivalence'" := (@predicate_equivalence glu_typ_pred_args) (only parsing).
 (* This type annotation is to distinguish this notation from others *)
-Notation "Γ ⊢ A ® R" := ((R Γ A : Prop) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, A custom exp, R constr).
+Notation "Γ ⊢ A ® R" := ((R Γ A : (Prop : Type)) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, A custom exp, R constr).
 
 Notation "'glu_exp_pred_args'" := (Tcons ctx (Tcons typ (Tcons exp (Tcons domain Tnil)))).
 Notation "'glu_exp_pred'" := (predicate glu_exp_pred_args).
@@ -24,10 +24,10 @@ Notation "Γ ⊢ M : A ® m ∈ R" := (R Γ A M m : (Prop : (Type : Type))) (in
 Notation "'glu_sub_pred_args'" := (Tcons ctx (Tcons sub (Tcons env Tnil))).
 Notation "'glu_sub_pred'" := (predicate glu_sub_pred_args).
 Notation "'glu_sub_pred_equivalence'" := (@predicate_equivalence glu_sub_pred_args) (only parsing).
-Notation "Γ ⊢s σ ® ρ ∈ R" := (R Γ σ ρ : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, σ custom exp, ρ custom domain, R constr).
+Notation "Γ ⊢s σ ® ρ ∈ R" := ((R Γ σ ρ : Prop) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, σ custom exp, ρ custom domain, R constr).
 
-Notation "'DG' a ∈ R ↘ P ↘ El" := (R P El a : (Prop : (Type : Type))) (in custom judg at level 90, a custom domain, R constr, P constr, El constr).
-Notation "'EG' A ∈ R ↘ Sb " := (R Sb A : (Prop : (Type : Type))) (in custom judg at level 90, A custom exp, R constr, Sb constr).
+Notation "'DG' a ∈ R ↘ P ↘ El" := (R P El a : ((Prop : Type) : (Type : Type))) (in custom judg at level 90, a custom domain, R constr, P constr, El constr).
+Notation "'EG' A ∈ R ↘ Sb " := (R Sb A : ((Prop : (Type : Type)) : (Type : Type))) (in custom judg at level 90, A custom exp, R constr, Sb constr).
 
 Inductive glu_nat : ctx -> exp -> domain -> Prop :=
 | glu_nat_zero :
@@ -109,6 +109,7 @@ Hint Constructors neut_glu_exp_pred pi_glu_typ_pred pi_glu_exp_pred : mcltt.
 
 Definition univ_glu_typ_pred j i : glu_typ_pred := fun Γ T => {{ Γ ⊢ T ≈ Type@j :  Type@i }}.
 Arguments univ_glu_typ_pred j i Γ T/.
+Transparent univ_glu_typ_pred.
 
 Section Gluing.
   Variable

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -489,28 +489,28 @@ Ltac handle_functional_glu_univ_elem :=
   apply_predicate_equivalence;
   clear_dups.
 
-Lemma glu_univ_elem_pi_clean_inversion : forall {i a p B in_rel elem_rel typ_rel el_rel},
+Lemma glu_univ_elem_pi_clean_inversion : forall {i a p B in_rel typ_rel el_rel},
   {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
-  {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} ->
   {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
   exists IP IEl (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
-     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred),
+     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
       {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} /\
         (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
             {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
             {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
+        {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\
         (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
         (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
 Proof.
   intros *.
   simpl.
-  intros Hinper Hper Hglu.
+  intros Hinper Hglu.
   basic_invert_glu_univ_elem Hglu.
   handle_functional_glu_univ_elem.
   handle_per_univ_elem_irrel.
-  do 4 eexists.
+  do 5 eexists.
   repeat split.
-  1: eassumption.
+  1,3: eassumption.
   1: instantiate (1 := fun c equiv_c Γ A M m => forall (b : domain) Pb Elb,
                           {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
                           {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
@@ -563,9 +563,11 @@ Proof.
     intuition.
 Qed.
 
+Arguments glu_univ_elem_pi_clean_inversion _ _ _ _ _ _ _ _ _ &.
+
 Ltac invert_glu_univ_elem H :=
-  (unshelve eapply (glu_univ_elem_pi_clean_inversion _ _) in H; [eassumption | eassumption | | |];
-   destruct H as [? [? [? [? [? [? []]]]]]])
+  (unshelve eapply (glu_univ_elem_pi_clean_inversion _) in H; shelve_unifiable; [eassumption |];
+   destruct H as [? [? [? [? [? [? [? [? []]]]]]]]])
   + basic_invert_glu_univ_elem H.
 
 Lemma glu_univ_elem_morphism_helper : forall i a a' P El,
@@ -587,6 +589,7 @@ Proof.
     destruct_rel_mod_eval.
     handle_per_univ_elem_irrel.
     intuition.
+  - reflexivity.
   - apply neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
     eassumption.
   - apply neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
@@ -665,39 +668,8 @@ Ltac saturate_glu_info :=
   clear_dups;
   repeat saturate_glu_info1.
 
-(* TODO: strengthen the result (implication from P to P' / El to El') *)
-Lemma glu_univ_elem_cumu_ge : forall {i j a P El},
-    i <= j ->
-    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    exists P' El', {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }}.
-Proof.
-  simpl.
-  intros * Hge Hglu. gen j.
-  induction Hglu using glu_univ_elem_ind; intros;
-    handle_functional_glu_univ_elem; try solve [do 2 eexists; glu_univ_elem_econstructor; try (reflexivity + lia); mauto].
-
-  edestruct IHHglu; [eassumption |].
-  destruct_conjs.
-  do 2 eexists.
-  glu_univ_elem_econstructor; try reflexivity; mauto.
-  instantiate (1 := fun c equiv_c Γ A M m => forall b Pb Elb,
-                        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
-                        glu_univ_elem j Pb Elb b ->
-                        {{ Γ ⊢ M : A ® m ∈ Elb }}).
-  instantiate (1 := fun c equiv_c Γ A => forall b Pb Elb,
-                        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
-                        glu_univ_elem j Pb Elb b ->
-                        {{ Γ ⊢ A ® Pb }}).
-  intros.
-  assert (exists (P' : ctx -> typ -> Prop) (El' : ctx -> typ -> typ -> domain -> Prop), glu_univ_elem j P' El' b) as [] by mauto.
-  destruct_conjs.
-  rewrite simple_glu_univ_elem_morphism_iff; try (eassumption + reflexivity);
-    split; intros; handle_functional_glu_univ_elem; intuition.
-Qed.
-
 #[local]
- Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt.
-
+Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt.
 
 Lemma glu_univ_elem_typ_monotone : forall i a P El,
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -709,7 +681,7 @@ Proof.
   simpl. induction 1 using glu_univ_elem_ind; intros;
     saturate_weakening_escape;
     handle_functional_glu_univ_elem;
-    apply_equiv_left;
+    simpl in *;
     try solve [bulky_rewrite].
   - simpl_glu_rel. econstructor; eauto; try solve [bulky_rewrite]; mauto 3.
     intros.
@@ -719,12 +691,8 @@ Proof.
     destruct_rel_mod_eval.
     simplify_evals.
     deepexec H1 ltac:(fun H => pose proof H).
-    autorewrite with mcltt in H15.
-    autorewrite with mcltt in H17.
-    autorewrite with mcltt.
-    + eapply H11; mauto 2.
-    + econstructor; mauto 2.
-      bulky_rewrite.
+    autorewrite with mcltt in *.
+    mauto 3.
 
   - destruct_conjs.
     split; [mauto 3 |].
@@ -745,7 +713,7 @@ Proof.
   simpl. induction 1 using glu_univ_elem_ind; intros;
     saturate_weakening_escape;
     handle_functional_glu_univ_elem;
-    apply_equiv_left;
+    simpl in *;
     destruct_all.
   - repeat eexists; mauto 2; bulky_rewrite.
     eapply glu_univ_elem_typ_monotone; eauto.
@@ -763,8 +731,7 @@ Proof.
       destruct_rel_mod_app.
       simplify_evals.
       deepexec H1 ltac:(fun H => pose proof H).
-      autorewrite with mcltt in H17.
-      autorewrite with mcltt in H19.
+      autorewrite with mcltt in *.
       repeat eexists; eauto.
       assert {{ Δ0 ⊢s σ0,, m' : Δ, ~ (a_sub IT σ) }}. {
         econstructor; mauto 2.
@@ -781,7 +748,7 @@ Proof.
       }
 
       bulky_rewrite.
-      edestruct H13 with (b := b) as [? []];
+      edestruct H10 with (b := b) as [? []];
         simplify_evals; [| | eassumption];
       mauto.