Experiment on contra-variant subtyping

.gitignore

@@ -1,3 +1,5 @@
+.vscode
+
 # Dune outputs
 _build
 *.opam

theories/Core/Completeness.v

@@ -1,32 +1,106 @@
 From Mctt Require Import LibTactics.
 From Mctt.Core Require Import Base.
-From Mctt.Core.Completeness Require Export FundamentalTheorem.
-From Mctt.Core.Semantic Require Import Realizability.
+From Mctt.Core.WCompleteness Require Export FundamentalTheorem.
+From Mctt.Core.Semantic Require Import WRealizability.
 From Mctt.Core.Semantic Require Export NbE.
-From Mctt.Core.Syntactic Require Export SystemOpt.
+From Mctt.Core.Syntactic.WCong Require Import Definitions Lemmas.
+From Mctt.Core.Syntactic Require Export SystemOpt Corollaries CtxSub.
 Import Domain_Notations.
 
+
 Theorem completeness : forall {Γ M M' A},
   {{ Γ ⊢ M ≈ M' : A }} ->
-  exists W, nbe Γ M A W /\ nbe Γ M' A W.
+  exists W W', nbe Γ M A W /\ nbe Γ M' A W' /\ {{ ⊢nf W ≈≈ W' }}.
 Proof with mautosolve.
   intros * [env_relΓ]%completeness_fundamental_exp_eq.
   destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p] by (eauto using per_ctx_then_per_env_initial_env).
