# Library Pairs

Require Export Lvw bijection Enum Lists Equality.

Instance eq_dec_pair : eq_dec (nat * nat).

Proof.

intros; unfold dec; repeat decide equality.

Qed.

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 : forall n : nat, exists x B, C (S n) = C n ++ x :: B.

Proof.

repeat eexists.

Qed.

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

Proof.

destruct (sublist_C n) as [x [B H]].
rewrite H. eapply elAt_app.
Qed.

Lemma C_ge p n1 n2 m : n2 >= n1 -> C n1 .[ m ] = Some p -> C n2 .[ m ] = Some p.

Proof.

remember (S n1) as n1'.
induction 1; inv Heqn1'; eauto using C_S.
Qed.

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

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

Proof.

destruct p as [n m].
induction m.
- simpl.
rewrite plus_0_r. destruct n; simpl; auto.
- simpl.

decide ( (n,S m) el C (n + S m) ).

+ auto.

+ eapply in_app_iff.
right. right.
eapply in_filter_iff.
split.
* eapply in_map_iff.
exists (n, m). split. reflexivity. assert (n + S m = 1 + n + m) by omega. rewrite H. eassumption.
* eassumption.

Qed.

Lemma C_longenough n : |C n| > n.

Proof.

induction n; simpl.

- omega.

- rewrite app_length.
simpl. omega.
Qed.

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.

Proof.

unfold c_inv.
destruct( pos p (C (eSize p)) ) eqn:A.
unfold c.
destruct (elAt (C n) n ) eqn:B.
- eapply pos_elAt in A.

destruct (lt_eq_lt_dec n (eSize p)) as [[D | D] | D].

+ eapply C_ge in B.
rewrite B in A. now inv A. omega.
+ subst.
rewrite A in B. now inv B.
+ eapply C_ge in A.
rewrite A in B. now inv B. omega.
- eapply nth_error_none in B.

assert (|C n| > n) by eapply C_longenough.
omega.
- assert (HIn : p el C (eSize p)) by eapply C_exhaustive.

eapply el_elAt in HIn.
destruct HIn. eapply elAt_el in H. eapply el_pos in H. destruct H. congruence. auto.
Qed.

Lemma c_surj : surjective c.

eapply right_inv_surj.
unfold right_inverse. eapply c_c_inv.
Qed.

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

Lemma penc_lam p : lambda (penc p).

Proof.
value. Qed.

Lemma penc_closed p : closed (penc p).

Proof.
value. Qed.

Hint Rewrite penc_closed : cbv.

Hint Resolve penc_lam penc_closed : cbv.

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

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

Proof.

crush.

Qed.

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

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

Proof.

destruct p as [n m].
simpl.
crush.

Qed.

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)).

Proof.

crush.

Qed.

Lemma PEq_correct p1 p2 : PEq (penc p1) (penc p2) == true /\ p1 = p2 \/ PEq (penc p1) (penc p2) == false /\ p1 <> p2.

Proof.

destruct p1 as [n1 m1], p2 as [n2 m2].

destruct (EqN_correct n1 n2) as [[E1 H1] | [E1 H1]],
(EqN_correct m1 m2) as [[E2 H2] | [E2 H2]]; rewrite PEq_rec;
[ left; split; [crush | congruence] | right; split; [crush | congruence] .. ].

Qed.

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)].

Proof.

crush.

Qed.

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))))).

Proof.

crush.

Qed.

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

Proof with ( intros; value; eauto with cbv ).

induction n.

- now rewrite CC_rec_0.

- rewrite CC_rec_S.
setoid_rewrite Eta at 1 3... setoid_rewrite IHn at 1 2.
rewrite Map_correct with (f := (fun p : nat * nat => let (p1,p2) := p in (p1,S p2)))...

rewrite Filter_correct with (p := (fun x => not (x el C n)))...

rewrite Succ_correct, Pair_correct, Cons_correct, Append_correct...

+ destruct El_correct with (s := x) (A := C n) (enc := penc) (Eq := PEq) as [[H1 H2] | [H1 H2]]...

* eapply PEq_correct.

* assert ( N : (Î» Not (((El PEq) 0) ((Î» CC 0) (enc n)))) (penc x) == Not (((El PEq) (penc x)) (CC (enc n)))).

transitivity (Not (((El PEq) (penc x)) ((Î» CC 0) (enc n)))).
crush. rewrite Eta...
rewrite N.
rewrite IHn. rewrite H1. right; firstorder. crush.
* assert ( N : (Î» Not (((El PEq) 0) ((Î» CC 0) (enc n)))) (penc x) == Not (((El PEq) (penc x)) (CC (enc n)))).

transitivity (Not (((El PEq) (penc x)) ((Î» CC 0) (enc n)))).
crush. rewrite Eta...
rewrite N.
rewrite IHn. rewrite H1. left; firstorder. crush.
+ split; value.

intros p.
destruct p as [n1 m1]. cbv. crush.
Qed.

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

Lemma Cn_closed : closed Cn.

Proof.

value.

Qed.

Hint Unfold Cn : cbv.

Hint Rewrite Cn_closed : cbv.

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

Proof.

transitivity (Nth (CC (enc n)) (enc n) I (penc (0,0))).
crush.
rewrite CC_correct.
unfold penc.
rewrite Nth_correct; value.

unfold c, elAt, oenc.

destruct (nth_error (C n) n); crush.

intros; value.
intros; value.
Qed.