Prove subtyping case for soundness

theories/Core/Soundness/EquivalenceLemmas.v

@@ -80,3 +80,15 @@ Proof.
     assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
     mauto 4.
 Qed.
+
+Lemma glu_univ_elem_per_univ_typ_iff : forall {i a a' P P' El El'},
+    {{ Dom a ≈ a' ∈ per_univ i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    (P <∙> P') /\ (El <∙> El').
+Proof.
+  intros * Hper **.
+  eapply functional_glu_univ_elem;
+    [eassumption | rewrite Hper];
+    eassumption.
+Qed.

theories/Core/Soundness/SubtypingLemmas.v

@@ -0,0 +1,164 @@
+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 EquivalenceLemmas.
+Import Domain_Notations.
+
+Lemma glu_univ_elem_per_subtyp_typ_escape : forall {i a a' P P' El El' Γ A A'},
+    {{ Sub a <: a' at i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ A ⊆ A' }}.
+Proof.
+  intros * Hsubtyp Hglu Hglu' HA HA'.
+  gen A' A Γ. gen El' El P' P.
+  induction Hsubtyp using per_subtyp_ind; intros; subst;
+    saturate_refl_for per_univ_elem;
+    invert_glu_univ_elem Hglu;
+    handle_functional_glu_univ_elem;
+    handle_per_univ_elem_irrel;
+    destruct_by_head pi_glu_typ_pred;
+    saturate_glu_by_per;
+    invert_glu_univ_elem Hglu';
+    handle_functional_glu_univ_elem;
+    try solve [simpl in *; mauto 4].
+  - match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Γ)) as [V []]).
+    simpl in *.
+    destruct_conjs.
+    assert {{ Γ ⊢ A[Id] ≈ A : Type@i }} as <- by mauto 4.
+    assert {{ Γ ⊢ A'[Id] ≈ A' : Type@i }} as <- by mauto 4.
+    assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
+    econstructor.
+    mauto 4.
+  - bulky_rewrite.
+    mauto 3.
+  - destruct_by_head pi_glu_typ_pred.
+    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
+    rename M0 into M'. rename IT0 into IT'. rename OT0 into OT'.
+    rename x3 into OP'. rename x4 into OEl'.
+    assert {{ Γ ⊢ IT ® IP }}.
+    {
+      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    assert {{ Γ ⊢ IT' ® IP }}.
+    {
+      assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    do 2 bulky_rewrite1.
+    assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto 4 using glu_univ_elem_per_univ_typ_escape.
+    enough {{ Γ, IT' ⊢ OT ⊆ OT' }} by mauto 3.
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
+    handle_per_univ_elem_irrel.
+    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.
+    rename a1 into b.
+    rename a3 into b'.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto.
+    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
+    assert {{ Γ, IT' ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}.
+    {
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by eauto using var_glu_elem_bot.
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ ⊢ Γ, IT' ≈ Γ, IT }} as -> by mauto.
+      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    assert {{ Γ, IT' ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}.
+    {
+      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® !(length Γ) ∈ glu_elem_bot i a' }} by eauto using var_glu_elem_bot.
+      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® ⇑! a' (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
+      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ≈ OT' : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    mauto 3.
+Qed.
+
+Lemma glu_univ_elem_per_subtyp_typ_if : forall {i a a' P P' El El' Γ A},
+    {{ Sub a <: a' at i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    exists A', {{ Γ ⊢ A' ® P' }}.
+Proof.
+  intros * Hsubtyp Hglu Hglu'.
+  gen A Γ. gen El' El P' P.
+  induction Hsubtyp using per_subtyp_ind; intros; subst;
+    saturate_refl_for per_univ_elem;
+    invert_glu_univ_elem Hglu;
+    handle_functional_glu_univ_elem;
+    handle_per_univ_elem_irrel;
+    destruct_by_head pi_glu_typ_pred;
+    saturate_glu_by_per;
+    invert_glu_univ_elem Hglu';
+    try solve [eexists; handle_functional_glu_univ_elem; simpl in *; mauto 4];
+    handle_functional_glu_univ_elem.
+  - exists A; handle_functional_glu_univ_elem.
+    split; firstorder.
+    match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Δ)) as [V' []]).
+    functional_read_rewrite_clear.
+    mauto.
+  - handle_per_univ_elem_irrel.
+    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
+    rename x3 into OP'. rename x4 into OEl'.
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
+    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.
+    rename a1 into b.
+    rename a3 into b'.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto.
+    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
+    assert {{ Γ ⊢ IT ® IP }}.
+    {
+      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}.
+    {
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by mauto using var_glu_elem_bot.
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    assert (exists OT', {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}) as [OT'] by mauto.
+    assert {{ Γ, IT ⊢ OT' : Type@i }} by mauto 3 using glu_univ_elem_univ_lvl.
+    exists {{{ Π IT OT' }}}.
+    apply_predicate_equivalence.
+    econstructor; mauto 4.
+    (* stuck.... *)
+    intros.
+    destruct_rel_mod_eval.
+    handle_per_univ_elem_irrel.
+    rename a1 into c.
+    rename equiv_a into equiv_c.
+    rename a2 into b0.
+    rename a7 into b'0.
+    assert (exists OT'', {{ Δ ⊢ OT'' ® OP' c equiv_c }}) as [OT''] by mauto.
+    assert {{ Γ, IT ⊢ OT' ® glu_typ_top i b' }} as [] by mauto 4.
+    assert {{ Δ ⊢ OT'' ® glu_typ_top i b'0 }} as [] by mauto 4.
+    assert {{ DG b'0 ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
+    enough {{ Δ ⊢ OT'[σ,,m] ≈ OT'' : Type@i }} as -> by mauto.
+    (* assert {{ Δ ⊢ OT''[Id] ≈ OT'' : Type@i }} as <- by mauto. *)
+    (* assert {{ Δ ⊢ m : IT[σ] }} by mauto 3 using glu_univ_elem_trm_escape. *)
+    (* assert {{ Δ ⊢s σ : Γ }} by mauto. *)
+    (* assert {{ Δ ⊢s Wk∘(Id,,m) ≈ Id : Δ }} as <- by mauto 3. *)
+    (* assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *)
+Abort.