From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationClasses.
From Coq Require Import Lia.
From CoLoR Require Import ListUtil.
Global Existing Instance relation_equivalence_equivalence.

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.

Open Scope signature_scope.
Set Implicit Arguments.

Global Instance eqlistA_per {A} {eqA} {eqA_per: @PER A eqA}:
  PER (eqlistA eqA).

Global Instance List_Setoid {A} `{Setoid A}: Setoid (list A) :=
  {| equiv := eqlistA equiv |}.

Global Instance List_Partial_Setoid {A} `{PartialSetoid A}: PartialSetoid (list A) :=
  {| pequiv := eqlistA pequiv |}.

Global Instance eqlistA_eq_is_eq (A: Type):
  subrelation (eqlistA (@eq A)) (@eq (list A)).

Section INA.

  Global Instance InA_compat_eqlistA {A} `{Setoid A}:
    Proper (equiv ==> eqlistA equiv ==> iff) (InA equiv).

  Lemma InA_app_app A (eqA:relation A): forall x l,
      Proper (eqlistA eqA) l -> InA eqA x l ->
      exists a b, eqlistA eqA (a ++ (x :: nil) ++ b) l.

  Lemma InA_app (A:Type) {SA:Setoid A}: forall (x:A) a b,
      InA equiv x (a ++ b) <-> ((InA equiv x a) \/ (InA equiv x b)).

  Lemma list_app_preserve {A} `{Setoid A}:
    forall (x: A) a1 b1 a2 b2,
      ~ InA equiv x a1 -> ~ InA equiv x b1 ->
      a1 ++ x :: b1 == a2 ++ x :: b2 -> a1 == a2 /\ b1 == b2.

End INA.

Section NoDupA.

  Lemma NoDupA_nil_iff: forall (A: Type) (eqA: A -> A -> Prop),
    NoDupA eqA nil <-> True.

  Lemma NoDupA_cons_iff: forall (A: Type) (eqA: A -> A -> Prop) x q,
      NoDupA eqA (x::q) <-> ~InA eqA x q /\ NoDupA eqA q.

  Global Instance NoDupA_compat {A} `{Setoid A}:
    Proper (eqlistA equiv ==> iff) (NoDupA equiv).

  Lemma NoDupA_app_alt {A} `{Setoid A}:
    forall l1 l2: list A, NoDupA equiv (l1++l2) ->
                          NoDupA equiv l1 /\ NoDupA equiv l2.

End NoDupA.

Section ForallA.

  Context {A: Type} (eqA: relation A).
  Context {eqA_refl: Reflexive eqA}.

  Section FF.

    Context (P: A -> Prop) {P_compat: Proper (eqA ==> iff) P}.

    Lemma Forall_forallA:
      forall (l : list A),
        Forall P l <-> (forall (x : A), InA eqA x l -> P x).

    Definition Forall_hd := Forall_inv.

    Lemma Forall_tl:
      forall a l, Forall P (a :: l) -> Forall P l.

  End FF.

  Global Instance Forall_compat :
    Proper ((eqA ==> iff) ==> (eqlistA eqA) ==> iff) (@Forall A).

  Global Instance Forall_compat_equiv :
    Proper ((eqA ==> iff) ==> (equivlistA eqA) ==> iff) (@Forall A).

  Lemma forall_inv_2:
    forall (P: A -> Prop) (a: A) (l: list A),
      Forall P (a :: l) -> Forall P l.

  Lemma Forall_head_and_tail:
    forall (h: A) t p, Forall p (h :: t) <-> p h /\ Forall p t.

  Lemma forall_app:
    forall (p: A -> Prop) l1 l2,
      Forall p (l1 ++ l2) <-> (Forall p l1) /\ (Forall p l2).

End ForallA.

