# Library Pairs

Instance eq_dec_pair : eq_dec (nat × nat).

Fixpoint C (n : nat) :=
match n with
| 0 ⇒ [(0,0)]
| S nC n ++ (S n, 0) :: filter (fun xnot (x el C n)) (map (fun p : nat × natlet (p1,p2) := p in (p1,S p2)) (C n))
end.

Lemma sublist_C : n : nat, x B, C (S n) = C n ++ x :: B.

Lemma C_S p n m : C n .[ m ] = Some pC (S n).[ m ] = Some p.

Lemma C_ge p n1 n2 m : n2 n1C n1 .[ m ] = Some pC n2 .[ m ] = Some p.

Fixpoint eSize (p : nat × nat) := let (n,m) := p in 1 + n + m.

Lemma C_exhaustive p : p el C( eSize p ).

Lemma C_longenough n : |C n| > n.

Definition c n : nat × nat := match elAt (C n) n with None(0,0) | Some pp end.
Definition c_inv p : nat := match pos p (C (eSize p)) with None ⇒ 0 | Some pp end.

Lemma c_c_inv p : c (c_inv p) = p.

Lemma c_surj : surjective c.

Definition penc (p : nat × nat) := lam(#0 (enc (fst p)) (enc (snd p))).

Lemma penc_lam p : lambda (penc p).

Lemma penc_closed p : closed (penc p).

Definition Pair : term := .\"n", "m", "p"; "p" "n" "m".

Lemma Pair_correct n m : Pair (enc n) (enc m) == penc (n, m).

Definition ESize : term := .\"p"; "p" (.\"n","m"; !Add !(enc 1) (!Add "n" "m")).

Lemma ESize_correct p : ESize (penc p) == enc(eSize p).

Definition PEq : term := .\"p1", "p2"; "p1" (.\"n1", "m1"; "p2" (.\"n2", "m2"; !Andalso (!EqN "n1" "n2") (!EqN "m1" "m2"))).

Lemma PEq_rec n1 m1 n2 m2 : PEq (penc (n1,m1)) (penc (n2,m2)) == Andalso (EqN (enc n1) (enc n2)) (EqN (enc m1) (enc m2)).

Lemma PEq_correct p1 p2 : PEq (penc p1) (penc p2) == true p1 = p2 PEq (penc p1) (penc p2) == false p1 p2.

Definition CC := R (.\ "C", "n"; "n" !(lenc penc [(0,0)]) (.\"n"; !Append ("C" "n")
(!Cons (!Pair (!Succ "n") !(enc 0))
(!Filter (.\ "x"; !Not (!(El PEq) "x" ("C" "n")))
(!Map (.\"p"; "p" (.\"n","m"; !Pair "n" (!Succ "m"))) ("C" "n")))))).

Lemma CC_rec_0 : CC (enc 0) == lenc penc [(0,0)].

Lemma CC_rec_S n : CC (enc (S n)) == Append ((lam (CC 0)) (enc n)) (Cons (Pair (Succ (enc n)) (enc 0))
(Filter (lam (Not (El PEq 0 (lam (CC 0) (enc n)))))
(Map (lam (0 (lam(lam(Pair 1 (Succ 0)))))) ((lam (CC 0)) (enc n))))).

Lemma CC_correct n : CC (enc n) == lenc penc (C n).

Definition Cn : term := (.\"n";
(!Nth (!CC "n") "n") !I !(penc (0,0))).

Lemma Cn_closed : closed Cn.

Lemma Cn_correct n : Cn (enc n) == penc(c n).