Library hydras.solutions_exercises.MinPR

Prove that Stdlib's function min is primitive recursive

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

Section Proof_of_MinIsPR.

  Let min_alt (a b: nat) : nat :=
    (charFunction 2 leBool a b ) × a +
    (charFunction 2 ltBool b a ) × b.

  Lemma min_alt_correct : extEqual 2 min_alt Nat.min.

  #[local] Instance minPR_PR : isPR 2 min_alt.

  #[export] Instance minIsPR : isPR 2 Nat.min.

End Proof_of_MinIsPR.