Working on subtyping (#122)

* initial commit for subtyping

* missing one premise

* add ctxsub

* add transitivity proof

* fix CtxEq

* fix Presup

* fix SystemOpt

* fix CoreInversions

* comment out semantic proofs

* fix Corollary

* comment out all stuff

* remove redundant lemma

theories/Core/Completeness.v

@@ -20,25 +20,25 @@ Proof with mautosolve.
   unshelve epose proof (per_elem_then_per_top _ _ (length Γ)) as [? []]; shelve_unifiable...
 Qed.
 
-Theorem completeness_for_typ_subsumption : forall {Γ A A'},
-  {{ Γ ⊢ A ⊆ A' }} ->
-  exists i W W', nbe Γ A {{{ Type@i }}} W /\ nbe Γ A' {{{ Type@i }}} W' /\ nf_subsumption W W'.
-Proof.
-  induction 1.
-  - assert {{ ⊨ Γ }} as [env_relΓ] by eauto using completeness_fundamental_ctx.
-    assert (exists p p' : env, initial_env Γ p /\ initial_env Γ p' /\ env_relΓ p p') by eauto using per_ctx_then_per_env_initial_env.
-    destruct_conjs.
-    functional_initial_env_rewrite_clear.
-    exists (S (S i)); do 2 eexists; repeat split; mauto.
-  - assert (exists W, nbe Γ A {{{ Type@i }}} W /\ nbe Γ A' {{{ Type@i }}} W) as [? []] by eauto using completeness.
-    do 3 eexists; repeat split; mauto.
-  - destruct IHtyp_subsumption1 as [i1].
-    destruct IHtyp_subsumption2 as [i2].
-    destruct_conjs.
-    functional_nbe_rewrite_clear.
-    exvar nf ltac:(fun W => assert (nbe Γ A {{{ Type@(max i1 i2) }}} W) by mauto using lift_nbe_max_left).
-    exvar nf ltac:(fun W => assert (nbe Γ A' {{{ Type@(max i1 i2) }}} W) by mauto using lift_nbe_max_left).
-    exvar nf ltac:(fun W => assert (nbe Γ A'' {{{ Type@(max i1 i2) }}} W) by mauto using lift_nbe_max_right).
-    do 3 eexists; repeat split; mauto.
-    etransitivity; eassumption.
-Qed.
+(* Theorem completeness_for_typ_subsumption : forall {Γ A A'}, *)
+(*   {{ Γ ⊢ A ⊆ A' }} -> *)
+(*   exists i W W', nbe Γ A {{{ Type@i }}} W /\ nbe Γ A' {{{ Type@i }}} W' /\ nf_subsumption W W'. *)
+(* Proof. *)
+(*   induction 1. *)
+(*   - assert {{ ⊨ Γ }} as [env_relΓ] by eauto using completeness_fundamental_ctx. *)
+(*     assert (exists p p' : env, initial_env Γ p /\ initial_env Γ p' /\ env_relΓ p p') by eauto using per_ctx_then_per_env_initial_env. *)
+(*     destruct_conjs. *)
+(*     functional_initial_env_rewrite_clear. *)
+(*     exists (S (S i)); do 2 eexists; repeat split; mauto. *)
+(*   - assert (exists W, nbe Γ A {{{ Type@i }}} W /\ nbe Γ A' {{{ Type@i }}} W) as [? []] by eauto using completeness. *)
+(*     do 3 eexists; repeat split; mauto. *)
+(*   - destruct IHtyp_subsumption1 as [i1]. *)
+(*     destruct IHtyp_subsumption2 as [i2]. *)
+(*     destruct_conjs. *)
+(*     functional_nbe_rewrite_clear. *)
+(*     exvar nf ltac:(fun W => assert (nbe Γ A {{{ Type@(max i1 i2) }}} W) by mauto using lift_nbe_max_left). *)
+(*     exvar nf ltac:(fun W => assert (nbe Γ A' {{{ Type@(max i1 i2) }}} W) by mauto using lift_nbe_max_left). *)
+(*     exvar nf ltac:(fun W => assert (nbe Γ A'' {{{ Type@(max i1 i2) }}} W) by mauto using lift_nbe_max_right). *)
+(*     do 3 eexists; repeat split; mauto. *)
+(*     etransitivity; eassumption. *)
+(* Qed. *)

theories/Core/Completeness/Consequences/Inversions.v

@@ -4,32 +4,32 @@ From Mcltt.Core Require Import Completeness Semantic.Realizability Completeness.
 From Mcltt.Core Require Export SystemOpt CoreInversions.
 Import Domain_Notations.
 
-Corollary wf_zero_inversion' : forall Γ A,
-    {{ Γ ⊢ zero : A }} ->
-    exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}.
-Proof with mautosolve 4.
-  intros * []%wf_zero_inversion%typ_subsumption_left_nat...
-Qed.
+(* Corollary wf_zero_inversion' : forall Γ A, *)
+(*     {{ Γ ⊢ zero : A }} -> *)
+(*     exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}. *)
+(* Proof with mautosolve 4. *)
+(*   intros * []%wf_zero_inversion%typ_subsumption_left_nat... *)
+(* Qed. *)
 
-#[export]
-Hint Resolve wf_zero_inversion' : mcltt.
+(* #[export] *)
+(* Hint Resolve wf_zero_inversion' : mcltt. *)
 
-Corollary wf_succ_inversion' : forall Γ A M,
-    {{ Γ ⊢ succ M : A }} ->
-    {{ Γ ⊢ M : ℕ }} /\ exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}.
-Proof with mautosolve.
-  intros * [? []%typ_subsumption_left_nat]%wf_succ_inversion...
-Qed.
+(* Corollary wf_succ_inversion' : forall Γ A M, *)
+(*     {{ Γ ⊢ succ M : A }} -> *)
+(*     {{ Γ ⊢ M : ℕ }} /\ exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}. *)
+(* Proof with mautosolve. *)
+(*   intros * [? []%typ_subsumption_left_nat]%wf_succ_inversion... *)
+(* Qed. *)
 
-#[export]
-Hint Resolve wf_succ_inversion' : mcltt.
+(* #[export] *)
+(* Hint Resolve wf_succ_inversion' : mcltt. *)
 
-Corollary wf_fn_inversion' : forall {Γ A M C},
-    {{ Γ ⊢ λ A M : C }} ->
-    exists B, {{ Γ, A ⊢ M : B }} /\ exists i, {{ Γ ⊢ Π A B ≈ C : Type@i }}.
-Proof with mautosolve.
-  intros * [? [? []%typ_subsumption_left_pi]]%wf_fn_inversion...
-Qed.
+(* Corollary wf_fn_inversion' : forall {Γ A M C}, *)
+(*     {{ Γ ⊢ λ A M : C }} -> *)
+(*     exists B, {{ Γ, A ⊢ M : B }} /\ exists i, {{ Γ ⊢ Π A B ≈ C : Type@i }}. *)
+(* Proof with mautosolve. *)
+(*   intros * [? [? []%typ_subsumption_left_pi]]%wf_fn_inversion... *)
+(* Qed. *)
 
-#[export]
-Hint Resolve wf_fn_inversion' : mcltt.
+(* #[export] *)
+(* Hint Resolve wf_fn_inversion' : mcltt. *)

theories/Core/Completeness/Consequences/Types.v

@@ -87,148 +87,149 @@ Hint Resolve is_typ_constr_and_exp_eq_nat_implies_eq_nat : mcltt.
 
 (* We cannot use this spec as the definition of [typ_subsumption] as
    then its transitivity requires [exp_eq_typ_implies_eq_level] or a similar semantic lemma *)
-Lemma typ_subsumption_spec : forall {Γ A A'},
-    {{ Γ ⊢ A ⊆ A' }} ->
-    {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}.
-Proof.
-  intros * H.
-  dependent induction H; split; mauto 3.
-  - (* typ_subsumption_typ *)
-    eexists.
-    right.
-    do 2 eexists.
-    repeat split; revgoals; mauto.
-  - (* typ_subsumption_trans *)
-    destruct IHtyp_subsumption1 as [? [? [| [i1 [i1']]]]]; destruct IHtyp_subsumption2 as [? [? [| [i2 [i2']]]]];
-      destruct_conjs;
-      only 1: mautosolve 4;
-      eexists; right; do 2 eexists.
-    + (* left & right *)
-      split; [eassumption |].
-      solve [mauto using lift_exp_eq_max_left].
-    + (* right & left *)
-      split; [eassumption |].
-      solve [mauto using lift_exp_eq_max_right].
-    + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto).
-      replace i2 with i1' in * by mauto.
-      split; [etransitivity; revgoals; eassumption |].
-      mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_spec : mcltt.
-
-Lemma not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : forall {Γ A A'},
-    is_typ_constr A ->
-    (forall i, A <> {{{ Type@i }}}) ->
-    {{ Γ ⊢ A ⊆ A' }} ->
-    exists j, {{ Γ ⊢ A ≈ A' : Type@j }}.
-Proof.
-  intros * ? ? H%typ_subsumption_spec.
-  destruct_all; mauto.
-  exfalso.
-  intuition.
-  mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ.
-Qed.
-
-#[export]
-Hint Resolve not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : mcltt.
-
-Lemma not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : forall {Γ A A'},
-    is_typ_constr A' ->
-    (forall i, A' <> {{{ Type@i }}}) ->
-    {{ Γ ⊢ A ⊆ A' }} ->
-    exists j, {{ Γ ⊢ A ≈ A' : Type@j }}.
-Proof.
-  intros * ? ? H%typ_subsumption_spec.
-  destruct_all; mauto.
-  exfalso.
-  intuition.
-  mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ.
-Qed.
-
-#[export]
-Hint Resolve not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : mcltt.
-
-Corollary typ_subsumption_left_nat : forall {Γ A'},
-    {{ Γ ⊢ ℕ ⊆ A' }} ->
-    exists j, {{ Γ ⊢ ℕ ≈ A' : Type@j }}.
-Proof.
-  intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto.
-  congruence.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_left_nat : mcltt.
-
-Corollary typ_subsumption_left_pi : forall {Γ A B C'},
-    {{ Γ ⊢ Π A B ⊆ C' }} ->
-    exists j, {{ Γ ⊢ Π A B ≈ C' : Type@j }}.
-Proof.
-  intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto.
-  congruence.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_left_pi : mcltt.
 
-Corollary typ_subsumption_left_typ : forall {Γ i A'},
-    {{ Γ ⊢ Type@i ⊆ A' }} ->
-    exists j i', i <= i' /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}.
-Proof.
-  intros * H%typ_subsumption_spec.
-  destruct_all; mauto.
-  (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst.
-  mauto using PeanoNat.Nat.lt_le_incl.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_left_typ : mcltt.
-
-Corollary typ_subsumption_right_nat : forall {Γ A},
-    {{ Γ ⊢ A ⊆ ℕ }} ->
-    exists j, {{ Γ ⊢ A ≈ ℕ : Type@j }}.
-Proof.
-  intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto.
-  congruence.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_right_nat : mcltt.
-
-Corollary typ_subsumption_right_pi : forall {Γ C A' B'},
-    {{ Γ ⊢ C ⊆ Π A' B' }} ->
-    exists j, {{ Γ ⊢ C ≈ Π A' B' : Type@j }}.
-Proof.
-  intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto.
-  congruence.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_right_pi : mcltt.
-
-Corollary typ_subsumption_right_typ : forall {Γ A i'},
-    {{ Γ ⊢ A ⊆ Type@i' }} ->
-    exists j i, i <= i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }}.
-Proof.
-  intros * H%typ_subsumption_spec.
-  destruct_all; mauto.
-  (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst.
-  mauto using PeanoNat.Nat.lt_le_incl.
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_right_typ : mcltt.
-
-Corollary typ_subsumption_typ_spec : forall {Γ i i'},
-    {{ Γ ⊢ Type@i ⊆ Type@i' }} ->
-    {{ ⊢ Γ }} /\ i <= i'.
-Proof with mautosolve.
-  intros * H.
-  pose proof (typ_subsumption_left_typ H).
-  destruct_conjs.
-  (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst...
-Qed.
-
-#[export]
-Hint Resolve typ_subsumption_typ_spec : mcltt.
+(* Lemma typ_subsumption_spec : forall {Γ A A'}, *)
+(*     {{ Γ ⊢ A ⊆ A' }} -> *)
+(*     {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
+(* Proof. *)
+(*   intros * H. *)
+(*   dependent induction H; split; mauto 3. *)
+(*   - (* typ_subsumption_typ *) *)
+(*     eexists. *)
+(*     right. *)
+(*     do 2 eexists. *)
+(*     repeat split; revgoals; mauto. *)
+(*   - (* typ_subsumption_trans *) *)
+(*     destruct IHtyp_subsumption1 as [? [? [| [i1 [i1']]]]]; destruct IHtyp_subsumption2 as [? [? [| [i2 [i2']]]]]; *)
+(*       destruct_conjs; *)
+(*       only 1: mautosolve 4; *)
+(*       eexists; right; do 2 eexists. *)
+(*     + (* left & right *) *)
+(*       split; [eassumption |]. *)
+(*       solve [mauto using lift_exp_eq_max_left]. *)
+(*     + (* right & left *) *)
+(*       split; [eassumption |]. *)
+(*       solve [mauto using lift_exp_eq_max_right]. *)
+(*     + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto). *)
+(*       replace i2 with i1' in * by mauto. *)
+(*       split; [etransitivity; revgoals; eassumption |]. *)
+(*       mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_spec : mcltt. *)
+
+(* Lemma not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
+(*     is_typ_constr A -> *)
+(*     (forall i, A <> {{{ Type@i }}}) -> *)
+(*     {{ Γ ⊢ A ⊆ A' }} -> *)
+(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
+(* Proof. *)
+(*   intros * ? ? H%typ_subsumption_spec. *)
+(*   destruct_all; mauto. *)
+(*   exfalso. *)
+(*   intuition. *)
+(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : mcltt. *)
+
+(* Lemma not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
+(*     is_typ_constr A' -> *)
+(*     (forall i, A' <> {{{ Type@i }}}) -> *)
+(*     {{ Γ ⊢ A ⊆ A' }} -> *)
+(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
+(* Proof. *)
+(*   intros * ? ? H%typ_subsumption_spec. *)
+(*   destruct_all; mauto. *)
+(*   exfalso. *)
+(*   intuition. *)
+(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : mcltt. *)
+
+(* Corollary typ_subsumption_left_nat : forall {Γ A'}, *)
+(*     {{ Γ ⊢ ℕ ⊆ A' }} -> *)
+(*     exists j, {{ Γ ⊢ ℕ ≈ A' : Type@j }}. *)
+(* Proof. *)
+(*   intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto. *)
+(*   congruence. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_left_nat : mcltt. *)
+
+(* Corollary typ_subsumption_left_pi : forall {Γ A B C'}, *)
+(*     {{ Γ ⊢ Π A B ⊆ C' }} -> *)
+(*     exists j, {{ Γ ⊢ Π A B ≈ C' : Type@j }}. *)
+(* Proof. *)
+(*   intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto. *)
+(*   congruence. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_left_pi : mcltt. *)
+
+(* Corollary typ_subsumption_left_typ : forall {Γ i A'}, *)
+(*     {{ Γ ⊢ Type@i ⊆ A' }} -> *)
+(*     exists j i', i <= i' /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
+(* Proof. *)
+(*   intros * H%typ_subsumption_spec. *)
+(*   destruct_all; mauto. *)
+(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
+(*   mauto using PeanoNat.Nat.lt_le_incl. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_left_typ : mcltt. *)
+
+(* Corollary typ_subsumption_right_nat : forall {Γ A}, *)
+(*     {{ Γ ⊢ A ⊆ ℕ }} -> *)
+(*     exists j, {{ Γ ⊢ A ≈ ℕ : Type@j }}. *)
+(* Proof. *)
+(*   intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto. *)
+(*   congruence. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_right_nat : mcltt. *)
+
+(* Corollary typ_subsumption_right_pi : forall {Γ C A' B'}, *)
+(*     {{ Γ ⊢ C ⊆ Π A' B' }} -> *)
+(*     exists j, {{ Γ ⊢ C ≈ Π A' B' : Type@j }}. *)
+(* Proof. *)
+(*   intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto. *)
+(*   congruence. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_right_pi : mcltt. *)
+
+(* Corollary typ_subsumption_right_typ : forall {Γ A i'}, *)
+(*     {{ Γ ⊢ A ⊆ Type@i' }} -> *)
+(*     exists j i, i <= i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }}. *)
+(* Proof. *)
+(*   intros * H%typ_subsumption_spec. *)
+(*   destruct_all; mauto. *)
+(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
+(*   mauto using PeanoNat.Nat.lt_le_incl. *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_right_typ : mcltt. *)
+
+(* Corollary typ_subsumption_typ_spec : forall {Γ i i'}, *)
+(*     {{ Γ ⊢ Type@i ⊆ Type@i' }} -> *)
+(*     {{ ⊢ Γ }} /\ i <= i'. *)
+(* Proof with mautosolve. *)
+(*   intros * H. *)
+(*   pose proof (typ_subsumption_left_typ H). *)
+(*   destruct_conjs. *)
+(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst... *)
+(* Qed. *)
+
+(* #[export] *)
+(* Hint Resolve typ_subsumption_typ_spec : mcltt. *)