+  assert (exists ρ ρ', initial_env Γ ρ /\ initial_env Γ ρ' /\ {{ Dom ρ ≈≈ ρ' ∈ env_relΓ }}) as [ρ] by (eauto using per_ctx_then_per_env_initial_env).
   destruct_conjs.
   functional_initial_env_rewrite_clear.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  rename x into elem_rel.
   destruct_by_head rel_typ.
   functional_eval_rewrite_clear.
   destruct_by_head rel_exp.
-  unshelve epose proof (per_elem_then_per_top _ _ (length Γ)) as [? []]; shelve_unifiable...
+  unshelve epose proof (per_elem_then_per_top _ _ (length Γ)) as [? [? [? []]]]; shelve_unifiable; mauto 3.
+  exists x, x0; repeat split; mauto 3.
 Qed.
 
 Lemma completeness_ty : forall {Γ i A A'},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    exists W, nbe_ty Γ A W /\ nbe_ty Γ A' W.
+    exists W W', nbe_ty Γ A W /\ nbe_ty Γ A' W' /\ {{ ⊢nf W ≈≈ W' }}  .
 Proof.
-  intros * [? [?%nbe_type_to_nbe_ty ?%nbe_type_to_nbe_ty]]%completeness.
-  mauto 3.
+  intros. apply completeness in H as [W [W' []]]; mauto 3.
+  destruct_all.
+  apply nbe_type_to_nbe_ty in H.
+  apply nbe_type_to_nbe_ty in H0.
+  do 2 eexists; repeat split; mauto 3.
 Qed.
+
+Lemma completeness_subtyp : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+      exists W W', nbe_ty Γ A W /\ nbe_ty Γ A' W' /\ {{ ⊢snf W ⊆ W' }}.
+Proof.
+  intros * HA.
+  eapply completeness_fundamental_subtyp in HA as [env_relΓ].
+  destruct_conjs.
+  assert (exists ρ ρ', initial_env Γ ρ /\  initial_env Γ ρ' /\ {{ Dom ρ ≈≈ ρ' ∈ env_relΓ }}) as [ρ] by (eauto using per_ctx_then_per_env_initial_env).
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  functional_eval_rewrite_clear.
+  destruct_by_head rel_exp.
+  functional_eval_rewrite_clear.
+  handle_per_univ_elem_irrel.
+  (on_all_hyp: fun H => epose proof (per_univ_then_per_top_typ H (length Γ)); destruct_all).
+  functional_read_rewrite_clear. clear_dups.
+  do 2 eexists.
+  repeat split; only 1-2: econstructor; try eassumption.
+  - eapply wrealize_persub_gen; mauto 3. 
+Abort.
+
+(* Lemma completeness_subtyp' : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+    forall Γ',
+      {{ ⊢ Γ' ⊆ Γ }} ->
+      exists W W', nbe_ty Γ' A W /\ nbe_ty Γ A' W' /\ {{ ⊢anf W ⊆ W' }}.
+Proof.
+  intros * HA. induction HA; intros.
+  - admit.
+  - admit.
+  - admit.
+  - admit.
+Admitted. *)
+
+
+(* Lemma completeness_subtyp : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+    forall Γ',
+      {{ ⊢ Γ' ⊆ Γ }} ->
+      exists W W', nbe_ty Γ' A W /\ nbe_ty Γ A' W' /\ {{ ⊢anf W ⊆ W' }}.
+Proof.
+  intros * HA ? HG.
+  assert {{ Γ' ⊢ A ⊆ A' }} as HA' by mauto 3.
+  eapply completeness_fundamental_subtyp in HA as [env_relΓ].
+  eapply completeness_fundamental_subtyp in HA' as [env_relΓ'].
+  destruct_conjs.
+  eapply completeness_fundamental_ctx_subtyp in HG.
+  assert (exists ρ ρ', initial_env Γ' ρ /\ initial_env Γ' ρ' /\ {{ Dom ρ ≈ ρ' ∈ env_relΓ' }}) as [ρ] by (eauto using per_ctx_then_per_env_initial_env).
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by (eapply per_ctx_env_subtyping; mauto 2).
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ').
+  destruct_by_head rel_typ.
+  functional_eval_rewrite_clear.
+  destruct_by_head rel_exp.
+  functional_eval_rewrite_clear.
+  handle_per_univ_elem_irrel.
+  (on_all_hyp: fun H => epose proof (per_univ_then_per_top_typ H (length Γ')); destruct_all).
+  functional_read_rewrite_clear. clear_dups.
+  do 2 eexists.
+  repeat split; only 1-2: econstructor; try eassumption.
+  - admit. (* initial_env Γ p, which is false *) (* We need a relation between initial environments of super/sub-context pair *)
+  - erewrite <- per_ctx_subtyp_respects_length; mautosolve.
+  - admit. (* {{ ⊢anf ~ ?W ⊆ ~ ?W' }} *)
+Abort. *)

theories/Core/Completeness/FunctionCases.v

@@ -40,7 +40,6 @@ Proof.
   eexists_rel_exp_with (max i j).
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  rename x0 into in_rel.
   destruct_by_head rel_typ.
   destruct_by_head rel_exp.
   eexists; split; econstructor; mauto.
@@ -229,13 +228,12 @@ Proof with intuition.
   intros.
   assert (equiv_p'_p' : env_relΓ ρ' ρ') by (etransitivity; [symmetry |]; eassumption).
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  rename x2 into in_rel.
   destruct_by_head rel_typ.
   destruct_by_head rel_exp.
   handle_per_univ_elem_irrel.
-  assert (in_rel m1 m2) by (etransitivity; [| symmetry]; eassumption).
-  assert (in_rel m1 m'2) by intuition.
-  (on_all_hyp: destruct_rel_by_assumption in_rel).
+  assert (in_rel0 m1 m2) by (etransitivity; [| symmetry]; eassumption).
+  assert (in_rel0 m1 m'2) by intuition.
+  (on_all_hyp: destruct_rel_by_assumption in_rel0).
   handle_per_univ_elem_irrel.
   eexists.
   split; econstructor; mauto...
@@ -259,7 +257,6 @@ Proof with mautosolve.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
-  rename x0 into in_rel.
   destruct_by_head rel_typ.
   handle_per_univ_elem_irrel.
   destruct_by_head rel_exp.
@@ -307,7 +304,6 @@ Proof with mautosolve.
   eexists_rel_exp_of_pi.
   intros.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  rename x into in_rel.
   destruct_by_head rel_typ.
   destruct_by_head rel_exp.
   do 2 eexists.

theories/Core/Completeness/LogicalRelation/Lemmas.v

@@ -43,3 +43,22 @@ Qed.
 
 #[export]
 Hint Resolve rel_typ_implies_rel_exp : mctt.
+
+Lemma rel_exp_clean_inversion : forall {Γ env_rel A M M'},
+    {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }} ->
+    {{ Γ ⊨ M ≈ M' : A }} ->
+    exists i,
+    forall ρ ρ' (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ env_rel }}),
+    exists (elem_rel : relation domain),
+      rel_typ i A ρ A ρ' elem_rel /\ rel_exp M ρ M' ρ' elem_rel.
+Proof.
+  intros * ? [].
+  destruct_conjs.
+  handle_per_ctx_env_irrel.
+  eexists.
+  eassumption.
+Qed.
+
+Ltac invert_rel_exp H :=
+  (unshelve (epose proof (rel_exp_clean_inversion _ H); deex); shelve_unifiable; [eassumption |]; clear H)
+  + dependent destruction H.

theories/Core/Completeness/NatCases.v

@@ -36,7 +36,6 @@ Proof.
   eexists; split; mauto.
   econstructor; mauto.
   per_univ_elem_econstructor; mauto.
-  reflexivity.
 Qed.
 
 #[export]

theories/Core/Completeness/SubstitutionCases.v

@@ -71,7 +71,8 @@ Proof with mautosolve.
   (on_all_hyp: destruct_rel_by_assumption env_relΔ).
   destruct_by_head rel_typ.
   invert_rel_typ_body_nouip.
-  destruct_by_head rel_exp...
+  destruct_by_head rel_exp.
+  econstructor; mauto 3.
 Qed.
 
 #[export]

theories/Core/Completeness/SubtypingCases.v

@@ -2,7 +2,7 @@ From Coq Require Import Morphisms_Relations RelationClasses.
 
 From Mctt Require Import LibTactics.
 From Mctt.Core Require Import Base.
-From Mctt.Core.Completeness Require Import LogicalRelation FunctionCases.
+From Mctt.Core.Completeness Require Import LogicalRelation FunctionCases UniverseCases.
 Import Domain_Notations.
 
 Lemma subtyp_refl : forall Γ M M' i,
@@ -71,15 +71,18 @@ Proof.
 Qed.
 
 Lemma subtyp_pi : forall Γ A A' B B' i,
-  {{ Γ ⊨ A ≈ A' : Type@i }} ->
+  {{ Γ ⊨ A' ⊆ A }} ->
+  {{ Γ , A ⊨ B : Type@i }} ->
   {{ Γ , A' ⊨ B ⊆ B' }} ->
   {{ Γ ⊨ Π A B ⊆ Π A' B' }}.
 Proof.
-  intros * [env_relΓ] [env_relΓA' [? [k]]].
+  intros * [env_relΓ [HΓ [i]]] [env_relΓA]%rel_exp_of_typ_inversion [env_relΓA' [HΓA' [k]]].
   destruct_conjs.
   pose env_relΓ.
+  pose env_relΓA.
   pose env_relΓA'.
   match_by_head (per_ctx_env env_relΓA') invert_per_ctx_env.
+  match_by_head (per_ctx_env env_relΓA) invert_per_ctx_env.
   handle_per_ctx_env_irrel.
   eexists_subtyp.
   intros.
@@ -95,36 +98,44 @@ Proof.
       assert_fails (unify ρ ρ0);
       rename ρ0 into ρ'
   end.
-  rename x0 into head_rel.
 
   assert (forall c c', head_rel ρ ρ' equiv_ρ_ρ' c c' -> env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as HΓA'
       by (intros; apply_relation_equivalence; unshelve eexists; eassumption).
 
-  (** The proofs for the next two assertions are basically the same *)
+  assert (forall c c', head_rel0 ρ ρ' equiv_ρ_ρ' c c' -> env_relΓA d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as HΓA
+      by (intros; apply_relation_equivalence; unshelve eexists; eassumption).
+
+  (** with contra-variant subtyping, the following two cases are no longer similar *)
   exvar (relation domain)
-    ltac:(fun R => assert ({{ DF Π m0 ρ B ≈ Π m1 ρ' B ∈ per_univ_elem (Nat.max i k) ↘ R }})).
+    ltac:(fun R => assert ({{ DF Π a0 ρ B ≈ Π a ρ' B ∈ per_univ_elem (Nat.max i (Nat.max i0 k)) ↘ R }})).
   {
     intros.
     per_univ_elem_econstructor; [| | solve_refl].
     - etransitivity; [| symmetry]; mauto using per_univ_elem_cumu_max_left.
     - eapply rel_exp_pi_core; [| reflexivity].
       intros.
-      assert (env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as equiv_ρc_ρ'c' by (apply HΓA'; intuition).
+      assert (env_relΓA d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as equiv_ρc_ρ'c'. {
+        eapply HΓA; intuition.
+      }
       apply_relation_equivalence.
       (on_all_hyp: fun H => destruct (H _ _ equiv_ρc_ρ'c')).
       destruct_conjs.
       destruct_by_head rel_typ.
-      econstructor; mauto using per_univ_elem_cumu_max_right.
+      econstructor; mauto using per_univ_elem_cumu_max_right, per_univ_elem_cumu_max_left.
+      destruct H13 as [].
+      eexists.
+      eapply per_univ_elem_cumu_max_right.
+      eapply per_univ_elem_cumu_max_left. mauto.
   }
   exvar (relation domain)
-    ltac:(fun R => assert ({{ DF Π a0 ρ B' ≈ Π a ρ' B' ∈ per_univ_elem (Nat.max i k) ↘ R }})).
+    ltac:(fun R => assert ({{ DF Π a3 ρ B' ≈ Π a2 ρ' B' ∈ per_univ_elem (Nat.max i (Nat.max i0 k)) ↘ R }})).
   {
     intros.
     per_univ_elem_econstructor; [| | solve_refl].
     - etransitivity; [symmetry |]; mauto using per_univ_elem_cumu_max_left.
     - eapply rel_exp_pi_core; [| reflexivity].
       intros.
-      assert (env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as equiv_ρc_ρ'c' by (apply HΓA'; intuition).
+      assert (env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as equiv_ρc_ρ'c' by (eapply HΓA'; intuition).
       apply_relation_equivalence.
       (on_all_hyp: fun H => destruct (H _ _ equiv_ρc_ρ'c')).
       destruct_conjs.
@@ -133,8 +144,13 @@ Proof.
   }
 
   do 2 eexists.
-  repeat split; econstructor; mauto 2.
-  econstructor; only 3-4: try (saturate_refl; mautosolve 2).
+  repeat split; econstructor; mauto 2. 
+  econstructor; only 3-4: try (saturate_refl; mautosolve 3).
+  - eauto using per_univ_elem_cumu_max_left.
+    eapply per_subtyp_trans with (A2:=a).
+    eapply per_subtyp_cumu_left; mauto 3.
+    eapply per_subtyp_cumu_left.
+    eapply per_subtyp_refl2; mauto 3.
   - eauto using per_univ_elem_cumu_max_left.
   - intros.
     assert (env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as equiv_ρc_ρ'c' by (apply HΓA'; intuition).
@@ -143,7 +159,8 @@ Proof.
     destruct_conjs.
     destruct_by_head rel_exp.
     simplify_evals.
-    mauto 2 using per_subtyp_cumu_right.
+    mauto 3 using per_subtyp_cumu_right.
+  - etransitivity; [symmetry|]; mauto 3.
 Qed.
 
 #[export]

theories/Core/Completeness/UniverseCases.v

@@ -34,9 +34,6 @@ Proof.
   intros.
   eexists; split; eauto.
   econstructor; mauto.
-  per_univ_elem_econstructor; eauto.
-  unfold per_univ.
-  reflexivity.
 Qed.
 
 #[export]

theories/Core/Semantic/PER/CoreTactics.v

@@ -6,16 +6,30 @@ From Mctt.Core Require Import Base.
 From Mctt.Core.Semantic Require Import PER.Definitions.
 Import Domain_Notations.
 
+Hint Extern 1 (?R <~> ?R) => reflexivity : mctt.
+Hint Extern 1 (?R <∙> ?R) => reflexivity : mctt.
+
+(* this is specific for destruct_rel_by_assumption, 
+   so H must have shape forall c c' (c ≈ c' ∈ rel ), P *)
+Ltac deex_destruct_rel H H' :=
+  match type of H with
+  | forall _ _ _, exists _, _ => 
+      let H'' := fresh "H" in
+        pose proof (H _ _ H') as H''; deex_once_in H''
+  | _ => destruct (H _ _ H') as []
+  end.
+
 Ltac destruct_rel_by_assumption in_rel H :=
   repeat
     match goal with
     | H' : {{ Dom ^?c ≈ ^?c' ∈ ?in_rel0 }} |- _ =>
         unify in_rel0 in_rel;
-        destruct (H _ _ H') as [];
+        deex_destruct_rel H H';
         destruct_all;
         mark_with H' 1
     end;
   unmark_all_with 1.
+
 Ltac destruct_rel_mod_eval :=
   repeat
     match goal with

theories/Core/Semantic/PER/Definitions.v

@@ -246,7 +246,8 @@ Inductive per_subtyp : nat -> domain -> domain -> Prop :=
      {{ Sub 𝕌@i <: 𝕌@j at k }} )
 | per_subtyp_pi :
   `( forall (in_rel : relation domain) elem_rel elem_rel',
-        {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel }} ->
+        {{ Sub a' <: a at i }} ->
+        {{ DF a' ≈ a' ∈ per_univ_elem i ↘ in_rel }} ->
         (forall c c' b b',
             {{ Dom c ≈ c' ∈ in_rel }} ->
             {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->