finish completeness proof using only co-variant subtyping

theories/Algorithmic/Subtyping/Definitions.v

@@ -21,7 +21,7 @@ Inductive alg_subtyping_nf : nf -> nf -> Prop :=
     i <= j ->
     {{ ⊢anf Type@i ⊆ Type@j }}
 | asnf_pi : forall A B A' B',
-    {{ ⊢anf A' ⊆ A }} ->
+    A = A' ->
     {{ ⊢anf B ⊆ B' }} ->
     {{ ⊢anf Π A B ⊆ Π A' B' }}
 where "⊢anf M ⊆ N" := (alg_subtyping_nf M N) (in custom judg) : type_scope.

theories/Algorithmic/Subtyping/Lemmas.v

@@ -1,5 +1,6 @@
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import System Evaluation Readback NbE CoreTypeInversions Presup CtxSub.
+From Mcltt.Core Require Import System Evaluation Readback NbE CoreTypeInversions Presup CtxSub SystemOpt.
+From Mcltt.Core.Completeness Require Import Consequences.Rules.
 From Mcltt Require Import Completeness Soundness.
 From Mcltt.Algorithmic Require Import Subtyping.Definitions.
 Import Syntax_Notations.
@@ -32,8 +33,8 @@ Proof.
                fail_if_dup
            end.
     apply_subtyping.
-    deepexec IHalg_subtyping_nf1 ltac:(fun H => pose proof H).
-    eapply wf_subtyp_pi with (i := i); mauto.
+    deepexec IHalg_subtyping_nf ltac:(fun H => pose proof H).
+    mauto 3.
 Qed.
 
 Lemma alg_subtyping_nf_trans : forall M1 M0 M2,
@@ -74,31 +75,36 @@ Qed.
  Hint Resolve alg_subtyping_trans : mcltt.
 
 
-(* Lemma alg_subtyping_complete : forall Γ M N, *)
-(*     {{ Γ ⊢ M ⊆ N }} -> *)
-(*     {{ Γ ⊢a M ⊆ N }}. *)
-(* Proof. *)
-(*   induction 1; mauto. *)
-(*   - apply completeness in H. *)
-(*     destruct H as [W [? ?]]. *)
-(*     econstructor; mauto. *)
-(*   - assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto. *)
-(*     assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto. *)
-(*     apply soundness in H1. *)
-(*     apply soundness in H2. *)
-(*     destruct_all. *)
-(*     econstructor; try eassumption. *)
-(*     progressive_inversion. *)
-(*     mauto. *)
-(*   - assert {{ Γ ⊢ Π A B : Type@i }} as HΠ1 by mauto. *)
-(*     assert {{ Γ ⊢ Π A' B' : Type@i }} as HΠ2 by mauto. *)
-(*     apply soundness in HΠ1. *)
-(*     apply soundness in HΠ2. *)
-(*     destruct_all. *)
-(*     econstructor; try eassumption. *)
-(*     progressive_inversion. *)
-(*     simpl in *. *)
-(*     functional_initial_env_rewrite_clear. *)
-(*     simplify_evals. *)
-(*     functional_read_rewrite_clear. *)
-(*     eapply asnf_pi; trivial. *)
+Lemma alg_subtyping_complete : forall Γ M N,
+    {{ Γ ⊢ M ⊆ N }} ->
+    {{ Γ ⊢a M ⊆ N }}.
+Proof.
+  induction 1; mauto.
+  - apply completeness in H.
+    destruct H as [W [? ?]].
+    econstructor; mauto.
+  - assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto.
+    assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto.
+    on_all_hyp: fun H => apply soundness in H.
+    destruct_all.
+    econstructor; try eassumption.
+    progressive_inversion.
+    mauto.
+  - assert {{ Γ ⊢ Π A B : Type@i }} as HΠ1 by mauto.
+    assert {{ Γ ⊢ Π A' B' : Type@i }} as HΠ2 by mauto.
+    assert {{ ⊢ Γ , A ≈ Γ , A' }} by mauto.
+    eapply ctxeq_nbe_eq in H5; [ |eassumption].
+    match goal with
+    | H : _ |- _ => apply completeness in H
+    end.
+    apply soundness in HΠ1.
+    apply soundness in HΠ2.
+    destruct_all.
+    econstructor; try eassumption.
+    progressive_inversion.
+    simpl in *.
+    functional_initial_env_rewrite_clear.
+    simplify_evals.
+    functional_read_rewrite_clear.
+    eapply asnf_pi; trivial.
+Qed.

theories/Core/Completeness/Consequences/Rules.v

@@ -0,0 +1,23 @@
+From Coq Require Import RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability PER.
+From Mcltt.Core Require Export SystemOpt.
+Import Domain_Notations.
+
+Lemma ctxeq_nbe_eq : forall Γ Γ' M A,
+    {{ Γ ⊢ M : A }} ->
+    {{ ⊢ Γ ≈ Γ' }} ->
+    exists w, nbe Γ M A w /\ nbe Γ' M A w.
+Proof.
+  intros ? ? ? ? [envR [Henv [i ?]]]%completeness_fundamental_exp [envR' Henv']%completeness_fundamental_ctx_eq.
+  handle_per_ctx_env_irrel.
+  destruct (per_ctx_then_per_env_initial_env Henv') as [p [p' [? [? ?]]]].
+  deepexec H ltac:(fun H => destruct H as [R [? ?]]).
+  progressive_inversion.
+  deepexec @per_elem_then_per_top ltac:(fun H => destruct H as [w [? ?]]).
+  exists w.
+  split; econstructor; eauto.
+  erewrite per_ctx_respects_length; try eassumption.
+  eexists. symmetry.
+  eassumption.
+Qed.

theories/LibTactics.v

@@ -267,7 +267,7 @@ Ltac deepexec lem tac :=
                       lazymatch type of T with
                       | Prop => match goal with
                             | H : _ |- _ => unify x H
-                            | _ => idtac
+                            | _ => tac lem
                             end
                       | _ => idtac
                       end;
@@ -294,7 +294,7 @@ Ltac cutexec lem C tac :=
                         (lazymatch type of T with
                          | Prop => match goal with
                                | H : _ |- _ => unify x H
-                               | _ => idtac
+                               | _ => tac lem
                                end
                          | _ => idtac
                          end;

theories/_CoqProject

@@ -6,6 +6,7 @@
 ./Algorithmic/Subtyping/Lemmas.v
 ./Core/Axioms.v
 ./Core/Base.v
+./Core/Completeness/Consequences/Rules.v
 ./Core/Completeness/Consequences/Types.v
 ./Core/Completeness/Consequences/Inversions.v
 ./Core/Completeness/ContextCases.v