Change system rules

theories/Algorithmic/Subtyping/Lemmas.v

@@ -21,7 +21,7 @@ Lemma alg_subtyping_nf_sound : forall M N,
       {{ Γ ⊢ M ⊆ N }}.
 Proof.
   induction 1; intros; subst; simpl in *.
-  - econstructor. mauto.
+  - eapply wf_subtyp_refl'; mauto.
   - assert (i < j \/ i = j) as H2 by lia.
     destruct H2; mauto 3.
   - on_all_hyp: fun H => (apply wf_pi_inversion in H; destruct H as [? ?]).
@@ -33,6 +33,8 @@ Proof.
                fail_if_dup
            end.
     apply_subtyping.
+    assert {{ Γ, ~(nf_to_exp A') ⊢ B : Type@(max x x0) }} by mauto using lift_exp_max_right.
+    assert {{ Γ, ~(nf_to_exp A') ⊢ B' : Type@(max x x0) }} by mauto using lift_exp_max_left.
     deepexec IHalg_subtyping_nf ltac:(fun H => pose proof H).
     mauto 3.
 Qed.
@@ -80,8 +82,8 @@ Lemma alg_subtyping_complete : forall Γ M N,
     {{ Γ ⊢a M ⊆ N }}.
 Proof.
   induction 1; mauto.
-  - apply completeness in H.
-    destruct H as [W [? ?]].
+  - apply completeness in H0.
+    destruct H0 as [W [? ?]].
     econstructor; mauto.
   - assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto.
     assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto.

theories/Core/Completeness/FundamentalTheorem.v

@@ -13,7 +13,6 @@ From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Section completeness_fundamental.
-
   Theorem completeness_fundamental :
     (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\
       (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\
@@ -37,7 +36,7 @@ Section completeness_fundamental.
   Theorem completeness_fundamental_ctx : forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}.
   Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_ctx_sub : forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}.
+  Theorem completeness_fundamental_ctx_subtyp : forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}.
   Proof. solve_it. Qed.
 
   Theorem completeness_fundamental_exp : forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}.
@@ -59,8 +58,7 @@ Section completeness_fundamental.
   Proof.
     induction 1.
     - apply valid_ctx_empty.
-    - apply completeness_fundamental_exp_eq in H2.
+    - assert {{ Γ ⊨ A ≈ A' : Type@i }} by mauto using completeness_fundamental_exp_eq.
       mauto.
   Qed.
-
 End completeness_fundamental.

theories/Core/Completeness/LogicalRelation/Definitions.v

@@ -45,15 +45,15 @@ Hint Transparent valid_sub_under_ctx : mcltt.
 #[export]
 Hint Unfold valid_sub_under_ctx : mcltt.
 
-Definition sub_typ_under_ctx Γ M M' :=
+Definition subtyp_under_ctx Γ M M' :=
   exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
   forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
     exists R R', rel_typ i M p M p' R /\ rel_typ i M' p M' p' R' /\ rel_exp M p M' p' (per_subtyp i).
 
 Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
 Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).
 Notation "Γ ⊨ M ≈ M' : A" := (rel_exp_under_ctx Γ A M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
-Notation "Γ ⊨ M ⊆ M'" := (sub_typ_under_ctx Γ M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp).
+Notation "Γ ⊨ M ⊆ M'" := (subtyp_under_ctx Γ M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp).
 Notation "Γ ⊨ M : A" := (valid_exp_under_ctx Γ A M) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
 Notation "Γ ⊨s σ ≈ σ' : Δ" := (rel_sub_under_ctx Γ Δ σ σ') (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
 Notation "Γ ⊨s σ : Δ" := (valid_sub_under_ctx Γ Δ σ) (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).

theories/Core/Completeness/LogicalRelation/Tactics.v

@@ -18,12 +18,12 @@ Ltac eexists_rel_sub :=
   eexists;
   eexists; [eassumption |].
 
-Ltac eexists_sub_typ :=
+Ltac eexists_subtyp :=
   eexists;
   eexists; [eassumption |];
   eexists.
 
-Ltac eexists_sub_typ_with i :=
+Ltac eexists_subtyp_with i :=
   eexists;
   eexists; [eassumption |];
   exists i.

theories/Core/Completeness/SubtypingCases.v

@@ -3,13 +3,13 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.FunctionCases Evaluation.
 Import Domain_Notations.
 
-Lemma sub_typ_subtyp_refl : forall Γ M M' i,
+Lemma subtyp_refl : forall Γ M M' i,
     {{ Γ ⊨ M ≈ M' : Type@i }} ->
     {{ Γ ⊨ M ⊆ M' }}.
 Proof.
   intros * [env_relΓ].
   destruct_conjs.
-  eexists_sub_typ.
+  eexists_subtyp.
   intros.
   saturate_refl.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -23,7 +23,7 @@ Proof.
     etransitivity; try eassumption; symmetry; eassumption.
 Qed.
 
-Lemma sub_typ_subtyp_trans : forall Γ M M' M'',
+Lemma subtyp_trans : forall Γ M M' M'',
     {{ Γ ⊨ M ⊆ M' }} ->
     {{ Γ ⊨ M' ⊆ M'' }} ->
     {{ Γ ⊨ M ⊆ M'' }}.
@@ -32,7 +32,7 @@ Proof.
   destruct_conjs.
   pose env_relΓ.
   handle_per_ctx_env_irrel.
-  eexists_sub_typ_with (max i j).
+  eexists_subtyp_with (max i j).
   intros.
   saturate_refl.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -48,16 +48,16 @@ Proof.
 Qed.
 
 #[export]
-Instance sub_typ_trans Γ : Transitive (sub_typ_under_ctx Γ).
-Proof. eauto using sub_typ_subtyp_trans. Qed.
+Instance subtyp_Transitive Γ : Transitive (subtyp_under_ctx Γ).
+Proof. eauto using subtyp_trans. Qed.
 
-Lemma sub_typ_subtyp_univ : forall Γ i j,
+Lemma subtyp_univ : forall Γ i j,
     {{ ⊨ Γ }} ->
     i < j ->
     {{ Γ ⊨ Type@i ⊆ Type@j }}.
 Proof.
   intros * [env_relΓ] ?.
-  eexists_sub_typ.
+  eexists_subtyp.
   intros.
   assert (i < S (max i j)) by lia.
   assert (j < S (max i j)) by lia.
@@ -68,7 +68,7 @@ Proof.
   econstructor; lia.
 Qed.
 
-Lemma sub_typ_subtyp_pi : forall Γ A A' B B' i,
+Lemma subtyp_pi : forall Γ A A' B B' i,
   {{ Γ ⊨ A ≈ A' : Type@i }} ->
   {{ Γ , A' ⊨ B ⊆ B' }} ->
   {{ Γ ⊨ Π A B ⊆ Π A' B' }}.
@@ -79,7 +79,7 @@ Proof.
   pose env_relΓA'.
   match_by_head (per_ctx_env env_relΓA') invert_per_ctx_env.
   handle_per_ctx_env_irrel.
-  eexists_sub_typ.
+  eexists_subtyp.
   intros.
   saturate_refl.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -140,4 +140,4 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve sub_typ_subtyp_refl sub_typ_subtyp_trans sub_typ_subtyp_univ sub_typ_subtyp_pi : mcltt.
+Hint Resolve subtyp_refl subtyp_trans subtyp_univ subtyp_pi : mcltt.

theories/Core/Soundness/FundamentalTheorem.v

@@ -14,21 +14,13 @@ From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Section soundness_fundamental.
-
   Theorem soundness_fundamental :
     (forall Γ, {{ ⊢ Γ }} -> {{ ⊩ Γ }}) /\
       (forall Γ A M, {{ Γ ⊢ M : A }} -> {{ Γ ⊩ M : A }}) /\
       (forall Γ Δ σ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊩s σ : Δ }}).
   Proof.
     apply syntactic_wf_mut_ind'; mauto 3.
-
-    - intros.
-      assert (exists i, {{ Γ ⊩ A' : Type@i }}) as [] by admit. (* this should be added to the syntactic judgement *)
-      mauto.
-    - intros.
-      assert {{ ⊩ Δ' }} by admit. (* this should be added to the syntactic judgement *)
-      mauto.
-  Admitted.
+  Qed.
 
   #[local]
   Ltac solve_it := pose proof soundness_fundamental; firstorder.
@@ -41,5 +33,4 @@ Section soundness_fundamental.
 
   Theorem soundness_fundamental_sub : forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊩s σ : Δ }}.
   Proof. solve_it. Qed.
-
 End soundness_fundamental.

theories/Core/Soundness/LogicalRelation/CoreLemmas.v

@@ -821,19 +821,20 @@ Proof.
         bulky_rewrite.
       }
       assert {{Δ0 ⊢ (m [σ][σ0]) m' ≈ (m [σ ∘ σ0]) m' : OT [σ ∘ σ0,, m']}}. {
-        rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-        rewrite <- exp_eq_sub_compose_typ; mauto 3;
+        rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
+        rewrite <- @exp_eq_sub_compose_typ; mauto 3;
           [eapply wf_exp_eq_app_cong' |];
           mauto 4.
         symmetry.
         bulky_rewrite_in H4.
-        eapply wf_exp_eq_conv; mauto 3.
+        assert {{ Δ0 ⊢ Π IT[σ ∘ σ0] (OT[q (σ ∘ σ0)]) ≈ (Π IT OT)[σ ∘ σ0] : Type@(S (max i4 i)) }} by mauto.
+        eapply wf_exp_eq_conv'; mauto 4.
       }
 
       bulky_rewrite.
       edestruct H10 with (b := b) as [? []];
         simplify_evals; [| | eassumption];
-      mauto.
+        mauto.
 
   - simpl_glu_rel.
     econstructor; repeat split; mauto 3;

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -402,7 +402,7 @@ Proof.
     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.
+    eapply wf_subtyp_refl'.
     mauto 4.
   - bulky_rewrite.
     mauto 3.

theories/Core/Soundness/Realizability.v

@@ -61,7 +61,7 @@ Proof.
     etransitivity; [eapply wf_exp_eq_sub_compose; mauto 3 |].
     pose proof (wf_ctx_sub_length _ _ H0).
 
-    rewrite <- exp_eq_sub_compose_typ; mauto 2.
+    rewrite <- @exp_eq_sub_compose_typ; mauto 2.
     deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [? [? [? [? [-> [? [-> []]]]]]]]).
     repeat rewrite List.app_length in *.
     rewrite H6 in *.
@@ -70,14 +70,14 @@ Proof.
 
     etransitivity.
     + eapply wf_exp_eq_sub_cong; [ |mauto 3].
-      eapply wf_exp_eq_subtyp.
+      eapply wf_exp_eq_subtyp'.
       * eapply wf_exp_eq_var_weaken; [mauto 3|]; eauto.
       * mauto 4.
-    + eapply wf_exp_eq_subtyp.
+    + eapply wf_exp_eq_subtyp'.
       * eapply IHweakening with (Γ1 := T :: _).
         reflexivity.
-      * eapply wf_subtyping_subst; [ |mauto 3].
-        simpl. eapply wf_subtyping_subst; mauto 3.
+      * eapply wf_subtyp_subst; [ |mauto 3].
+        simpl. eapply wf_subtyp_subst; mauto 3.
 Qed.
 
 Lemma var_glu_elem_bot : forall A i P El Γ T,
@@ -226,16 +226,16 @@ Proof.
       etransitivity.
       * rewrite sub_decompose_q_typ; mauto 4.
       * simpl.
-        rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-        rewrite <- exp_eq_sub_compose_typ; mauto 3;
+        rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
+        rewrite <- @exp_eq_sub_compose_typ; mauto 3;
           [eapply wf_exp_eq_app_cong' |].
         -- specialize (H12 _ {{{σ ∘ σ0}}} _ ltac:(mauto 3) ltac:(eassumption)).
            rewrite wf_exp_eq_sub_compose with (M := t) in H12; mauto 3.
            bulky_rewrite_in H12.
-        -- rewrite <- exp_eq_sub_compose_typ; mauto 3.
+        -- rewrite <- @exp_eq_sub_compose_typ; mauto 3.
         -- econstructor; mauto 3.
            autorewrite with mcltt.
-           rewrite <- exp_eq_sub_compose_typ; mauto 3.
+           rewrite <- @exp_eq_sub_compose_typ; mauto 3.
 
   - handle_functional_glu_univ_elem.
     handle_per_univ_elem_irrel.
@@ -280,9 +280,9 @@ Proof.
       do 2 (rewrite wf_exp_eq_sub_id in H40; mauto 4).
       etransitivity; [|eassumption].
       simpl.
-      assert {{ Δ, IT[σ] ⊢ # 0 : IT[σ ∘ Wk] }} by (rewrite <- exp_eq_sub_compose_typ; mauto 3).
-      rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-      rewrite <- exp_eq_sub_compose_typ; mauto 2.
+      assert {{ Δ, IT[σ] ⊢ # 0 : IT[σ ∘ Wk] }} by (rewrite <- @exp_eq_sub_compose_typ; mauto 3).
+      rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
+      rewrite <- @exp_eq_sub_compose_typ; mauto 2.
       2:eapply sub_q; mauto 4.
       2:gen_presup H41; econstructor; mauto 3.
       eapply wf_exp_eq_app_cong'; [| mauto 3].

theories/Core/Soundness/SubtypingCases.v

@@ -8,12 +8,12 @@ From Mcltt.Core.Syntactic Require Import Corollaries.
 Import Domain_Notations.
 
 Lemma glu_rel_exp_subtyp : forall {Γ M A A' i},
-    {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊢ A ⊆ A' }} ->
     {{ Γ ⊩ M : A' }}.
 Proof.
-  intros * HA' [Sb [? [i]]] [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
+  intros * [Sb [? [i]]] HA' [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
   destruct_conjs.
   eapply destruct_glu_rel_exp in HA'; try eassumption.
   destruct_conjs.
@@ -53,21 +53,20 @@ Proof.
   eapply glu_univ_elem_per_subtyp_trm_if; mauto.
   - assert (k <= max i (max j k)) by lia.
     eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto.
-  - assert (i <= max i (max j k)) by lia.
-    eapply glu_univ_elem_exp_cumu_ge; mauto.
+  - eapply glu_univ_elem_exp_cumu_max_left; revgoals; mauto.
 Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_subtyp : mcltt.
 
 Lemma glu_rel_sub_subtyp : forall {Γ σ Δ Δ'},
-    {{ ⊩ Δ' }} ->
     {{ Γ ⊩s σ : Δ }} ->
+    {{ ⊩ Δ' }} ->
     {{ ⊢ Δ ⊆ Δ' }} ->
     {{ Γ ⊩s σ : Δ' }}.
 Proof.
-  intros * [SbΔ'] [SbΓ [SbΔ]] Hsubtyp.
-  pose proof (completeness_fundamental_ctx_sub _ _ Hsubtyp).
+  intros * [SbΓ [SbΔ]] [SbΔ'] Hsubtyp.
+  pose proof (completeness_fundamental_ctx_subtyp _ _ Hsubtyp).
   destruct_conjs.
   econstructor; eexists; repeat split; [eassumption | eassumption |].
   intros.