Library Enum

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

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

Fixpoint T n :=
match n with
| 0 ⇒ [#n]
| S nlet 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 sT (S n).[ m ] = Some s.

Lemma T_ge s n1 n2 m : n2 n1T n1 .[ m ] = Some sT 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 nt el T ns t el T (S n).

Lemma T_el_ge s n m : n ms el T ms el T n.

Lemma T_lam s n : s el T nlam s el T (S n).

Fixpoint exh_size s := match s with
| #nn
| 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 nn end.
Definition g_inv n := match elAt (T n) n with None#0 | Some nn 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 Adupfree Bdupfree (appCross A B).

Lemma dupfree_T : n, dupfree (T n).

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

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

Lemma g_T : bijective g.