fux subtyping impl

theories/Extraction/Subtyping.v

@@ -6,53 +6,39 @@ From Equations Require Import Equations.
 Import Domain_Notations.
 
 
-Equations subtyping_nf_impl (A B : nf) : bool :=
+#[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 _ => true;
-  | right _ => false
+  | left _ => left _;
+  | right _ => right _
   }
 | n{{{ Π A B }}}, n{{{ Π A' B' }}} with nf_eq_dec A A' => {
-  | left _ => subtyping_nf_impl B B'
-  | right _ => false
+  | left _ with subtyping_nf_impl B B' => {
+    | left _ => left _
+    | right _ => right _
+    }
+  | right _ => right _
   }
 | A, B with nf_eq_dec A B => {
-  | left _ => true
-  | right _ => false
+  | left _ => left _
+  | right _ => right _
   }.
 
-Theorem subtyping_nf_impl_sound : forall A B,
-    subtyping_nf_impl A B = true ->
-    alg_subtyping_nf A B.
-Proof.
-  intros. funelim (subtyping_nf_impl A B); mauto 2.
-  all:simp subtyping_nf_impl in *;
-    repeat match goal with
-      | H : _ = _ |- _ => rewrite H in *
-      end;
-    subst;
-    simpl in *;
-    try congruence.
-  all:try solve [econstructor; simpl; trivial].
-  mauto.
-Qed.
-
-Theorem subtyping_nf_impl_complete : forall A B,
-    alg_subtyping_nf A B ->
-    subtyping_nf_impl A B = true.
-Proof.
-  induction 1; subst.
-  - destruct (nf_eq_dec N N) eqn:?; try congruence.
-    destruct N; simp subtyping_nf_impl;
-      try rewrite Heqs;
-      simpl in *;
-      try contradiction;
-      trivial.
-  - simp subtyping_nf_impl.
-    destruct (Compare_dec.le_lt_dec i j);
-      simpl; lia.
-  - simp subtyping_nf_impl.
-    destruct (nf_eq_dec A' A'); simpl; congruence.
-Qed.
 
 
 (* Equations subtyping_impl Γ A B : bool := *)

theories/_CoqProject

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