Library hydras.solutions_exercises.MinPR2

Prove that Stdlib's function Min is primitive recursive this is a variant of the exercise MinPR

From hydras Require Import primRec extEqualNat.
From Coq Require Import ArithRing Lia Compare_dec.

Define an n-ary if-then-else

Fixpoint naryIf (n:nat) :
  naryRel n → naryFunc n → naryFunc n → naryFunc n
  :=
    match n return (naryRel n → naryFunc n → naryFunc n → naryFunc n) with
      0 ⇒ (fun b x y ⇒ if b then x else y)
    | S m ⇒ fun (p': naryRel (S m)) (g h: naryFunc (S m)) ⇒
               fun x ⇒ naryIf m (p' x) (g x) (h x)
    end.

#[export] Instance If2IsPR (p: naryRel 2)(f g : naryFunc 2):
  isPRrel 2 p → isPR 2 f → isPR 2 g →
  isPR 2 (naryIf 2 p f g).

Section Proof_of_MinIsPR.

  Let minPR : naryFunc 2 :=
    naryIf 2 leBool
           (fun x _ ⇒ x)
           (fun _ y ⇒ y).

  Lemma minPR_correct : extEqual 2 minPR PeanoNat.Nat.min.

  #[local] Instance minPR_PR : isPR 2 minPR.

  #[export] Instance minIsPR : isPR 2 min.

End Proof_of_MinIsPR.