From 5ac38615c06822c9072173033508c5a7f09a4df3 Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Fri, 27 Oct 2023 18:34:24 +0200
Subject: [PATCH] New notations for PR functions and FOL formulas
 (experimental)

---
 theories/ordinals/Ackermann/cPair.v         | 12 +++++-------
 theories/ordinals/Ackermann/primRec.v       | 14 ++++++--------
 theories/ordinals/MoreAck/PrimRecExamples.v | 12 ++++++------
 3 files changed, 17 insertions(+), 21 deletions(-)

diff --git a/theories/ordinals/Ackermann/cPair.v b/theories/ordinals/Ackermann/cPair.v
index 67e49adf..21c61228 100644
--- a/theories/ordinals/Ackermann/cPair.v
+++ b/theories/ordinals/Ackermann/cPair.v
@@ -5,7 +5,7 @@
 Require Import Arith Coq.Lists.List Lia.
 From hydras Require Import extEqualNat primRec.
 From hydras Require Export Compat815 ssrnat_extracts.
-
+Import PRNotations.
 Import Nat.
 
 
@@ -603,13 +603,11 @@ Proof.
     induction H0 as (x0, p0).
     induction H1 as (x1, p1).
     exists
-      (primRecFunc n (composeFunc n 0 (PRnil _) zeroFunc)
-         (composeFunc (S (S n)) 2
-            (PRcons _ _ x
-               (PRcons _ _ (projFunc n.+2 n
+      (primRecFunc n (PRcomp zeroFunc [ ])
+       (PRcomp x0 
+            [ x ;  projFunc n.+2 n
                               (Nat.lt_lt_succ_r n n.+1
-                                 (Nat.lt_succ_diag_r  n)))
-                  (PRnil _))) x0)).
+                                 (Nat.lt_succ_diag_r n))]))%pr.
     apply
       extEqualTrans
       with
diff --git a/theories/ordinals/Ackermann/primRec.v b/theories/ordinals/Ackermann/primRec.v
index c9a8d10a..a2de3d8e 100644
--- a/theories/ordinals/Ackermann/primRec.v
+++ b/theories/ordinals/Ackermann/primRec.v
@@ -14,6 +14,7 @@ Require Export Bool.
 Require Export EqNat.
 Require Import Lia. 
 
+
 (** * Definitions *)
 
 (** [PrimRec n] : data type of primitive recursive functions of arity [n] 
@@ -72,7 +73,7 @@ End PRNotations.
 
 (* end snippet PRNotations *)
 
-
+Import PRNotations.
 
 
 Scheme PrimRec_PrimRecs_rec := Induction for PrimRec Sort Set
@@ -351,14 +352,13 @@ Proof. exists succFunc; cbn; reflexivity. Qed.
 Proof.
   induction n as [|n [x Hx]].
   - exists zeroFunc; reflexivity. 
-  - exists (composeFunc _ _ (PRcons _ _ x (PRnil _)) succFunc);
-      cbn; now rewrite Hx.
+  - exists (PRcomp succFunc [x]%pr)%pr; cbn; now rewrite Hx.
 Qed.
 
 #[export] Instance const1_NIsPR n: isPR 1 (fun _ => n).
 Proof.
   destruct (const0_NIsPR n) as [x Hx]. 
-  exists (composeFunc 1 _ (PRnil _) x); cbn in *; auto.
+  exists (PRcomp x [])%pr;  cbn in *; auto.
 Qed.
 
 (** ** Usual projections (in curried form) are primitive recursive *)
@@ -366,15 +366,13 @@ Qed.
 (* begin snippet idIsPR:: no-out *)
 #[export] Instance idIsPR : isPR 1 (fun x : nat => x).
 Proof.
-  assert (H: 0 < 1) by auto.
-  exists (projFunc 1 0 H); cbn; auto.
+  exists pi1_1; cbn; reflexivity.
 Qed.
 (* end snippet idIsPR *)
 
 #[export] Instance pi1_2IsPR : isPR 2 (fun a b : nat => a).
 Proof.
- assert (H: 1 < 2) by auto.
- exists (projFunc _ _ H); cbn; reflexivity.
+  exists pi1_2; cbn; reflexivity.
 Qed.
 
 #[export] Instance pi2_2IsPR : isPR 2 (fun a b : nat => b).
diff --git a/theories/ordinals/MoreAck/PrimRecExamples.v b/theories/ordinals/MoreAck/PrimRecExamples.v
index 617a9ece..7132ba9e 100644
--- a/theories/ordinals/MoreAck/PrimRecExamples.v
+++ b/theories/ordinals/MoreAck/PrimRecExamples.v
@@ -119,7 +119,7 @@ Compute (evalPrimRec _ pi2_3) 1 2 3.
 .. coq:: no-out 
 |*)
 
-Check  (PRcons _ _ pi2_3 (PRnil _)).
+Check  [pi2_3]%pr.
 
 Definition plus := (PRrec pi1_1
                       (PRcomp succFunc [pi2_3]))%pr.
@@ -203,7 +203,7 @@ End MoreExamples.
    make the construction more   concrete *)
 
 Definition PRcompose1 (g f : PrimRec 1) : PrimRec 1 :=
-  composeFunc 1  _ (PRcons _  _  f  (PRnil _) ) g.
+  PRcomp g [f]%pr.  
 
 Goal forall f g x, evalPrimRec 1 (PRcompose1 g f) x =
                  evalPrimRec 1 g (evalPrimRec 1 f x).
@@ -321,8 +321,7 @@ Fact compose_01 :
     forall (x:PrimRec 0) (t : PrimRec 1),
     let c := evalPrimRec 0 x in
     let f := evalPrimRec 1 t in
-    evalPrimRec 0
-      (composeFunc 0 1 (PRcons 0 0 x (PRnil 0)) t)
+    evalPrimRec 0 (PRcomp t [x])%pr
     = f c. 
 Proof. reflexivity. Qed.
 (*||*)
@@ -341,7 +340,7 @@ Proof.
   induction n.
  - apply zeroIsPR.
  - destruct IHn as [x Hx].
-   exists (composeFunc 0 1 (PRcons 0 0 x (PRnil 0)) succFunc). 
+   exists (PRcomp succFunc [x])%pr.
    cbn in *; intros; now rewrite Hx.
 Qed.
 
@@ -455,7 +454,8 @@ Qed.
 
 (* Move to MoreAck *)
 
-Section Exs. (* Todo: exercise *)Let f: naryFunc 2 := fun x y => x + pred (cPairPi1 y).
+Section Exs. (* Todo: exercise *)
+Let f: naryFunc 2 := fun x y => x + pred (cPairPi1 y).
 
   (* To prove !!! *)