From Coq Require Import Arith Peano_dec Compare_dec List Eqdep_dec Utf8.
From hydras Require Import extEqualNat misc Compat815.
From Coq Require Vector Bool EqNat.
From Coq Require Import Lia.

Inductive PrimRec : nat → Set :=
  | succFunc : PrimRec 1
  | zeroFunc : PrimRec 0
  | projFunc : ∀ n m : nat, m < n → PrimRec n
  | composeFunc :
      ∀ (n m : nat) (g : PrimRecs n m) (h : PrimRec m),
        PrimRec n
  | primRecFunc :
      ∀ (n : nat) (g : PrimRec n) (h : PrimRec (S (S n))),
        PrimRec (S n)
with PrimRecs : nat → nat → Set :=
  | PRnil : ∀ n : nat, PrimRecs n 0
  | PRcons : ∀ n m : nat, PrimRec n → PrimRecs n m →
                               PrimRecs n (S m).


  Notation "f '=x=' g" := (extEqual _ f g) (at level 70, no associativity).


  Module PRNotations.
    Declare Scope pr_scope.
    Delimit Scope pr_scope with pr.
    Notation "h :: t" := (PRcons _ _ h t) (at level 60, right associativity)
        : pr_scope.
    Notation "[ x ]" := (PRcons _ _ x (PRnil _)) : pr_scope.

    Notation "[ x ; y ; .. ; z ]" :=
      (PRcons _ _ x (PRcons _ _ y .. (PRcons _ _ z (PRnil _)) ..)) : pr_scope.

    Notation PRcomp f v := (composeFunc _ _ v f).

    Notation PRrec f0 fS := (primRecFunc _ f0 fS).

    Notation pi1_1 := (projFunc 1 0 (le_n 1)).

    Notation pi1_2 := (projFunc 2 1 (le_n 2)).
    Notation pi2_2 := (projFunc 2 0 (le_S 1 1 (le_n 1))).

    Notation pi1_3 := (projFunc 3 2 (le_n 3)).
    Notation pi2_3 := (projFunc 3 1 (le_S 2 2 (le_n 2))).
    Notation pi3_3 := (projFunc 3 0 (le_S 1 2 (le_S 1 1 (le_n 1)))).

  End PRNotations.


Import PRNotations.

Scheme PrimRec_PrimRecs_rec := Induction for PrimRec Sort Set
  with PrimRecs_PrimRec_rec := Induction for PrimRecs Sort Set.

Arguments PrimRec_PrimRecs_rec P P0 : rename.
Arguments PrimRecs_PrimRec_rec P P0 : rename.


Scheme PrimRec_PrimRecs_ind := Induction for PrimRec Sort Prop
    with PrimRecs_PrimRec_ind := Induction for PrimRecs Sort Prop.

Arguments PrimRec_PrimRecs_ind P P0 : rename.
Arguments PrimRecs_PrimRec_ind P P0 : rename.

Check PrimRec_PrimRecs_ind.

Fixpoint evalConstFunc (n m : nat) {struct n} : naryFunc n :=
  match n return (naryFunc n) with
  | O ⇒ m
  | S n' ⇒ fun _ ⇒ evalConstFunc n' m
  end.

