logical-foundations/Indprop.v

From LF Require Export Logic.

Fixpoint div2 (n : nat) :=
  match n with
  | 0 => 0
  | 1 => 0
  | S (S n) => S (div2 n)
  end.

Definition f (n : nat) :=
  if even n
  then div2 n
  else (3 * n) + 1.

Inductive Collatz_holds_for : nat -> Prop :=
| Chf_done : Collatz_holds_for 1
| Chf_more (n : nat) : Collatz_holds_for (f n) -> Collatz_holds_for n.

Example Collatz_holds_for_12 : Collatz_holds_for 12.
Proof.  
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_more. unfold f. simpl.
 apply Chf_done.
Qed.

Conjecture collatz: forall n, Collatz_holds_for n.

Inductive le : nat -> nat -> Prop :=
| le_n (n : nat) : le n n
| le_S (n m : nat) (H: le n m) : le n (S m).

Notation "n <= m" := (le n m) (at level 70).
Notation "n >= m" := (le m n) (at level 70).

Example le_3_5 : 3 <= 5.
Proof.
  apply le_S. apply le_S. apply le_n.
Qed.

Inductive clos_trans {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
| t_step (x y : X) :
  R x y -> clos_trans R x y
| t_trans (x y z : X):
  clos_trans R x y ->
  clos_trans R y z ->
  clos_trans R x z.

Inductive close_refl_trans {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
| crt_step (x y : X) :
  R x y -> close_refl_trans R x y
| crt_refl (x : X) : close_refl_trans R x x
| crt_trans (x y z : X) :
  close_refl_trans R x y ->
  close_refl_trans R y z ->
  close_refl_trans R x z.

Inductive Perm3 {X : Type} : list X -> list X -> Prop :=
| perm3_swap12 (a b c : X) :
  Perm3 [a;b;c] [b;a;c]
| perm3_swap23 (a b c : X) :
  Perm3 [a;b;c] [a;c;b]
| perm3_trans (l1 l2 l3 : list X) :
  Perm3 l1 l2 -> Perm3 l2 l3 -> Perm3 l1 l3.

Example Perm3_exercise1 : Perm3 [1;2;3] [1;2;3].
Proof.
  apply perm3_trans with (l2 := [2;1;3]).
  - apply perm3_swap12.
  - apply perm3_swap12.
Qed.

Example Perm3_example1 : Perm3 [1;2;3] [2;3;1].
Proof.
  apply perm3_trans with [2;1;3].
  - apply perm3_swap12.
  - apply perm3_swap23.
Qed.

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

Example ev_4 : ev 4.
Proof.
  repeat apply ev_SS.
  apply ev_0.
Qed.

Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
Proof.
  intros n.
  simpl.
  intros Hn.
  apply ev_SS.
  apply ev_SS.
  apply Hn.
Qed.

Theorem ev_double : forall n,
    ev (double n).
Proof.
  induction n as [ | n' IHn'].
  - simpl. apply ev_0.
  - simpl. apply ev_SS. apply IHn'.
Qed.

Theorem ev_inversion : forall (n : nat),
    ev n ->
    (n = 0) \/ (exists n', n = S (S n') /\ ev n').
Proof.
  intros n E.
  destruct E as [ | n' E'] eqn:EE.
  - left. reflexivity.
  - right. exists n'. split.
    + reflexivity.
    + apply E'.
Qed.

Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
Proof.
  intros n H.
  apply ev_inversion in H.
  destruct H as [H0 | H1].
  - discriminate.
  - destruct H1 as [n' [Hnm Hev]].
    injection Hnm as Heq.
    rewrite Heq. apply Hev.
Qed.

Theorem evSS_ev' : forall n,
    ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [ | n' E' Heq].
  apply E'.
Qed.

Theorem one_not_even : ~ ev 1.
Proof.
  intros H.
  inversion H.
Qed.

Theorem SSSSev_even : forall n,
    ev (S (S (S (S n)))) -> ev n.
Proof.
  intros n E.
  inversion E as [ | n' E' H].
  inversion E' as [ | n'' E'' H1].
  apply E''.
Qed.

Theorem SSSSev_even' : forall n,
    ev (S (S (S (S n)))) -> ev n.
Proof.
  intros n E.
  apply ev_inversion in E.
  destruct E as [H0 | [n' [HSS E']]].
  - discriminate.
  - apply ev_inversion in E'.
    destruct E' as [H0 | [n'' [HSSSS E'']]].
    + rewrite H0 in HSS.
      discriminate.
    + injection HSS as HSS.
      rewrite <- HSS in HSSSS.
      injection HSSSS as HSSSS.
      rewrite <- HSSSS in E''.
      apply E''.
Qed.

Theorem ev5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
  intros E.
  inversion E as [ | n E' H].
  inversion E' as [ | n' E'' H'].
  inversion E'' as [ | n'' E''' H''].
Qed.

Example inversion_ex1 : forall (n m o : nat),
    [n;m] = [o;o] -> [n] = [m].
Proof.
  intros n m o H.
  inversion H.
  reflexivity.
Qed.

Lemma ev_Even : forall n,
    ev n -> Even n.
Proof.
  intros n E.
  induction E as [ | n' E' IH].
  - unfold Even. exists 0. reflexivity.
  - unfold Even in IH.
    destruct IH as [k Hk].
    rewrite Hk.
    unfold Even.
    exists (S k).
    reflexivity.
Qed.

Theorem ev_Even_iff : forall n,
    ev n <-> Even n.
Proof.
  intros n. split.
  - apply ev_Even.
  - unfold Even. intros [k Hk]. rewrite Hk. apply ev_double.
Qed.

Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
Proof.
  intros n m E.
  induction E as [ | n' E' IH].
  - intros E.
    simpl.
    apply E.
  - intros Em.
    simpl.
    apply ev_SS.
    apply IH.
    apply Em.
Qed.

Inductive ev' : nat -> Prop :=
| ev'_0 : ev' 0
| ev'_2 : ev' 2
| ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m).

Theorem ev'_ev : forall n, ev' n <-> ev n.
Proof.
  intros n.
  split.
  - intros E.
    induction E as [ | | n' m' Hn Hm].
    + apply ev_0.
    + apply ev_SS. apply ev_0.
    + apply ev_sum.
      * apply Hm.
      * apply IHE1.
  - intros E.
    induction E as [ | n' E' IH].
    + apply ev'_0.
    + inversion E'.
      * apply ev'_2.
      * rewrite H0.
        rewrite <- plus_0_n.
        rewrite <- plus_n_Sm.
        rewrite <- plus_n_Sm.
        assert (G : S (0 + n') = 1 + n').
        { reflexivity. }
        rewrite G.
        assert (G' : S (1 + n') = 2 + n').
        { reflexivity. }
        rewrite G'.
        apply ev'_sum.
        -- apply ev'_2.
        -- apply IH.
Qed.

Theorem ev_ev__ev : forall n m,
    ev (n + m) -> ev n -> ev m.
Proof.
  intros n m E1 E2.
  generalize dependent E1.
  induction E2.
  - trivial.
  - simpl.
    intros H.
    apply IHE2.
    apply evSS_ev in H.
    apply H.
Qed.

Theorem ev_plus_plus : forall n m p,
    ev (n + m) -> ev (n + p) -> ev (m + p).
Proof.
  intros n m p E1 E2.
  apply ev_ev__ev with (n := n + n).
  - rewrite (add_assoc (n + n) m p).
    rewrite add_comm.
    rewrite (add_assoc p (n + n) m).
    rewrite add_assoc.
    rewrite <- (add_assoc (p + n) n m).
    rewrite (add_comm p n).
    apply ev_sum.
    + apply E2.
    + apply E1.
  - rewrite <- double_plus.
    apply ev_double.
Qed.

Module Playground.
  Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).

  Notation "n <= m" := (le n m).

  Example test_le1 :
    3 <= 3.
  Proof.
    apply le_n. Qed.

  Example test_le3 :
    (2 <= 1) -> 2 + 2 = 5.
  Proof.
    intros H.
    inversion H.
    inversion H2.
  Qed.

    Definition lt (n m : nat) := lt (S n) m.
    Notation "n < m" := (lt n m).

End Playground.

Inductive total_relation : nat -> nat -> Prop :=
| rel_0 (n : nat) : total_relation 0 n
| rel_Sn_m (n m : nat) (H : total_relation n m) : total_relation (S n) m.

Theorem total_relation_is_total : forall n m, total_relation n m.
Proof.
  intros n m.
  induction n as [ | n' IHn'].
  - apply rel_0.
  - apply rel_Sn_m.
    apply IHn'.
Qed.

Inductive empty_relation : nat -> nat -> Prop :=
| rel_contra (n m : nat) (H : S n = 0) : empty_relation n m.

Theorem empty_relation_is_empty : forall n m, ~empty_relation n m.
Proof.
  intros n m contra.
  inversion contra.
  discriminate H.
Qed.

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
  intros m n o H1 H2.
  induction H2.
  - apply H1.
  - apply le_S.
    apply IHle.
    apply H1.
Qed.

Theorem O_le_n : forall n,
    0 <= n.
Proof.
  induction n as [ | n' IHn'].
  - apply le_n.
  - apply le_S. apply IHn'.
Qed.

Theorem n_le_m__Sn_le_Sm : forall n m,
    n <= m -> S n <= S m.
Proof.
  intros n m H.
  induction H.
  - apply le_n.
  - apply le_S.
    apply IHle.
Qed.

Theorem Sn_le_Sm__n_le_m : forall n m,
    S n <= S m -> n <= m.
Proof.
  intros n m.
  generalize dependent n.
  induction m as [ | m' IHm'].
  - intros n H.
    inversion H.
    + apply le_n.
    + inversion H2.
  - intros n H.
    inversion H.
    + apply le_n.
    + apply IHm' in H2.
      apply le_S.
      apply H2.
Qed.

Theorem lt_ge_cases : forall n m,
    n <= m \/ ~(n <= m).
Proof.
  induction n as [ | n' IHn'].
  - intros m.
    left.
    apply O_le_n.
  - intros [ | m].
    + right.
      intros contra.
      inversion contra.
    + destruct IHn' with (m := m) as [ H | H ].
      * left.
        apply n_le_m__Sn_le_Sm.
        apply H.
      * right.
        intros contra.
        apply H.
        apply Sn_le_Sm__n_le_m.
        apply contra.
Qed.

Theorem le_plus_l : forall a b,
    a <= a + b.
Proof.
  intros a b.
  generalize dependent a.
  induction b as [ | b' IHb'].
  - intros a.
    rewrite add_0_r.
    apply le_n.
  - intros a.
    rewrite <- plus_n_Sm.
    apply le_S.
    apply IHb'.
Qed.

Theorem plus_le : forall n1 n2 m,
    n1 + n2 <= m ->
    n1 <= m /\ n2 <= m.
Proof.
  intros n1 n2 m.
  generalize dependent n2.
  generalize dependent n1.
  induction m as [ | m' IHm'].
  - intros n1 n2 H.
    split.
    + inversion H.
      apply le_plus_l.
    + inversion H.
      rewrite add_comm.
      apply le_plus_l.
  - intros n1 n2 H.
    split.
    + inversion H.
      * apply le_plus_l.
      * apply IHm' in H2 as [H2 H2'].
        apply le_S.
        apply H2.
    + inversion H.
      * rewrite add_comm.
        apply le_plus_l.
      * apply IHm' in H2 as [H2 H2'].
        apply le_S.
        apply H2'.
Qed.

Theorem add_le_cases : forall n m p q,
    n + m <= p + q -> n <= p \/ m <= q.
Proof.
  induction n as [ | n' IHn'].
  { intros m p q H. left. apply O_le_n. }
  intros m p.
  generalize dependent m.
  induction p as [ | p' IHp'].
  - intros m q H.
    assert (G : 0 + q = q).
    { reflexivity. }
    rewrite G in H.
    apply plus_le in H as [H1 H2].
    right.
    apply H2.
  - intros m q H.
    simpl in H.
    apply Sn_le_Sm__n_le_m in H.
    apply IHn' in H as [H | H].
    + left.
      apply n_le_m__Sn_le_Sm.
      apply H.
    + right.
      apply H.
Qed.

Theorem plus_le_compat_l : forall n m p,
    n <= m ->
    p + n <= p + m.
Proof.
  intros n m p H.
  induction p as [ | p' IHp'].
  - simpl. apply H.
  - simpl. apply n_le_m__Sn_le_Sm.
    apply IHp'.
Qed.

Theorem plus_le_compat_r : forall n m p,
    n <= m ->
    n + p <= m + p.
Proof.
  intros n m p H.
  induction p as [ | p' IHp'].
  - rewrite add_0_r.
    rewrite add_0_r.
    apply H.
  - repeat rewrite <- plus_n_Sm.
    apply n_le_m__Sn_le_Sm.
    apply IHp'.
Qed.

Theorem le_plus_trans : forall n m p,
    n <= m ->
    n <= m + p.
Proof.
  intros n m p H.
  induction p as [ | p' IHp'].
  - rewrite add_0_r. apply H.
  - rewrite <- plus_n_Sm.
    apply le_S.
    apply IHp'.
Qed.

Theorem leb_complete : forall n m,
    n <=? m = true -> n <= m.
Proof.
  induction n as [ | n' IHn'].
  - intros m H.
    apply O_le_n.
  - intros [ | m].
    + intros H.
      simpl in H.
      discriminate H.
    + intros H.
      simpl in H.
      apply n_le_m__Sn_le_Sm.
      apply IHn'.
      apply H.
Qed.

Theorem leb_correct : forall n m,
    n <= m ->
    n <=? m = true.
Proof.
  intros n m.
  generalize dependent n.
  induction m as [ | m' IHm'].
  - intros n H.
    inversion H.
    reflexivity.
  - intros [ | n].
    + intros H.
      reflexivity.
    + intros H.
      simpl.
      apply IHm'.
      apply Sn_le_Sm__n_le_m.
      apply H.
Qed.

Theorem leb_iff : forall n m,
    n <=? m = true <-> n <= m.
Proof.
  intros n m.
  split.
  - apply leb_complete.
  - apply leb_correct.
Qed.

Theorem leb_true_trans : forall n m o,
    n <=? m = true -> m <=? o = true -> n <=? o = true.
Proof.
  intros n m o H1 H2.
  apply leb_correct.
  apply leb_complete in H1.
  apply leb_complete in H2.
  apply le_trans with (n := m).
  - apply H1.
  - apply H2.
Qed.

Inductive R : nat -> nat -> nat -> Prop :=
| c1 : R 0 0 0
| c2 m n o (H : R m n o) : R (S m) n (S o)
| c3 m n o (H : R m n o) : R m (S n) (S o)
| c4 m n o (H : R (S m) (S n) (S (S o))) : R m n o
| c5 m n o (H : R m n o) : R n m o.

Example r112 : R 1 1 2.
Proof.
  apply c2.
  apply c3.
  apply c1.
Qed.

Definition fR : nat -> nat -> nat := plus.

Theorem R_equiv_fR : forall m n o, R m n o <-> fR m n = o.
Proof.
  intros m n o.
  split.
  - intros H.
    induction H.
    + reflexivity.
    + unfold fR.
      simpl.
      unfold fR in IHR.
      rewrite IHR.
      reflexivity.
    + unfold fR.
      rewrite <- plus_n_Sm.
      unfold fR in IHR.
      rewrite IHR.
      reflexivity.
    + unfold fR.
      unfold fR in IHR.
      simpl in IHR.
      injection IHR as IHR.
      rewrite <- plus_n_Sm in IHR.
      injection IHR as IHR.
      apply IHR.
    + unfold fR.
      unfold fR in IHR.
      rewrite add_comm.
      apply IHR.
  - intros H.
    unfold fR in H.
    generalize dependent n.
    generalize dependent m.
    induction o as [ | o' IHo'].
    + intros m n H.
      destruct m as [ | m'].
      * simpl in H.
        rewrite H.
        apply c1.
      * simpl in H.
        discriminate H.
    + intros m n H.
      destruct m as [ | m'].
      * simpl in H.
        rewrite H.
        apply c3.
        apply IHo'.
        reflexivity.
      * simpl in H.
        injection H as H.
        apply c2.
        apply IHo'.
        apply H.
Qed.

Inductive subseq {X : Type} : list X -> list X -> Prop :=
| empty_sub (l : list X) : subseq [] l
| unequal_sub (l1 l2 : list X) (x : X) (E : subseq l1 l2) : subseq l1 (x :: l2)
| equal_sub (l1 l2 : list X) (x : X) (E : subseq l1 l2) : subseq (x :: l1) (x :: l2).

Theorem subseq_refl : forall X (l : list X),
    subseq l l.
Proof.
  intros x.
  induction l as [ | h t IHt].
  - apply empty_sub.
  - apply equal_sub.
    apply IHt.
Qed.

Theorem subseq_app : forall X (l1 l2 l3 : list X),
    subseq l1 l2 ->
    subseq l1 (l2 ++ l3).
Proof.
  intros X l1 l2 l3 H.
  induction H.
  - apply empty_sub.
  - simpl.
    apply unequal_sub.
    apply IHsubseq.
  - simpl.
    apply equal_sub.
    apply IHsubseq.
Qed.

Lemma tail_subseq : forall X (l1 l2 : list X) (x : X),
    subseq (x :: l1) l2 ->
    subseq l1 l2.
Proof.
  intros X l1 l2 x H.
  induction l2 as [ | h t].
  - inversion H.
  - inversion H.
    + apply unequal_sub.
      apply IHt.
      apply E.
    + apply unequal_sub.
      apply E.
Qed.

Theorem subseq_trans : forall X (l1 l2 l3 : list X),
    subseq l1 l2 ->
    subseq l2 l3 ->
    subseq l1 l3.
Proof.
  intros X l1 l2 l3 H1 H2.
  generalize dependent l1.
  induction H2.
  - intros l1 H.
    inversion H.
    apply empty_sub.
  - intros l0 H.
    apply unequal_sub.
    apply IHsubseq.
    apply H.
  - intros l0 H.
    inversion H.
    + apply empty_sub.
    + apply unequal_sub. apply IHsubseq. apply E.
    + apply equal_sub.
      apply IHsubseq.
      apply E.
Qed.

Inductive reg_exp (T : Type) : Type :=
| EmptySet
| EmptyStr
| Char (t : T)
| App (r1 r2 : reg_exp T)
| Union (r1 r2 : reg_exp T)
| Star (r : reg_exp T).

Arguments EmptySet {T}.
Arguments EmptyStr {T}.
Arguments Char {T} _.
Arguments App {T} _ _.
Arguments Union {T} _ _.
Arguments Star {T} _.

Reserved Notation "s =~ re" (at level 80).

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
| MEmpty : [] =~ EmptyStr
| MChar x : [x] =~ (Char x)
| MApp s1 re1 s2 re2
    (H1 : s1 =~ re1)
    (H2 : s2 =~ re2)
  : (s1 ++ s2) =~ (App re1 re2)
| MUnionL s1 re1 re2
    (H1 : s1 =~ re1)
  : s1 =~ (Union re1 re2)
| MUnionR s2 re1 re2
    (H2 : s2 =~ re2)
  : s2 =~ (Union re1 re2)
| MStar0 re : [] =~ (Star re)
| MStarApp s1 s2 re
    (H1 : s1 =~ re)
    (H2 : s2 =~ (Star re))
  : (s1 ++ s2) =~ (Star re)

where "s =~ re" := (exp_match s re).

Example reg_exp_ex1 : [1] =~ Char 1.
Proof.
  apply MChar.
Qed.

Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
  apply (MApp [1]).
  - apply MChar.
  - apply MChar.
Qed.

Example reg_exp_ex3 : ~ ([1; 2] =~ Char 1).
Proof.
  intros H.
  inversion H.
Qed.

Fixpoint reg_exp_of_list {T} (l : list T) :=
  match l with
  | [] => EmptyStr
  | x :: l' => App (Char x) (reg_exp_of_list l')
  end.

Example reg_exp_ex4 : [1; 2; 3] =~ reg_exp_of_list [1; 2; 3].
Proof.
  simpl. apply (MApp [1]).
  { apply MChar. }
  apply (MApp [2]).
  { apply MChar. }
  apply (MApp [3]).
  { apply MChar. }
  apply MEmpty.
Qed.

Lemma MStar1 :
  forall T s (re : reg_exp T),
    s =~ re ->
    s =~ Star re.
Proof.
  intros T s re H.
  rewrite <- (app_nil_r _ s).
  apply MStarApp.
  - apply H.
  - apply MStar0.
Qed.

Lemma empty_is_empty : forall T (s : list T),
    ~(s =~ EmptySet).
Proof.
  intros T s H. inversion H.
Qed.

Lemma MUnion' : forall T (s : list T) (re1 re2 : reg_exp T),
    s =~ re1 \/ s =~ re2 ->
    s =~ Union re1 re2.
Proof.
  intros T s re1 re2 [ H | H ].
  - apply MUnionL. apply H.
  - apply MUnionR. apply H.
Qed.

Lemma MStar' : forall T (ss : list (list T)) (re : reg_exp T),
    (forall s, In s ss -> s =~ re) ->
    fold app ss [] =~ Star re.
Proof.
  intros T.
  induction ss as [ | h t IHt].
  - intros re H.
    simpl. apply MStar0.
  - intros re H.
    simpl. apply MStarApp.
    + apply H.
      simpl. left. reflexivity.
    + apply IHt.
      intros s H2.
      apply H.
      simpl. right. apply H2.
Qed.

Fixpoint re_chars {T} (re : reg_exp T) : list T :=
  match re with
  | EmptySet => []
  | EmptyStr => []
  | Char x => [x]
  | App re1 re2 => re_chars re1 ++ re_chars re2
  | Union re1 re2 => re_chars re1 ++ re_chars re2
  | Star re => re_chars re
  end.

Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T),
    s =~ re ->
    In x s ->
    In x (re_chars re).
Proof.
  intros T s re x Hmatch Hin.
  induction Hmatch
    as [
    | x'
    | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
    | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
    | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
  - simpl in Hin. destruct Hin.
  - simpl. simpl in Hin. apply Hin.
  - simpl.
    rewrite In_app_iff in *.
    destruct Hin as [Hin | Hin].
    + left. apply (IH1 Hin).
    + right. apply (IH2 Hin).
  - simpl. rewrite In_app_iff.
    left. apply (IH Hin).
  - simpl. rewrite In_app_iff. right. apply (IH Hin).
  - destruct Hin.
  - simpl. rewrite In_app_iff in Hin.
    destruct Hin as [Hin | Hin].
    + apply (IH1 Hin).
    + apply (IH2 Hin).
Qed.

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => true
  | App r1 r2 => re_not_empty r1 && re_not_empty r2
  | Union r1 r2 => re_not_empty r1 || re_not_empty r2
  | Star r => true
  end.

Theorem re_not_empty_correct : forall T (re : reg_exp T),
    (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  intros T re.
  split.
  - intros [s E].
    induction E.
    + reflexivity.
    + reflexivity.
    + simpl.
      rewrite IHE1.
      rewrite IHE2.
      reflexivity.
    + simpl.
      rewrite IHE.
      reflexivity.
    + simpl.
      rewrite IHE.
      destruct (re_not_empty re1) ; reflexivity.
    + reflexivity.
    + apply IHE2.
  - intros H.
    induction re.
    + discriminate H.
    + exists []. apply MEmpty.
    + exists [t]. apply MChar.
    + simpl in H.
      rewrite andb_true_iff in H.
      destruct H as [H1 H2].
      apply IHre1 in H1 as [s1 H1].
      apply IHre2 in H2 as [s2 H2].
      exists (s1 ++ s2).
      apply MApp.
      * apply H1.
      * apply H2.
    + simpl in H.
      rewrite orb_true_iff in H.
      destruct H as [H | H].
      * apply IHre1 in H as [s H].
        exists s.
        apply MUnionL.
        apply H.
      * apply IHre2 in H as [s H].
        exists s.
        apply MUnionR.
        apply H.
    + exists [].
      apply MStar0.
Qed.

Lemma star_app : forall T (s1 s2 : list T) (re : reg_exp T),
    s1 =~ Star re ->
    s2 =~ Star re ->
    s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
  induction H1.
  - discriminate.
  - discriminate.
  - discriminate.
  - discriminate.
  - discriminate.
  - intros H. apply H.
  - intros H.
    rewrite <- app_assoc.
    apply MStarApp.
    + apply H1_.
    + apply IHexp_match2.
      * apply Heqre'.
      * apply H.
Qed.

Lemma MStar'' : forall T (s : list T) (re : reg_exp T),
    s =~ Star re ->
    exists ss : list (list T),
      s = fold app ss []
      /\ forall s', In s' ss -> s' =~ re.
Proof.
  intros T s re H.
  remember (Star re) as re'.
  induction H
    as [ | x' | s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
       | s1 re1 re2 Hmatch IH | re1 s2' re2 Hmatch IH
       | re'' | s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
  - discriminate.
  - discriminate.
  - discriminate.
  - discriminate.
  - discriminate.
  - exists [].
    split.
    { reflexivity. }
    intros s H. simpl in H. exfalso. apply H.
  - apply IH2 in Heqre' as H2.
    injection Heqre' as Heqre''.
    destruct H2 as [tail [G1 G2]].
    exists (s1 :: tail).
    split.
    { simpl. rewrite G1. reflexivity. }
    intros s' H.
    destruct H as [H | H].
    + rewrite <- H.
      rewrite <- Heqre''.
      apply Hmatch1.
    + apply G2.
      apply H.
Qed.

Module Pumping.

  Fixpoint pumping_constant {T} (re : reg_exp T) : nat :=
    match re with
    | EmptySet => 1
    | EmptyStr => 1
    | Char _ => 2
    | App re1 re2 =>
        pumping_constant re1 + pumping_constant re2
    | Union re1 re2 =>
        pumping_constant re1 + pumping_constant re2
    | Star r => pumping_constant r
    end.

  Lemma pumping_constant_ge_1 :
    forall T (re : reg_exp T),
      pumping_constant re >= 1.
  Proof.
    intros T.
    induction re.
    - simpl. apply le_n.
    - simpl. apply le_n.
    - simpl. apply le_S. apply le_n.
    - simpl. apply le_plus_trans. apply IHre1.
    - simpl. apply le_plus_trans. apply IHre1.
    - simpl. apply IHre.
  Qed.

  Lemma pumping_constant_0_false :
    forall T (re : reg_exp T),
      pumping_constant re <> 0.
  Proof.
    intros T re H.
    assert (Hp1 : pumping_constant re >= 1).
    { apply pumping_constant_ge_1. }
    rewrite H in Hp1. inversion Hp1.
  Qed.

  Fixpoint napp {T} (n : nat) (l : list T) : list T :=
    match n with
    | 0 => []
    | S n' => l ++ napp n' l
    end.

  Lemma napp_plus : forall T (n m : nat) (l : list T),
      napp (n + m) l = napp n l ++ napp m l.
  Proof.
    intros T n m l.
    induction n as [ | n IHn].
    - reflexivity.
    - simpl. rewrite IHn, app_assoc. reflexivity.
  Qed.

  Lemma napp_star :
    forall T m s1 s2 (re : reg_exp T),
      s1 =~ re -> s2 =~ Star re ->
      napp m s1 ++ s2 =~ Star re.
  Proof.
    intros T m s1 s2 re Hs1 Hs2.
    induction m.
    - simpl. apply Hs2.
    - simpl. rewrite <- app_assoc.
      apply MStarApp.
      + apply Hs1.
      + apply IHm.
  Qed.

  Lemma napp_nil_nil : forall (T: Type) m,
      @napp T m [] = [].
  Proof.
    intros T.
    induction m as [ | m IHm].
    - reflexivity.
    - simpl. apply IHm.
  Qed.    

  Lemma weak_pumping : forall T (re : reg_exp T) s,
      s =~ re ->
      pumping_constant re <= length s ->
      exists s1 s2 s3,
        s = s1 ++ s2 ++ s3 /\
          s2 <> [] /\
          forall m, s1 ++ napp m s2 ++ s3 =~ re.
  Proof.
    intros T re s Hmatch.
    induction Hmatch
      as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
         | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
         | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
    - simpl. intros contra. inversion contra.
    - simpl.
      intros H.
      inversion H.
      inversion H2.
    - simpl. rewrite app_length.
      intros H.
      apply add_le_cases in H as [ H | H ].
      + apply IH1 in H as [t1 [t2 [t3 [G1 [G2 G3]]]]].
        exists t1, t2, (t3 ++ s2).
        split.
        { rewrite G1. repeat rewrite app_assoc. reflexivity. }
        split.
        { apply G2. }
        intros m.
        rewrite app_assoc.
        rewrite app_assoc.
        apply MApp.
        * rewrite <- app_assoc.
          apply G3.
        * apply Hmatch2.
      + apply IH2 in H as [t1 [t2 [t3 [G1 [G2 G3]]]]].
        exists (s1 ++ t1), t2, t3.
        split.
        { rewrite G1. repeat rewrite app_assoc. reflexivity. }
        split.
        { apply G2. }
        intros m.
        rewrite <- app_assoc.
        apply MApp.
        { apply Hmatch1. }
        apply G3.
    - simpl.
      intros H.
      apply plus_le in H as [H1 H2].
      apply IH in H1 as [t1 [t2 [t3 [G1 [G2 G3]]]]].
      exists t1, t2, t3.
      split.
      { apply G1. }
      split.
      { apply G2. }
      intros m.
      apply MUnionL.
      apply G3.
    - simpl.
      intros H.
      apply plus_le in H as [H1 H2].
      apply IH in H2 as [t1 [t2 [t3 [G1 [G2 G3]]]]].
      exists t1, t2, t3.
      split.
      { apply G1. }
      split.
      { apply G2. }
      intros m.
      apply MUnionR.
      apply G3.
    - simpl. intros H.
      inversion H.
      exfalso. apply pumping_constant_0_false in H2.
      apply H2.
    - simpl. rewrite app_length.
      intros H.
      simpl in IH2.
      destruct (length s1) as [ | n] eqn:Eqls2.
      + simpl in H.
        apply IH2 in H as [t1 [t2 [t3 [G1 [G2 G3]]]]].
        exists (s1 ++ t1), t2, t3.
        split.
        { rewrite G1. repeat rewrite <- app_assoc. reflexivity. }
        split.
        { apply G2. }
        intros m.
        rewrite <- app_assoc.
        apply MStarApp.
        * apply Hmatch1.          
        * apply G3.
      + exists [], s1, s2.
        split.
        { simpl. reflexivity. }
        split.
        * intros contra.
          rewrite contra in Eqls2.
          simpl in Eqls2.
          discriminate.
        * intros m.
          simpl.
          apply napp_star.
          { apply Hmatch1. }
          { apply Hmatch2. }
  Qed.

End Pumping.

Theorem filter_not_empty_In : forall n l,
    filter (fun x => n =? x) l <> [] ->
    In n l.
Proof.
  intros n l.
  induction l as [ | h t IHt].
  - simpl. intros contra. apply contra. reflexivity.
  - simpl. destruct (n =? h) eqn:H.
    + intros _. rewrite eqb_eq in H. rewrite H. left. reflexivity.
    + intros H'. right. apply IHt. apply H'.
Qed.

Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT (H: P) : reflect P true
| ReflectF (H: ~P) : reflect P false.

Theorem iff_reflect : forall P b, (P <-> b = true) -> reflect P b.
Proof.
  intros P b H.
  destruct b eqn:Eb.
  + apply ReflectT. rewrite H. reflexivity.
  + apply ReflectF. rewrite H. discriminate.
Qed.

Theorem reflect_iff : forall P b, reflect P b -> (P <-> b = true).
Proof.
  intros P b H.
  inversion H as [HP Hb | HNP Hb].
  - split.
    + intros _.
      reflexivity.
    + intros _.
      apply HP.
  - split.
    + intros G.
      exfalso.
      apply HNP.
      apply G.
    + intros contra.
      discriminate contra.
Qed.

Lemma eqbP : forall n m, reflect (n = m) (n =? m).
Proof.
  intros n m.
  apply iff_reflect.
  rewrite eqb_eq.
  reflexivity.
Qed.

Theorem filter_not_empty_In' : forall n l,
    filter (fun x => n =? x) l <> [] ->
    In n l.
Proof.
  intros n l.
  induction l as [ | h t IHt].
  - simpl. intros H. apply H. reflexivity.
  - simpl. destruct (eqbP n h) as [H | H].
    + intros _. left. rewrite H. reflexivity.
    + intros H'. right. apply IHt. apply H'.
Qed.

Fixpoint count n l :=
  match l with
  | [] => 0
  | h :: t => (if n =? h then 1 else 0) + count n t
  end.

Theorem eqbP_practice : forall n l,
    count n l = 0 -> ~(In n l).
Proof.
  intros n l Hcount.
  induction l as [ | h t IHt].
  - simpl. intros H. apply H.
  - intros contra. simpl in contra.
    simpl in Hcount.
    destruct (eqbP n h) as [H | H].
    + simpl in Hcount. discriminate Hcount.
    + simpl in Hcount.
      apply H.
      destruct contra as [contra | contra].
      * rewrite contra. reflexivity.
      * exfalso. apply IHt in Hcount. apply Hcount. apply contra.
Qed.

Inductive nostutter {X : Type} : list X -> Prop :=
| nostutter_empty : nostutter []
| nostutter_single (x : X) : nostutter [x]
| nostutter_diff
    (x : X)
    (y : X)
    (l : list X)
    (E1 : nostutter (y :: l))
    (E2 : x <> y): nostutter (x :: y :: l).

Example test_nostutter_1 : nostutter [3;1;4;1;5;6].
Proof.
  repeat constructor; apply eqb_neq; auto.
Qed.

Example test_nostutter_2 : nostutter (@nil nat).
Proof. apply nostutter_empty.
Qed.

Example test_nostutter_3 : nostutter [5].
Proof. apply (nostutter_single 5).
Qed.

Example test_nostutter_4 : not (nostutter [3;1;1;4]).
Proof.
  intro.
  repeat match goal with
           h : nostutter _ |- _ => inversion h; clear h; subst
         end.
  contradiction; auto. Qed.

Inductive merge {X : Type} : list X -> list X -> list X -> Prop :=
| merge_empty2 (l1 : list X):  merge l1 [] l1
| merge_empty1 (l2 : list X): merge [] l2 l2
| merge_cons1 (x : X) (l1 l2 l3: list X) (E : merge l1 l2 l3):
    merge (x :: l1) l2 (x :: l3)
| merge_cons2 (x : X) (l1 l2 l3: list X) (E : merge l1 l2 l3):
    merge l1 (x :: l2) (x :: l3).

Theorem merge_filter : forall (X : Set) (test : X -> bool) (l l1 l2 : list X),
    merge l1 l2 l ->
    All (fun n => test n = true) l1 ->
    All (fun n => test n = false) l2 ->
    filter test l = l1.
Proof.
  intros X test l l1 l2 H.
  induction H.
  - intros H1 H2.
    induction l1 as [ | h t IHt].
    + reflexivity.
    + simpl. simpl in H1.
      destruct H1 as [H1 H1'].
      rewrite H1.
      apply (f_equal (fun t => h :: t)).
      apply IHt.
      apply H1'.
  - simpl. intros _ H.
    induction l2 as [ | h t IHt].
    + reflexivity.
    + simpl. simpl in H.
      destruct H as [H1 H2].
      rewrite H1.
      apply IHt.
      apply H2.
  - simpl.
    intros [H1 H2] H3.
    rewrite H1.
    apply (f_equal (fun t => x :: t)).
    apply (IHmerge H2 H3).
  - simpl.
    intros H1 [H2 H3].
    rewrite H2.
    apply (IHmerge H1 H3).
Qed.

Lemma filter_subseq : forall (X: Set) (test : X -> bool) (l : list X),
    subseq (filter test l) l.
Proof.
  intros X test.
  induction l as [ | h t IHt].
  - simpl. apply empty_sub.
  - simpl.
    destruct (test h) as [ | ].
    + apply equal_sub.
      apply IHt.
    + apply unequal_sub.
      apply IHt.
Qed.

Inductive pal {X: Type}: list X -> Prop :=
| pal_empty : pal []
| pal_single (x: X) : pal [x]
| pal_more (x: X) (m: list X) (E : pal m) : pal (x :: m ++ [x]).

Theorem pal_app_rev : forall (X: Type) (l : list X),
    pal (l ++ (rev l)).
Proof.
  intros X.
  induction l.
  - simpl. apply pal_empty.
  - simpl.
    rewrite app_assoc.
    apply pal_more.
    apply IHl.
Qed.

Lemma rev_app_single : forall (X : Type) (l : list X) (x : X),
    rev (l ++ [x]) = x :: (rev l).
Proof.
  intros X.
  induction l as [ | h t IHt].
  - intros x.
    reflexivity.
  - intros x.
    simpl.
    rewrite IHt.
    reflexivity.
Qed.  

Theorem pal_rev : forall (X: Type) (l : list X), pal l -> l = rev l.
Proof.
  intros X l H.
  induction H.
  - reflexivity.
  - reflexivity.
  - simpl.
    rewrite rev_app_single.
    rewrite <- IHpal.
    reflexivity.
Qed.

Inductive NotIn {X: Type}: X -> list X -> Prop :=
| empty_notin (x: X): NotIn x []
| cons_notin (x: X) (x': X) (l: list X) (E1: x <> x') (E2: NotIn x l): NotIn x (x' :: l).

Inductive NoDup {X: Type}: list X -> Prop :=
| empty_nodup: NoDup []
| cons_nodup (x: X) (l: list X) (E: NoDup l) (pf: NotIn x l): NoDup (x :: l).

Inductive disjoint {X: Type}: list X -> list X -> Prop :=
| empty_disjoint l2 : disjoint [] l2
| cons_disjoint (x: X) (l1 l2: list X) (E1: disjoint l1 l2) (E2: NotIn x l2): disjoint (x :: l1) l2.

Example disjoint_ex1: disjoint [1; 2; 3] [4; 5; 6].
Proof.
  apply cons_disjoint.
  - apply cons_disjoint.
    + apply cons_disjoint.
      * apply empty_disjoint.
      * apply cons_notin.
        { trivial. }
        apply cons_notin.
        { intros H. discriminate H. }
        apply cons_notin.
        { discriminate. }
        apply empty_notin.
    + apply cons_notin.
      { discriminate. }
      apply cons_notin.
      { discriminate. }
      apply cons_notin.
      discriminate.
      apply empty_notin.
  - apply cons_notin.
    { discriminate. }
    apply cons_notin.
    { discriminate. }
    apply cons_notin.
    { discriminate. }
    apply empty_notin.
Qed.

Lemma in_split : forall (X: Type) (x: X) (l: list X),
    In x l ->
    exists l1 l2, l = l1 ++ x :: l2.
Proof.
  intros X x.
  induction l as [ | h t IHt].
  - intros H.
    simpl in H.
    exfalso.
    apply H.
  - intros H.
    destruct H as [H1 | H2].
    + exists [], t.
      simpl.
      rewrite H1.
      reflexivity.
    + apply IHt in H2.
      destruct H2 as [l1' [l2' H2]].
      exists (h :: l1'), l2'.
      rewrite H2.
      reflexivity.
Qed.

Inductive repeats {X: Type} : list X -> Prop :=
| repeats_cons (x: X) (l: list X) (E: In x l): repeats (x :: l)
| repeats_non (x: X) (l: list X) (E: repeats l): repeats (x :: l).

Require Import Arith.

Theorem pigeonhole_principle:
  excluded_middle -> forall (X: Type) (l1 l2: list X),
      (forall x, In x l1 -> In x l2) ->
      length l2 < length l1 ->
      repeats l1.
Proof.
  intros EM X l1. induction l1 as [ | h t IHt].
  - simpl. intros. inversion H0.
  - intros l2 H1 H2.
    destruct (EM (In h t)) as [G | G].
    + apply repeats_cons.
      apply G.
    + destruct l2 as [ | h2 t2].
      * simpl in H1.
        exfalso.
        apply H1 with (x := h).
        left.
        reflexivity.
      * destruct (in_split _ h (h2::t2)) as [la [lb E]].
        -- apply (H1 h).
           simpl.
           left.
           reflexivity.
        -- apply repeats_non.
           apply (IHt (la ++ lb)).
           ++ intros x G'.
              rewrite E in H1.
              assert (Neq : h <> x).
              { intros contra.
                rewrite contra in G.
                apply G.
                apply G'. }
              assert (In_split_Neq : In x (la ++ h :: lb) -> In x (la ++ lb)).
              { intros H'.
                apply In_app_iff.
                apply In_app_iff in H'.
                destruct H' as [H' | H'].
                - left. apply H'.
                - right. simpl in H'. destruct H' as [H' | H'].
                  + exfalso. apply Neq. apply H'.
                  + apply H'.
              } 
              apply In_split_Neq.
              apply H1.
              simpl.
              right.
              apply G'.
           ++ rewrite E in H2.
              rewrite app_length in H2.
              simpl in H2.
              rewrite <- plus_n_Sm in H2.
              rewrite app_length.
              apply PeanoNat.lt_S_n.
              apply H2.
Qed.