Library Pairs

Instance eq_dec_pair : eq_dec (nat × nat).

Fixpoint C (n : nat) :=
  match n with
    | 0 ⇒ [(0,0)]
    | S n ⇒ C n ++ (S n, 0) :: filter (fun x ⇒ not (x el C n)) (map (fun p : nat × nat ⇒ let (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 p → C (S n).[ m ] = Some p.

Lemma C_ge p n1 n2 m : n2 ≥ n1 → C n1 .[ m ] = Some p → C 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 p ⇒ p end.
Definition c_inv p : nat := match pos p (C (eSize p)) with None ⇒ 0 | Some p ⇒ p 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).