# Library Lists

Section Fix_X.

Variable X : Type.
Variable enc : Xterm.
Hypothesis enc_lam : ( x, lambda (enc x)).
Hypothesis enc_cls : ( x, closed (enc x)).

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

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

Lemma lenc_cls A : closed (lenc A).

Lemma lenc_lam A : lambda (lenc A).

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

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

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

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

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

Definition sim (F : term) f := proc F 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 FMap F Nil == Nil.

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

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

Variable Eq : term.
Hypothesis Eq_correct: s t : X,
(Eq (enc s) (enc t) == true s = t) (Eq (enc s) (enc t) == false s t).

Hypothesis Eq_cls : closed Eq.

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

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

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

Lemma El_correct s A : (El (enc s) (lenc A) == true s el A) (El (enc s) (lenc A) == false ¬ s el A).

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

Lemma Filter_Nil P : proc PFilter P Nil == Nil.

Lemma proc_lambda p : proc plambda p.

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

Lemma Filter_correct (P : term) p A (D : ( x : X, dec (p x))) :
proc P
( x, P (enc x) == true p x P (enc x) == false ¬ p x)
→ Filter P (lenc A) == lenc(@filter X p D A).

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.

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

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

Definition oenc x := match x with Nonenone | Some x ⇒ (lam(lam(#1 (enc x)))) end.

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

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.

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.

Lemma Pos_correct s A (E : eq_dec X) : Pos (enc s) (lenc A) == match pos s A with Nonenone | Some nsome (Nat.enc n) end.

End Fix_X.