Require Import List.

Notation "[ ]" := nil.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).

Definition If_Then_Else (P Q R : Prop) : Prop :=
  (P /\ Q) \/ (~ P /\ R).

(* Booleans *)
Lemma not_intro : forall b, negb (negb b) = b.
Proof. now intros []. Qed.

(*
Lemma not_elim : forall b, b = negb (negb b).
Proof. now intros []. Qed.
*)

(* Boolean words: Deck of cards *)
Definition Deck : Set := list bool.

Inductive Concat : Deck -> Deck -> Deck -> Prop :=
 | conc_emp : forall dk, Concat [] dk dk
 | conc_cons : forall dd dc dk b, Concat dd dc dk ->
   Concat (b :: dd) dc (b :: dk)
.
(*
  -- ALTERNATING WORDS: Decks of alternating cards and properties

  -- Alter b dk if dk ≡ [b, not b, not (not b), ..]
*)
Inductive Alter : bool -> Deck -> Prop :=
 | alt_emp : forall b, Alter b []
 | alt_cons : forall b dk, Alter (negb b) dk -> Alter b (b :: dk)
.

Inductive Alternate : Deck -> Prop :=
 | alternate : forall b dk, Alter b dk -> Alternate dk
.

Lemma alter2head_eq : forall b d dk, Alter b (d :: dk) -> b = d.
Proof. now intros b d dk h; inversion h. Qed.

Lemma alter2head_tail : forall b d dk, Alter b (d :: dk) ->
                    b = d /\ Alter (negb b) dk.
Proof. now intros b d dk h; inversion h; split. Qed.

Lemma alter_not_elim : forall b d dk,
 Alter (negb b) (d :: dk) ->  Alter b dk.
Proof.
intros b d dk h; inversion h.
now rewrite <- (not_intro b).
Qed.

Lemma alter_not_intro : forall b d dk,
 Alter b (d :: dk) -> Alter (negb b) dk.
Proof. now intros b d dk h; inversion h. Qed.

(* PARITY OF WORDS: Odd and Even and properties *)
Inductive Odd: Deck -> Prop :=
 | odd_sgl : forall b, Odd [ b ]
 | odd_cons : forall b d dk, Odd dk -> Odd (b :: d :: dk)
.

Hint Constructors Odd.

Inductive Even : Deck -> Prop :=
 | even_emp : Even []
 | even_cons : forall b d dk, Even dk -> Even (b :: d :: dk)
.

Hint Constructors Even.

Lemma odd_even : forall b dk, Odd dk -> Even (b :: dk).
Proof.
intros b dk h; revert b; induction h as [ b0 | b0 d0 dk h hi]; intros b;
  repeat constructor.
now apply hi.
Qed.

Hint Resolve odd_even.

Lemma even_odd : forall b dk, Even dk -> Odd (b :: dk).
Proof.
intros b dk h; revert b; induction h as [ | b0 d0 dk h hi]; intros b;
  repeat constructor.
now apply hi.
Qed.

Hint Resolve even_odd.

(*  -- Odd and Even are disjoint properties *)
Lemma not_odd_and_even : forall dk, Odd dk -> Even dk -> False.
Proof.
induction 1 as [ b0 | b0 d0 dk hdk hi]; intro h.
  now inversion h.
now apply hi; inversion h.
Qed.

