Library hydras.MoreAck.PrimRecExamples

From Coq Require Import Arith ArithRing List Vector Utf8.
Import VectorNotations.

From hydras Require Import primRec cPair.
Import extEqualNat PRNotations.

Check leBool : naryRel 2.

Check plus: naryFunc 2.

Check 42: naryFunc 0.

Check (fun n p q : nat ⇒ n × p + q): naryFunc 3.

Example extEqual_ex1: (Nat.mul: naryFunc 2) =x = fun x y ⇒ y × x + x - x.

Examples of terms of type PrimRec n and their interpretation

Example Ex1 : PReval zeroFunc = 0.

Example Ex2 a : PReval succFunc a = a .+1.

Example Ex3 a b c d e f: ∀ (H: 2 < 6),
    PReval (projFunc 6 2 H) a b c d e f = d.

Example Ex4 : extEqual 4 (fun a b c d: nat ⇒ 0)
                         (PReval (PRcomp zeroFunc (PRnil _))).

Section Composition.

  Variables (x y z : PrimRec 2) (t: PrimRec 3).
  Let u : PrimRec 2 := composeFunc 2 3 [x ; y ; z ]%pr t.
  Let f := PReval x.
  Let g := PReval y.
  Let h := PReval z.
  Let k := PReval t.
Goal ∀ n p , PReval u n p = k (f n p ) (g n p ) (h n p ).

  Let v := (PRcomp t [ pi1_2 ; pi1_2 ; pi2_2 ])%pr.

  Eval simpl in PReval v.

End Composition.

Section Primitive_recursion.
Variables (x: PrimRec 2)(y: PrimRec 4).
Let z := (primRecFunc _ x y).
Let g := PReval x.
Let h := PReval y.
Let f := PReval z.
Goal ∀ a b , f 0 a b = g a b.

Goal ∀ n a b , f n .+1 a b = h n (f n a b ) a b.

End Primitive_recursion.

Section compose2Examples.
Variables (f: naryFunc 1) (g: naryFunc 2) (h: naryFunc 3)
  (f': naryFunc 4) (g': naryFunc 5).

Eval simpl in compose2 1 f g.

Eval simpl in compose2 2 g h.

Eval simpl in compose2 _ f' g'.
End compose2Examples.

Module MoreExamples.

The unary constant function which returns 0

Definition cst0 : PrimRec 1 := (PRcomp zeroFunc (PRnil _))%pr.

The unary constant function which returns i

Fixpoint cst (i: nat) : PrimRec 1 :=
  match i with
    0 ⇒ cst0
  | S j ⇒ (PRcomp succFunc [cst j])%pr
end.

Addition

Definition plus : PrimRec 2 :=
(PRrec pi1_1 (PRcomp succFunc [pi2_3 ]))%pr.

Multiplication

Definition mult : PrimRec 2 :=
PRrec cst0
(PRcomp plus [pi2_3 ; pi3_3 ]%pr).

Factorial function

Definition fact : PrimRec 1 :=
  (PRrec
     (PRcomp succFunc [zeroFunc ])
     (PRcomp mult [pi2_2 ; PRcomp succFunc [pi1_2 ]]))%pr.

End MoreExamples.

Import MoreExamples.

Lemma cst0_correct : PRcorrect cst0 (fun _ ⇒ 0).

Lemma cst_correct (k:nat) : PRcorrect (cst k) (fun _ ⇒ k).

Lemma plus_correct: PRcorrect plus Nat.add.

Remark mult_eqn1 n p:
    PReval mult (S n) p =
      PReval plus (PReval mult n p) p.

Lemma mult_correct: PRcorrect mult Nat.mul.

Lemma fact_correct : PRcorrect fact Coq.Arith.Factorial.fact.

Understanding some constructions ...

These lemmas are trivial and theoretically useless, but they may help to make the construction more concrete

