Library Lists

Section Fix_X.

  Variable X : Type.
  Variable enc : X → term.
  Hypothesis enc_lam : (∀ x, lambda (enc x)).
  Hypothesis enc_cls : (∀ x, closed (enc x)).


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


  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 F → Map 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 P → Filter P Nil == Nil.

  Lemma proc_lambda p : proc p → lambda 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 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).

  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 None ⇒ none | Some n ⇒ some (Nat.enc n) end.

End Fix_X.