Lemma odd_or_even : forall dk, Odd dk \/ Even dk.
Proof.
induction dk as [ | hd [ | hd' tl] hi]; auto.
now destruct hi; auto.
Qed.

Lemma odd_even_concat : forall dd dc dk, Concat dd dc dk ->
  (Odd dk /\ ((Odd dd /\ Even dc) \/ (Even dd /\ Odd dc))) \/
  (Even dk /\ ((Odd dd /\ Odd dc) \/ (Even dd /\ Even dc))).
Proof.
induction 1 as [ dk | dd dc dk b h hi].
  now destruct (odd_or_even dk) as [hl | hr]; auto.
destruct hi as [[hl1 [[hl21 hl22] | [hl31 hl33]]] |
  [hr1 [[hr21 hr22] | [hr31 hr32]]]].
  now right; auto.
  now right; auto.
  now left; auto.
now left; auto.
Qed.

Lemma even_concat : forall dd dc dk, Concat dd dc dk -> Even dk ->
                (Odd dd /\ Odd dc) \/ (Even dd /\ Even dc).
Proof.
intros dd dc dk hc he.
destruct (odd_even_concat dd dc dk hc) as [ [h1 h2] | [h1 [h2 | h3]]].
  now case (not_odd_and_even dk h1 he).
  now left.
now right.
Qed.

(*  -- Subwords of alternating words are alternating *)
Lemma alter_concat_l : forall b dd dc dk, Concat dd dc dk ->
                   Alter b dk -> Alter b dd.
Proof.
intros b dd dc dk hc; revert b;
 induction hc as [ | dc0 dk0 dd0 b0 h hi] ;intros b ha;  auto.
  now constructor.
apply alter2head_tail in ha as (hl & hr).
rewrite hl; constructor.
now apply hi; rewrite <- hl.
Qed.

Lemma alter_concat_r : forall b dd dc dk, Concat dd dc dk -> Alter b dk
  -> (Odd dd /\ Alter (negb b) dc) \/ (Even dd /\ Alter b dc).
Proof.
intros b dd dc dk hc; revert b;
 induction hc as [ | dc0 dk0 dd0 b0 h hi] ;intros b ha;  auto.
inversion ha; subst; clear ha.
apply hi in H1 as [[hl1 hl2] | [hr1 hr2]].
  right; split.
    now apply odd_even.
  now rewrite <- (not_intro b0).
left; split; trivial.
now apply even_odd.
Qed.

(*  -- OPPOSITE WORDS: Opposite decks start with different booleans *)
Inductive Opposite : Deck -> Deck -> Prop :=
 | opp : forall b dc dk, Opposite (b :: dc) ((negb b) :: dk)
.

Lemma not_opp_emp_l : forall dk, ~ (Opposite [] dk).
Proof. now intros dk h; inversion h. Qed.

Lemma not_opp_emp_r : forall dk, ~ (Opposite dk []).
Proof. now intros dk h; inversion h. Qed.

Lemma not_opp_same : forall b dc dk, ~ (Opposite (b :: dc) (b :: dk)).
Proof.
intros b dc dk h; inversion h.
now destruct b.
Qed.

(*  -- The odd parts are there to ensure dc and dk are not empty *)
Lemma opposite1 : forall b dc dk,
              Odd dc -> Alter b dc -> Odd dk -> Alter (negb b) dk ->
              Opposite dc dk.
Proof.
intros b [ | hdc tlc] [ | hdk tlk] ho1 ha1 ho2 ha2; try now inversion ho1.
apply alter2head_eq in ha1; apply alter2head_eq in ha2; subst.
now constructor.
Qed.

Lemma opposite2 : forall b dc dk, Alter b dc -> Alter b dk ->
  ~ (Opposite dc dk).
Proof.
intros b [ | hdc tlc] [ | hdk tlk] ha1 ha2;
 try (apply not_opp_emp_l || apply not_opp_emp_r).
apply alter2head_eq in ha1; apply alter2head_eq in ha2; subst.
rewrite ha2.
now apply not_opp_same.
Qed.

(* PAIRED WORDS: of the form [not b1, b1, not b2, b2, ..., not bn, bn ]*)
Inductive Paired : Deck -> Prop :=
 | paired_emp : Paired []
 | paired_cons : forall b dk, Paired dk -> Paired (negb b :: b :: dk).

Hint Constructors Paired.

(*  -- Rotating decks: rotate [b1, b2, .., bn] = [b2, .., bn, b1] *)
Definition rotate d : Deck := match d with
 | [] => []
 | d :: dk => dk ++ [ d ]
end.

(*
  A deck is PairedRot iff rotating it 1 position makes it paired
  PairedRot b w <=> w = [b, not b1, b1, not b2, b2, ..., not bn, bn , not b]
*)
Inductive PairedRot : bool -> Deck -> Prop :=
  | prot_emp : forall b, PairedRot b []
  | prot_cons : forall b dk, Paired (dk ++ [ b ]) -> PairedRot b (b :: dk)
.

Hint Constructors PairedRot.

Lemma paired_rotate : forall b dk, PairedRot b dk -> Paired (rotate dk).
Proof. now intros b dk h; inversion h; auto. Qed.

Lemma paired_r_from_rot : forall b dk, PairedRot b dk ->
                      Paired (negb b :: dk ++ [ b ]).
Proof. now intros b dk h; inversion h; simpl; auto. Qed.

Lemma paired_r_from_rot_not : forall b dk, PairedRot (negb b) dk ->
                          Paired (b :: dk ++ [ negb b ]).
Proof.
intros b dk h; inversion h; subst; simpl;
 now rewrite <- (not_intro b) at 1; auto.
Qed.

(*
  A deck is PairedBet iff
  is obtained by prefixing and suffixing a paired deck with the same boolean
  PairedBet b w <=> w = [b, not b1, b1, not b2, b2, ..., not bn, bn, not b]
*)

Inductive PairedBet : bool -> Deck -> Prop :=
 | pbet_cons : forall b dk, Paired (dk ++ [ negb b ]) ->
                PairedBet b (b :: dk)
.

Hint Constructors PairedBet.

Lemma paired_r_from_bet : forall b dk, PairedBet (negb b) dk ->
                      Paired (b :: dk ++ [ b ]).
Proof.
intros b dk h; inversion h; subst.
rewrite <- (not_intro b) at 1 3.
now constructor.
Qed.


Lemma paired_r_from_bet_not : forall b dk, PairedBet b dk ->
                          Paired (negb b :: dk ++ [ negb b ]).
Proof.
intros b dk h; inversion h; subst.
now constructor.
Qed.


(*  -- SHUFFLING DECKS *)
Inductive Shuffle : Deck -> Deck -> Deck -> Prop :=
 | shuffle_emp : Shuffle [] [] []
 | shuffle_cons_l : forall b dd dc dk, Shuffle dd dc dk ->
                     Shuffle (b :: dd) dc (b :: dk)
 | shuffle_cons_r : forall b dd dc dk, Shuffle dd dc dk ->
                     Shuffle dd (b :: dc) (b :: dk)
.


Theorem shuffling : forall b dd dc dk, Shuffle dd dc dk -> Alter b dd ->
 (Odd dd /\ ((Odd dc /\ (Alter (negb b) dc -> Paired dk)
                     /\ (Alter b dc -> PairedBet b dk)) \/
             (Even dc /\ (Alter b dc -> Paired (negb b :: dk))
                      /\ (Alter (negb b) dc -> Paired (dk ++ [ negb b ])))))
 \/
 (Even dd /\ ((Odd dc /\ (Alter (negb b) dc -> Paired (dk ++ [ b ]))
                      /\ (Alter b dc -> Paired (negb b :: dk))) \/
              (Even dc /\ (Alter b dc -> PairedRot b dk)
                       /\ (Alter (negb b) dc -> Paired dk)))).
Proof.
intros b dd dc dk h; revert b;
 induction h as [ | b dd dc dk h hi | b dd dc dk h hi]; intros b1 ha.
(*  -- both decks empty *)
  now right; auto.

(*  -- dd goes first: Shuffle (d :: dd) dc (d :: dk) *)
  replace b with b1 in * by (now apply alter2head_eq in ha).
  destruct (hi _ (alter_not_intro _ _ _ ha)) as
 [ [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]] |
   [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]]]; clear hi.
 right; split; auto.
 left; split; auto.
 split; intro hs.
   now apply paired_r_from_bet; apply ho23.
 now rewrite <- (not_intro b1) in hs; auto.

 right; split; auto.
 right; split; auto.
 split; intro hs.
  now rewrite (not_intro b1) in ho33; auto.
 now rewrite (not_intro b1) in ho32; apply ho32; auto.

 left; split; auto.
 left; split; auto.
 split; intro hs.
  now rewrite (not_intro b1) in ho23; auto.
 now rewrite (not_intro b1) in ho22; constructor; apply ho22; auto.

 left; split; auto.
 right; split; auto.
 split; intro hs.
  now rewrite (not_intro b1) in ho33; auto.
 now apply paired_r_from_rot_not; apply ho32.
