Require Import Bool.
Require Import List.
Require Import String.
Require Import Sumbool.
Require Import Lia.
Require Import Permutation.
Require Import Morphisms.
Require Import Setoid.
Require Import RelationClasses.
Require Import EquivDec.
Require Import Equivalence.
Require Import Peano_dec.
Require Import ZArith.
Require Import Zdigits.
Require Import Znat.
Require Import Recdef.
Require Import Compare_dec.

Create HintDb fml.

Ltac qauto := auto with fml.
Ltac qeauto := eauto with fml.
Ltac qtrivial := trivial with fml.

Section CoqLibAdd.

Properties of Booleans

  
  Section Booleans.
    
    Lemma andb_true_inversion:
      forall b1 b2 : bool,
        andb b1 b2 = true <-> b1 = true /\ b2 = true.

    Lemma four_cases {A:Type} :
      forall (p1 p2: A -> bool) (a:A),
        ((((p1 a) = true) /\ ((p2 a) = true)) \/
         (((p1 a) = true) /\ ((p2 a) = false))) \/
        ((((p1 a) = false) /\ ((p2 a) = true)) \/
         (((p1 a) = false) /\ ((p2 a) = false))).

    Lemma two_cases {A:Type} :
      forall (p: A -> bool) (a:A),
        ((p a) = true) \/ ((p a) = false).

    Lemma notand p q:
      ~(p \/ q) -> ~p /\ ~q.

    Lemma eq_implies_pred {A:Type} :
      forall (p:A -> bool), forall (x1 x2:A),
          x1 = x2 -> (p x1) = (p x2).
    
    Lemma not_pred_implies_neq {A:Type}:
      forall (p:A -> bool), forall (x1 x2:A),
          (p x1) <> (p x2) -> x1 <> x2.

  End Booleans.

