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.
transitivity (Add (enc 1) (Add (enc n) (enc m))). crush.
now rewrite !Add_correct.
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.
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.
transitivity (Add (enc 1) (Add (enc n) (enc m))). crush.
now rewrite !Add_correct.
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.