(*  -- dc goes first: Shuffle dd (d :: dc) (d :: dk) *)
  destruct (hi _ ha) as
 [ [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]] |
   [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]]]; clear hi.
 left; split; auto.
 right; split; auto.
 split; intro hs.
  replace b with b1 in * by (now apply alter2head_eq in hs).
  now constructor; apply ho22; inversion hs.
 replace b with (negb b1) in * by (now apply alter2head_eq in hs).
 apply paired_r_from_bet_not; apply ho23.
 now rewrite <- (not_intro b1); inversion hs.

 left; split; auto.
 left; split; auto.
 split; intro hs.
  replace b with (negb b1) in * by (now apply alter2head_eq in hs).
  apply ho32.
  now rewrite <- (not_intro b1); inversion hs.
 replace b with b1 in * by (now apply alter2head_eq in hs).
 now constructor; apply ho33; inversion hs.

 right; split; auto.
 right; split; auto.
 split; intro hs.
   replace b with b1 in * by (now apply alter2head_eq in hs).
   now constructor; apply ho22; inversion hs.
 replace b with (negb b1) in * by (now apply alter2head_eq in hs).
 now apply ho23; rewrite <- (not_intro b1); inversion hs.

 right; split; auto.
 left; split; auto.
 split; intro hs.
   replace b with (negb b1) in * by (now apply alter2head_eq in hs).
   apply paired_r_from_rot; apply ho32.
   now rewrite <- (not_intro b1); inversion hs.
 replace b with b1 in * by (now apply alter2head_eq in hs).
 now constructor; apply ho33; inversion hs.
