working on subtyping impl

theories/Extraction/NbE.v

@@ -107,45 +107,125 @@ Qed.
 #[local]
   Hint Resolve nbe_order_sound : mcltt.
 
-#[local]
-  Ltac impl_obl_tac1 :=
+Section NbEDef.
+
+  #[local]
+    Ltac impl_obl_tac1 :=
   match goal with
   | H : nbe_order _ _ _ |- _ => progressive_invert H
   end.
 
+  #[local]
+    Ltac impl_obl_tac :=
+    repeat impl_obl_tac1; try econstructor; mauto.
+
+  #[tactic="impl_obl_tac"]
+    Equations nbe_impl G M A (H : nbe_order G M A) : { w | nbe G M A w } by struct H :=
+  | G, M, A, H =>
+      let (p, Hp) := initial_env_impl G _ in
+      let (a, Ha) := eval_exp_impl A p _ in
+      let (m, Hm) := eval_exp_impl M p _ in
+      let (w, Hw) := read_nf_impl (length G) d{{{ ⇓ a m }}} _ in
+      exist _ w _.
+
+  Lemma nbe_impl_complete' : forall G M A w,
+      nbe G M A w ->
+      forall (H : nbe_order G M A),
+      exists H', nbe_impl G M A H = exist _ w H'.
+  Proof.
+    induction 1;
+      pose proof initial_env_impl_complete';
+      pose proof eval_exp_impl_complete';
+      pose proof read_nf_impl_complete';
+      intros; simp nbe_impl;
+      repeat complete_tac;
+      eauto.
+  Qed.
+
+End NbEDef.
+
 #[local]
-  Ltac impl_obl_tac :=
-  repeat impl_obl_tac1; try econstructor; mauto.
-
-#[tactic="impl_obl_tac"]
-  Equations nbe_impl G M A (H : nbe_order G M A) : { w | nbe G M A w } by struct H :=
-| G, M, A, H =>
-    let (p, Hp) := initial_env_impl G _ in
-    let (a, Ha) := eval_exp_impl A p _ in
-    let (m, Hm) := eval_exp_impl M p _ in
-    let (w, Hw) := read_nf_impl (length G) d{{{ ⇓ a m }}} _ in
-    exist _ w _.
-
-Lemma nbe_impl_complete' : forall G M A w,
+  Hint Resolve nbe_impl_complete' : mcltt.
+
+Lemma nbe_impl_complete : forall G M A w,
     nbe G M A w ->
