Library hydras.solutions_exercises.MorePRExamples

Require Import primRec Arith ArithRing List.
Import extEqualNat.

Definition double n := n × 2.

Lemma doubleIsPR : isPR 1 double.


Fixpoint exp n p :=
  match p with
    0 ⇒ 1
  | S m ⇒ exp n m × n
  end.


Definition exp_alt := fun a b ⇒ nat_rec (fun _ ⇒ nat)
                                     1
                                     (fun _ y ⇒ y × a)
                                     b.

Remark exp_alt_ok : extEqual 2 exp_alt exp.

#[local] Instance exp_alt_PR : isPR 2 exp_alt.

#[export] Instance expIsPR : isPR 2 exp.


Fixpoint tower2 n :=
  match n with
    0 ⇒ 1
  | S p ⇒ exp 2 (tower2 p)
  end.


Definition tower2_alt h : nat := nat_rec (fun n ⇒ nat)
                                1
                                (fun _ y ⇒ exp 2 y)
                                h.

Remark tower2_alt_ok : extEqual 1 tower2_alt tower2.

#[local] Instance tower2_alt_PR : isPR 1 tower2_alt.

#[export] Instance tower2IsPR : isPR 1 tower2.

Fixpoint fact n :=
  match n with 0 ⇒ 1
          | S p ⇒ n × fact p
  end.

Definition fact_alt
  : nat → nat :=
  fun a ⇒ nat_rec _ 1 (fun x y ⇒ S x × y) a.

Remark fact_alt_ok : extEqual 1 fact_alt fact.

#[local] Instance fact_altIsPR : isPR 1 fact_alt.

#[export] Instance factIsPR : isPR 1 fact.