Qed.

Section Main.
Variable b: bool.
Variable dd dc dx dk: Deck.
Variable ex : Even dx.
Variable alt_dx: Alter b dx.
Variable con : Concat dd dc dx.
Variable shf: Shuffle dd dc dk.


Lemma alt_dd : Alter b dd.
Proof. now apply alter_concat_l with (b:=b) in con. Qed.

Hint Resolve alt_dd.

Section CaseOdd.
Variable od : Odd dd.

Lemma odd_dc : Odd dc.
Proof.
destruct (even_concat _ _ _ con ex) as [ [hl hr] | [hl hr]]; trivial.
now case (not_odd_and_even _ od hl).
Qed.

Hint Resolve odd_dc.

Lemma alt_dc : Alter (negb b) dc.
Proof.
apply alter_concat_r with (b:=b) in con as [ [_ hl] | [hr _]]; trivial.
now case (not_odd_and_even _ od hr).
Qed.

Hint Resolve alt_dc.

Lemma opp_dd_dc : Opposite dd dc.
Proof. now apply opposite1 with (b:=b); auto. Qed.


Lemma paired_dk : Paired dk.
Proof.
destruct (shuffling _ _ _ _ shf alt_dd) as
 [ [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]] |
   [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]]].
  now apply ho22; auto.
  now destruct (not_odd_and_even _ odd_dc ho31).
  now destruct (not_odd_and_even _ od ho1).
  now apply ho33.
Qed.
End CaseOdd.

Section CaseEven.
Variable ed : Even dd.

Lemma even_dc : Even dc.
Proof.
apply even_concat in con as [[hl hr] | [hl hr]]; trivial.
now destruct (not_odd_and_even _ hl ed).
Qed.

Hint Resolve even_dc.

Lemma alt_dc' : Alter b dc.
Proof.
apply alter_concat_r with (b := b) in con as  [[hl hr] | [hl hr]]; trivial.
now destruct (not_odd_and_even _ hl ed).
Qed.

Hint Resolve alt_dc'.

Lemma nopp_dd_dc : ~ (Opposite dd dc).
Proof. now apply opposite2 with (b := b). Qed.

Lemma paired_rot_dk : Paired (rotate dk).
Proof.
destruct (shuffling _ _ _ _ shf alt_dd) as
 [ [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]] |
   [ho1 [[ho21 [ho22 ho23]] | [ho31 [ho32 ho33]]]]].
  now destruct (not_odd_and_even _ ho1 ed).
  now destruct (not_odd_and_even _ ho1 ed).
  now destruct (not_odd_and_even _ ho21 even_dc).
now apply paired_rotate with (b :=b); apply ho32; auto.
Qed.

End CaseEven.

Lemma opp_vs_paired :
  If_Then_Else (Opposite dd dc) (Paired dk) (Paired (rotate dk)).
Proof.
destruct (odd_or_even dd) as [hd | hd].
  left; split.
    now apply opp_dd_dc.
  now apply paired_dk.
right; split.
 now apply nopp_dd_dc.
now apply paired_rot_dk.
Qed.

End Main.

Theorem gilbreath_trick : forall dd dc dx dk, Even dx -> Alternate dx ->
  Concat dd dc dx -> Shuffle dd dc dk ->
  If_Then_Else (Opposite dd dc) (Paired dk) (Paired (rotate dk)).
Proof.
intros dd dc dx dk de da dC ds.
inversion da; subst.
now apply opp_vs_paired with (b:=b) (dx :=dx); auto.
Qed.