(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Max Omega Wellfounded Bool.

Require Import utils.

Set Implicit Arguments.

Notation Zero := false.
Notation One  := true.

Fact list_bool_dec (l m : list bool) : { l = m } + { l <> m }.
(* Goal: sumbool (@eq (list bool) l m) (not (@eq (list bool) l m)) *)
Proof.  apply list_eq_dec, bool_dec. Qed.

(* {0,1}* = 0*1{0,1}* + 0* *)

Fact list_bool_choose lb : { k : _ & { tl | lb = list_repeat Zero k ++ One :: tl } }
                         + { k            | lb = list_repeat Zero k }.
Proof.
(* Goal: sum (@sigT nat (fun k : nat => @sig (list bool) (fun tl : list bool => @eq (list bool) lb (@app bool (@list_repeat bool true k) (@cons bool false tl))))) (@sig nat (fun k : nat => @eq (list bool) lb (@list_repeat bool true k))) *)
  induction lb as [ | [] lb IHlb ].
  * right; exists 0; auto.
  * left; exists 0, lb; auto.
  * destruct IHlb as [ (k & lc & H) | (k & H) ].
    - left; exists (S k), lc; subst; auto.
    - right; exists (S k); subst; auto.
Qed.

(* {0,1}* = 1*0{0,1}* + 1* *)

Fact list_bool_choose_sym lb : { k : _ & { tl | lb = list_repeat One k ++ Zero :: tl } }
                             + { k            | lb = list_repeat One k }.
Proof.
(* Goal: sum (@sigT nat (fun k : nat => @sig (list bool) (fun tl : list bool => @eq (list bool) lb (@app bool (@list_repeat bool true k) (@cons bool false tl))))) (@sig nat (fun k : nat => @eq (list bool) lb (@list_repeat bool true k))) *)
  induction lb as [ | [] lb IHlb ].
  * right; exists 0; auto.
  * destruct IHlb as [ (k & lc & H) | (k & H) ].
    - left; exists (S k), lc; subst; auto.
    - right; exists (S k); subst; auto.
  * left; exists 0, lb; auto.
Qed.

(* [n1,...,nk] ---> 0...{n1}...01 0{n2}1 ... 0{nk}1 *) 

Fixpoint list_nat_bool ln :=
  match ln with
    | nil   => nil
    | x::ll => list_repeat Zero x ++ One :: list_nat_bool ll
  end.

Lemma list_bool_decomp k lb : { ln : _ & { lc | lb = list_nat_bool ln ++ lc 
                                             /\ Exists (fun x => k <= x) ln } }
                            + { ln : _ & { r  | lb = list_nat_bool ln ++ list_repeat Zero r 
                                             /\ Forall (fun x => x < k) ln } }.
Proof.
(* Goal: sum (@sigT (list nat) (fun ln : list nat => @sig (list bool) (fun lc : list bool => and (@eq (list bool) lb (@app bool (list_nat_bool ln) lc)) (@Exists nat (fun x : nat => le k x) ln)))) (@sigT (list nat) (fun ln : list nat => @sig nat (fun r : nat => and (@eq (list bool) lb (@app bool (list_nat_bool ln) (@list_repeat bool false r))) (@Forall nat (fun x : nat => lt x k) ln)))) *)
  induction lb as [ lb IH ] using (measure_rect (@length _)).
(* Goal: sum (@sigT (list nat) (fun ln : list nat => @sig (list bool) (fun lc : list bool => and (@eq (list bool) lb (@app bool (list_nat_bool ln) lc)) (@Exists nat (fun x : nat => le k x) ln)))) (@sigT (list nat) (fun ln : list nat => @sig nat (fun r : nat => and (@eq (list bool) lb (@app bool (list_nat_bool ln) (@list_repeat bool false r))) (@Forall nat (fun x : nat => lt x k) ln)))) *)
  destruct (list_bool_choose lb) as [ (x & lr & Hlb) | (x & Hlb) ].
  * destruct (le_lt_dec k x) as [ Hk | Hk ].
    + left; exists (x::nil), lr; split; simpl.
      - subst; solve list eq.
      - constructor 1; auto.
    + destruct (IH lr) as [ (ln & ld & H2 & H3) | (ln & r & H2 & H3) ].
      - subst; rew length; omega.
      - left; exists (x::ln), ld; split.
        ** subst; solve list eq.
        ** constructor 2; auto.
      - right; exists (x::ln), r; split.
        ** subst; solve list eq.
        ** constructor; auto.
  * right; exists nil, x; split.
     - subst; solve list eq.
     - constructor.
Qed.

Definition list_bool_valid   k lb ln := lb = list_nat_bool ln /\ Forall (fun x => x < k) ln.
Definition list_bool_invalid k lb ln := exists lc, lb = list_nat_bool ln ++ lc
                                            /\ (   Exists (fun x => k <= x) ln
                                               \/  Forall (fun x => x < k) ln 
                                                /\ exists p, lc = list_repeat Zero (S p)).

Fact list_bool_valid_dec k lb : { ln | list_bool_valid k lb ln } + { ln | list_bool_invalid k lb ln }.
Proof.
(* Goal: sum (@sig (list nat) (fun ln : list nat => list_bool_valid k lb ln)) (@sig (list nat) (fun ln : list nat => list_bool_invalid k lb ln)) *)
  destruct (list_bool_decomp k lb) as [ (ln & lc & H1 & H2) | (ln & [|p] & H1 & H2) ].
  * right; exists ln, lc; tauto.
  * left; exists ln; split; auto; subst; solve list eq.
  * right; exists ln, (list_repeat Zero (S p)); split; auto.
(* Goal: or (@Exists nat (fun x : nat => le k x) ln) (and (@Forall nat (fun x : nat => lt x k) ln) (@ex nat (fun p0 : nat => @eq (list bool) (@list_repeat bool false (S p)) (@list_repeat bool false (S p0))))) *)
    right; split; auto; exists p; auto.
Qed.

Fixpoint list_bool_nat l :=
  match l with 
    | nil     => 1
    | Zero::l => 0 + 2*list_bool_nat l
    | One::l  => 1 + 2*list_bool_nat l
  end.

Fact list_bool_nat_ge_1 l : 1 <= list_bool_nat l.
Proof. induction l as [ | [] ]; simpl in *; omega. Qed.

Unset Elimination Schemes.

Inductive list_bool_succ : list bool -> list bool -> Prop :=
  | in_lbs_0 : forall k l, list_bool_succ (list_repeat One k ++ Zero :: l) (list_repeat Zero k ++ One :: l)
  | in_lbs_1 : forall k,   list_bool_succ (list_repeat One k)              (list_repeat Zero (S k)).

Set Elimination Schemes.

Section list_bool_succ_props.

  Fact list_One_Zero_inj a b l m : list_repeat One a ++ Zero :: l = list_repeat One b ++ Zero :: m -> a = b /\ l = m.
  Proof.
(* Goal: forall _ : @eq (list bool) (@app bool (@list_repeat bool true a) (@cons bool false l)) (@app bool (@list_repeat bool true b) (@cons bool false m)), and (@eq nat a b) (@eq (list bool) l m) *)
    revert b l m; induction a as [ | a IHa ]; intros [ | b ] l m; simpl; try discriminate.
(* Goal: forall _ : @eq (list bool) (@cons bool false l) (@cons bool false m), and (@eq nat O O) (@eq (list bool) l m) *)
(* Goal: forall _ : @eq (list bool) (@cons bool true (@app bool (@list_repeat bool true a) (@cons bool false l))) (@cons bool true (@app bool (@list_repeat bool true b) (@cons bool false m))), and (@eq nat (S a) (S b)) (@eq (list bool) l m) *)
    inversion 1; auto.
(* Goal: forall _ : @eq (list bool) (list_bool_next (@iter (list bool) list_bool_next l n)) (@nil bool), and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    intros H.
(* Goal: False *)
    inversion H as [ H1 ].
(* Goal: and (@eq nat (S a) (S b)) (@eq (list bool) l m) *)
    apply IHa in H1.
(* Goal: and (@eq nat (S a) (S b)) (@eq (list bool) l m) *)
    destruct H1; subst; auto.
  Qed.

  Fact list_One_Zero_not a b l : list_repeat One a ++ Zero :: l <> list_repeat One b.
  Proof.
(* Goal: not (@eq (list bool) (@app bool (@list_repeat bool true a) (@cons bool false l)) (@list_repeat bool true b)) *)
    revert b l; induction a as [ | a IHa ]; intros [ | b ] l; simpl; try discriminate.
(* Goal: forall _ : @eq (list bool) (list_bool_next (@iter (list bool) list_bool_next l n)) (@nil bool), and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    intros H.
(* Goal: False *)
    inversion H as [ H1 ].
(* Goal: False *)
    apply IHa in H1; auto.
  Qed.

  Fact list_One_inj a b : list_repeat One a = list_repeat One b -> a = b.
  Proof.
(* Goal: forall _ : @eq (list bool) (@list_repeat bool true a) (@list_repeat bool true b), @eq nat a b *)
    intros H; apply f_equal with (f := @length _) in H; revert H.
(* Goal: forall _ : @eq nat (@length bool (@list_repeat bool true a)) (@length bool (@list_repeat bool true b)), @eq nat a b *)
    do 2 rewrite list_repeat_length; auto.
  Qed.

  Fact list_bool_succ_fun l m1 m2 : list_bool_succ l m1 -> list_bool_succ l m2 -> m1 = m2.
  Proof.
(* Goal: forall (_ : list_bool_succ l m1) (_ : list_bool_succ l m2), @eq (list bool) m1 m2 *)
    intros H; revert l m1 H m2.
(* Goal: forall (l m1 : list bool) (_ : list_bool_succ l m1) (m2 : list bool) (_ : list_bool_succ l m2), @eq (list bool) m1 m2 *)
    intros ? ? [ k l | k ]; inversion 1.
(* Goal: @eq (list bool) (@app bool (@list_repeat bool false k) (@cons bool true l)) (@app bool (@list_repeat bool false k0) (@cons bool true l1)) *)
(* Goal: @eq (list bool) (@app bool (@list_repeat bool false k) (@cons bool true l)) (@list_repeat bool false (S k0)) *)
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@app bool (@list_repeat bool false k0) (@cons bool true l)) *)
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@list_repeat bool false (S k0)) *)
    apply list_One_Zero_inj in H1; destruct H1; subst k0 l1; auto.
