Library pairing.extEqualNat
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.
Fixpoint naryFunc (n : nat) : Set :=
match n with
| O ⇒ nat
| S n ⇒ nat → naryFunc n
end.
Fixpoint naryRel (n : nat) : Set :=
match n with
| O ⇒ bool
| S n ⇒ nat → naryRel n
end.
Definition extEqual (n : nat) (a b : naryFunc n) : Prop.
Defined.
Lemma extEqualRefl : ∀ (n : nat) (a : naryFunc n), extEqual n a a.
Lemma extEqualSym :
∀ (n : nat) (a b : naryFunc n), extEqual n a b → extEqual n b a.
Lemma extEqualTrans :
∀ (n : nat) (a b c : naryFunc n),
extEqual n a b → extEqual n b c → extEqual n a c.
Fixpoint charFunction (n : nat) : naryRel n → naryFunc n :=
match n return (naryRel n → naryFunc n) with
| O ⇒ fun R : bool ⇒ match R with
| true ⇒ 1
| false ⇒ 0
end
| S m ⇒ fun (R : naryRel (S m)) (a : nat) ⇒ charFunction m (R a)
end.
Fixpoint naryFunc (n : nat) : Set :=
match n with
| O ⇒ nat
| S n ⇒ nat → naryFunc n
end.
Fixpoint naryRel (n : nat) : Set :=
match n with
| O ⇒ bool
| S n ⇒ nat → naryRel n
end.
Definition extEqual (n : nat) (a b : naryFunc n) : Prop.
Defined.
Lemma extEqualRefl : ∀ (n : nat) (a : naryFunc n), extEqual n a a.
Lemma extEqualSym :
∀ (n : nat) (a b : naryFunc n), extEqual n a b → extEqual n b a.
Lemma extEqualTrans :
∀ (n : nat) (a b c : naryFunc n),
extEqual n a b → extEqual n b c → extEqual n a c.
Fixpoint charFunction (n : nat) : naryRel n → naryFunc n :=
match n return (naryRel n → naryFunc n) with
| O ⇒ fun R : bool ⇒ match R with
| true ⇒ 1
| false ⇒ 0
end
| S m ⇒ fun (R : naryRel (S m)) (a : nat) ⇒ charFunction m (R a)
end.
This page has been generated by coqdoc