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.


Lemma appCross_correct A B s t : (s el A /\ t el B) <-> (app s t) el appCross A B.

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.