(* Goal: @eq (list bool) (@app bool (@list_repeat bool false k) (@cons bool true l)) (@list_repeat bool false (S k0)) *)
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@app bool (@list_repeat bool false k0) (@cons bool true l)) *)
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@list_repeat bool false (S k0)) *)
    symmetry in H1; apply list_One_Zero_not in H1; tauto.
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@app bool (@list_repeat bool false k0) (@cons bool true l)) *)
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@list_repeat bool false (S k0)) *)
    apply list_One_Zero_not in H1; tauto.
(* Goal: @eq (list bool) (@list_repeat bool false (S k)) (@list_repeat bool false (S k0)) *)
    apply list_One_inj in H1; subst; auto.
  Qed.

  Fact list_bool_succ_nil l : list_bool_succ nil l -> l = Zero::nil.
  Proof.
(* Goal: forall _ : list_bool_succ (@nil bool) l, @eq (list bool) l (@cons bool false (@nil bool)) *)
    intros H; symmetry; revert H; apply list_bool_succ_fun.
(* Goal: list_bool_succ (@nil bool) (@cons bool false (@nil bool)) *)
    constructor 2 with (k := 0).
  Qed.

  Fact list_bool_succ_neq : forall l m, list_bool_succ l m -> l <> m.
  Proof.
