# Library Lists

Require Export Bool Options.

Section Fix_X.

Variable X : Type.

Variable enc : X -> term.

Hypothesis enc_lam : (forall x, lambda (enc x)).

Hypothesis enc_cls : (forall x, closed (enc x)).

Hint Resolve enc_lam enc_cls : cbv.

Hint Rewrite enc_cls : cbv.

Fixpoint lenc (A : list X) :=
match A with
| nil => lam (lam #1)
| a::A => lam(lam (#0 (enc a) (lenc A)))
end.

Definition Nil : term := .\ "n", "c"; "n".

Definition Cons: term := .\ "a", "A", "n", "c"; "c" "a" "A".

Hint Unfold Nil Cons : cbv.

Lemma lenc_cls A : closed (lenc A).

Proof.

induction A.

- value.

- intros ? ? ; simpl; now rewrite IHA, enc_cls.

Qed.

Lemma lenc_lam A : lambda (lenc A).

Proof.

destruct A; value.

Qed.

Hint Resolve lenc_cls lenc_lam : cbv.

Hint Rewrite lenc_cls : cbv.

Lemma Cons_correct a A : Cons (enc a) (lenc A) == lenc(a::A).

Proof.

crush.

Qed.

Definition Append := R (.\ "app", "A", "B";
"A" "B" (.\"a", "A"; !Cons "a" ("app" "A" "B"))).

Hint Unfold Append : cbv.

Lemma Append_rec_Nil B : Append Nil (lenc B) == (lenc B).

Proof.

crush.

Qed.

Lemma Append_rec_Cons a A B : Append (lenc (a::A)) (lenc B) == Cons (enc a) ((lam (Append #0)) (lenc A) (lenc B)).

Proof.

crush.

Qed.

Lemma Append_correct A B : Append (lenc A) (lenc B) == lenc(A ++ B).

Proof.

induction A.

- eapply Append_rec_Nil.

- rewrite Append_rec_Cons.

now rewrite !Eta, IHA, Cons_correct; value.

Qed.

Definition sim (F : term) f := proc F /\ forall x, F (enc x) == (enc (f x)).

Definition Map := R (.\ "map", "F", "A";
"A" !Nil (.\"a", "A"; !Cons ("F" "a") ("map" "F" "A"))).

Lemma Map_rec_Nil F : proc F -> Map F Nil == Nil.

Proof.

intros [? ?]; crush.

Qed.

Lemma Map_rec_Cons a A F : proc F ->
Map F (lenc (a::A)) == Cons (F (enc a)) ((lam (Map #0)) F (lenc A)).

Proof.

intros [? ?]; crush.

Qed.

Lemma Map_correct f A F : sim F f ->
Map F (lenc A) == lenc(map f A).

Proof.

intros [[? ?] ?].

induction A.

- eapply Map_rec_Nil; eauto.

- rewrite Map_rec_Cons; eauto.

now rewrite !Eta, H1, IHA, Cons_correct; value.

Qed.

Variable Eq : term.

Hypothesis Eq_correct: forall s t : X,
(Eq (enc s) (enc t) == true /\ s = t) \/ (Eq (enc s) (enc t) == false /\ s <> t).

Hypothesis Eq_cls : closed Eq.

Hint Resolve Eq_cls.

Hint Rewrite Eq_cls.

Definition El := R (.\ "El", "x", "A";
"A" !false (.\"a", "A"; !Orelse (!Eq "a" "x") ("El" "x" "A"))).

Hint Unfold El : cbv.

Lemma El_nil s : El (enc s) Nil == false.

Proof.

crush.

Qed.

Lemma El_Cons s a A : El (enc s) (lenc (a :: A)) == Orelse (Eq (enc a) (enc s)) ((lam (El #0)) (enc s) (lenc A)).

Proof.

crush.

Qed.

Lemma El_correct s A : (El (enc s) (lenc A) == true /\ s el A) \/ (El (enc s) (lenc A) == false /\ ~ s el A).

Proof.

induction A.

- eauto using El_nil.

- destruct (Eq_correct a s) as [[HE E] | [HE N]].

+ subst.
left. split; auto. rewrite El_Cons, HE, !Eta; value. destruct IHA as [[H _] | [H _]]; rewrite H; eauto using Orelse_rec_tt, Orelse_rec_tf; auto.
+ destruct IHA as [[H I] | [H I]].

* left.
split; auto.
rewrite El_Cons, HE, !Eta, H; value.
eapply Orelse_rec_ft.
* right.
split; auto.
rewrite El_Cons, HE, !Eta, H; value.
eapply Orelse_rec_ff.
firstorder.

Qed.

Definition Filter := R (.\ "F", "p", "A";
"A" !Nil (.\"a", "A"; ("p" "a") (!Cons "a" ("F" "p" "A")) ("F" "p" "A"))).

Hint Unfold Filter : cbv.

Lemma Filter_Nil P : proc P -> Filter P Nil == Nil.

Proof.

destruct 1; crush.

Qed.

Lemma proc_lambda p : proc p -> lambda p.

Proof.

firstorder intuition.

Qed.

Hint Resolve proc_lambda : cbv.

Lemma Filter_Cons (P : term) a A :
proc P ->
Filter P (lenc (a::A))
== (P (enc a)) (Cons (enc a) ((lam (Filter #0)) P (lenc A))) ((lam (Filter #0)) P (lenc A)).

Proof.

intros.
crush.
Qed.

Lemma Filter_correct (P : term) p A (D : (forall x : X, dec (p x))) :
proc P ->
(forall x, P (enc x) == true /\ p x \/ P (enc x) == false /\ ~ p x)
-> Filter P (lenc A) == lenc(@filter X p D A).

Proof with eauto.

intros proc_P dec_P.

induction A.

- now rewrite Filter_Nil.

- rewrite Filter_Cons...
destruct (dec_P a) as [[HP Hp] | [HP Hp]];
simpl; decide (p a); try tauto;
rewrite !Eta; value;
rewrite HP, IHA, Cons_correct;
crush.

Qed.

Definition Nth := R (.\ "nth", "A", "n";
"n" ("A" !none (.\ "a", "A"; !some "a"))
(.\"n"; ("A" !none (.\"a", "A"; "nth" "A" "n"))) ).

Lemma Nth_Nil n : Nth Nil (Nat.enc n) == none.

Proof.

destruct n; crush.

Qed.

Lemma Nth_0 a A : Nth (lenc(a::A)) Zero == some (enc a).

Proof.

transitivity ((Î» (Î» #1 (enc a)))).
crush.
symmetry.
crush.
Qed.

Lemma Nth_Sn a A n : Nth (lenc(a::A)) (Nat.enc(S n)) == (lam (Nth #0)) (lenc A) (Nat.enc n).

Proof.

crush.

Qed.

Definition oenc x := match x with None => none | Some x => (lam(lam(#1 (enc x)))) end.

Lemma Nth_correct A n : Nth (lenc A) (Nat.enc n) == oenc(nth_error A n).

Proof.

revert A; induction n; intros A.

- destruct A.

+ now rewrite Nth_Nil.

+ rewrite Nth_0; crush.

- destruct A.

+ now rewrite Nth_Nil.

+ rewrite Nth_Sn.

now rewrite !Eta, IHn; value.

Qed.

Definition Pos := R (.\ "pos", "s", "A";
"A" !none (.\ "a", "A"; !Eq "s" "a" !(lam (some Zero))
(.\""; "pos" "s" "A" (.\"n"; !some (!Succ "n")) !none) !I)).

Lemma Pos_rec_nil s : Pos (enc s) Nil == none.

Proof.

crush.

Qed.

Lemma Pos_rec_cons s a A : Pos (enc s) (lenc(a::A)) ==
Eq (enc s) (enc a) (lam(some Zero)) (lam ( (lam(Pos #0)) (enc s) (lenc A) (lam(some (Succ #0))) none)) I.

Proof.

crush.

Qed.

Lemma Pos_correct s A (E : eq_dec X) : Pos (enc s) (lenc A) == match pos s A with None => none | Some n => some (Nat.enc n) end.

Proof.

induction A.

- now rewrite Pos_rec_nil.

- rewrite Pos_rec_cons.
simpl. destruct (Eq_correct s a) as [[F B] | [F B]].
+ rewrite F.
decide (s = a); try tauto. crush.
+ rewrite F.
decide (s = a); try tauto; destruct (pos s A); crush.
Qed.

End Fix_X.