Section map_compat.

  Context {A: Type} (eqA: relation A).
  Context {B: Type} (eqB: relation B).

  Global Instance map_compat:
    Proper ((eqA ==> eqB) ==> eqlistA eqA ==> eqlistA eqB)
           (@List.map A B).

  Lemma map_eq_locality :
    forall (eqA_refl: Reflexive eqA)
           (eqB_PER: PER eqB)
           (f1: A -> B) (p1: Proper (eqA ==> eqB) f1)
           (f2: A -> B) (p2: Proper (eqA ==> eqB) f2)
           (l1 l2: list A) (el: eqlistA eqA l1 l2),
      (forall a, InA eqA a l1 -> eqB (f1 a) (f2 a)) ->
      eqlistA eqB (map f1 l1) (map f2 l2).

End map_compat.

Section map_compat_equivlist.

  Context {A: Type} `{SA:Setoid A}.
  Context {B: Type} `{SB:Setoid B}.

  Global Instance map_compat_equiv :
    Proper (fequiv ==> equivlistA equiv ==> equivlistA equiv)
           (@List.map A B).

  Lemma InA_map_iff:
    forall (f: A -> B) {f_compat: Proper fequiv f}
           (l: list A) (b: B),
      InA equiv b (map f l) <->
      (exists a : A, (f a) == b /\ InA equiv a l).

End map_compat_equivlist.

Section Existsb_Forallb.

  Variable (A: Type).
  Variable (f: A -> bool)
           (notf: A -> bool)
           (H: forall a, f a = negb (notf a)).

  Lemma existsb_forallb:
    forall l, existsb f l = negb (forallb notf l).

  Lemma forallb_existsb:
    forall l, forallb f l = negb (existsb notf l).

End Existsb_Forallb.

Section filter.

  Context {A: Type} `{SA:Setoid A}.

  Global Instance filter_compat :
    Proper (fequiv ==> eqlistA equiv ==> eqlistA equiv)
           (filter (A:=A)).

  Global Instance filter_compat_equiv :
    Proper (fequiv ==> equivlistA equiv ==> equivlistA equiv)
           (filter (A:=A)).

  Lemma filter_nil:
    forall (f: A -> bool) (l: list A), filter f l = nil
                                       <-> existsb f l = false.

  Lemma filter_nil':
    forall (f: A -> bool) (l: list A),
      filter f l = nil <-> forallb (fun a => negb (f a)) l = true.

  Lemma filter_eq_locality:
    forall (f1 f2: A -> bool) (l1 l2: list A),
      equivlistA equiv l1 l2 ->
      Proper fequiv f1 -> Proper fequiv f2 ->
      (forall a, InA equiv a l1 -> f1 a = f2 a) ->
      equivlistA equiv (filter f1 l1) (filter f2 l2).

  Lemma filter_InA_locality:
    forall (f: A -> bool),
    forall (l: list A),
      (forall x y, x == y -> InA equiv x l -> f x = f y) ->
      forall x,
        InA equiv x (filter f l) <-> InA equiv x l /\ f x = true.

  Lemma filter_NoDupA:
    forall (f: A -> bool) (f_c: Proper pequiv f)
           (l: list A),
      NoDupA equiv l -> NoDupA equiv (filter f l).

  Lemma filter_app_preserve:
    forall (f: A -> bool) (pf: Proper pequiv f),
    forall l l1 x l2 (hl: l == l1 ++ x :: l2)
           (inx1: ~ InA equiv x l1) (inx2: ~ InA equiv x l2) lf1 lf2,
      filter f l == lf1 ++ x :: lf2 ->
      filter f l1 == lf1 /\ filter f l2 == lf2.

End filter.

Section RESTRICTA.

  Definition RestrictA A (eqA:relation A) (P: A -> Prop) a1 a2 :=
    eqA a1 a2 /\ P a1.

  Instance RestrictA_per {A: Type} `{SA:PartialSetoid A}
           {P: A -> Prop} {P_proper: Proper fequiv P}: PER (RestrictA pequiv P).

  Instance RestrictA_per_s {A: Type} `{SA:Setoid A}
           {P: A -> Prop} {P_proper: Proper fequiv P}: PER (RestrictA equiv P).

End RESTRICTA.

Section ConsistentA.

  Context {A: Type} `{SA:Setoid A}.
  Context {B: Type} `{SB:Setoid B}.

  Definition ConsistentA (l: list (A*B)) :=
    forall a1 a2 b1 b2, InA equiv (a1,b1) l ->
                        InA equiv (a2,b2) l ->
                        a1 == a2 -> b1 == b2.

  Global Instance ConsistentA_compat:
    Proper (equivlistA equiv ==> iff) ConsistentA .

End ConsistentA.

Section AssocA.

  Context {A: Type} `{SA: Setoid A}.
  Context `{Adec: Decider equiv}.

  Context {B: Type} `{SB: Setoid B}.

  Fixpoint assocA (x: A) (l: list (A * B)): option B :=
    match l with
    | nil => None
    | (y, v)::q => if Adec x y then Some v else
                     assocA x q end.

  Global Instance assocA_compat:
    Proper fequiv assocA.

  Lemma assocA_none:
    forall (l: list(A * B)) (a: A),
      (assocA a l) == None <->
      forall (b: B), ~ InA equiv (a, b) l.

  Lemma assocA_InA:
    forall (l: list(A*B)) (a: A) (b: B),
      (assocA a l) == (Some b) ->
      InA equiv (a, b) l.

  Lemma InA_AssocA:
    forall (l: list(A*B)) (a: A) (b: B),
      ConsistentA l ->
      (InA equiv (a, b) l <->
       (assocA a l) == (Some b)).

  Global Instance assocA_compat2:
    Proper (equiv ==> RestrictA (equivlistA equiv) ConsistentA ==> equiv)
           assocA.

  Lemma assoc_dec:
    forall (eqB_dec: Decider (equiv (A := B))) (a: A) l,
      {b: B | InA equiv (a, b) l}
      +
      {forall b, ~ (InA equiv (a, b) l)}.

