Library Enum

Notation "A '.[' i ']'" := (elAt A i) (no associativity, at level 50).

Fixpoint appCross A B :=
match A with
| nil ⇒ nil
| a :: A ⇒ appCross A B ++ map (app a) B
end.

Fixpoint T n :=
match n with
| 0 ⇒ [#n]
| S n ⇒ let A := T n in A ++ [#(S n)] ++ filter (fun x ⇒ ¬ x el T n) ( map lam A ++ appCross A A )
end.

Lemma sublist_T : ∀ n : nat, ∃ (x : term) (B : list term), T (S n) = T n ++ x :: B.

Lemma T_S s n m : T n .[ m ] = Some s → T (S n).[ m ] = Some s.

Lemma T_ge s n1 n2 m : n2 ≥ n1 → T n1 .[ m ] = Some s → T n2 .[ m ] = Some s.

Lemma appCross_correct A B s t : (s el A ∧ t el B) ↔ (app s t) el appCross A B.

Lemma T_var n : #n el T n.

Lemma T_app s t n : s el T n → t el T n → s t el T (S n).

Lemma T_el_ge s n m : n ≥ m → s el T m → s el T n.

Lemma T_lam s n : s el T n → lam s el T (S n).

Fixpoint exh_size s := match s with
| #n ⇒ n
| app s1 s2 ⇒ 1 + exh_size s1 + exh_size s2
| lam s ⇒ 1 + exh_size s
end.

Lemma T_exhaustive s : s el (T (exh_size s)).

Lemma T_longenough m : |T m| > m.

Definition g s := match pos s (T (exh_size s)) with None ⇒ 0 | Some n ⇒ n end.
Definition g_inv n := match elAt (T n) n with None ⇒ #0 | Some n ⇒ n end.

Lemma g_inv_g s : g_inv (g s) = s.


Lemma disjoint_symm X (A B : list X) : disjoint A B ↔ disjoint B A.

Lemma map_lam A : ∀ x, x el map lam A → ∃ t, x = lam t.

Lemma appCross_app A B : ∀ x, x el appCross A B → ∃ s t, x = app s t.

Lemma T_var_not n m : m > n → ¬ #m el T n.

Lemma appCross_dupfree A B : dupfree A → dupfree B → dupfree (appCross A B).

Lemma dupfree_T : ∀ n, dupfree (T n).

Lemma T_dup n1 n2 m1 m2 x : T n1 .[m1 ] = Some x → T n2 .[m2] = Some x → m1 = m2.

Lemma g_g_inv n : g(g_inv n) = n.


Lemma g_T : bijective g.