working on realizability (#140)

* working on realizability * add a few more cases * reorganize * keep moving * improve autorewrite a bit * more rewrite tricks * keep working on more lemmas * need a few more morphisms * readjusted the order of the arguments * keep moving forward * keep moving forward * keep moving forward * finish proof * prettify * finish the lemmas * use this definition instead * comment out lemma * flip instantiation * Update theories/Core/Syntactic/SystemOpt.v Co-authored-by: Junyoung/"Clare" Jang <[email protected]> * move theorems --------- Co-authored-by: Junyoung/"Clare" Jang <[email protected]>
Beluga-lang · Jul 29, 2024 · 1e6f531 · 1e6f531
1 parent 86f48d9
commit 1e6f531
Show file tree

Hide file tree

Showing 17 changed files with 717 additions and 77 deletions.
diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v
@@ -16,9 +16,9 @@ Section completeness_fundamental.
   Theorem completeness_fundamental :
     (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\
       (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\
-      (forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\
+      (forall Γ A M, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\
       (forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}) /\
-      (forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\
+      (forall Γ Δ σ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\
       (forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}) /\
       (forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}).
   Proof.

diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
@@ -235,6 +235,17 @@ Proof.
     [setoid_rewrite <- HRR' | setoid_rewrite HRR']; eassumption.
 Qed.
 
+Lemma domain_app_per : forall f f' a a',
+  {{ Dom f ≈ f' ∈ per_bot }} ->
+  {{ Dom a ≈ a' ∈ per_top }} ->
+  {{ Dom f a ≈ f' a' ∈ per_bot }}.
+Proof.
+  intros. intros s.
+  destruct (H s) as [? []].
+  destruct (H0 s) as [? []].
+  mauto.
+Qed.
+
 Ltac rewrite_relation_equivalence_left :=
   repeat match goal with
     | H : ?R1 <~> ?R2 |- _ =>

diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
@@ -110,3 +110,11 @@ Proof.
     erewrite per_ctx_respects_length; mauto.
     eexists; eauto.
 Qed.
+
+Lemma var_per_elem : forall {A B i R} n,
+    {{ DF A ≈ B ∈ per_univ_elem i ↘ R }} ->
+    {{ Dom ⇑! A n ≈ ⇑! B n ∈ R }}.
+Proof.
+  intros.
+  eapply per_bot_then_per_elem; mauto.
+Qed.
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -16,10 +16,10 @@ Notation "'glu_typ_pred_equivalence'" := (@predicate_equivalence glu_typ_pred_ar
 (* 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 "'glu_exp_pred_args'" := (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil)))).
+Notation "'glu_exp_pred_args'" := (Tcons ctx (Tcons typ (Tcons exp (Tcons domain Tnil)))).
 Notation "'glu_exp_pred'" := (predicate glu_exp_pred_args).
 Notation "'glu_exp_pred_equivalence'" := (@predicate_equivalence glu_exp_pred_args) (only parsing).
-Notation "Γ ⊢ M : A ® m ∈ R" := (R Γ M A m : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp, m custom domain, R constr).
+Notation "Γ ⊢ M : A ® m ∈ R" := (R Γ A M m : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp, m custom domain, R constr).
 
 Notation "'glu_sub_pred_args'" := (Tcons ctx (Tcons sub (Tcons env Tnil))).
 Notation "'glu_sub_pred'" := (predicate glu_sub_pred_args).
@@ -48,7 +48,7 @@ Hint Constructors glu_nat : mcltt.
 Definition nat_glu_typ_pred i : glu_typ_pred := fun Γ M => {{ Γ ⊢ M ≈ ℕ : Type@i }}.
 Arguments nat_glu_typ_pred i Γ M/.
 
-Definition nat_glu_exp_pred i : glu_exp_pred := fun Γ m M a => {{ Γ ⊢ M ® nat_glu_typ_pred i }} /\ glu_nat Γ m a.
+Definition nat_glu_exp_pred i : glu_exp_pred := fun Γ M m a => {{ Γ ⊢ M ® nat_glu_typ_pred i }} /\ glu_nat Γ m a.
 Arguments nat_glu_exp_pred i Γ m M a/.
 
 Definition neut_glu_typ_pred i C : glu_typ_pred :=
@@ -73,6 +73,7 @@ Inductive pi_glu_typ_pred i
   (OP : forall c (equiv_c : {{ Dom c ≈ c ∈ IR }}), glu_typ_pred) : glu_typ_pred :=
 | mk_pi_glu_typ_pred :
     `{ {{ Γ ⊢ M ≈ Π IT OT : Type@i }} ->
+       {{ Γ ⊢ IT : Type@i }} ->
        {{ Γ , IT ⊢ OT : Type@i }} ->
        (forall Δ σ, {{ Δ ⊢w σ : Γ }} -> {{ Δ ⊢ IT[σ] ® IP }}) ->
        (forall Δ σ m a,
@@ -92,6 +93,7 @@ Inductive pi_glu_exp_pred i
   `{ {{ Γ ⊢ m : M }} ->
      {{ Dom a ≈ a ∈ elem_rel }} ->
      {{ Γ ⊢ M ≈ Π IT OT : Type@i }} ->
+       {{ Γ ⊢ IT : Type@i }} ->
      {{ Γ , IT ⊢ OT : Type@i }} ->
      (forall Δ σ, {{ Δ ⊢w σ : Γ }} -> {{ Δ ⊢ IT[σ] ® IP }}) ->
      (forall Δ σ m' b,
@@ -113,7 +115,7 @@ Section Gluing.
       (glu_univ_typ_rec : forall {j}, j < i -> domain -> glu_typ_pred).
 
   Definition univ_glu_exp_pred' {j} (lt_j_i : j < i) : glu_exp_pred :=
-    fun Γ m M A =>
+    fun Γ M m A =>
       {{ Γ ⊢ m : M }} /\
         {{ Γ ⊢ M ≈ Type@j : Type@i }} /\
         {{ Γ ⊢ m ® glu_univ_typ_rec lt_j_i A }}.
@@ -172,7 +174,7 @@ Definition glu_univ_typ (i : nat) (A : domain) : glu_typ_pred :=
 Arguments glu_univ_typ i A Γ M/.
 
 Definition univ_glu_exp_pred j i : glu_exp_pred :=
-    fun Γ m M A =>
+    fun Γ M m A =>
       {{ Γ ⊢ m : M }} /\ {{ Γ ⊢ M ≈ Type@j : Type@i }} /\
         {{ Γ ⊢ m ® glu_univ_typ j A }}.
 Arguments univ_glu_exp_pred j i Γ t T a/.
@@ -250,28 +252,38 @@ Section GluingInduction.
   Qed.
 End GluingInduction.
 
-Inductive glu_neut i A Γ m M c : Prop :=
-| mk_glu_neut :
-    {{ Γ ⊢ m : M }} ->
-    {{ Γ ⊢ M ® glu_univ_typ i A }} ->
+Inductive glu_elem_bot i A Γ T t c : Prop :=
+| glu_elem_bot_make : forall P El,
+    {{ Γ ⊢ t : T }} ->
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ Γ ⊢ T ® P }} ->
     {{ Dom c ≈ c ∈ per_bot }} ->
-    (forall Δ σ a, {{ Δ ⊢w σ : Γ }} -> {{ Rne c in length Δ ↘ a }} -> {{ Δ ⊢ m[σ] ≈ a : M[σ] }}) ->
-    {{ Γ ⊢ m : M ® c ∈ glu_neut i A }}.
+    (forall Δ σ w, {{ Δ ⊢w σ : Γ }} -> {{ Rne c in length Δ ↘ w }} -> {{ Δ ⊢ t [ σ ] ≈ w : T [ σ ] }}) ->
+    {{ Γ ⊢ t : T ® c ∈ glu_elem_bot i A }}.
+#[export]
+  Hint Constructors glu_elem_bot : mcltt.
 
-Inductive glu_norm i A Γ m M a : Prop :=
-| mk_glu_norm :
-    {{ Γ ⊢ m : M }} ->
-    {{ Γ ⊢ M ® glu_univ_typ i A }} ->
-    {{ Dom ⇓ A a ≈ ⇓ A a ∈ per_top }} ->
-    (forall Δ σ b, {{ Δ ⊢w σ : Γ }} -> {{ Rnf ⇓ A a in length Δ ↘ b }} -> {{ Δ ⊢ m [ σ ] ≈  b : M [ σ ] }}) ->
-    {{ Γ ⊢ m : M ® a ∈ glu_norm i A }}.
 
-Inductive glu_typ i A Γ M : Prop :=
-| mk_glu_typ : forall P El,
-    {{ Γ ⊢ M : Type@i }} ->
+Inductive glu_elem_top i A Γ T t a : Prop :=
+| glu_elem_top_make : forall P El,
+    {{ Γ ⊢ t : T }} ->
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    (forall Δ σ a, {{ Δ ⊢w σ : Γ }} -> {{ Rtyp A in length Δ ↘ a }} -> {{ Δ ⊢ M[σ] ≈ a : Type@i }}) ->
-    {{ Γ ⊢ M ® glu_typ i A }}.
+    {{ Γ ⊢ T ® P }} ->
+    {{ Dom ⇓ A a ≈ ⇓ A a ∈ per_top }} ->
+    (forall Δ σ w, {{ Δ ⊢w σ : Γ }} -> {{ Rnf ⇓ A a in length Δ ↘ w }} -> {{ Δ ⊢ t [ σ ] ≈ w : T [ σ ] }}) ->
+    {{ Γ ⊢ t : T ® a ∈ glu_elem_top i A }}.
+#[export]
+  Hint Constructors glu_elem_top : mcltt.
+
+
+Inductive glu_typ_top i A Γ T : Prop :=
+| glu_typ_top_make :
+    {{ Γ ⊢ T : Type@i }} ->
+    {{ Dom A ≈ A ∈ per_top_typ }} ->
+    (forall Δ σ W, {{ Δ ⊢w σ : Γ }} -> {{ Rtyp A in length Δ ↘ W }} -> {{ Δ ⊢ T [ σ ] ≈ W : Type@i }}) ->
+    {{ Γ ⊢ T ® glu_typ_top i A }}.
+#[export]
+  Hint Constructors glu_typ_top : mcltt.
 
 Ltac invert_glu_rel1 :=
   match goal with

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -15,7 +15,7 @@ Lemma pi_glu_exp_pred_pi_glu_typ_pred : forall i IR IP IEl (OP : forall c (equiv
 Proof.
   inversion_clear 1; econstructor; eauto.
   intros.
-  edestruct H5 as [? []]; eauto.
+  edestruct H6 as [? []]; eauto.
 Qed.
 
 Lemma glu_nat_per_nat : forall Γ m a,
@@ -113,6 +113,16 @@ Proof.
   assert {{ Δ ⊢ T[σ] ≈ V : Type@i }}; mauto.
 Qed.
 
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (P Γ)
+    with signature wf_exp_eq Γ {{{Type@i}}} ==> iff as glu_univ_elem_typ_morphism_iff1.
+Proof.
+  intros. split; intros;
+    eapply glu_univ_elem_typ_resp_equiv;
+    mauto 2.
+Qed.
+
+
 Lemma glu_univ_elem_trm_resp_typ_equiv : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ t T a T',
@@ -128,6 +138,14 @@ Proof.
   assert {{ Δ ⊢ M[σ] ≈ V : Type@i }}; mauto.
 Qed.
 
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (El Γ)
+    with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_elem_morphism_iff1.
+Proof.
+  split; intros;
+    eapply glu_univ_elem_trm_resp_typ_equiv;
+    mauto 2.
+Qed.
+
 Lemma glu_univ_elem_typ_resp_ctx_equiv : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ T Δ,
@@ -141,6 +159,15 @@ Proof.
     econstructor; mauto.
 Qed.
 
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : P
+    with signature wf_ctx_eq ==> eq ==> iff as glu_univ_elem_typ_morphism_iff2.
+Proof.
+  intros. split; intros;
+    eapply glu_univ_elem_typ_resp_ctx_equiv;
+    mauto 2.
+Qed.
+
+
 Lemma glu_nat_resp_wk' : forall Γ m a,
     glu_nat Γ m a ->
     forall Δ σ,
@@ -242,7 +269,7 @@ Proof.
   match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
   intros.
   destruct_rel_mod_eval.
-  edestruct H11 as [? []]; eauto.
+  edestruct H12 as [? []]; eauto.
 Qed.
 
 Lemma glu_univ_elem_trm_univ_lvl : forall i P El A,
@@ -274,7 +301,7 @@ Proof.
     intros.
     destruct_rel_mod_eval.
     assert {{ Δ ⊢ m' : IT [σ]}} by eauto using glu_univ_elem_trm_escape.
-    edestruct H12 as [? []]; eauto.
+    edestruct H13 as [? []]; eauto.
     eexists; split; eauto.
     enough {{ Δ ⊢ m[σ] m' ≈ t'[σ] m' : OT[σ,,m'] }} by eauto.
     assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
@@ -289,6 +316,16 @@ Proof.
     mauto 4.
 Qed.
 
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ T : (El Γ T)
+    with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_elem_morphism_iff2.
+Proof.
+  split; intros;
+    eapply glu_univ_elem_trm_resp_equiv;
+    mauto 2.
+Qed.
+
+
 Lemma glu_univ_elem_core_univ' : forall j i typ_rel el_rel,
     j < i ->
     (typ_rel <∙> univ_glu_typ_pred j i) ->
@@ -482,7 +519,7 @@ Proof.
   do 4 eexists.
   repeat split.
   1: eassumption.
-  1: instantiate (1 := fun c equiv_c Γ M A m => forall (b : domain) Pb Elb,
+  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 }} ->
                           {{ Γ ⊢ M : A ® m ∈ Elb }}).
@@ -496,7 +533,7 @@ Proof.
     assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
     apply -> simple_glu_univ_elem_morphism_iff; [| reflexivity | |]; [eauto | |].
     + intros ? ? ? ?.
-      split; [intros; handle_functional_glu_univ_elem |]; intuition.
+      split; intros; handle_functional_glu_univ_elem; intuition.
     + intros ? ?.
       split; [intros; handle_functional_glu_univ_elem |]; intuition.
   - rename a0 into c.
@@ -596,7 +633,7 @@ Proof.
     do 2 eexists.
     glu_univ_elem_econstructor; try (eassumption + reflexivity).
     + saturate_refl; eassumption.
-    + instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ M A m =>
+    + instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ A M m =>
                           forall b P El,
                             {{ ⟦ B' ⟧ p' ↦ c ↘ b }} ->
                             glu_univ_elem i P El b ->
@@ -620,6 +657,22 @@ Proof.
     glu_univ_elem_econstructor; try reflexivity; mauto.
 Qed.
 
+Ltac saturate_glu_info1 :=
+  match goal with
+  | H : glu_univ_elem _ ?P _ _,
+      H1 : ?P _ _ |- _ =>
+      pose proof (glu_univ_elem_univ_lvl _ _ _ _ H _ _ H1);
+      fail_if_dup
+  | H : glu_univ_elem _ _ ?El _,
+      H1 : ?El _ _ _ _ |- _ =>
+      pose proof (glu_univ_elem_trm_escape _ _ _ _ H _ _ _ _ H1);
+      fail_if_dup
+  end.
+
+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 ->
@@ -635,7 +688,7 @@ Proof.
   destruct_conjs.
   do 2 eexists.
   glu_univ_elem_econstructor; try reflexivity; mauto.
-  instantiate (1 := fun c equiv_c Γ M A m => forall b Pb Elb,
+  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 }}).