Add some templates (#91)

* Add placeholder for soundness

* Update names

* Add algorithm to decide conversion

theories/Core/Completeness.v

@@ -4,7 +4,7 @@ Import Domain_Notations.
 
 Theorem completeness : forall {Γ M M' A},
   {{ Γ ⊢ M ≈ M' : A }} ->
-  exists m, nbe Γ M A m /\ nbe Γ M' A m.
+  exists W, nbe Γ M A W /\ nbe Γ M' A W.
 Proof with mautosolve.
   intros * [env_relΓ]%completeness_fundamental_exp_eq.
   destruct_conjs.

theories/Core/Semantic/NbE.v

@@ -1,5 +1,6 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Evaluation Readback.
+From Mcltt.Core Require Export Domain.
 Import Domain_Notations.
 
 Generalizable All Variables.
@@ -60,3 +61,14 @@ Proof.
   functional_read_rewrite_clear;
   reflexivity.
 Qed.
+
+#[export]
+Hint Resolve functional_nbe : mcltt.
+
+Ltac functional_nbe_rewrite_clear1 :=
+  let tactic_error o1 o2 := fail 3 "functional_nbe equality between" o1 "and" o2 "cannot be solved by mauto" in
+  match goal with
+  | H1 : nbe ?G ?M ?A ?W, H2 : nbe ?G ?M ?A ?W' |- _ =>
+      clean replace W' with W by first [solve [mauto] | tactic_error W' W]; clear H2
+  end.
+Ltac functional_nbe_rewrite_clear := repeat functional_nbe_rewrite_clear1.

theories/Core/Soundness.v

@@ -0,0 +1,8 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Semantic.Domain Semantic.NbE System.
+Import Domain_Notations.
+
+Theorem soundness : forall {Γ M A},
+  {{ Γ ⊢ M : A }} ->
+  exists W, nbe Γ M A W /\ {{ Γ ⊢ M ≈ W : A }}.
+Admitted.

theories/Core/Syntactic/Syntax.v

@@ -99,6 +99,15 @@ with ne_to_exp (M : ne) : exp :=
 Coercion nf_to_exp : nf >-> exp.
 Coercion ne_to_exp : ne >-> exp.
 
+Fact nf_eq_dec : forall (M M' : nf),
+    ({M = M'} + {M <> M'})%type
+with ne_eq_dec : forall (M M' : ne),
+    ({M = M'} + {M <> M'})%type.
+Proof.
+  all: intros; decide equality;
+    apply PeanoNat.Nat.eq_dec.
+Defined.
+
 #[global] Declare Custom Entry exp.
 #[global] Declare Custom Entry nf.
 

theories/Extraction/TypeCheck.v

@@ -0,0 +1,35 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness NbE Soundness System.
+From Mcltt.Extraction Require Import NbE.
+From Equations Require Import Equations.
+Import Domain_Notations.
+
+#[local]
+Ltac impl_obl_tac :=
+  match goal with
+  | |- nbe_order ?G ?M ?A =>
+      (on_all_hyp: fun H => apply soundness in H);
+      destruct_conjs;
+      eapply nbe_order_sound; eassumption
+  | |- False =>
+      (on_all_hyp: fun H => apply completeness in H);
+      destruct_conjs;
+      functional_nbe_rewrite_clear;
+      congruence
+  | _ =>
+      (on_all_hyp: fun H => apply soundness in H);
+      destruct_conjs;
+      functional_nbe_rewrite_clear;
+      mauto
+  end.
+
+#[tactic="impl_obl_tac"]
+Equations conversion_dec G A M (HM : {{ G ⊢ M : A }}) M' (HM' : {{ G ⊢ M' : A }}) : { {{ G ⊢ M ≈ M' : A}} } + { ~ {{ G ⊢ M ≈ M' : A}} } :=
+| G, A, M, HM, M', HM' =>
+    let (W, HW) := nbe_impl G M A _ in
+    let (W', HW') := nbe_impl G M' A _ in
+    match nf_eq_dec W W' with
+    | left _ => left _
+    | right _ => right _
+    end.
+Next Obligation. impl_obl_tac. Qed.

theories/_CoqProject

@@ -37,13 +37,15 @@
 ./Core/Syntactic/System.v
 ./Core/Syntactic/System/Definitions.v
 ./Core/Syntactic/System/Lemmas.v
+./Core/Soundness.v
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definition.v
 ./Frontend/Elaborator.v
 ./Frontend/Parser.v
 ./Frontend/ParserExtraction.v
 ./Extraction/Evaluation.v
-./Extraction/Readback.v
 ./Extraction/NbE.v
+./Extraction/Readback.v
+./Extraction/TypeCheck.v
 ./LibTactics.v