Fixpoint evalProjFunc (n : nat) :
  ∀ m : nat, m < n → naryFunc n :=
  match n return (∀ m : nat, m < n → naryFunc n) with
  | O ⇒ fun (m : nat) (l : m < 0) ⇒ False_rec _ (Nat.nlt_0_r _ l)
  | S n' ⇒
      fun (m : nat) (l : m < S n') ⇒
      match eq_nat_dec m n' with
      | left _ ⇒ fun a : nat ⇒ evalConstFunc _ a
      | right l1 ⇒
          fun _ ⇒
          evalProjFunc n' m
            match Compat815.le_lt_or_eq _ _
                    (Compat815.lt_n_Sm_le _ _ l) with
            | or_introl l2 ⇒ l2
            | or_intror l2 ⇒ False_ind _ (l1 l2)
            end
      end
  end.

Lemma evalProjFuncInd :
 ∀ (n m : nat) (p1 p2 : m < n),
 evalProjFunc n m p1 = evalProjFunc n m p2.

Fixpoint evalList (m : nat) (l : Vector.t nat m) {struct l} :
  naryFunc m → nat :=
  match l in (Vector.t _ m) return (naryFunc m → nat) with
  | Vector.nil ⇒ fun x : naryFunc 0 ⇒ x
  | Vector.cons a n l' ⇒
    fun x : naryFunc (S n) ⇒ evalList n l' (x a)
  end.


Fixpoint evalOneParamList (n m a : nat) (l : Vector.t (naryFunc (S n)) m)
 {struct l} : Vector.t (naryFunc n) m :=
  match l in (Vector.t _ m) return (Vector.t (naryFunc n) m) with
  | Vector.nil ⇒ Vector.nil (naryFunc n)
  | Vector.cons f m' l' ⇒
      Vector.cons _ (f a) m' (evalOneParamList n m' a l')
  end.

Fixpoint evalComposeFunc (n : nat) :
  ∀ m : nat,
    Vector.t (naryFunc n) m → naryFunc m → naryFunc n :=
  match
    n
    return
    (∀ m : nat,
        Vector.t (naryFunc n) m → naryFunc m → naryFunc n)
  with
  | O ⇒ evalList
  | S n' ⇒
      fun (m : nat) (l : Vector.t (naryFunc (S n')) m)
          (f : naryFunc m) (a : nat) ⇒
        evalComposeFunc n' m (evalOneParamList _ _ a l) f
  end.

Fixpoint compose2 (n : nat) :
  naryFunc n → naryFunc (S n) → naryFunc n :=
  match n return (naryFunc n → naryFunc (S n) → naryFunc n) with
  | O ⇒ fun (a : nat) (g : nat → nat) ⇒ g a
  | S n' ⇒
      fun (f : naryFunc (S n')) (g : naryFunc (S (S n'))) (a : nat) ⇒
        compose2 n' (f a) (fun x : nat ⇒ g x a)
  end.

Fixpoint evalPrimRecFunc (n : nat) (g : naryFunc n)
 (h : naryFunc (S (S n))) (a : nat) {struct a} : naryFunc n :=
  match a with
  | O ⇒ g
  | S a' ⇒ compose2 _ (evalPrimRecFunc n g h a') (h a')
  end.

Fixpoint evalPrimRec (n : nat) (f : PrimRec n) {struct f} :
 naryFunc n :=
  match f in (PrimRec n) return (naryFunc n) with
  | succFunc ⇒ S
  | zeroFunc ⇒ 0
  | projFunc n m pf ⇒ evalProjFunc n m pf
  | composeFunc n m l f ⇒
      evalComposeFunc n m (evalPrimRecs _ _ l) (evalPrimRec _ f)
  | primRecFunc n g h ⇒
      evalPrimRecFunc n (evalPrimRec _ g) (evalPrimRec _ h)
  end
 
 with evalPrimRecs (n m : nat) (fs : PrimRecs n m) {struct fs} :
 Vector.t (naryFunc n) m :=
  match fs in (PrimRecs n m) return (Vector.t (naryFunc n) m) with
  | PRnil a ⇒ Vector.nil (naryFunc a)
  | PRcons a b g gs ⇒
    Vector.cons _ (evalPrimRec _ g) _ (evalPrimRecs _ _ gs)
  end.

Notation PReval f := (evalPrimRec _ f).
Notation PRevalN fs := (evalPrimRecs _ _ fs).

Definition PRcorrect {n:nat}(p:PrimRec n)(f: naryFunc n) :=
  PReval p =x= f.


Definition extEqualVectorGeneral (n m : nat) (l : Vector.t (naryFunc n) m) :
  ∀ (m' : nat) (l' : Vector.t (naryFunc n) m'), Prop.
Defined.

Definition extEqualVector n:
  ∀ m (l l' : Vector.t (naryFunc n) m), Prop.

Lemma extEqualVectorRefl (n m: nat):
  ∀ (l : Vector.t (naryFunc n) m), extEqualVector n m l l.

Lemma extEqualOneParamList :
  ∀ (n m : nat) (l1 l2 : Vector.t (naryFunc (S n)) m) (c : nat),
    extEqualVector (S n) m l1 l2 →
    extEqualVector n m (evalOneParamList n m c l1)
      (evalOneParamList n m c l2).

Lemma extEqualCompose :
  ∀ (n m : nat) (l1 l2 : Vector.t (naryFunc n) m)
         (f1 f2 : naryFunc m),
    extEqualVector n m l1 l2 →
    f1 =x= f2 →
    evalComposeFunc n m l1 f1 =x= evalComposeFunc n m l2 f2.

Lemma extEqualCompose2 :
  ∀ (n : nat) (f1 f2 : naryFunc n),
     f1 =x= f2 →
    ∀ g1 g2 : naryFunc (S n),
       g1 =x= g2 →
       compose2 n f1 g1 =x= compose2 n f2 g2.

Lemma extEqualPrimRec :
  ∀ (n : nat) (g1 g2 : naryFunc n) (h1 h2 : naryFunc (S (S n))),
     g1 =x= g2 → h1 =x= h2 →
       (evalPrimRecFunc n g1 h1: naryFunc (S n)) =x=
         evalPrimRecFunc n g2 h2.

Class isPR (n : nat) (f : naryFunc n) : Set :=
  is_pr : {p : PrimRec n | extEqual n (PReval p) f}.

Definition fun2PR {n:nat}(f: naryFunc n)
  {p: isPR _ f}: PrimRec n := proj1_sig p.

Class isPRrel (n : nat) (R : naryRel n) : Set :=
  is_pr_rel: isPR n (charFunction n R).

#[export] Instance succIsPR : isPR 1 S.

#[export] Instance const0_NIsPR (n:nat): isPR 0 n.

#[export] Instance const1_NIsPR n: isPR 1 (fun _ ⇒ n).

#[export] Instance idIsPR : isPR 1 (fun x : nat ⇒ x).

#[export] Instance pi1_2IsPR : isPR 2 (fun a b : nat ⇒ a).

#[export] Instance pi2_2IsPR : isPR 2 (fun a b : nat ⇒ b).

#[export] Instance pi1_3IsPR : isPR 3 (fun a b c : nat ⇒ a).

#[export] Instance pi2_3IsPR : isPR 3 (fun a b c : nat ⇒ b).

#[export] Instance pi3_3IsPR : isPR 3 (fun a b c : nat ⇒ c).

#[export] Instance pi1_4IsPR : isPR 4 (fun a b c d : nat ⇒ a).

#[export] Instance pi2_4IsPR : isPR 4 (fun a b c d : nat ⇒ b).

#[export] Instance pi3_4IsPR : isPR 4 (fun a b c d : nat ⇒ c).

#[export] Instance pi4_4IsPR : isPR 4 (fun a b c d : nat ⇒ d).

#[export] Instance filter01IsPR (g : nat → nat) (H : isPR 1 g):
  isPR 2 (fun a b : nat ⇒ g b).

#[export] Instance filter10IsPR (g : nat → nat) (H: isPR 1 g):
  isPR 2 (fun a b : nat ⇒ g a).

#[export] Instance filter100IsPR(g : nat → nat)(H: isPR 1 g) :
  isPR 3 (fun a b c : nat ⇒ g a).

#[export] Instance filter010IsPR (g : nat → nat)(H: isPR 1 g):
  isPR 3 (fun a b c : nat ⇒ g b).

#[export] Instance filter001IsPR (g:nat → nat)(H: isPR 1 g) :
 isPR 3 (fun a b c : nat ⇒ g c).

#[export] Instance filter011IsPR (g: nat → nat → nat)(H: isPR 2 g):
   isPR 3 (fun a b c : nat ⇒ g b c).

#[export] Instance filter110IsPR(g : nat → nat → nat) :
  isPR 2 g → isPR 3 (fun a b c : nat ⇒ g a b).

#[export] Instance filter101IsPR :
  ∀ g : nat → nat → nat, isPR 2 g →
                                isPR 3 (fun a b c : nat ⇒ g a c).

#[export] Instance filter0011IsPR (g : nat → nat → nat) :
  isPR 2 g → isPR 4 (fun a b c d : nat ⇒ g c d).

#[export] Instance filter1000IsPR (g : nat → nat):
  isPR 1 g → isPR 4 (fun a b c d : nat ⇒ g a).

#[export] Instance filter1011IsPR (g : nat → nat → nat → nat) :
 isPR 3 g → isPR 4 (fun a b c d : nat ⇒ g a c d).

#[export] Instance filter1100IsPR (g : nat → nat → nat) :
  isPR 2 g → isPR 4 (fun a b c d : nat ⇒ g a b).

#[export] Instance compose1_1IsPR (f : nat → nat):
  isPR 1 f →
  ∀ g : nat → nat, isPR 1 g → isPR 1 (fun x : nat ⇒ g (f x)).

#[export] Instance compose1_2IsPR :
  ∀ f : nat → nat,
    isPR 1 f →
    ∀ f' : nat → nat,
      isPR 1 f' →
      ∀ g : nat → nat → nat,
        isPR 2 g → isPR 1 (fun x : nat ⇒ g (f x) (f' x)).

#[export] Instance compose1_3IsPR :
 ∀ f1 : nat → nat,
 isPR 1 f1 →
 ∀ f2 : nat → nat,
 isPR 1 f2 →
 ∀ f3 : nat → nat,
 isPR 1 f3 →
 ∀ g : nat → nat → nat → nat,
 isPR 3 g → isPR 1 (fun x : nat ⇒ g (f1 x) (f2 x) (f3 x)).

#[export] Instance compose2_1IsPR :
  ∀ f : nat → nat → nat,
    isPR 2 f →
    ∀ g : nat → nat, isPR 1 g →
                           isPR 2 (fun x y : nat ⇒ g (f x y)).

#[export] Instance compose2_2IsPR :
 ∀ f : nat → nat → nat,
 isPR 2 f →
 ∀ g : nat → nat → nat,
 isPR 2 g →
 ∀ h : nat → nat → nat,
 isPR 2 h → isPR 2 (fun x y : nat ⇒ h (f x y) (g x y)).

#[export] Instance compose2_3IsPR :
  ∀ f1 : nat → nat → nat,
    isPR 2 f1 →
    ∀ f2 : nat → nat → nat,
      isPR 2 f2 →
      ∀ f3 : nat → nat → nat,
        isPR 2 f3 →
        ∀ g : nat → nat → nat → nat,
          isPR 3 g →
          isPR 2 (fun x y : nat ⇒ g (f1 x y) (f2 x y) (f3 x y)).

#[export] Instance compose2_4IsPR :
 ∀ f1 : nat → nat → nat,
 isPR 2 f1 →
 ∀ f2 : nat → nat → nat,
 isPR 2 f2 →
 ∀ f3 : nat → nat → nat,
 isPR 2 f3 →
 ∀ f4 : nat → nat → nat,
 isPR 2 f4 →
 ∀ g : nat → nat → nat → nat → nat,
 isPR 4 g →
 isPR 2 (fun x y : nat ⇒ g (f1 x y) (f2 x y) (f3 x y) (f4 x y)).

#[export] Instance compose3_1IsPR :
  ∀ f : nat → nat → nat → nat,
    isPR 3 f →
    ∀ g : nat → nat, isPR 1 g →
                           isPR 3 (fun x y z : nat ⇒ g (f x y z)).

#[export] Instance compose3_2IsPR :
  ∀ f1 : nat → nat → nat → nat,
    isPR 3 f1 →
    ∀ f2 : nat → nat → nat → nat,
      isPR 3 f2 →
      ∀ g : nat → nat → nat,
        isPR 2 g → isPR 3 (fun x y z : nat ⇒ g (f1 x y z) (f2 x y z)).

#[export] Instance compose3_3IsPR :
 ∀ f1 : nat → nat → nat → nat,
 isPR 3 f1 →
 ∀ f2 : nat → nat → nat → nat,
 isPR 3 f2 →
 ∀ f3 : nat → nat → nat → nat,
 isPR 3 f3 →
 ∀ g : nat → nat → nat → nat,
 isPR 3 g → isPR 3 (fun x y z : nat ⇒ g (f1 x y z) (f2 x y z) (f3 x y z)).

#[export] Instance compose4_2IsPR :
 ∀ f1 : nat → nat → nat → nat → nat,
 isPR 4 f1 →
 ∀ f2 : nat → nat → nat → nat → nat,
 isPR 4 f2 →
 ∀ g : nat → nat → nat,
 isPR 2 g → isPR 4 (fun w x y z : nat ⇒ g (f1 w x y z) (f2 w x y z)).

#[export] Instance compose4_3IsPR :
 ∀ f1 : nat → nat → nat → nat → nat,
 isPR 4 f1 →
 ∀ f2 : nat → nat → nat → nat → nat,
 isPR 4 f2 →
 ∀ f3 : nat → nat → nat → nat → nat,
 isPR 4 f3 →
 ∀ g : nat → nat → nat → nat,
 isPR 3 g →
 isPR 4 (fun w x y z : nat ⇒ g (f1 w x y z) (f2 w x y z) (f3 w x y z)).

#[export] Instance swapIsPR :
  ∀ f : nat → nat → nat, isPR 2 f → isPR 2 (fun x y : nat ⇒ f y x).

#[export] Instance indIsPR :
  ∀ f : nat → nat → nat,
    isPR 2 f →
    ∀ g : nat,
      isPR 1
           (fun a : nat ⇒ nat_rec (fun _ : nat ⇒ nat) g
                             (fun x y : nat ⇒ f x y) a).

#[export] Instance ind1ParamIsPR :
  ∀ f : nat → nat → nat → nat,
    isPR 3 f →
    ∀ g : nat → nat,
      isPR 1 g →
      isPR 2
           (fun a b : nat ⇒
              nat_rec (fun n : nat ⇒ nat) (g b) (fun x y : nat ⇒ f x y b) a).

#[export] Instance ind2ParamIsPR :
  ∀ f : nat → nat → nat → nat → nat,
    isPR 4 f →
    ∀ g : nat → nat → nat,
      isPR 2 g →
      isPR 3
        (fun a b c : nat ⇒
           nat_rec (fun n : nat ⇒ nat) (g b c) (fun x y : nat ⇒ f x y b c) a).

#[export] Instance plusIndIsPR : isPR 3 (fun n fn b : nat ⇒ S fn).

#[export] Instance plusIsPR : isPR 2 plus.

#[export] Instance multIndIsPR : isPR 3 (fun n fn b : nat ⇒ fn + b).

#[export] Instance multIsPR : isPR 2 mult.

#[export] Instance predIsPR : isPR 1 pred.

#[export] Instance minusIndIsPR : isPR 3 (fun n fn b : nat ⇒ pred fn).

#[export] Instance minusIsPR : isPR 2 minus.

Definition notZero (a : nat) :=
  nat_rec (fun n : nat ⇒ nat) 0 (fun x y : nat ⇒ 1) a.

#[export] Instance notZeroIsPR : isPR 1 notZero.

Definition ltBool (a b : nat) : bool :=
  if le_lt_dec b a then false else true.

Lemma ltBoolTrue : ∀ a b : nat, ltBool a b = true → a < b.

Lemma ltBoolFalse : ∀ a b : nat, ltBool a b = false → ¬ a < b.

#[export] Instance ltIsPR : isPRrel 2 ltBool.

#[export] Instance maxIsPR : isPR 2 max.

#[export] Instance gtIsPR : isPRrel 2 (fun a b : nat ⇒ ltBool b a).

Remark replaceCompose2 :
 ∀ (n : nat) (a b a' b' : naryFunc n) (c c' : naryFunc 2),
 extEqual n a a' →
 extEqual n b b' →
 extEqual 2 c c' →
 extEqual
   n
   (evalComposeFunc _ _
                    (Vector.cons _ a _
                                 (Vector.cons _ b _
                                              (Vector.nil (naryFunc n)))) c)
   (evalComposeFunc _ _
                    (Vector.cons _ a' _
                                 (Vector.cons _ b' _
                                              (Vector.nil (naryFunc n)))) c').

Definition orRel (n : nat) (R S : naryRel n) : naryRel n.

Lemma orRelPR :
  ∀ (n : nat) (R R' : naryRel n),
    isPRrel n R → isPRrel n R' → isPRrel n (orRel n R R').

Definition andRel (n : nat) (R S : naryRel n) : naryRel n.

Lemma andRelPR :
  ∀ (n : nat) (R R' : naryRel n),
    isPRrel n R → isPRrel n R' → isPRrel n (andRel n R R').

Definition notRel (n : nat) (R : naryRel n) : naryRel n.

Lemma notRelPR (n : nat) (R : naryRel n):
  isPRrel n R → isPRrel n (notRel n R).

Fixpoint bodd (n : nat) : bool :=
  match n with
  | O ⇒ false
  | S n' ⇒ negb (bodd n')
  end.

#[export] Instance boddIsPR : isPRrel 1 bodd.

Lemma nat_eqb_false (a b: nat) : a ≠ b → Nat.eqb a b = false.

#[local] Instance neqIsPR : isPRrel 2 (fun a b : nat ⇒ negb (Nat.eqb a b)).

#[export] Instance eqIsPR : isPRrel 2 Nat.eqb.

Definition leBool (a b : nat) : bool :=
  if le_lt_dec a b then true else false.

#[export] Instance leIsPR : isPRrel 2 leBool.

Section Ignore_Params.

  Fixpoint ignoreParams (n m : nat) (f : naryFunc n) {struct m} :
    naryFunc (m + n) :=
    match m return (naryFunc (m + n)) with
    | O ⇒ f
    | S x ⇒ fun _ ⇒ ignoreParams n x f
    end.

  Definition projectionListPR (n m : nat) (p : m ≤ n) : PrimRecs n m.

  Definition projectionList (n m : nat) (p : m ≤ n) :
    Vector.t (naryFunc n) m := evalPrimRecs n m (projectionListPR n m p).

  Lemma projectionListInd :
    ∀ (n m : nat) (p1 p2 : m ≤ n),
      projectionList n m p1 = projectionList n m p2.

  Lemma projectionListApplyParam :
    ∀ (m n c : nat) (p1 : m ≤ n) (p2 : m ≤ S n),
      extEqualVector _ _ (projectionList n m p1)
                     (evalOneParamList n m c (projectionList (S n) m p2)).

  Lemma projectionListId :
    ∀ (n : nat) (f : naryFunc n) (p : n ≤ n),
      extEqual n f (evalComposeFunc n n (projectionList n n p) f).

  #[export] Instance ignoreParamsIsPR :
    ∀ (n m : nat) (f : naryFunc n),
      isPR _ f → isPR _ (ignoreParams n m f).

End Ignore_Params.

Lemma reduce1stCompose :
  ∀ (c n m : nat) (v : Vector.t (naryFunc n) m) (g : naryFunc (S m)),
    extEqual n
      (evalComposeFunc n _ (Vector.cons (naryFunc n)
                              (evalConstFunc n c) _ v) g)
      (evalComposeFunc n _ v (g c)).

Lemma reduce2ndCompose :
  ∀ (c n m : nat) (v : Vector.t (naryFunc n) m) (n0 : naryFunc n)
         (g : naryFunc (S (S m))),
    extEqual n
      (evalComposeFunc n _
         (Vector.cons
            (naryFunc n) n0 _
            (Vector.cons (naryFunc n)
               (evalConstFunc n c) _ v))
         g)
      (evalComposeFunc n _ (Vector.cons (naryFunc n) n0 _ v)
         (fun x : nat ⇒ g x c)).

Lemma evalPrimRecParam :
  ∀ (n c d : nat) (g : naryFunc (S n)) (h : naryFunc (S (S (S n)))),
     evalPrimRecFunc n (g d) (fun x y : nat ⇒ h x y d) c =x=
      evalPrimRecFunc (S n) g h c d.

#[export] Instance compose2IsPR :
  ∀ (n : nat) (f : naryFunc n) (p : isPR n f) (g : naryFunc (S n))
         (q : isPR (S n) g), isPR n (compose2 n f g).

#[export] Instance compose1_NIsPR :
  ∀ (n : nat) (g : naryFunc (S n)),
    isPR (S n) g →
    ∀ f : naryFunc 1, isPR 1 f →
                           isPR (S n) (fun x : nat ⇒ g (f x)).

Definition switchPR : naryFunc 3 :=
  fun n x y ⇒ match n with 0 ⇒ y | _ ⇒ x end.

#[export] Instance switchIsPR : isPR 3 switchPR.

Fixpoint boundedSearchHelp (P : naryRel 1) (b : nat) {struct b} : nat :=
  match b with
  | O ⇒ 0
  | S b' ⇒ let q := boundedSearchHelp P b'
            in
      match eq_nat_dec q b' with
      | left _ ⇒ match P b' with
                  | true ⇒ b'
                  | false ⇒ S b'
                  end
      | right _ ⇒ q
      end
  end.

Definition boundedSearch (P : naryRel 2) (b : nat) : nat :=
  boundedSearchHelp (P b) b.

Module Examples.

  Definition sqrtHelp (n: nat) :=
    boundedSearch (fun _ x ⇒ Nat.eqb (x × x) n) (S (n / 2)).

  Definition exact_sqrt (n: nat) :=
    let q := sqrtHelp n
    in if Nat.eqb (q × q) n then Some q else None.


  End Examples.

  Lemma boundedSearch1 :
    ∀ (P : naryRel 2) (b x : nat), x < boundedSearch P b →
                                        P b x = false.

Lemma boundedSearch2 :
  ∀ (P : naryRel 2) (b : nat),
    boundedSearch P b = b ∨ P b (boundedSearch P b) = true.

#[export] Instance boundSearchIsPR :
  ∀ P : naryRel 2,
    isPRrel 2 P → isPR 1 (boundedSearch P).

Definition iterate (g : nat → nat) :=
  nat_rec (fun _ ⇒ nat → nat) (fun x : nat ⇒ x)
          (fun (_ : nat) (rec : nat → nat) (x : nat) ⇒ g (rec x)).

#[export] Instance iterateIsPR :
  ∀ g : nat → nat, isPR 1 g →
                         ∀ n : nat, isPR 1 (iterate g n).

#[export] Instance isPRTrans (n:nat) (f g : naryFunc n):
  f =x= g → isPR n f → isPR n g.

#[export] Instance isPRextEqual (n:nat) (f g : naryFunc n):
  isPR n f → f =x= g → isPR n g.