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
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 : natSet :=
  | succFunc : PrimRec 1
  | zeroFunc : PrimRec 0
  | projFunc : ∀ n m : nat, m < nPrimRec 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 : natnatSet :=
  | PRnil : ∀ n : nat, PrimRecs n 0
  | PRcons : ∀ n m : nat, PrimRec nPrimRecs n mPrimRecs 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
  | Om
  | S n'fun _evalConstFunc n' m
  end.

Fixpoint evalProjFunc (n : nat) : ∀ m : nat, m < nnaryFunc n :=
  match n return (∀ m : nat, m < nnaryFunc n) with
  | Ofun (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 : natevalConstFunc _ a
      | right l1
          fun _
          evalProjFunc n' m
            match le_lt_or_eq _ _ (lt_n_Sm_le _ _ l) with
            | or_introl l2l2
            | or_intror l2False_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 mnat :=
  match l in (vector _ m) return (naryFunc mnat) with
  | Vnilfun 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
  | VnilVnil (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) mnaryFunc mnaryFunc n :=
  match
    n
    return
      (∀ m : nat, vector (naryFunc n) mnaryFunc mnaryFunc n)
  with
  | OevalList
  | 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 nnaryFunc (S n) → naryFunc n :=
  match n return (naryFunc nnaryFunc (S n) → naryFunc n) with
  | Ofun (a : nat) (g : natnat) ⇒ g a
  | S n'
      fun (f : naryFunc (S n')) (g : naryFunc (S (S n'))) (a : nat) ⇒
      compose2 n' (f a) (fun x : natg x a)
  end.

Fixpoint evalPrimRecFunc (n : nat) (g : naryFunc n)
 (h : naryFunc (S (S n))) (a : nat) {struct a} : naryFunc n :=
  match a with
  | Og
  | 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
  | succFuncS
  | zeroFunc ⇒ 0
  | projFunc n m pfevalProjFunc 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 aVnil (naryFunc a)
  | PRcons a b g gsVcons _ (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 g2extEqual 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 : natx).

Lemma pi1_2IsPR : isPR 2 (fun a b : nata).

Lemma pi2_2IsPR : isPR 2 (fun a b : natb).

Lemma pi1_3IsPR : isPR 3 (fun a b c : nata).

Lemma pi2_3IsPR : isPR 3 (fun a b c : natb).

Lemma pi3_3IsPR : isPR 3 (fun a b c : natc).

Lemma pi1_4IsPR : isPR 4 (fun a b c d : nata).

Lemma pi2_4IsPR : isPR 4 (fun a b c d : natb).

Lemma pi3_4IsPR : isPR 4 (fun a b c d : natc).

Lemma pi4_4IsPR : isPR 4 (fun a b c d : natd).

Lemma filter01IsPR :
 ∀ g : natnat, isPR 1 gisPR 2 (fun a b : natg b).

Lemma filter10IsPR :
 ∀ g : natnat, isPR 1 gisPR 2 (fun a b : natg a).

Lemma filter100IsPR :
 ∀ g : natnat, isPR 1 gisPR 3 (fun a b c : natg a).

Lemma filter010IsPR :
 ∀ g : natnat, isPR 1 gisPR 3 (fun a b c : natg b).

Lemma filter001IsPR :
 ∀ g : natnat, isPR 1 gisPR 3 (fun a b c : natg c).

Lemma filter011IsPR :
 ∀ g : natnatnat, isPR 2 gisPR 3 (fun a b c : natg b c).

Lemma filter110IsPR :
 ∀ g : natnatnat, isPR 2 gisPR 3 (fun a b c : natg a b).

Lemma filter101IsPR :
 ∀ g : natnatnat, isPR 2 gisPR 3 (fun a b c : natg a c).

Lemma filter0011IsPR :
 ∀ g : natnatnat,
 isPR 2 gisPR 4 (fun a b c d : natg c d).

Lemma filter1000IsPR :
 ∀ g : natnat, isPR 1 gisPR 4 (fun a b c d : natg a).

Lemma filter1011IsPR :
 ∀ g : natnatnatnat,
 isPR 3 gisPR 4 (fun a b c d : natg a c d).

Lemma filter1100IsPR :
 ∀ g : natnatnat,
 isPR 2 gisPR 4 (fun a b c d : natg a b).

Lemma compose1_1IsPR :
 ∀ f : natnat,
 isPR 1 f
 ∀ g : natnat, isPR 1 gisPR 1 (fun x : natg (f x)).

