working on algorithmic subtyping

theories/Algorithmic/Subtyping/Definitions.v

@@ -0,0 +1,40 @@
+From Mcltt Require Import Base.
+From Mcltt.Core Require Import System.Definitions NbE.
+From Mcltt Require Export Syntax.
+Import Syntax_Notations.
+
+Reserved Notation "Γ ⊢a A ⊆ A'" (in custom judg at level 80, Γ custom exp, A custom exp, A' custom exp).
+Reserved Notation "⊢anf A ⊆ A'" (in custom judg at level 80, A custom nf, A' custom nf).
+
+Definition not_univ_pi (A : nf) : Prop :=
+  match A with
+  | nf_typ _ | nf_pi _ _ => False
+  | _ => True
+  end.
+
+Inductive alg_subtyping_nf : nf -> nf -> Prop :=
+| asnf_refl : forall M N,
+    not_univ_pi M ->
+    M = N ->
+    {{ ⊢anf M ⊆ N }}
+| asnf_univ : forall i j,
+    i <= j ->
+    {{ ⊢anf Type@i ⊆ Type@j }}
+| asnf_pi : forall A B A' B',
+    A = A' ->
+    {{ ⊢anf B ⊆ B' }} ->
+    {{ ⊢anf Π A B ⊆ Π A' B' }}
+where "⊢anf M ⊆ N" := (alg_subtyping_nf M N) (in custom judg) : type_scope.
+
+
+Inductive alg_subtyping : ctx -> typ -> typ -> Prop :=
+| alg_subtyp_run :
+  forall Γ M N i j A B,
+    nbe Γ M {{{ Type@i }}} A ->
+    nbe Γ N {{{ Type@j }}} B ->
+    {{ ⊢anf A ⊆ B }} ->
+    {{ Γ ⊢a M ⊆ N }}
+where "Γ ⊢a M ⊆ N" := (alg_subtyping Γ M N) (in custom judg) : type_scope.
+
+#[export]
+  Hint Constructors alg_subtyping_nf alg_subtyping: mcltt.

theories/Algorithmic/Subtyping/Lemmas.v

@@ -0,0 +1,127 @@
+From Mcltt Require Import Base LibTactics.
+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.
+
+#[local]
+  Ltac apply_subtyping :=
+  repeat match goal with
+    | H : {{ ~?Γ ⊢ ~?A : ~?M }},
+        H1 : {{ ~?Γ ⊢ ~?M ⊆ ~?N }} |- _ =>
+        assert {{ Γ ⊢ A : N }} by mauto; clear H
+    end.
+
+Lemma alg_subtyping_nf_sound : forall M N,
+    {{ ⊢anf M ⊆ N }} ->
+    forall Γ i,
+      {{ Γ ⊢ M : Type@i }} ->
+      {{ Γ ⊢ N : Type@i }} ->
+      {{ Γ ⊢ M ⊆ N }}.
+Proof.
+  induction 1; intros; subst; simpl in *.
+  - econstructor. 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 [? ?]).
+    destruct_all.
+    gen_presups.
+    repeat match goal with
+           | H : {{ ~?Γ ⊢ ~?M ⊆ ~?N }}, H1: {{ ⊢ ~?Γ , ~_ }} |- _ =>
+               pose proof (wf_subtyp_univ_weaken _ _ _ _ H H1);
+               fail_if_dup
+           end.
+    apply_subtyping.
+    deepexec IHalg_subtyping_nf ltac:(fun H => pose proof H).
+    mauto 3.
+Qed.
+
+Lemma alg_subtyping_nf_trans : forall M1 M0 M2,
+    {{ ⊢anf M0 ⊆ M1 }} ->
+    {{ ⊢anf M1 ⊆ M2 }} ->
+    {{ ⊢anf M0 ⊆ M2 }}.
+Proof.
+  intro M1; induction M1; intros ? ? H1 H2;
+    dependent destruction H1;
+    dependent destruction H2;
+    simpl in *;
+    try contradiction;
+    mauto.
+  apply asnf_univ. lia.
+Qed.
+
+Lemma alg_subtyping_nf_refl : forall M,
+    {{ ⊢anf M ⊆ M }}.
+Proof.
+  intro M; induction M;
+    solve [constructor; simpl; trivial].
+Qed.
+
+#[local]
+ Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mcltt.
+
+Lemma alg_subtyping_trans : forall Γ M0 M1 M2,
+    {{ Γ ⊢a M0 ⊆ M1 }} ->
+    {{ Γ ⊢a M1 ⊆ M2 }} ->
+    {{ Γ ⊢a M0 ⊆ M2 }}.
+Proof.
+  intros. progressive_inversion.
+  functional_nbe_rewrite_clear.
+  mauto.
+Qed.
+
+#[local]
+ 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.
+    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.
+
+Lemma alg_subtyping_sound : forall Γ M N i,
+    {{ Γ ⊢a M ⊆ N }} ->
+    {{ Γ ⊢ M : Type@i }} ->
+    {{ Γ ⊢ N : Type@i }} ->
+    {{ Γ ⊢ M ⊆ N }}.
+Proof.
+  intros. destruct H.
+  on_all_hyp: fun H => apply soundness in H.
+  destruct_all.
+  functional_nbe_rewrite_clear.
+  gen_presups.
+  eapply alg_subtyping_nf_sound in H3; try eassumption.
+  etransitivity; [mauto |].
+  etransitivity; [eassumption |].
+  mauto.
+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/Core/Syntactic/System/Definitions.v

@@ -309,10 +309,10 @@ with wf_subtyping : ctx -> typ -> typ -> Prop :=
      {{ Γ ⊢ Type@i ⊆ Type@j }} )
 | wf_subtyp_pi :
   `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ B : Type@i }} ->
      {{ Γ ⊢ A' : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
      {{ Γ , A' ⊢ B' : Type@i }} ->
-     {{ Γ ⊢ A' ⊆ A }} ->
      {{ Γ , A' ⊢ B ⊆ B' }} ->
      {{ Γ ⊢ Π A B ⊆ Π A' B' }} )
 where "Γ ⊢ A ⊆ A'" := (wf_subtyping Γ A A') (in custom judg) : type_scope.

theories/Core/Syntactic/System/Lemmas.v

@@ -818,7 +818,7 @@ Proof.
   induction 1; intros; mauto 4.
   - transitivity {{{ Type@i}}}; [mauto |].
     transitivity {{{ Type@j}}}; [| mauto].
-    mauto.
+    mauto 3.
   - transitivity {{{ Π (A[σ]) (B [ q σ ]) }}}; [ mauto |].
     transitivity {{{ Π (A'[σ]) (B' [ q σ ]) }}}; [ | mauto].
     eapply wf_subtyp_pi with (i := i); mauto 4.
@@ -828,6 +828,19 @@ Qed.
 Hint Resolve wf_subtyping_sub : mcltt.
 
 
+Lemma wf_subtyp_univ_weaken : forall Γ i j A,
+    {{ Γ ⊢ Type@i ⊆ Type@j }} ->
+    {{ ⊢ Γ , A }} ->
+    {{ Γ , A ⊢ Type@i ⊆ Type@j }}.
+Proof.
+  intros.
+  eapply wf_subtyping_sub with (σ := {{{ Wk }}}) in H.
+  - transitivity {{{ Type@i[Wk] }}}; [mauto |].
+    etransitivity; mauto.
+  - mauto.
+Qed.
+
+
 Lemma ctx_sub_ctx_lookup : forall Γ Δ, {{ ⊢ Δ ⊆ Γ }} -> forall A x, {{ #x : A ∈ Γ }} -> exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢ B ⊆ A }}.
 Proof.
   induction 1; intros; progressive_inversion.

theories/Core/Syntactic/SystemOpt.v

@@ -267,3 +267,21 @@ Qed.
 Hint Resolve wf_exp_eq_pi_eta' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_pi_eta : mcltt.
+
+
+Lemma wf_subtyp_pi' : forall Γ A A' B B' i,
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ , A' ⊢ B ⊆ B' }} ->
+    {{ Γ ⊢ Π A B ⊆ Π A' B' }}.
+Proof.
+  intros. gen_presups.
+  eapply wf_subtyp_pi with (i := max i i0);
+    mauto 3 using lift_exp_max_left, lift_exp_max_right, lift_exp_eq_max_left.
+  eapply ctxeq_exp; [ | mauto 3 using lift_exp_max_right].
+  mauto 4.
+Qed.
+
+#[export]
+Hint Resolve wf_subtyp_pi' : mcltt.
+#[export]
+Remove Hints wf_subtyp_pi : mcltt.

theories/_CoqProject

@@ -2,8 +2,11 @@
 
 -arg -w -arg -cast-in-pattern,-notation-overridden
 
+./Algorithmic/Subtyping/Definitions.v
+./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