Library pairing.primRec
This code is part of Russell O'Connor's formalisation of Goedel's
Incompleteness Theorem in Coq, released into the Public Domain.
http://r6.ca/Goedel/goedel1.html
http://r6.ca/Goedel/goedel1.html
Require Import Arith.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Coq.Lists.List.
Require Import Eqdep_dec.
Require Import extEqualNat.
Require Import Bvector.
Require Import misc.
Require Export Bool.
Require Export EqNat.
Require Import Even.
Require Import Max.
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).
Scheme PrimRec_PrimRecs_rec := Induction for PrimRec
Sort Set
with PrimRecs_PrimRec_rec := Induction for PrimRecs
Sort Set.
Scheme PrimRec_PrimRecs_ind := Induction for PrimRec
Sort Prop
with PrimRecs_PrimRec_ind := Induction for PrimRecs
Sort Prop.
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 _ (lt_n_O _ 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 le_lt_or_eq _ _ (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 nat m) {struct l} :
naryFunc m → nat :=
match l in (vector _ m) return (naryFunc m → nat) with
| Vnil ⇒ fun x : naryFunc 0 ⇒ x
| Vcons a n l' ⇒ fun x : naryFunc (S n) ⇒ evalList n l' (x a)
end.
Fixpoint evalOneParamList (n m a : nat) (l : vector (naryFunc (S n)) m)
{struct l} : vector (naryFunc n) m :=
match l in (vector _ m) return (vector (naryFunc n) m) with
| Vnil ⇒ Vnil (naryFunc n)
| Vcons f m' l' ⇒ Vcons _ (f a) m' (evalOneParamList n m' a l')
end.
Fixpoint evalComposeFunc (n : nat) :
∀ m : nat, vector (naryFunc n) m → naryFunc m → naryFunc n :=
match
n
return
(∀ m : nat, vector (naryFunc n) m → naryFunc m → naryFunc n)
with
| O ⇒ evalList
| S n' ⇒
fun (m : nat) (l : vector (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 (naryFunc n) m :=
match fs in (PrimRecs n m) return (vector (naryFunc n) m) with
| PRnil a ⇒ Vnil (naryFunc a)
| PRcons a b g gs ⇒ Vcons _ (evalPrimRec _ g) _ (evalPrimRecs _ _ gs)
end.
Definition extEqualVectorGeneral (n m : nat) (l : vector (naryFunc n) m)
(m' : nat) (l' : vector (naryFunc n) m') : Prop.
Defined.
Definition extEqualVector (n m : nat) (l l' : vector (naryFunc n) m) : Prop.
Defined.
Lemma extEqualVectorRefl :
∀ (n m : nat) (l : vector (naryFunc n) m), extEqualVector n m l l.
Lemma extEqualOneParamList :
∀ (n m : nat) (l1 l2 : vector (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 (naryFunc n) m) (f1 f2 : naryFunc m),
extEqualVector n m l1 l2 →
extEqual m f1 f2 →
extEqual n (evalComposeFunc n m l1 f1) (evalComposeFunc n m l2 f2).
Lemma extEqualCompose2 :
∀ (n : nat) (f1 f2 : naryFunc n),
extEqual n f1 f2 →
∀ g1 g2 : naryFunc (S n),
extEqual (S n) g1 g2 → extEqual n (compose2 n f1 g1) (compose2 n f2 g2).
Lemma extEqualPrimRec :
∀ (n : nat) (g1 g2 : naryFunc n) (h1 h2 : naryFunc (S (S n))),
extEqual n g1 g2 →
extEqual (S (S n)) h1 h2 →
extEqual (S n) (evalPrimRecFunc n g1 h1) (evalPrimRecFunc n g2 h2).
Definition isPR (n : nat) (f : naryFunc n) : Set :=
{p : PrimRec n | extEqual n (evalPrimRec _ p) f}.
Definition isPRrel (n : nat) (R : naryRel n) : Set :=
isPR n (charFunction n R).
Lemma succIsPR : isPR 1 S.
Lemma const0_NIsPR : ∀ n : nat, isPR 0 n.
Lemma const1_NIsPR : ∀ n : nat, isPR 1 (fun _ ⇒ n).
Lemma idIsPR : isPR 1 (fun x : nat ⇒ x).
Lemma pi1_2IsPR : isPR 2 (fun a b : nat ⇒ a).
Lemma pi2_2IsPR : isPR 2 (fun a b : nat ⇒ b).
Lemma pi1_3IsPR : isPR 3 (fun a b c : nat ⇒ a).
Lemma pi2_3IsPR : isPR 3 (fun a b c : nat ⇒ b).
Lemma pi3_3IsPR : isPR 3 (fun a b c : nat ⇒ c).
Lemma pi1_4IsPR : isPR 4 (fun a b c d : nat ⇒ a).
Lemma pi2_4IsPR : isPR 4 (fun a b c d : nat ⇒ b).
Lemma pi3_4IsPR : isPR 4 (fun a b c d : nat ⇒ c).
Lemma pi4_4IsPR : isPR 4 (fun a b c d : nat ⇒ d).
Lemma filter01IsPR :
∀ g : nat → nat, isPR 1 g → isPR 2 (fun a b : nat ⇒ g b).
Lemma filter10IsPR :
∀ g : nat → nat, isPR 1 g → isPR 2 (fun a b : nat ⇒ g a).
Lemma filter100IsPR :
∀ g : nat → nat, isPR 1 g → isPR 3 (fun a b c : nat ⇒ g a).
Lemma filter010IsPR :
∀ g : nat → nat, isPR 1 g → isPR 3 (fun a b c : nat ⇒ g b).
Lemma filter001IsPR :
∀ g : nat → nat, isPR 1 g → isPR 3 (fun a b c : nat ⇒ g c).
Lemma filter011IsPR :
∀ g : nat → nat → nat, isPR 2 g → isPR 3 (fun a b c : nat ⇒ g b c).
Lemma filter110IsPR :
∀ g : nat → nat → nat, isPR 2 g → isPR 3 (fun a b c : nat ⇒ g a b).
Lemma filter101IsPR :
∀ g : nat → nat → nat, isPR 2 g → isPR 3 (fun a b c : nat ⇒ g a c).
Lemma filter0011IsPR :
∀ g : nat → nat → nat,
isPR 2 g → isPR 4 (fun a b c d : nat ⇒ g c d).
Lemma filter1000IsPR :
∀ g : nat → nat, isPR 1 g → isPR 4 (fun a b c d : nat ⇒ g a).
Lemma filter1011IsPR :
∀ g : nat → nat → nat → nat,
isPR 3 g → isPR 4 (fun a b c d : nat ⇒ g a c d).
Lemma filter1100IsPR :
∀ g : nat → nat → nat,
isPR 2 g → isPR 4 (fun a b c d : nat ⇒ g a b).
Lemma compose1_1IsPR :
∀ f : nat → nat,
isPR 1 f →
∀ g : nat → nat, isPR 1 g → isPR 1 (fun x : nat ⇒ g (f x)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma swapIsPR :
∀ f : nat → nat → nat, isPR 2 f → isPR 2 (fun x y : nat ⇒ f y x).
Lemma indIsPR :
∀ f : nat → nat → nat,
isPR 2 f →
∀ g : nat,
isPR 1
(fun a : nat ⇒ nat_rec (fun n : nat ⇒ nat) g (fun x y : nat ⇒ f x y) a).
Lemma 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).
Lemma 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).
Lemma plusIndIsPR : isPR 3 (fun n fn b : nat ⇒ S fn).
Lemma plusIsPR : isPR 2 plus.
Lemma multIndIsPR : isPR 3 (fun n fn b : nat ⇒ fn + b).
Lemma multIsPR : isPR 2 mult.
Lemma predIsPR : isPR 1 pred.
Lemma minusIndIsPR : isPR 3 (fun n fn b : nat ⇒ pred fn).
Lemma minusIsPR : isPR 2 minus.
Definition notZero (a : nat) :=
nat_rec (fun n : nat ⇒ nat) 0 (fun x y : nat ⇒ 1) a.
Lemma notZeroIsPR : isPR 1 notZero.
Definition ltBool (a b : nat) : bool.
Defined.
Lemma ltBoolTrue : ∀ a b : nat, ltBool a b = true → a < b.
Lemma ltBoolFalse : ∀ a b : nat, ltBool a b = false → ¬ a < b.
Lemma ltIsPR : isPRrel 2 ltBool.
Lemma maxIsPR : isPR 2 max.
Lemma 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 _ _ (Vcons _ a _ (Vcons _ b _ (Vnil (naryFunc n)))) c)
(evalComposeFunc _ _ (Vcons _ a' _ (Vcons _ b' _ (Vnil (naryFunc n)))) c').
Definition orRel (n : nat) (R S : naryRel n) : naryRel n.
Defined.
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.
Defined.
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.
Defined.
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.
Lemma boddIsPR : isPRrel 1 bodd.
Lemma beq_nat_not_refl : ∀ a b : nat, a ≠ b → beq_nat a b = false.
Lemma neqIsPR : isPRrel 2 (fun a b : nat ⇒ negb (beq_nat a b)).
Lemma eqIsPR : isPRrel 2 beq_nat.
Definition leBool (a b : nat) : bool.
Defined.
Lemma 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.
Defined.
Definition projectionList (n m : nat) (p : m ≤ n) :
vector (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).
Lemma 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 (naryFunc n) m) (g : naryFunc (S m)),
extEqual n
(evalComposeFunc n _ (Vcons (naryFunc n) (evalConstFunc n c) _ v) g)
(evalComposeFunc n _ v (g c)).
Lemma reduce2ndCompose :
∀ (c n m : nat) (v : vector (naryFunc n) m) (n0 : naryFunc n)
(g : naryFunc (S (S m))),
extEqual n
(evalComposeFunc n _
(Vcons (naryFunc n) n0 _ (Vcons (naryFunc n) (evalConstFunc n c) _ v))
g)
(evalComposeFunc n _ (Vcons (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)))),
extEqual _ (evalPrimRecFunc n (g d) (fun x y : nat ⇒ h x y d) c)
(evalPrimRecFunc (S n) g h c d).
Lemma 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).
Lemma 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.
Defined.
Lemma switchIsPR : isPR 3 switchPR.
Fixpoint boundedSearchHelp (P : naryRel 1) (b : nat) {struct b} : nat :=
match b with
| O ⇒ 0
| S b' ⇒
match eq_nat_dec (boundedSearchHelp P b') b' with
| left _ ⇒ match P b' with
| true ⇒ b'
| false ⇒ S b'
end
| right _ ⇒ boundedSearchHelp P b'
end
end.
Definition boundedSearch (P : naryRel 2) (b : nat) : nat :=
boundedSearchHelp (P b) b.
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.
Lemma boundSearchIsPR :
∀ P : naryRel 2,
isPRrel 2 P → isPR 1 (fun b : nat ⇒ boundedSearch P b).
Definition iterate (g : nat → nat) :=
nat_rec (fun _ ⇒ nat → nat) (fun x : nat ⇒ x)
(fun (_ : nat) (rec : nat → nat) (x : nat) ⇒ g (rec x)).
Lemma iterateIsPR :
∀ g : nat → nat, isPR 1 g → ∀ n : nat, isPR 1 (iterate g n).
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Coq.Lists.List.
Require Import Eqdep_dec.
Require Import extEqualNat.
Require Import Bvector.
Require Import misc.
Require Export Bool.
Require Export EqNat.
Require Import Even.
Require Import Max.
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).
Scheme PrimRec_PrimRecs_rec := Induction for PrimRec
Sort Set
with PrimRecs_PrimRec_rec := Induction for PrimRecs
Sort Set.
Scheme PrimRec_PrimRecs_ind := Induction for PrimRec
Sort Prop
with PrimRecs_PrimRec_ind := Induction for PrimRecs
Sort Prop.
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 _ (lt_n_O _ 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 le_lt_or_eq _ _ (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 nat m) {struct l} :
naryFunc m → nat :=
match l in (vector _ m) return (naryFunc m → nat) with
| Vnil ⇒ fun x : naryFunc 0 ⇒ x
| Vcons a n l' ⇒ fun x : naryFunc (S n) ⇒ evalList n l' (x a)
end.
Fixpoint evalOneParamList (n m a : nat) (l : vector (naryFunc (S n)) m)
{struct l} : vector (naryFunc n) m :=
match l in (vector _ m) return (vector (naryFunc n) m) with
| Vnil ⇒ Vnil (naryFunc n)
| Vcons f m' l' ⇒ Vcons _ (f a) m' (evalOneParamList n m' a l')
end.
Fixpoint evalComposeFunc (n : nat) :
∀ m : nat, vector (naryFunc n) m → naryFunc m → naryFunc n :=
match
n
return
(∀ m : nat, vector (naryFunc n) m → naryFunc m → naryFunc n)
with
| O ⇒ evalList
| S n' ⇒
fun (m : nat) (l : vector (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 (naryFunc n) m :=
match fs in (PrimRecs n m) return (vector (naryFunc n) m) with
| PRnil a ⇒ Vnil (naryFunc a)
| PRcons a b g gs ⇒ Vcons _ (evalPrimRec _ g) _ (evalPrimRecs _ _ gs)
end.
Definition extEqualVectorGeneral (n m : nat) (l : vector (naryFunc n) m)
(m' : nat) (l' : vector (naryFunc n) m') : Prop.
Defined.
Definition extEqualVector (n m : nat) (l l' : vector (naryFunc n) m) : Prop.
Defined.
Lemma extEqualVectorRefl :
∀ (n m : nat) (l : vector (naryFunc n) m), extEqualVector n m l l.
Lemma extEqualOneParamList :
∀ (n m : nat) (l1 l2 : vector (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 (naryFunc n) m) (f1 f2 : naryFunc m),
extEqualVector n m l1 l2 →
extEqual m f1 f2 →
extEqual n (evalComposeFunc n m l1 f1) (evalComposeFunc n m l2 f2).
Lemma extEqualCompose2 :
∀ (n : nat) (f1 f2 : naryFunc n),
extEqual n f1 f2 →
∀ g1 g2 : naryFunc (S n),
extEqual (S n) g1 g2 → extEqual n (compose2 n f1 g1) (compose2 n f2 g2).
Lemma extEqualPrimRec :
∀ (n : nat) (g1 g2 : naryFunc n) (h1 h2 : naryFunc (S (S n))),
extEqual n g1 g2 →
extEqual (S (S n)) h1 h2 →
extEqual (S n) (evalPrimRecFunc n g1 h1) (evalPrimRecFunc n g2 h2).
Definition isPR (n : nat) (f : naryFunc n) : Set :=
{p : PrimRec n | extEqual n (evalPrimRec _ p) f}.
Definition isPRrel (n : nat) (R : naryRel n) : Set :=
isPR n (charFunction n R).
Lemma succIsPR : isPR 1 S.
Lemma const0_NIsPR : ∀ n : nat, isPR 0 n.
Lemma const1_NIsPR : ∀ n : nat, isPR 1 (fun _ ⇒ n).
Lemma idIsPR : isPR 1 (fun x : nat ⇒ x).
Lemma pi1_2IsPR : isPR 2 (fun a b : nat ⇒ a).
Lemma pi2_2IsPR : isPR 2 (fun a b : nat ⇒ b).
Lemma pi1_3IsPR : isPR 3 (fun a b c : nat ⇒ a).
Lemma pi2_3IsPR : isPR 3 (fun a b c : nat ⇒ b).
Lemma pi3_3IsPR : isPR 3 (fun a b c : nat ⇒ c).
Lemma pi1_4IsPR : isPR 4 (fun a b c d : nat ⇒ a).
Lemma pi2_4IsPR : isPR 4 (fun a b c d : nat ⇒ b).
Lemma pi3_4IsPR : isPR 4 (fun a b c d : nat ⇒ c).
Lemma pi4_4IsPR : isPR 4 (fun a b c d : nat ⇒ d).
Lemma filter01IsPR :
∀ g : nat → nat, isPR 1 g → isPR 2 (fun a b : nat ⇒ g b).
Lemma filter10IsPR :
∀ g : nat → nat, isPR 1 g → isPR 2 (fun a b : nat ⇒ g a).
Lemma filter100IsPR :
∀ g : nat → nat, isPR 1 g → isPR 3 (fun a b c : nat ⇒ g a).
Lemma filter010IsPR :
∀ g : nat → nat, isPR 1 g → isPR 3 (fun a b c : nat ⇒ g b).
Lemma filter001IsPR :
∀ g : nat → nat, isPR 1 g → isPR 3 (fun a b c : nat ⇒ g c).
Lemma filter011IsPR :
∀ g : nat → nat → nat, isPR 2 g → isPR 3 (fun a b c : nat ⇒ g b c).
Lemma filter110IsPR :
∀ g : nat → nat → nat, isPR 2 g → isPR 3 (fun a b c : nat ⇒ g a b).
Lemma filter101IsPR :
∀ g : nat → nat → nat, isPR 2 g → isPR 3 (fun a b c : nat ⇒ g a c).
Lemma filter0011IsPR :
∀ g : nat → nat → nat,
isPR 2 g → isPR 4 (fun a b c d : nat ⇒ g c d).
Lemma filter1000IsPR :
∀ g : nat → nat, isPR 1 g → isPR 4 (fun a b c d : nat ⇒ g a).
Lemma filter1011IsPR :
∀ g : nat → nat → nat → nat,
isPR 3 g → isPR 4 (fun a b c d : nat ⇒ g a c d).
Lemma filter1100IsPR :
∀ g : nat → nat → nat,
isPR 2 g → isPR 4 (fun a b c d : nat ⇒ g a b).
Lemma compose1_1IsPR :
∀ f : nat → nat,
isPR 1 f →
∀ g : nat → nat, isPR 1 g → isPR 1 (fun x : nat ⇒ g (f x)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma 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)).
Lemma swapIsPR :
∀ f : nat → nat → nat, isPR 2 f → isPR 2 (fun x y : nat ⇒ f y x).
Lemma indIsPR :
∀ f : nat → nat → nat,
isPR 2 f →
∀ g : nat,
isPR 1
(fun a : nat ⇒ nat_rec (fun n : nat ⇒ nat) g (fun x y : nat ⇒ f x y) a).
Lemma 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).
Lemma 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).
Lemma plusIndIsPR : isPR 3 (fun n fn b : nat ⇒ S fn).
Lemma plusIsPR : isPR 2 plus.
Lemma multIndIsPR : isPR 3 (fun n fn b : nat ⇒ fn + b).
Lemma multIsPR : isPR 2 mult.
Lemma predIsPR : isPR 1 pred.
Lemma minusIndIsPR : isPR 3 (fun n fn b : nat ⇒ pred fn).
Lemma minusIsPR : isPR 2 minus.
Definition notZero (a : nat) :=
nat_rec (fun n : nat ⇒ nat) 0 (fun x y : nat ⇒ 1) a.
Lemma notZeroIsPR : isPR 1 notZero.
Definition ltBool (a b : nat) : bool.
Defined.
Lemma ltBoolTrue : ∀ a b : nat, ltBool a b = true → a < b.
Lemma ltBoolFalse : ∀ a b : nat, ltBool a b = false → ¬ a < b.
Lemma ltIsPR : isPRrel 2 ltBool.
Lemma maxIsPR : isPR 2 max.
Lemma 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 _ _ (Vcons _ a _ (Vcons _ b _ (Vnil (naryFunc n)))) c)
(evalComposeFunc _ _ (Vcons _ a' _ (Vcons _ b' _ (Vnil (naryFunc n)))) c').
Definition orRel (n : nat) (R S : naryRel n) : naryRel n.
Defined.
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.
Defined.
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.
Defined.
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.
Lemma boddIsPR : isPRrel 1 bodd.
Lemma beq_nat_not_refl : ∀ a b : nat, a ≠ b → beq_nat a b = false.
Lemma neqIsPR : isPRrel 2 (fun a b : nat ⇒ negb (beq_nat a b)).
Lemma eqIsPR : isPRrel 2 beq_nat.
Definition leBool (a b : nat) : bool.
Defined.
Lemma 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.
Defined.
Definition projectionList (n m : nat) (p : m ≤ n) :
vector (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).
Lemma 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 (naryFunc n) m) (g : naryFunc (S m)),
extEqual n
(evalComposeFunc n _ (Vcons (naryFunc n) (evalConstFunc n c) _ v) g)
(evalComposeFunc n _ v (g c)).
Lemma reduce2ndCompose :
∀ (c n m : nat) (v : vector (naryFunc n) m) (n0 : naryFunc n)
(g : naryFunc (S (S m))),
extEqual n
(evalComposeFunc n _
(Vcons (naryFunc n) n0 _ (Vcons (naryFunc n) (evalConstFunc n c) _ v))
g)
(evalComposeFunc n _ (Vcons (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)))),
extEqual _ (evalPrimRecFunc n (g d) (fun x y : nat ⇒ h x y d) c)
(evalPrimRecFunc (S n) g h c d).
Lemma 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).
Lemma 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.
Defined.
Lemma switchIsPR : isPR 3 switchPR.
Fixpoint boundedSearchHelp (P : naryRel 1) (b : nat) {struct b} : nat :=
match b with
| O ⇒ 0
| S b' ⇒
match eq_nat_dec (boundedSearchHelp P b') b' with
| left _ ⇒ match P b' with
| true ⇒ b'
| false ⇒ S b'
end
| right _ ⇒ boundedSearchHelp P b'
end
end.
Definition boundedSearch (P : naryRel 2) (b : nat) : nat :=
boundedSearchHelp (P b) b.
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.
Lemma boundSearchIsPR :
∀ P : naryRel 2,
isPRrel 2 P → isPR 1 (fun b : nat ⇒ boundedSearch P b).
Definition iterate (g : nat → nat) :=
nat_rec (fun _ ⇒ nat → nat) (fun x : nat ⇒ x)
(fun (_ : nat) (rec : nat → nat) (x : nat) ⇒ g (rec x)).
Lemma iterateIsPR :
∀ g : nat → nat, isPR 1 g → ∀ n : nat, isPR 1 (iterate g n).
This page has been generated by coqdoc