-    forall (H : nbe_order G M A),
-      exists H', nbe_impl G M A H = exist _ w H'.
+      exists H H', nbe_impl G M A H = exist _ w H'.
+Proof.
+  repeat unshelve mauto.
+Qed.
+
+
+Inductive nbe_ty_order G A : Prop :=
+| nbe_ty_order_run :
+  `( initial_env_order G ->
+     (forall p, initial_env G p ->
+           eval_exp_order A p) ->
+     (forall p a,
+         initial_env G p ->
+         {{ ⟦ A ⟧ p ↘ a }} ->
+         read_typ_order (length G) a) ->
+     nbe_ty_order G A ).
+
+#[local]
+  Hint Constructors nbe_ty_order : mcltt.
+
+
+Lemma nbe_ty_order_sound : forall G A w,
+    nbe_ty G A w ->
+    nbe_ty_order G A.
+Proof with (econstructor; intros;
+            functional_initial_env_rewrite_clear;
+            functional_eval_rewrite_clear;
+            functional_read_rewrite_clear;
+            mauto).
+  induction 1...
+Qed.
+
+#[local]
+  Hint Resolve nbe_ty_order_sound : mcltt.
+
+Section NbETyDef.
+
+  #[local]
+    Ltac impl_obl_tac1 :=
+  match goal with
+  | H : nbe_ty_order _ _ |- _ => progressive_invert H
+  end.
+
+  #[local]
+    Ltac impl_obl_tac :=
+    repeat impl_obl_tac1; try econstructor; mauto.
+
+  #[tactic="impl_obl_tac"]
+    Equations nbe_ty_impl G A (H : nbe_ty_order G A) : { w | nbe_ty G A w } by struct H :=
+  | G, A, H =>
+      let (p, Hp) := initial_env_impl G _ in
+      let (a, Ha) := eval_exp_impl A p _ in
+      let (w, Hw) := read_typ_impl (length G) a _ in
+      exist _ w _.
+
+End NbETyDef.
+
+Lemma nbe_ty_impl_complete' : forall G A w,
+    nbe_ty G A w ->
+    forall (H : nbe_ty_order G A),
+      exists H', nbe_ty_impl G A H = exist _ w H'.
 Proof.
   induction 1;
     pose proof initial_env_impl_complete';
     pose proof eval_exp_impl_complete';
-    pose proof read_nf_impl_complete';
-    intros; simp nbe_impl;
+    pose proof read_typ_impl_complete';
+    intros; simp nbe_ty_impl;
     repeat complete_tac;
     eauto.
 Qed.
 
 #[local]
-  Hint Resolve nbe_impl_complete' : mcltt.
+  Hint Resolve nbe_ty_impl_complete' : mcltt.
 
-Lemma nbe_impl_complete : forall G M A w,
-    nbe G M A w ->
-      exists H H', nbe_impl G M A H = exist _ w H'.
+Lemma nbe_ty_impl_complete : forall G A w,
+    nbe_ty G A w ->
+      exists H H', nbe_ty_impl G A H = exist _ w H'.
 Proof.
   repeat unshelve mauto.
 Qed.

theories/Extraction/Subtyping.v

@@ -0,0 +1,113 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Algorithmic Require Import Subtyping.Definitions.
+From Mcltt.Core Require Import NbE.
+From Mcltt.Extraction Require Import Evaluation NbE.
+From Equations Require Import Equations.
+Import Domain_Notations.
+
+
+#[local]
+  Ltac subtyping_tac :=
+  lazymatch goal with
+  | |- {{ ⊢anf ~_ ⊆ ~_ }} =>
+      subst;
+      mauto 4;
+      try congruence;
+      econstructor; simpl; trivial
+  | |- ~ {{ ⊢anf ~_ ⊆ ~_ }} =>
+      let H := fresh "H" in
+      intro H; dependent destruction H; simpl in *;
+      try lia;
+      try congruence
+  end.
+
+#[tactic="subtyping_tac"]
+Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆ B }} } :=
+| n{{{ Type@i }}}, n{{{ Type@j }}} with Compare_dec.le_lt_dec i j => {
+  | left _ => left _;
+  | right _ => right _
+  }
+| n{{{ Π A B }}}, n{{{ Π A' B' }}} with nf_eq_dec A A' => {
+  | left _ with subtyping_nf_impl B B' => {
+    | left _ => left _
+    | right _ => right _
+    }
+  | right _ => right _
+  }
+| A, B with nf_eq_dec A B => {
+  | left _ => left _
+  | right _ => right _
+  }.
+
+Theorem subtyping_nf_impl_complete : forall A B,
+    {{ ⊢anf A ⊆ B }} ->
+    exists H, subtyping_nf_impl A B = left H.
+Proof.
+  intros; dec_complete.
+Qed.
+
+
+Inductive subtyping_order G A B :=
+| subtyping_order_run :
+  nbe_ty_order G A ->
+  nbe_ty_order G B ->
+  subtyping_order G A B.
+#[local]
+  Hint Constructors subtyping_order : mcltt.
+
+
+Lemma subtyping_order_sound : forall G A B,
+    {{ G ⊢a A ⊆ B }} ->
+    subtyping_order G A B.
+Proof.
+  intros * H.
+  dependent destruction H.
+  mauto using nbe_ty_order_sound.
+Qed.
+
+#[local]
+  Ltac subtyping_impl_tac1 :=
+  match goal with
+  | H : subtyping_order _ _ _ |- _ => progressive_invert H
+  | H : nbe_ty_order _ _ |- _ => progressive_invert H
+  end.
+
+#[local]
+  Ltac subtyping_impl_tac :=
+  repeat subtyping_impl_tac1; try econstructor; mauto.
+
+
+#[tactic="subtyping_impl_tac"]
+Equations subtyping_impl G A B (H : subtyping_order G A B) :
+  { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
+| G, A, B, H =>
+    let (a, Ha) := nbe_ty_impl G A _ in
+    let (b, Hb) := nbe_ty_impl G B _ in
+    match subtyping_nf_impl a b with
+    | left _ => left _
+    | right _ => right _
+    end.
+Next Obligation.
+  progressive_inversion.
+  functional_nbe_rewrite_clear.
+  contradiction.
+Qed.
+
+
+Theorem subtyping_impl_complete' : forall G A B,
+    {{G ⊢a A ⊆ B}} ->
+    forall (H : subtyping_order G A B),
+      exists H', subtyping_impl G A B H = left H'.
+Proof.
+  intros; dec_complete.
+Qed.
+
+#[local]
+ Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt.
+
+Theorem subtyping_impl_complete : forall G A B,
+    {{G ⊢a A ⊆ B}} ->
+    exists H H', subtyping_impl G A B H = left H'.
+Proof.
+  repeat unshelve mauto.
+Qed.

theories/LibTactics.v

@@ -486,3 +486,16 @@ Ltac bulky_rewrite_in1 HT :=
   end.
 
 Ltac bulky_rewrite_in HT := repeat (bulky_rewrite_in1 HT; mauto 2).
+
+
+(** This tactic provides a trivial proof for the completeness of a decision procedure. *)
+Ltac dec_complete :=
+  lazymatch goal with
+  | |- exists _, ?L = _ =>
+      lazymatch type of L with
+      | sumbool _ _ =>
+          let Heq := fresh "Heq" in
+          destruct L eqn:Heq; eauto;
+          contradiction
+      end
+  end.

theories/_CoqProject

@@ -77,4 +77,5 @@
 ./Extraction/NbE.v
 ./Extraction/Readback.v
 ./Extraction/TypeCheck.v
+./Extraction/Subtyping.v
 ./LibTactics.v