Lemma compose1_2IsPR :
 ∀ f : natnat,
 isPR 1 f
 ∀ f' : natnat,
 isPR 1 f'
 ∀ g : natnatnat,
 isPR 2 gisPR 1 (fun x : natg (f x) (f' x)).

Lemma compose1_3IsPR :
 ∀ f1 : natnat,
 isPR 1 f1
 ∀ f2 : natnat,
 isPR 1 f2
 ∀ f3 : natnat,
 isPR 1 f3
 ∀ g : natnatnatnat,
 isPR 3 gisPR 1 (fun x : natg (f1 x) (f2 x) (f3 x)).

Lemma compose2_1IsPR :
 ∀ f : natnatnat,
 isPR 2 f
 ∀ g : natnat, isPR 1 gisPR 2 (fun x y : natg (f x y)).

Lemma compose2_2IsPR :
 ∀ f : natnatnat,
 isPR 2 f
 ∀ g : natnatnat,
 isPR 2 g
 ∀ h : natnatnat,
 isPR 2 hisPR 2 (fun x y : nath (f x y) (g x y)).

Lemma compose2_3IsPR :
 ∀ f1 : natnatnat,
 isPR 2 f1
 ∀ f2 : natnatnat,
 isPR 2 f2
 ∀ f3 : natnatnat,
 isPR 2 f3
 ∀ g : natnatnatnat,
 isPR 3 gisPR 2 (fun x y : natg (f1 x y) (f2 x y) (f3 x y)).

Lemma compose2_4IsPR :
 ∀ f1 : natnatnat,
 isPR 2 f1
 ∀ f2 : natnatnat,
 isPR 2 f2
 ∀ f3 : natnatnat,
 isPR 2 f3
 ∀ f4 : natnatnat,
 isPR 2 f4
 ∀ g : natnatnatnatnat,
 isPR 4 gisPR 2 (fun x y : natg (f1 x y) (f2 x y) (f3 x y) (f4 x y)).

Lemma compose3_1IsPR :
 ∀ f : natnatnatnat,
 isPR 3 f
 ∀ g : natnat, isPR 1 gisPR 3 (fun x y z : natg (f x y z)).

Lemma compose3_2IsPR :
 ∀ f1 : natnatnatnat,
 isPR 3 f1
 ∀ f2 : natnatnatnat,
 isPR 3 f2
 ∀ g : natnatnat,
 isPR 2 gisPR 3 (fun x y z : natg (f1 x y z) (f2 x y z)).

Lemma compose3_3IsPR :
 ∀ f1 : natnatnatnat,
 isPR 3 f1
 ∀ f2 : natnatnatnat,
 isPR 3 f2
 ∀ f3 : natnatnatnat,
 isPR 3 f3
 ∀ g : natnatnatnat,
 isPR 3 gisPR 3 (fun x y z : natg (f1 x y z) (f2 x y z) (f3 x y z)).

Lemma compose4_2IsPR :
 ∀ f1 : natnatnatnatnat,
 isPR 4 f1
 ∀ f2 : natnatnatnatnat,
 isPR 4 f2
 ∀ g : natnatnat,
 isPR 2 gisPR 4 (fun w x y z : natg (f1 w x y z) (f2 w x y z)).

Lemma compose4_3IsPR :
 ∀ f1 : natnatnatnatnat,
 isPR 4 f1
 ∀ f2 : natnatnatnatnat,
 isPR 4 f2
 ∀ f3 : natnatnatnatnat,
 isPR 4 f3
 ∀ g : natnatnatnat,
 isPR 3 g
 isPR 4 (fun w x y z : natg (f1 w x y z) (f2 w x y z) (f3 w x y z)).

Lemma swapIsPR :
 ∀ f : natnatnat, isPR 2 fisPR 2 (fun x y : natf y x).

Lemma indIsPR :
 ∀ f : natnatnat,
 isPR 2 f
 ∀ g : nat,
 isPR 1
   (fun a : natnat_rec (fun n : natnat) g (fun x y : natf x y) a).

Lemma ind1ParamIsPR :
 ∀ f : natnatnatnat,
 isPR 3 f
 ∀ g : natnat,
 isPR 1 g
 isPR 2
   (fun a b : nat
    nat_rec (fun n : natnat) (g b) (fun x y : natf x y b) a).

Lemma ind2ParamIsPR :
 ∀ f : natnatnatnatnat,
 isPR 4 f
 ∀ g : natnatnat,
 isPR 2 g
 isPR 3
   (fun a b c : nat
    nat_rec (fun n : natnat) (g b c) (fun x y : natf x y b c) a).

Lemma plusIndIsPR : isPR 3 (fun n fn b : natS fn).

Lemma plusIsPR : isPR 2 plus.

Lemma multIndIsPR : isPR 3 (fun n fn b : natfn + b).

Lemma multIsPR : isPR 2 mult.

Lemma predIsPR : isPR 1 pred.

Lemma minusIndIsPR : isPR 3 (fun n fn b : natpred fn).

Lemma minusIsPR : isPR 2 minus.

Definition notZero (a : nat) :=
  nat_rec (fun n : natnat) 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 = truea < 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 : natltBool 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 RisPRrel 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 RisPRrel 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 RisPRrel n (notRel n R).

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

Lemma boddIsPR : isPRrel 1 bodd.

Lemma beq_nat_not_refl : ∀ a b : nat, abbeq_nat a b = false.

Lemma neqIsPR : isPRrel 2 (fun a b : natnegb (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
  | Of
  | S xfun _ignoreParams n x f
  end.

Definition projectionListPR (n m : nat) (p : mn) : PrimRecs n m.
Defined.

Definition projectionList (n m : nat) (p : mn) :
  vector (naryFunc n) m := evalPrimRecs n m (projectionListPR n m p).

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

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

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

Lemma ignoreParamsIsPR :
 ∀ (n m : nat) (f : naryFunc n), isPR _ fisPR _ (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 : natg 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 : nath 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 fisPR (S n) (fun x : natg (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
                  | trueb'
                  | falseS 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 bP b x = false.

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

Lemma boundSearchIsPR :
 ∀ P : naryRel 2,
 isPRrel 2 PisPR 1 (fun b : natboundedSearch P b).

Definition iterate (g : natnat) :=
  nat_rec (fun _natnat) (fun x : natx)
    (fun (_ : nat) (rec : natnat) (x : nat) ⇒ g (rec x)).

Lemma iterateIsPR :
 ∀ g : natnat, isPR 1 g → ∀ n : nat, isPR 1 (iterate g n).

This page has been generated by coqdoc