function definition

.gitignore

@@ -17,4 +17,7 @@ Makefile.coq.conf
 
 _opam
 
-*.dot
+*.dot
+docs/dependency_graph.png
+
+docs/dependency_graph.pre

_CoqProject

@@ -75,6 +75,8 @@ theories/Decidability/Completeness.v
 theories/Decidability/Termination.v
 theories/Decidability.v
 
+theories/Decidability/UntypedFunctions.v
+
 theories/TermNotations.v
 theories/Decidability/Execution.v
 theories/Positivity.v

theories/BasicAst.v

@@ -1,6 +1,4 @@
 (** * LogRel.BasicAst: definitions preceding those of the AST of terms: sorts, binder annotations… *)
-From Coq Require Import String Bool.
-From LogRel.AutoSubst Require Import core unscoped.
 
 Inductive sort :=
   | set : sort.

theories/Decidability/Functions.v

@@ -435,7 +435,7 @@ Equations to_neutral_diag (t u : term) : option (ne_view1 t × ne_view1 u) :=
     | _ , _ => None
   }.
 
-Time Equations conv_ne : conv_stmt ne_state :=
+Equations conv_ne : conv_stmt ne_state :=
   | (Γ;inp; t; t') with t, t', to_neutral_diag t t' :=
   {
     | _, _, Some (ne_view1_rel n, ne_view1_rel n') with n =? n' :=
@@ -557,18 +557,25 @@ Equations conv_ne_red : conv_stmt ne_red_state :=
     Ainf ← rec (ne_state;Γ;tt;t;u) ;;
     ecall tt Ainf.
 
-Equations conv : ∇[singleton_store wh_red] (x : conv_full_dom), conv_full_cod x :=
+Equations _conv : ∇[singleton_store wh_red] (x : conv_full_dom), conv_full_cod x :=
   | (ty_state; Γ ; inp ; T; V) := conv_ty (Γ; inp; T; V);
   | (ty_red_state; Γ ; inp ; T; V) := conv_ty_red (Γ; inp; T; V);
   | (tm_state; Γ ; inp ; T; V) := conv_tm (Γ; inp; T; V);
   | (tm_red_state; Γ ; inp ; T; V) := conv_tm_red (Γ; inp; T; V);
   | (ne_state; Γ ; inp ; T; V) := conv_ne (Γ; inp; T; V);
   | (ne_red_state; Γ ; inp ; T; V) := conv_ne_red (Γ; inp; T; V).
 
+Import StdInstance.
+
+Equations tconv : (context × term × term) ⇀ result unit :=
+  tconv (Γ,T,V) := call _conv (ty_state;Γ;tt;T;V).
+
 End Conversion.
 
 Section Typing.
 
+Variable conv : (context × term × term) -> StdInstance.orec (context × term × term) (fun _ => result unit) (result unit).
+
 Variant typing_state : Type :=
   | inf_state (** inference *)
   | check_state (** checking *)
@@ -598,7 +605,7 @@ Definition binary_pfun@{u a b} {F1 F2: Type@{u}} (f1 : F1) (f2 : F2)
   `{h1: PFun@{u a b} F1 f1} `{h2: PFun@{u a b} F2 f2} :
   forall b, PFun@{u a b} (binary_store f1 f2 b).
 Proof.
-  intros b; destruct b; [destruct h1| destruct h2]; now econstructor.
+  intros [] ; cbn ; assumption.
 Defined.
 
 #[local]
@@ -630,7 +637,7 @@ Equations typing_wf_ty : typing_stmt wf_ty_state :=
   {
     | ty_view1_ty (eSort s) := success ;
     | ty_view1_ty (eProd A B) :=
-        rA ← rec (wf_ty_state;Γ;tt;A) ;;
+        rec (wf_ty_state;Γ;tt;A) ;;[M]
         rec (wf_ty_state;Γ,,A;tt;B) ;
     | ty_view1_ty (eNat) := success ;
     | ty_view1_ty (eEmpty) := success ;
@@ -768,7 +775,7 @@ Equations typing_wf_ty : typing_stmt wf_ty_state :=
   Equations typing_check : typing_stmt check_state :=
   | (Γ;T;t) :=
     T' ← rec (inf_state;Γ;tt;t) ;;
-    call (ϕ:=ϕ) conv_key (ty_state;Γ;tt;T';T).
+    call (ϕ:=ϕ) conv_key (Γ,T',T).
 
   Equations typing : ∇[ϕ] x, typing_full_cod x :=
   | (wf_ty_state; Γ; inp; T) := typing_wf_ty (Γ;inp;T)
@@ -780,11 +787,14 @@ End Typing.
 
 Section CtxTyping.
 
-  #[local] Instance: forall x, PFun (singleton_store typing x) := singleton_pfun typing.
+Variable conv : (context × term × term) -> StdInstance.orec (context × term × term) (fun _ => result unit) (result unit).
+
+
+  #[local] Instance: forall x, PFun (singleton_store (typing conv) x) := singleton_pfun (typing conv).
 
-  #[local] Instance: Monad (errrec (singleton_store typing) (A:=context) (B:=(fun _ => result unit))) := monad_erec.
+  #[local] Instance: Monad (errrec (singleton_store (typing conv)) (A:=context) (B:=(fun _ => result unit))) := monad_erec.
 
-  Equations check_ctx : context ⇀[singleton_store typing] result unit :=
+  Equations check_ctx : context ⇀[singleton_store (typing conv)] result unit :=
     check_ctx ε := ret tt ;
     check_ctx (Γ,,A) :=
       rec Γ ;;

theories/Decidability/Soundness.v

@@ -148,7 +148,7 @@ Section CtxAccessCorrect.
 End CtxAccessCorrect.
 
 Ltac funelim_conv :=
-  funelim (conv _); 
+  funelim (_conv _); 
     [ funelim (conv_ty _) | funelim (conv_ty_red _) | 
       funelim (conv_tm _) | funelim (conv_tm_red _) | 
       funelim (conv_ne _) | funelim (conv_ne_red _) ].
@@ -172,7 +172,7 @@ Section ConversionSound.
   end.
 
   Lemma _implem_conv_sound :
-    funrect conv (fun _ => True) conv_sound_type.
+    funrect _conv (fun _ => True) conv_sound_type.
   Proof.
     intros x _.
     funelim_conv ; cbn.
@@ -204,28 +204,47 @@ Section ConversionSound.
     - split; tea. now econstructor.
   Qed.
 
-  Corollary implem_conv_sound x r :
-    graph conv x r ->
-    conv_sound_type x r.
+  Arguments conv_full_cod _ /.
+  Arguments conv_cod _/.
+
+  Corollary implem_conv_sound Γ T V r :
+    graph tconv (Γ,T,V) (ok r) ->
+    [Γ |-[al] T ≅ V].
   Proof.
-    eapply funrect_graph.
-    1: now apply _implem_conv_sound.
-    easy.
+    assert (funrect tconv (fun _ => True)
+      (fun '(Γ,T,V) r => match r with | ok _ => [Γ |-[al] T ≅ V] | _ => True end)) as Hrect.
+    {
+     intros ? _.
+     funelim (tconv _) ; cbn.
+     intros [] ; cbn ; [|easy].
+     eintros ?%funrect_graph.
+     2: now apply _implem_conv_sound.
+     all: now cbn in *.
+    }
+    eintros ?%funrect_graph.
+    2: eassumption.
+    all: now cbn in *.
   Qed.
 
 End ConversionSound.
 
 Ltac funelim_typing :=
-  funelim (typing _); 
-    [ funelim (typing_inf _) | 
-      funelim (typing_check _) |
-      funelim (typing_inf_red _) | 
-      funelim (typing_wf_ty _) ].
+  funelim (typing _ _); 
+    [ funelim (typing_inf _ _) | 
+      funelim (typing_check _ _) |
+      funelim (typing_inf_red _ _) | 
+      funelim (typing_wf_ty _ _) ].
 
-Section TypingCorrect.
+Section TypingSound.
 
   #[local]Existing Instance ty_errors.
 
+  Variable conv : (context × term × term) -> StdInstance.orec (context × term × term) (fun _ => result unit) (result unit).
+
+  Hypothesis conv_sound : forall Γ T V r,
+    graph conv (Γ,T,V) (ok r) ->
+    [Γ |-[al] T ≅ V].
+
   Lemma ty_view1_small_can T n : build_ty_view1 T = ty_view1_small n -> ~ isCanonical T.
   Proof.
     destruct T ; cbn.
@@ -244,9 +263,8 @@ Section TypingCorrect.
   | (check_state;Γ;T;t), (ok _) => [Γ |-[al] t ◃ T]
   end.
 
-
   Lemma _implem_typing_sound :
-    funrect typing (fun _ => True) typing_sound_type.
+    funrect (typing conv) (fun _ => True) typing_sound_type.
   Proof.
     intros x _.
     funelim_typing ; cbn.
@@ -269,23 +287,19 @@ Section TypingCorrect.
   Qed.
 
   Lemma implem_typing_sound x r:
-    graph typing x r ->
+    graph (typing conv) x r ->
     typing_sound_type x r.
   Proof.
     eapply funrect_graph.
     1: now apply _implem_typing_sound.
     easy.
   Qed.
 
-End TypingCorrect.
-
-Section CtxTypingSound.
-
   Lemma _check_ctx_sound :
-    funrect check_ctx (fun _ => True) (fun Γ r => if r then [|- Γ] else True).
+    funrect (check_ctx conv) (fun _ => True) (fun Γ r => if r then [|- Γ] else True).
   Proof.
     intros ? _.
-    funelim (check_ctx _) ; cbn.
+    funelim (check_ctx _ _) ; cbn.
     - now constructor.
     - split ; [easy|].
       intros [|] ; cbn ; try easy.
@@ -295,12 +309,12 @@ Section CtxTypingSound.
   Qed.
 
   Lemma check_ctx_sound Γ :
-    graph check_ctx Γ (ok tt) ->
+    graph (check_ctx conv) Γ (ok tt) ->
     [|-[al] Γ].
   Proof.
     eintros ?%funrect_graph.
     2: eapply _check_ctx_sound.
     all: easy.
   Qed.
 
-End CtxTypingSound.
+End TypingSound.