From 2f51444ee8f6a700546ab5054c0f77cbacbdca7c Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Thu, 4 Jan 2024 16:16:23 +0100
Subject: [PATCH] Decidability of conversion

---
 theories/AlgorithmicConvProperties.v |  9 ++++++-
 theories/Decidability.v              | 37 +++++++++++++++++++++++-----
 theories/Decidability/Termination.v  | 20 ++++++++++++---
 theories/Readme.v                    |  5 ++--
 4 files changed, 59 insertions(+), 12 deletions(-)

diff --git a/theories/AlgorithmicConvProperties.v b/theories/AlgorithmicConvProperties.v
index f8d874ed..8b6d2f4e 100644
--- a/theories/AlgorithmicConvProperties.v
+++ b/theories/AlgorithmicConvProperties.v
@@ -2854,4 +2854,11 @@ Lemma algo_conv_complete Γ A B :
   [Γ |-[al] A ≅ B].
 Proof.
   now intros [HΓ ? _ []%(escapeEq (ta := bni))]%Fundamental.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma algo_convtm_complete Γ t u A :
+  [Γ |-[de] t ≅ u : A] ->
+  [Γ |-[al] t ≅ u : A].
+Proof.
+   now intros [HΓ ??? []%(escapeTmEq (ta := bni))]%Fundamental.
+Qed.
diff --git a/theories/Decidability.v b/theories/Decidability.v
index a7ad7263..004ba1b3 100644
--- a/theories/Decidability.v
+++ b/theories/Decidability.v
@@ -14,7 +14,7 @@ Import IndexedDefinitions.
 Definition inspect {A} (a : A) : {b | a = b} :=
   exist _ a eq_refl.
   
-Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
+Notation "x 'eq:' p" := (exist _ x p) (only parsing, at level 20).
 
 Obligation Tactic := try easy.
 
@@ -23,8 +23,8 @@ Equations check_ty (Γ : context) (T : term) (hΓ : [|- Γ]) :
 
 check_ty Γ T hΓ with (inspect (def typing (wf_ty_state;Γ;tt;T) _)) :=
   {
-    | ok _ eqn: e => inl _
-    | error _ eqn: e => inr _
+    | ok _ eq: e => inl _
+    | error _ eq: e => inr _
   }.
 Next Obligation.
   intros.
@@ -81,13 +81,16 @@ Next Obligation.
   now inversion hΓ'.
 Qed.
 
+
+
+
 Equations check (Γ : context) (T t : term) (hΓ : [|- Γ]) (hT : [Γ |- T]) :
   [Γ |- t : T] + ~[Γ |- t : T] :=
 
 check Γ T t hΓ hT with (inspect (def typing (check_state;Γ;T;t) _)) :=
   {
-    | ok _ eqn: e => inl _
-    | error _ eqn: e => inr _
+    | ok _ eq: e => inl _
+    | error _ eq: e => inr _
   }.
 Next Obligation.
   intros.
@@ -144,4 +147,26 @@ Next Obligation.
   eauto with boundary.
 Qed.
 
-Print Assumptions check_full.
\ No newline at end of file
+Print Assumptions check_full.
+
+Definition check_conv (Γ : context) (T t t' : term) (hΓ : [|- Γ]) (hT : [Γ |- T]) (ht : [Γ |- t : T]) (ht' : [Γ |- t' : T]) :
+  [Γ |- t ≅ t' : T] + ~[Γ |- t ≅ t' : T].
+Proof.
+  assert (hdom : domain conv (tm_state; Γ; T; t; t')).
+  1: now eapply conv_terminates.
+  pose (x := (def conv (tm_state;Γ;T;t;t') hdom)).
+  destruct x as [|] eqn:e; [left| right]; cbn in *.
+  all: pose proof (def_graph_sound _ _ hdom) as Hgraph.
+  - unfold x in e; rewrite e in Hgraph.
+    apply implem_conv_sound in Hgraph ; cbn in Hgraph.
+    now eapply algo_conv_sound in Hgraph.
+  - intros Hty.
+    enough (graph conv (tm_state;Γ;T;t;t') (ok tt)).
+    {
+      eapply orec_graph_functional in Hgraph ; tea.
+      pose proof (eq_trans Hgraph e) as [=].
+    }
+    eapply algo_convtm_complete in Hty; inversion Hty; subst.
+    apply implem_conv_complete.
+    now constructor.
+Qed.
diff --git a/theories/Decidability/Termination.v b/theories/Decidability/Termination.v
index 1ac513d9..a9069260 100644
--- a/theories/Decidability/Termination.v
+++ b/theories/Decidability/Termination.v
@@ -563,7 +563,7 @@ Proof.
       now eexists.
   Qed.
   
-  Corollary conv_terminates Γ A A' :
+  Corollary convty_terminates Γ A A' :
     [Γ |-[de] A] ->
     [Γ |-[de] A'] ->
     forall v,
@@ -577,6 +577,20 @@ Proof.
     all: boundary.
   Qed.
 
+  Corollary conv_terminates Γ A t u :
+    [Γ |-[de] A] ->
+    [Γ |-[de] t : A] ->
+    [Γ |-[de] u : A] ->
+    domain conv (tm_state;Γ;A;t;u).
+  Proof.
+    intros.
+    eapply _conv_terminates ; tea.
+    split.
+    5: eapply algo_convtm_complete.
+    5: econstructor.
+    all: boundary.
+  Qed.
+
 End ConversionTerminates.
 
 Section TypingTerminates.
@@ -831,7 +845,7 @@ Proof.
       intros ?%implem_typing_sound%algo_typing_sound ; cbn in * ; tea.
       split.
       2: easy.
-      eapply conv_terminates ; tea.
+      eapply convty_terminates ; tea.
       boundary.
   - split.
     + apply IH ; cbn ; try easy.
@@ -876,4 +890,4 @@ Proof.
     intros [[]|] ; now cbn.
 Qed.
 
-End TypingTerminates.
\ No newline at end of file
+End TypingTerminates.
diff --git a/theories/Readme.v b/theories/Readme.v
index f906fa3e..4101670c 100644
--- a/theories/Readme.v
+++ b/theories/Readme.v
@@ -103,7 +103,7 @@ About redtm_map_comp.
 
 From LogRel Require Import DeclarativeTyping DeclarativeInstance AlgorithmicTyping.
 
-(* Declaratve typing *)
+(* Declarative typing *)
 Print TypingDecl.
 
 (* Algorithmic conversion *)
@@ -412,7 +412,8 @@ About typing_terminates.
  
 From LogRel Require Import Decidability Normalisation Consequences.
  
-(* Decidability of typechecking *)
+(* Decidability of conversion and typechecking *)
+About check_conv.
 About check_full.
 
 (* Normalisation *)