Definition PRcompose1 (g f : PrimRec 1) : PrimRec 1 := PRcomp g [f ]%pr.

Goal ∀ f g x , evalPrimRec 1 (PRcompose1 g f ) x =
                     evalPrimRec 1 g (evalPrimRec 1 f x ).

Remark compose2_0 (a:nat) (g: nat → nat) : compose2 0 a g = g a.

Remark compose2_1 (f: nat → nat) (g : nat → nat → nat) x
  : compose2 1 f g x = g (f x) x.

Remark compose2_2 (f: naryFunc 2) (g : naryFunc 3) x y
  : compose2 2 f g x y = g (f x y) x y.

Remark compose2_3 (f: naryFunc 3) (g : naryFunc 4) x y z
  : compose2 3 f g x y z = g (f x y z) x y z.

Remark PrimRec_0_0 (a:nat)(g : nat → nat → nat) :
  evalPrimRecFunc 0 a g 0 = a.

Remark PrimRec_0_S (a : nat) (g : nat → nat → nat) (i:nat):
  let phi := evalPrimRecFunc 0 a g
  in phi (S i) = g i (phi i).

Remark PrimRec_1_0 (f : nat →nat)(g : nat → nat → nat → nat) :
  ∀ x, evalPrimRecFunc 1 f g 0 x = f x.

Remark PrimRec_1_S (f: nat →nat)
       (g : nat → nat → nat → nat) (i:nat):
  let phi := evalPrimRecFunc 1 f g
  in ∀ x, phi (S i) x = g i (phi i x) x.

Remark PrimRec_2_0 (f : naryFunc 2) (g : naryFunc 4) :
  ∀ x y, evalPrimRecFunc 2 f g 0 x y = f x y.

Remark PrimRec_2_S (f: naryFunc 2) (g : naryFunc 4) (i:nat) :
  let phi := evalPrimRecFunc 2 f g
  in ∀ x y, phi (S i) x y = g i (phi i x y) x y.

First proofs of isPR statements

The module Alt presents proofs of lemmas already proven in primRec.v We just hope that such a redundancy will help the reader to get familiar with the various patterns allowed by that library.

Module Alt.

#[export] Instance zeroIsPR : isPR 0 0.

#[export] Instance succIsPR : isPR 1 S.

#[export] Instance addIsPR : isPR 2 Nat.add.

#[export] Instance pi2_5IsPR : isPR 5 (fun a b c d e ⇒ b).

Check composeFunc 0 1.

Remark compose_01 (x:PrimRec 0) (t : PrimRec 1) :
    PReval (PRcomp t [x ])%pr = PReval t (PReval x).

#[export] Instance const0_NIsPR n : isPR 0 n.
Search (isPR 2 (fun _ _ ⇒ nat_rec _ _ _ _)).

Check isPRextEqual.

Check filter010IsPR.

Definition add' x y :=
  nat_rec (fun n : nat ⇒ nat)
    y
    (fun z t ⇒ S t)
    x.

Lemma add'_ok:
  extEqual 2 add' Nat.add.

#[export] Instance addIsPR' : isPR 2 Nat.add.

Definition xpred := primRecFunc 0 zeroFunc pi1_2.

#[export] Instance predIsPR : isPR 1 Nat.pred.
End Alt.

Definition double (n:nat) := 2 × n.

#[export] Instance doubleIsPR : isPR 1 double.

using cPair

Section Exs.
Let f: naryFunc 2 := fun x y ⇒ x + pred (cPairPi1 y).

  Let ffib : naryFunc 2 :=
        fun c A ⇒
          match c with
            0 | 1 ⇒ 1
          | _ ⇒ codeNth 0 A + codeNth 1 A
          end.
  Let fdiv2 : naryFunc 2 :=
        fun (n acc: nat) ⇒
          match n with
            0 | 1 ⇒ 0
          | _ ⇒ S (codeNth 1 acc)
          end.

End Exs.