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
Require Import Arith.

Fixpoint naryFunc (n : nat) : Set :=
  match n with
  | Onat
  | S nnatnaryFunc n
  end.

Fixpoint naryRel (n : nat) : Set :=
  match n with
  | Obool
  | S nnatnaryRel 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 bextEqual n b a.

Lemma extEqualTrans :
 ∀ (n : nat) (a b c : naryFunc n),
 extEqual n a bextEqual n b cextEqual n a c.

Fixpoint charFunction (n : nat) : naryRel nnaryFunc n :=
  match n return (naryRel nnaryFunc n) with
  | Ofun R : boolmatch R with
                         | true ⇒ 1
                         | false ⇒ 0
                         end
  | S mfun (R : naryRel (S m)) (a : nat) ⇒ charFunction m (R a)
  end.

This page has been generated by coqdoc