Require Import List Arith Max Lia Wellfounded Bool.

From Undecidability.Shared.Libs.DLW
  Require Import Utils.utils.

Set Implicit Arguments.

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

Fact list_bool_dec (l m : list bool) : { l = m } + { l <> m }.
Proof. apply list_eq_dec, bool_dec. Qed.


Fact list_bool_choose lb : { k : _ & { tl | lb = list_repeat Zero k ++ One :: tl } }
                         + { k | lb = list_repeat Zero k }.
Proof.
  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.


Fact list_bool_choose_sym lb : { k : _ & { tl | lb = list_repeat One k ++ Zero :: tl } }
                             + { k | lb = list_repeat One k }.
Proof.
  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.


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.
  induction lb as [ lb IH ] using (measure_rect (@length _)).
  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; lia.
      - 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.
  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.
    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 *; lia. 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.
    revert b l m; induction a as [ | a IHa ]; intros [ | b ] l m; simpl; try discriminate.
    inversion 1; auto.
    intros H.
    inversion H as [ H1 ].
    apply IHa in H1.
    destruct H1; subst; auto.
  Qed.

  Fact list_One_Zero_not a b l : list_repeat One a ++ Zero :: l <> list_repeat One b.
  Proof.
    revert b l; induction a as [ | a IHa ]; intros [ | b ] l; simpl; try discriminate.
    intros H.
    inversion H as [ H1 ].
    apply IHa in H1; auto.
  Qed.

  Fact list_One_inj a b : list_repeat One a = list_repeat One b -> a = b.
  Proof.
    intros H; apply f_equal with (f := @length _) in H; revert H.
    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.
    intros H; revert l m1 H m2.
    intros ? ? [ k l | k ]; inversion 1.
    apply list_One_Zero_inj in H1; destruct H1; subst k0 l1; auto.
    symmetry in H1; apply list_One_Zero_not in H1; tauto.
    apply list_One_Zero_not in H1; tauto.
    apply list_One_inj in H1; subst; auto.
  Qed.

  Fact list_bool_succ_nil l : list_bool_succ nil l -> l = Zero::nil.
  Proof.
    intros H; symmetry; revert H; apply list_bool_succ_fun.
    constructor 2 with (k := 0).
  Qed.

  Fact list_bool_succ_neq : forall l m, list_bool_succ l m -> l <> m.
  Proof.
    intros ? ? [ [|k] l | [|k] ]; discriminate.
  Qed.

  Fact list_bool_succ_neq_nil l : ~ list_bool_succ l nil.
  Proof.
    inversion 1.
    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.
    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.
    intros H.
    generalize (list_bool_next_spec l).
    rewrite H.
    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.
    destruct n as [ | n ].
    simpl; auto.
    replace (S n) with (n+1) by lia.
    rewrite iter_plus; simpl.
    intros H.
    apply list_bool_next_neq_nil in H.
    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 *; lia.
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.
    induction n as [ | n IHn ]; intros l Hl.
    * generalize (list_bool_nat_ge_1 l); lia.
    * 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; lia.
  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.


Theorem list_bool_next_total l : l <> nil -> { n | l = iter list_bool_next (Zero::nil) n }.
Proof.
  induction l as [ | l m Hlm IH ] using list_bool_succ_rect.
  intros []; auto.
  intros Hm.
  destruct (list_bool_choose_sym l) as [ (k & tl & H) | ([|k] & H) ].
  * destruct IH as (n & Hn).
    { subst; destruct k; discriminate. }
    exists (n+1); rewrite iter_plus; simpl.
    rewrite <- Hn.
    generalize (list_bool_next_spec l).
    apply list_bool_succ_fun; auto.
  * exists 0; simpl.
    apply list_bool_succ_fun with (1 := Hlm).
    subst; simpl; constructor 2 with (k := 0).
  * destruct IH as (n & Hn).
    { subst; simpl; discriminate. }
    exists (n+1); rewrite iter_plus; simpl.
    rewrite <- Hn.
    generalize (list_bool_next_spec l).
    apply list_bool_succ_fun; auto.
Qed.