(* Goal: forall (l m : list bool) (_ : list_bool_succ l m), not (@eq (list bool) l m) *)
    intros ? ? [ [|k] l | [|k] ]; discriminate.
  Qed.

  Fact list_bool_succ_neq_nil l : ~ list_bool_succ l nil.
  Proof.
(* Goal: not (list_bool_succ l (@nil bool)) *)
    inversion 1.
(* Goal: False *)
    destruct k; discriminate.
  Qed.

End list_bool_succ_props.

Section list_bool_next.

  Let list_bool_next_def l : { m | list_bool_succ l m }.
  Proof.
(* Goal: @sig (list bool) (fun m : list bool => list_bool_succ l m) *)
    destruct (list_bool_choose_sym l) as [ (k & tl & H) | (k & H) ]; subst l.
    * exists (list_repeat Zero k ++ One :: tl); constructor.
    * exists (list_repeat Zero (S k)); constructor.
  Qed.

  Definition list_bool_next l := proj1_sig (list_bool_next_def l).
  Definition list_bool_next_spec l : list_bool_succ l (list_bool_next l). 
  Proof. apply (@proj2_sig _ _). Qed.

  Fact list_bool_next_neq_nil l : list_bool_next l <> nil.
  Proof.
(* Goal: forall _ : @eq (list bool) (list_bool_next (@iter (list bool) list_bool_next l n)) (@nil bool), and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    intros H.
(* Goal: @eq (list bool) m (list_bool_next l) *)
    generalize (list_bool_next_spec l).
(* Goal: forall _ : list_bool_succ l (list_bool_next l), False *)
    rewrite H.
(* Goal: forall _ : list_bool_succ l (@nil bool), False *)
    apply list_bool_succ_neq_nil.
  Qed.

  Fact iter_list_bool_next_nil l n : iter list_bool_next l n = nil -> n = 0 /\ l = nil.
  Proof.
(* Goal: forall _ : @eq (list bool) (@iter (list bool) list_bool_next l n) (@nil bool), and (@eq nat n O) (@eq (list bool) l (@nil bool)) *)
    destruct n as [ | n ].
(* Goal: forall _ : @eq (list bool) (@iter (list bool) list_bool_next l O) (@nil bool), and (@eq nat O O) (@eq (list bool) l (@nil bool)) *)
(* Goal: forall _ : @eq (list bool) (@iter (list bool) list_bool_next l (S n)) (@nil bool), and (@eq nat (S n) O) (@eq (list bool) l (@nil bool)) *)
    simpl; auto.
    replace (S n) with (n+1) by omega.
(* Goal: forall _ : @eq (list bool) (@iter (list bool) list_bool_next l (Init.Nat.add n (S O))) (@nil bool), and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    rewrite iter_plus; simpl.
(* Goal: forall _ : @eq (list bool) (list_bool_next (@iter (list bool) list_bool_next l n)) (@nil bool), and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    intros H.
(* Goal: and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    apply list_bool_next_neq_nil in H.
(* Goal: and (@eq nat (Init.Nat.add n (S O)) O) (@eq (list bool) l (@nil bool)) *)
    destruct H.
  Qed.

End list_bool_next.

Fact list_bool_succ_nat l m : list_bool_succ l m -> 1 + list_bool_nat l = list_bool_nat m.
Proof.
  revert l m; intros ? ? [ k l | k ]; induction k; simpl in *; omega.
Qed.
 
Section list_bool_succ_rect.

  Variable (P : list bool -> Type)
           (HP0 : P nil)
           (HPS : forall l m, list_bool_succ l m -> P l -> P m).

  Let list_bool_succ_rec n : forall l, list_bool_nat l = n -> P l.
  Proof.
(* Goal: forall (l : list bool) (_ : @eq nat (list_bool_nat l) n), P l *)
    induction n as [ | n IHn ]; intros l Hl.
    * generalize (list_bool_nat_ge_1 l); omega.
    * destruct (list_bool_choose l) as [ (k & tl & H) | ([ | k] & H) ]; subst l;
      [ generalize (in_lbs_0 k tl) | apply HP0 | generalize (in_lbs_1 k) ];
        intros E; apply HPS with (1 := E), IHn;
        apply list_bool_succ_nat in E; omega.
  Qed.

  Theorem list_bool_succ_rect : forall l, P l.
  Proof. intro; apply list_bool_succ_rec with (1 := eq_refl). Qed.

End list_bool_succ_rect.


(* The iteration of list_bool_next from Zero::nil visits every non-empty list of booleans *)

Theorem list_bool_next_total l : l <> nil -> { n | l = iter list_bool_next (Zero::nil) n }.
Proof.
(* Goal: forall _ : not (@eq (list bool) l (@nil bool)), @sig nat (fun n : nat => @eq (list bool) l (@iter (list bool) list_bool_next (@cons bool false (@nil bool)) n)) *)
  induction l as [ | l m Hlm IH ] using list_bool_succ_rect.
(* Goal: forall _ : not (@eq (list bool) (@nil bool) (@nil bool)), @sig nat (fun n : nat => @eq (list bool) (@nil bool) (@iter (list bool) list_bool_next (@cons bool false (@nil bool)) n)) *)
(* Goal: forall _ : not (@eq (list bool) m (@nil bool)), @sig nat (fun n : nat => @eq (list bool) m (@iter (list bool) list_bool_next (@cons bool false (@nil bool)) n)) *)
  intros []; auto.
(* Goal: forall _ : not (@eq (list bool) m (@nil bool)), @sig nat (fun n : nat => @eq (list bool) m (@iter (list bool) list_bool_next (@cons bool false (@nil bool)) n)) *)
  intros Hm.
(* Goal: @sig nat (fun n : nat => @eq (list bool) m (@iter (list bool) list_bool_next (@cons bool false (@nil bool)) n)) *)
  destruct (list_bool_choose_sym l) as [ (k & tl & H) | ([|k] & H) ].
  * destruct IH as (n & Hn).
(* Goal: False *)
    { subst; destruct k; discriminate. }
    exists (n+1); rewrite iter_plus; simpl.
    rewrite <- Hn.
(* Goal: @eq (list bool) m (list_bool_next l) *)
    generalize (list_bool_next_spec l).
(* Goal: forall _ : list_bool_succ l (list_bool_next l), @eq (list bool) m (list_bool_next l) *)
    apply list_bool_succ_fun; auto.
  * exists 0; simpl.
(* Goal: @eq (list bool) m (@cons bool false (@nil bool)) *)
    apply list_bool_succ_fun with (1 := Hlm).
(* Goal: list_bool_succ (@nil bool) (@cons bool false (@nil bool)) *)
    subst; simpl; constructor 2 with (k := 0).
  * destruct IH as (n & Hn).
(* Goal: not (@eq (list bool) l (@nil bool)) *)
(* Goal: @sig nat (fun n : nat => @eq (list bool) m (@iter (list bool) list_bool_next (@cons bool false (@nil bool)) n)) *)
    { subst; simpl; discriminate. }
    exists (n+1); rewrite iter_plus; simpl.
    rewrite <- Hn.
(* Goal: @eq (list bool) m (list_bool_next l) *)
    generalize (list_bool_next_spec l).
(* Goal: forall _ : list_bool_succ l (list_bool_next l), @eq (list bool) m (list_bool_next l) *)
    apply list_bool_succ_fun; auto.
Qed.