End AssocA.

Section Rev_List.

  Lemma rev_equivlistA {A} `{SA:Setoid A}:
    forall l: list A, equivlistA equiv l (rev l).

  Lemma rev_rev_eqlistA {A} `{SA:Setoid A}:
    forall (l l': list A),
      eqlistA equiv l (rev l') <-> eqlistA equiv (rev l) l'.

  Lemma rev_app_cons {A} `{SA:Setoid A}:
    forall (x: A) (l1 l2: list A),
      rev (l1 ++ x :: l2) == rev l2 ++ x :: rev l1.

End Rev_List.

Section Existsb_InA.

  Lemma existsb_exists_InA {A: Type} `{SA: Setoid A}:
    forall (f : A -> bool) (f_compat: Proper fequiv f)
           (l : list A),
      existsb f l = true <-> (exists x : A, InA equiv x l /\ f x = true).

End Existsb_InA.

Section Forallb_InA.

  Lemma forallb_forall_InA {A: Type} `{SA: Setoid A}:
    forall (f : A -> bool) (f_compat: Proper fequiv f)
           (l : list A),
      forallb f l = true <-> (forall x : A, InA equiv x l -> f x = true).

End Forallb_InA.

Section Existsb_Forallb_compat.

  Global Instance existsb_compat:
    forall A (eqA: relation A),
      Proper ( (eqA ==> eq) ==> (eqlistA eqA) ==> eq) (existsb (A:=A)).

  Global Instance forallb_compat:
    forall A (eqA: relation A),
      Proper ( (eqA ==> eq) ==> (eqlistA eqA) ==> eq) (forallb (A:=A)).

End Existsb_Forallb_compat.

Section Other_forallb.

  Lemma forallb_compat1:
    forall (A: Type) (eqA: A -> A -> Prop) (refl: Reflexive eqA)
           (f1 f2: A -> bool) (EF: (eqA ==> eq) f1 f2)
           (l : list A),
      forallb f1 l = forallb f2 l.

  Global Instance forallb_compat_equiv:
    forall (A : Type) (SA : Setoid A),
      Proper ((equiv ==> eq) ==> equivlistA equiv ==> eq) (forallb (A:=A)).

End Other_forallb.

Section Decidability_on_Lists.

  Lemma eqlistA_dec:
    forall {A: Type} {eqA: relation A},
      Decider eqA -> Decider (eqlistA eqA).

  Lemma equivlistA_dec:
    forall {A: Type} {SA: Setoid A},
      Decider (equiv (A := A)) -> Decider (equivlistA equiv).

End Decidability_on_Lists.

Section Rev.

  Variable (A: Type).

  Lemma rev_intro:
    forall l l': list A, l = l' <-> rev l = rev l'.

  Definition list_rev_destruct:
    forall eqA (eqA_refl: Reflexive eqA) (l:list A),
      {first:list A & {last:A | eqlistA eqA l (first++ last::nil) }}
      + {eqlistA eqA l nil}.

  Global Instance removelast_eqlistA_compat :
    forall eqA, Proper (eqlistA eqA ==> eqlistA eqA) (@removelast A).

End Rev.

Section map_filter.

  Context {A: Type} `{SA: Setoid A}.
  Context {B: Type} `{SB: Setoid B}.

  Section Fixed_fopt.

    Context (fopt: A -> option B).

    Context {fopt_compat: Proper fequiv fopt}.

    Fixpoint map_filter (l: list A) :=
      match l with
        nil => nil
      | a :: q =>
        match fopt a with
          None => map_filter q
        | Some b => b::map_filter q
        end end.

    Lemma InA_map_filter_iff:
      forall (l: list A) (b: B),
        InA equiv b (map_filter l) <->
        (exists a: A, InA equiv a l /\ (fopt a) == (Some b)).

  End Fixed_fopt.

  Global Instance map_filter_compat:
    Proper (fequiv ==> equivlistA equiv ==> equivlistA equiv) map_filter.

  Lemma map_filter_eq_locality:
    forall (f1 f2: A -> option B) (l1 l2: list A),
      equivlistA equiv l1 l2 ->
      Proper fequiv f1 -> Proper fequiv f2 ->
      (forall a, InA equiv a l1 -> f1 a == f2 a) ->
      equivlistA equiv (map_filter f1 l1) (map_filter f2 l2).

  Lemma map_filter_eq_locality_converse:
    Decider (equiv (A := B)) ->
    forall (f1 f2: A -> option B) (l1 l2: list A),
      equivlistA equiv l1 l2 ->
      Proper fequiv f1 -> Proper fequiv f2 ->
      ~ equivlistA equiv (map_filter f1 l1) (map_filter f2 l2) ->
      exists a, InA equiv a l1 /\ ~ f1 a == f2 a.

End map_filter.

Global Instance map_filter_compat_eqlistA:
  forall A B (eqA: relation A) (eqB: relation B),
    Proper ((eqA ==> eqoptionA eqB)
              ==> eqlistA eqA ==> eqlistA eqB) map_filter.

Section EqlistA_Utils.

  Variable (A : Type) (eqA : relation A).

  Lemma l_eqlistA_nil : forall l, eqlistA eqA l nil <-> l = nil.

  Lemma l_eqlistA_cons : forall l1 h2 t2, eqlistA eqA l1 (h2 :: t2) ->
                                          exists h1 t1, l1 = h1 :: t1.

  Lemma cons_eqlistA_cons :
    forall h1 t1 h2 t2, eqlistA eqA (h1 :: t1) (h2 :: t2) <->
                        eqA h1 h2 /\ eqlistA eqA t1 t2.

End EqlistA_Utils.

Global Instance nth_compat (A:Type) (SA:PartialSetoid A) : Proper fequiv (nth (A:=A)).

Ltac lsplit pl :=
  hnf in pl;
  match (type of pl) with
  | (eqlistA ?R (cons ?a1 ?l1) (cons ?a2 ?l2)) =>
    let X := fresh "X" in
    assert (X:=proj1 (cons_eqlistA_cons R a1 l1 a2 l2) pl);
    clear pl;rename X into pl
  | (eqlistA ?R nil nil) => clear pl
  | (eqlistA ?R nil (cons _ _)) =>
    inversion pl
  | (eqlistA ?R (cons _ _) nil) =>
    inversion pl
  end.

Section Stutter.

  Fixpoint stutter A n (l:list A):=
    match l with
      nil => nil
    | i :: q =>
      match n with
        0 => i :: removelast (i::q)
      | S n => i :: stutter n q end end.

  Lemma removelast_length: forall A (l:list A), length (removelast l) = (length l) - 1.

  Lemma stutter_length: forall A n l, length (stutter (A:=A) n l) = length l.

  Lemma removelast_Forall: forall A P (l:list A), Forall P l ->
                                                  Forall P (removelast l).

  Lemma stutter_Forall: forall A P n l,
      Forall P l -> Forall P (stutter (A:=A) n l).

  Lemma stutter_nth_le: forall A a (l:list A) i j,
      i <= j ->
      nth i l a = nth i (stutter j l) a.

  Lemma stutter_nth_gt: forall A a (l:list A) i j,
      j <= i - 1 -> i < length l ->
      nth (i - 1) l a = nth i (stutter j l) a.

  Lemma stutter_nth_gt2: forall A a (l:list A) i j,
      j <= i -> i < length l - 1 ->
      nth i l a = nth (1+i) (stutter j l) a.

  Lemma stutter_last_id:
    forall A (l:list A) j, j = length l - 1 ->
                           stutter j l = l.

  Lemma stutter_app_r:
    forall A (l1 l2:list A) j, j >= length l1 ->
                               stutter j (l1++l2) = l1 ++ stutter (j - length l1) l2.

End Stutter.

Section List_builders.


  Fixpoint uc min len :=
    match len with 0 => nil | S n => min :: uc (min+1) n end.

  Lemma uc_length: forall min len, length (uc min len) = len.


  Fixpoint dc min len :=
    match len with 0 => nil | S n => min+n :: dc min n end.

  Lemma dc_length: forall min len, length (dc min len) = len.


  Fixpoint rep cte len : list nat :=
    match len with 0 => nil | S n => cte :: rep cte n end.

  Lemma rep_length: forall cte len, length (rep cte len) = len.


  Fixpoint repl A (lcte:list A) len : list A :=
    match len with 0 => nil | S n => lcte ++ repl lcte n end.

  Lemma repl_length: forall A lcte len, length (repl (A:=A) lcte len) = len * length lcte.

  Fixpoint flatmap A B (f:A -> list B) l : list B :=
    match l with nil => nil | x::q => f x ++ flatmap f q end.

  Lemma flatmap_length:
    forall A B f l, length (flatmap (A:=A) (B:=B) f l) =
                    fold_right plus 0 (List.map (fun a => length (f a)) l).

  Lemma dc_le: forall min len, Forall (le min) (dc min len).

  Lemma dc_gt: forall min len, Forall (gt (min+len)) (dc min len).

  Lemma dc_nth: forall min len x i, i < len -> nth i (dc min len) x = min + len - i - 1.

  Lemma dc_last: forall min len x, len > 0 -> last (dc min len) x = min.

  Lemma dc_removelast: forall min len,
      len > 0 ->
      removelast (dc min len) = dc (min+1) (len-1).

  Lemma uc_le: forall min len, Forall (le min) (uc min len).

  Lemma uc_gt: forall min len, Forall (gt (min+len)) (uc min len).

  Lemma rep_app: forall x n p, rep x (n+p)=rep x n ++ rep x p.

  Lemma last_cons: forall A x d (l:list A), l <> nil -> last (x::l) d = last l d.

  Lemma last_app: forall A d (l1 l2:list A), l2 <> nil -> last (l1++l2) d=last l2 d.

End List_builders.

Section App.

  Context {A: Type} `{SA: PartialSetoid A}.

  Lemma app_proper_l:
    forall (a b: list A), Proper pequiv (a ++ b) -> Proper pequiv a.

  Lemma app_proper_r:
    forall (a b: list A), Proper pequiv (a ++ b) -> Proper pequiv b.

  Lemma app_cut:
    forall (l1 l2 m1 m2: list A),
      l1 ++ l2 =~= m1 ++ m2 ->
      (exists x, l1 =~= m1 ++ x /\ m2 =~= x ++ l2) \/
      (exists y, m1 =~= l1 ++ y /\ l2 =~= y ++ m2).

End App.

Close Scope signature_scope.
Unset Implicit Arguments.