# Library Enum

Require Import Encoding Equality bijection.

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 : forall n : nat, exists (x : term) (B : list term), T (S n) = T n ++ x :: B.

Proof.

intros n.
exists (# (S n)). simpl. eexists; reflexivity.
Qed.

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

Proof.

destruct (sublist_T n) as [x [B H]].
rewrite H. eapply elAt_app.
Qed.

Lemma T_ge s n1 n2 m : n2 >= n1 -> T n1 .[ m ] = Some s -> T n2 .[ m ] = Some s.

Proof.

remember (S n1) as n1'.
induction 1; inv Heqn1'; eauto using T_S.
Qed.

Proof.

split.

- induction A; simpl; intuition; subst; eauto using in_map.

- induction A; simpl; try rewrite in_app_iff in *; intros H; try tauto; destruct H as [H1 | H2]; intuition; rewrite in_map_iff in *; destruct H2; destruct H; [left|]; congruence.

Qed.

Lemma T_var n : #n el T n.

Proof.

destruct n; simpl; auto.

Qed.

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

Proof.

intros; simpl.
decide (s t el T n); auto; simpl.
rewrite in_app_iff; simpl.

rewrite in_filter_iff, in_app_iff, <- appCross_correct.

intuition.

Qed.

Lemma T_el_ge s n m : n >= m -> s el T m -> s el T n.

Proof.

intros A B; destruct (el_elAt B); eapply elAt_el, T_ge; eassumption.

Qed.

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

Proof.

intros; simpl; decide (lam s el T n); auto.

rewrite in_app_iff; simpl; rewrite in_filter_iff, in_app_iff, in_map_iff.

right.
right. split; try left; eauto.
Qed.

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

Proof with
simpl; repeat rewrite in_app_iff; repeat rewrite in_filter_iff; try rewrite <- appCross_correct; eauto using in_filter_iff, in_app_iff, appCross_correct, el_elAt, elAt_el, T_ge, in_map.

induction s.

- destruct n; simpl; auto.

- eapply T_app; eapply T_el_ge; try eassumption; fold exh_size plus; omega.

- now eapply T_lam.

Qed.

Lemma T_longenough m : |T m| > m.

induction m.

- simpl; omega.

- simpl.
rewrite app_length. simpl. omega.
Qed.

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.

Proof.

unfold g.
destruct( pos s (T (exh_size s)) ) eqn:A.
unfold g_inv.
destruct (T n .[ n ] ) eqn:B.
- eapply pos_elAt in A.

destruct (lt_eq_lt_dec n (exh_size s)) as [[D | D] | D].

+ eapply T_ge in B.
rewrite B in A. now inv A. omega.
+ subst.
rewrite A in B. now inv B.
+ eapply T_ge in A.
rewrite A in B. now inv B. omega.
- eapply nth_error_none in B.

assert (|T n| > n) by eapply T_longenough.
omega.
- assert (HIn : s el T (exh_size s)) by eapply T_exhaustive.

eapply el_elAt in HIn.
destruct HIn. eapply elAt_el in H. eapply el_pos in H. destruct H. congruence. auto.
Qed.

Hint Unfold left_inverse injective right_inverse surjective.

Lemma disjoint_symm X (A B : list X) : disjoint A B <-> disjoint B A.

Proof.

rewrite !disjoint_forall; firstorder.

Qed.

Lemma map_lam A : forall x, x el map lam A -> exists t, x = lam t.

Proof.

intros x B; rewrite in_map_iff in B; destruct B as [? [B _]]; subst; eauto.

Qed.

Lemma appCross_app A B : forall x, x el appCross A B -> exists s t, x = app s t.

Proof.

induction A.

- inversion 1.

- simpl; intros.
rewrite in_app_iff in H. destruct H; eauto. rewrite in_map_iff in H. destruct H as [t [H1 H2]]; eauto; subst; eauto.
Qed.

Lemma T_var_not n m : m > n -> ~ #m el T n.

Proof.

induction n.

- destruct m; destruct 2; try omega.
congruence. auto.
- simpl; intros A; rewrite !in_app_iff.

intros [H | H].

+ eapply IHn; now try omega.

+ destruct H as [H | H].
inv H; omega.
rewrite filter_app in H.
rewrite in_app_iff in H.
destruct H as [H | H]; rewrite in_filter_iff in H; destruct H as [H1 H2].

* rewrite in_map_iff in H1.
destruct H1 as [x [H1 _]]. inv H1.
* destruct (appCross_app H1) as [s [t H3]]; inv H3.

Qed.

Lemma appCross_dupfree A B : dupfree A -> dupfree B -> dupfree (appCross A B).

Proof with eauto using dupfree; intuition.

induction 1; intros dpf_B; simpl...

eapply dupfree_app...
eapply disjoint_forall. intros y Hy.
destruct (appCross_app Hy) as [y1 [y2 Hyy]]; subst.
eapply appCross_correct in Hy.
intros D.
eapply in_map_iff in D. destruct D as [d [D1 D2]]. inv D1...
eapply dupfree_map...
congruence.
Qed.

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

Proof.

induction n.

- simpl.
repeat econstructor. eauto.
- simpl.
eapply dupfree_app.
+ eapply disjoint_symm, disjoint_cons.
split.
* eapply T_var_not; omega.

* rewrite filter_app, disjoint_symm, disjoint_forall.

intros s A B.
eapply in_app_iff in B. destruct B; eapply in_filter_iff in H; tauto.
+ eassumption.

+ eapply dupfreeC.
rewrite in_filter_iff.
intros [A _].
rewrite in_app_iff in A. destruct A.
eapply map_lam in H.
destruct H; inv H.
eapply appCross_app in H.
destruct H as [s [t H]]. inv H.
eapply dupfree_filter.
eapply dupfree_app.
rewrite disjoint_forall.

intros x A B.
destruct (map_lam A), (appCross_app B) as [x1 [x2 B1]]. subst. inv B1.
eapply dupfree_map; congruence.

now eapply appCross_dupfree.

Qed.

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

Proof.

destruct (lt_eq_lt_dec n1 n2) as [[H | H] | H]; try subst;
try eapply lt_le_weak in H;
eauto using (T_ge), dupfree_elAt, dupfree_T.

Qed.

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

Proof.

unfold g_inv.
destruct (T n .[ n ] ) eqn:B.
unfold g.
destruct( pos t (T (exh_size t)) ) eqn:A.
- eauto using pos_elAt, T_dup.

- assert (HIn : t el T (exh_size t)) by eapply T_exhaustive.

eapply el_elAt in HIn.
destruct HIn.
eapply elAt_el in H.
eapply el_pos in H. destruct H. congruence. auto.   - eapply nth_error_none in B.
assert (|T n| > n) by eapply T_longenough.

omega.

Qed.

Hint Unfold left_inverse injective surjective g g_inv.

Lemma g_T : bijective g.

Proof.

split.

- eauto using left_inv_inj, g_inv_g.

- eauto using right_inv_surj, g_g_inv.

Qed.