Properties of In

  Section In.
    Context {A:Type}.

    Lemma In_app (x:A) (l1 l2:list A):
      In x (l1 ++ l2) -> In x l1 \/ In x l2.

    Lemma In_app_comm (v:A) (l1 l2:list A) :
      In v (l1++l2) -> In v (l2++l1).
    
    Lemma In_app_iff (v:A) (l1 l2:list A) :
      In v (l1++l2) <-> In v (l2++l1).
    
    Lemma find_In {f l} {b:A} : find f l = Some b -> In b l.

    Lemma find_correct {f l} {b:A} : find f l = Some b -> f b = true.
    
    Lemma app_or_in (x:A) (l1 l2: list A) :
      In x (l1 ++ l2) -> In x l1 \/ In x l2.
    
    Lemma app_or_in_iff (x:A) (l1 l2: list A) :
      In x (l1 ++ l2) <-> In x l1 \/ In x l2.

    Lemma in_or_not (eqd:forall a a':A, {a=a'} + {a<>a'}) (l:list A) a:
      (In a l) \/ ~(In a l).

    Lemma nin_app_or (x:A) a b :
      (~ In x (a ++ b)) <-> (~ In x a /\ ~ In x b).

    Lemma in_in_app_false {l l1 l2} :
      (forall x:A,
          In x l ->
          In x (l1 ++ l2) -> False) ->
      ((forall x,
           In x l ->
           In x l1 -> False) /\
       (forall x,
           In x l ->
           In x l2 -> False)).

    Lemma in_in_cons_app_false {v l l1 l2} :
      (forall x:A,
          In x l ->
          v = x \/ In x (l1 ++ l2) -> False) ->
      ((forall x,
           In x l ->
           In x (l1) -> False) /\
       (forall x,
           In x l ->
           In x (l2) -> False) /\
       ~ (In v l)).

    Lemma in_in_cons_cons_app_app_false {v v0 l l1 l2 l3} :
      (forall x:A,
          In x l ->
          v = x \/ v0 = x \/ In x (l1 ++ l2 ++ l3) -> False) ->
      ((forall x,
           In x l ->
           In x l1 -> False) /\
       (forall x,
           In x l ->
           In x l2 -> False) /\
       (forall x,
           In x l ->
           In x l3 -> False) /\
       ~ (In v l) /\
       ~ (In v0 l)).

    Lemma forall_in_dec P (l:list A)
          (dec:forall x, In x l -> {P x} + {~ P x}):
      {forall x, In x l -> P x} + {~ forall x, In x l -> P x}.

    Lemma exists_in_dec P (l:list A)
          (dec:forall x, In x l -> {P x} + {~ P x}):
      {exists x, In x l /\ P x} + {~ exists x, In x l /\ P x}.

    Lemma exists_nforall_in_dec P (l:list A)
          (dec:forall x, In x l -> {P x} + {~ P x}):
      {exists x, In x l /\ P x} + {forall x, In x l -> ~P x}.

    Lemma existsb_ex (f : A -> bool) (l : list A) :
      existsb f l = true -> {x : A | In x l /\ f x = true}.
    
    Lemma forall_in_weaken (P Q:A -> Prop) l:
      (forall x : A, P x \/ In x l -> Q x)
      -> (forall x : A, In x l -> Q x).
    
  End In.

Properties of Forallt

  Section Forallt.
    Inductive Forallt {A : Type} (P : A -> Type) : list A -> Type :=
      Forallt_nil : Forallt P nil
    | Forallt_cons : forall (x : A) (l : list A),
        P x -> Forallt P l -> Forallt P (x :: l).

    Hint Constructors Forallt : fml.

    Lemma list_Forallt_eq_dec {A:Type}:
      forall (c l: list A),
        Forallt (fun x : A => forall y : A, {x = y} + {x <> y}) c -> {c = l} + {c <> l}.

    Lemma forallt_impl {A} {P1 P2:A->Type} {l:list A} :
      Forallt P1 l -> Forallt (fun x => P1 x -> P2 x) l -> Forallt P2 l.

    Lemma forallt_weaken {A} P : (forall x:A, P x) -> forall l, Forallt P l.

    Lemma Forallt_inv: forall A P (a:A) l, Forallt P (a :: l) -> P a.
    
    Lemma Forallt_inv2: forall A P (a:A) l, Forallt P (a :: l) -> Forallt P l.

    Lemma Forallt_In {A:Type} {P:A->Type} {r} {eq:EqDec A eq}:
      Forallt P r -> forall a, In a r -> P a.
    
    Lemma Forall_app {A} (P:A->Prop) (l1 l2:list A):
      Forall P l1 -> Forall P l2 ->
      Forall P (l1 ++ l2).

    Lemma Forall_app_inv {A : Type} {P : A -> Prop} (l1 l2 : list A) :
      Forall P (l1 ++ l2) -> Forall P l1 /\ Forall P l2.

    Lemma Forall_map {A B} P (f:A->B) l:
      Forall P (map f l) <->
      Forall (fun x => P (f x)) l.
    

    Lemma Forall_impl_in {A} {P Q : A -> Prop} {l} :
      (forall a, In a l -> P a -> Q a) ->
      Forall P l -> Forall Q l.
    
    Lemma Forallt_Forall {A:Prop} (P:A->Prop) (l:list A) :
      Forallt P l -> Forall P l.

  End Forallt.

Properties of forallb

  Section forallb.

    Lemma forallb_ext {A} f1 f2 (l:list A) :
      (forall x, In x l -> f1 x = f2 x) ->
      forallb f1 l = forallb f2 l.

    Lemma forallb_incl {A} f (l1 l2 : list A) :
      incl l1 l2 ->
      forallb f l2 = true ->
      forallb f l1 = true.

    Lemma forallb_app {A} (f:A->bool) l1 l2 :
      forallb f (l1 ++ l2) = true <->
      (forallb f l1 = true /\ forallb f l2 = true).
    
    Lemma forallb_map {A B} f (mf:A->B) m : forallb f (map mf m) = forallb ((fun x => f (mf x))) m.

    Lemma existsb_not_forallb {A} f (l:list A)
      : existsb f l = negb (forallb (fun x => negb (f x)) l).

    Lemma forallb_not_existb {A} f (l:list A)
      : forallb f l = negb (existsb (fun x => negb (f x)) l).

    Lemma map_eq {A B} {f g:A->B} {l} :
      Forall (fun x => f x = g x) l ->
      map f l = map g l.

    Lemma map_id {A} (c:list A) :
      map id c = c.

    Lemma map_eq_id {A} {f:A->A} {l} :
      Forall (fun x => f x = x) l ->
      map f l = l.
    
    Lemma map_cons {A B:Type} (f:A->B) (l:list A) (a:A) :
      map f (a::l) = (f a)::map f l.

    Lemma map_eq_cons {A B} (f : A -> B) (l:list A) b l' :
      map f l = b::l' ->
      {a : A & {ls:list A | l = a::ls /\f a = b /\ map f ls = l'}}.

  End forallb.

Properties of pairs

  Section Pairs.

    Lemma pair_eq_dec {A B:Type} (a1:A) (b1:B) (a2:A) (b2:B) :
      {a1 = a2} + {a1 <> a2} ->
      {b1 = b2} + {b1 <> b2} ->
      {(a1, b1) = (a2, b2)} + {(a1, b1) <> (a2, b2)}.

    Global Instance string_eqdec : EqDec String.string eq := String.string_dec.
    Global Instance pair_eqdec {A B} `{EqDec A eq} `{EqDec B eq} : EqDec (prod A B) eq.

    Global Instance option_eqdec {A:Type} `{EqDec A eq}: EqDec (option A) eq.

  End Pairs.

Arithmetics

Natural numbers

  
  Section Nutil.
    Lemma min_zero:
      forall (n1 n2:nat), min n1 (S n2) = 0 -> n1 = 0.

    Lemma min_against_one:
      forall (n:nat), min n 1 = 0 \/ min n 1 = 1.

    Lemma compare_either (n1 n2:nat):
      (n1 <= n2) \/ (n2 <= n1).
    
    Lemma min_one_yields_one:
      forall n:nat, min n 1 = 1 -> 1 <= n.

    Lemma fold_left_arith_dist1 {A} (x0:nat) (l:list A) (f:A -> nat):
      fold_left (fun (x:nat) (y:A) => (f y) + x) l x0 =
      (fold_left (fun (x:nat) (y:A) => (f y) + x) l 0) + x0.
    
    Lemma fold_left_arith_dist2 {A} (x0 n0:nat) (l:list A) (f:A -> nat):
      fold_left (fun (x:nat) (y:A) => n0 * (f y) + x) l x0 =
      n0 * (fold_left (fun (x:nat) (y:A) => (f y) + x) l 0) + x0.

    Lemma fold_left_arith_dist3 {A} (x0 n0:nat) (l:list A) (f:A -> nat):
      n0 * (fold_left (fun (x:nat) (y:A) => (f y) + x) l 0) + x0 =
      n0 * (fold_left (fun (x:nat) (y:A) => x + (f y)) l 0) + x0.

    Lemma fold_left_arith_dist4 {A} (x0 n0:nat) (l:list A) (f:A -> nat):
      fold_left (fun (x:nat) (y:A) => n0 * (f y) + x) l x0 =
      n0 * (fold_left (fun (x:nat) (y:A) => x + (f y)) l 0) + x0.

  End Nutil.

Integers

  Section Zutil.
    Open Scope Z_scope.
    
    Definition ZToSignedNat (z:Z) : (bool*nat) :=
      match (Z.sgn z) with
      | -1 => (false,(Z.to_nat z))
      | _ => (true, (Z.to_nat z))
      end.
    
    Lemma pos_succ_inv (n1 n2:positive):
      (Pos.succ n1 = Pos.succ n2 -> n1 = n2).
    
    Lemma Pos_of_nat_inv (n1 n2:nat) :
      Pos.of_nat (S n1) = Pos.of_nat (S n2) -> n1 = n2.
    
    Lemma of_nat_inv (n1 n2:nat) :
      Z.of_nat n1 = Z.of_nat n2 -> n1 = n2.
    
    Lemma pos_succ_nat_inv (n1 n2:nat) :
      Pos.of_succ_nat n1 = Pos.of_succ_nat n2 -> n1 = n2.

    Global Instance Z_eqdec : EqDec Z eq.

  End Zutil.

Iterator on lists

  
  Section Iter.
    Lemma repeat_plus {A} (x:A) (n1 n2:nat) :
      repeat x (n1+n2) = repeat x n1 ++ repeat x n2.

    Fixpoint iter {A} (f:A->A) (iterations:nat) (a:A)
      := match iterations with
         | 0 => a
         | S n => iter f n (f a)
         end.

    Lemma iter_fold_left_list {A B} (f:A->A) (l:list B) (a:A)
      : iter f (List.length l) a = fold_left (fun x y => f x) l a.

    Lemma iter_fold_left_repeat {A} (f:A->A) (iterations:nat) (a:A)
      : iter f iterations a = fold_left (fun x y => f x) (repeat 0 iterations) a.

    Lemma iter_fold_right_list {A B} (f:A->A) (l:list B) (a:A)
      : iter f (List.length l) a = fold_right (fun x y => f y) a l.

    Lemma iter_plus {A} (f:A->A) (iterations1 iterations2:nat) (a:A) :
      iter f (iterations1+iterations2) a = iter f iterations2 (iter f iterations1 a).

    Lemma iter_trans {A} (R:relation A) {pre:PreOrder R} f
          (pf:forall x, R x (f x)) (iterations:nat) a :
      R a (iter f iterations a).

  End Iter.

Iterator with a cost functions

  Section Cost.

    Context {A:Type}.
    Function iter_cost (optim: A -> A) (cost: A -> nat) (p: A) { measure cost p } :=
      let p' := optim p in
      if lt_dec (cost p') (cost p)
      then iter_cost optim cost p'
      else p.

    Lemma iter_cost_trans (R:relation A) {pre:PreOrder R} f
          (pf:forall x, R x (f x)) (cost:A->nat) a :
      R a (iter_cost f cost a).

  End Cost.

Assertion

  
  Section Holds.
    
    Definition is_true {A B} (x:{A}+{B}) : bool :=
      Eval vm_compute in (if x then true else false).

    Definition holds {A B} (x:{A}+{B}) : Prop :=
      is_true x = true.
  End Holds.

  Lemma compose_inj {A B C} (f:B->C) (g:A->B) :
    (forall x y, f x = f y -> x = y) ->
    (forall x y, g x = g y -> x = y) ->
    (forall x y, f (g x) = f (g y) -> x = y).

  Lemma sumbool_and {P Q} : {P} + {~ P} -> {Q} + {~ Q} -> {P /\ Q} + {~ (P /\ Q)}.

  Lemma eqdec_neq {A} `{EqDec A eq} (x y:A) : {x <> y} + {~ x <> y}.

  Section equiv.
    
    Lemma Equivalence_by_iff {A} (R1 R2:A->A->Prop):
      (forall a b, R1 a b <-> R2 a b) ->
      Equivalence R1 <-> Equivalence R2.

    Lemma EqDec_by_iff {A} (R1 R2:A->A->Prop)
          {equiv1:Equivalence R1} {equiv2:Equivalence R2} :
      (forall a b, R1 a b <-> R2 a b) ->
      EqDec A R1 -> EqDec A R2.

    Lemma EqDec_by_iff' {A} (R1 R2:A->A->Prop)
          {equiv1:Equivalence R1} {equiv2:Equivalence R2} :
      (forall a b, R1 a b <-> R2 a b) ->
      EqDec A R2 -> EqDec A R1.

    Lemma Equivalence_pullback {A B} (R:B->B->Prop) (f:A->B):
      Equivalence R ->
      Equivalence (fun x y => R (f x) (f y)).
          
  End equiv.
End CoqLibAdd.

Tactics

Ltac dest_eqdec :=
  match goal with
  | [|- context [eq_nat_dec ?x ?y]] => destruct (eq_nat_dec x y)
  | [H: context [eq_nat_dec ?x ?y] |- _] => destruct (eq_nat_dec x y)
                                                     
  | [|- context [@equiv_dec ?a ?b ?c ?d ?x ?y]] => destruct (@equiv_dec a b c d x y)
  | [H: context [@equiv_dec ?a ?b ?c ?d ?x ?y] |- _] => destruct (@equiv_dec a b c d x y)
  end; unfold Equivalence.equiv, RelationClasses.complement in *; try subst.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
      set (x := name); move_to_top x
    | assert_eq x name; move_to_top x
    | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.


Ltac notHyp P :=
  match goal with
  | [ _ : P |- _ ] => fail 1
  | _ => idtac
  end.

Ltac extend P :=
  let t := type of P in
  notHyp t; generalize P; intro.

Ltac match_destr
  := match goal with [|- context [match ?x with _ => _ end]] => destruct x end; trivial; try discriminate.

Ltac match_destr_in H
  := match type of H with context [match ?x with _ => _ end] => destruct x end; trivial; try discriminate.

Ltac match_case
  := match goal with [|- context [match ?x with _ => _ end]] => case_eq x end; trivial; try discriminate.

Ltac match_case_in H
  := match type of H with context [match ?x with _ => _ end] => case_eq x end; trivial; try discriminate.

Ltac match_option
  := let eqq := fresh "eqq" in
     match goal with
       [|- context [match ?x with | Some _ => _ | None => _ end]] =>
       case_eq x end; [ intros ? eqq | intros eqq]; try rewrite eqq;
     trivial; try discriminate.

Ltac match_option_in H
  := let eqq := fresh "eqq" in
     match type of H with
       context [match ?x with | Some _ => _ | None => _ end] =>
       case_eq x end; [ intros ? eqq | intros eqq]; rewrite eqq in H;
     trivial; try discriminate.


Ltac cut_to H :=
  match type of H with
  | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> _ -> ?b => cut (b); [clear H; intros H|apply H]
  | _ -> ?b => cut (b); [clear H; intros H|apply H]
  end.

Ltac invcs H := inversion H; clear H; try subst.

Class ToString (A:Type)
  := {
      toString (a:A) : string
    }.

Ltac string_eqdec_to_equiv :=
  replace string_eqdec with (equiv_dec (EqDec:=string_eqdec)) in * by trivial.

Ltac string_dec_to_equiv :=
  replace string_dec with (equiv_dec (EqDec:=string_dec)) in * by trivial.