Require Import Coq.Arith.EqNat.
Require Import Coq.Relations.Relations.
Require Import Coq.Sorting.Permutation.

Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.

Require Import VST.msl.Coqlib2.
Require Export VST.msl.eq_dec.

Lemma max_two_power_nat: forall n1 n2, Z.max (two_power_nat n1) (two_power_nat n2) = two_power_nat (Nat.max n1 n2).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: @eq Z (Z.max (two_power_nat n1) (two_power_nat n2)) (two_power_nat (Nat.max n1 n2)) *)
  rewrite !two_power_nat_two_p.
(* Goal: @eq Z (Z.max (two_p (Z.of_nat n1)) (two_p (Z.of_nat n2))) (two_p (Z.of_nat (Nat.max n1 n2))) *)
  pose proof Zle_0_nat n1; pose proof Zle_0_nat n2.
(* Goal: @eq Z (Z.max (two_p (Z.of_nat n1)) (two_p (Z.of_nat n2))) (two_p (Z.of_nat (Nat.max n1 n2))) *)
  rewrite Nat2Z.inj_max.
(* Goal: @eq Z (Z.max (two_p (Z.of_nat n1)) (two_p (Z.of_nat n2))) (two_p (Z.max (Z.of_nat n1) (Z.of_nat n2))) *)
  forget (Z.of_nat n1) as m1; forget (Z.of_nat n2) as m2.
(* Goal: iff (Z.divide (Z.max m1 m2) m) (and (Z.divide m1 m) (Z.divide m2 m)) *)
  destruct (Z_le_dec m1 m2).
  + rewrite (Z.max_r m1 m2) by omega.
(* Goal: @eq Z (Z.max (two_p m1) (two_p m2)) (two_p m2) *)
    apply Z.max_r.
(* Goal: Z.le (two_p m2) (two_p m1) *)
    apply two_p_monotone; omega.
  + rewrite (Z.max_l m1 m2) by omega.
(* Goal: @eq Z (Z.max (two_p m1) (two_p m2)) (two_p m1) *)
    apply Z.max_l.
(* Goal: Z.le (two_p m2) (two_p m1) *)
    apply two_p_monotone; omega.
Qed.

Lemma Z_max_two_p: forall m1 m2, (exists n, m1 = two_power_nat n) -> (exists n, m2 = two_power_nat n) -> (exists n, Z.max m1 m2 = two_power_nat n).
Proof.
(* Goal: forall (m1 m2 : Z) (_ : @ex nat (fun n : nat => @eq Z m1 (two_power_nat n))) (_ : @ex nat (fun n : nat => @eq Z m2 (two_power_nat n))), @ex nat (fun n : nat => @eq Z (Z.max m1 m2) (two_power_nat n)) *)
  intros ? ? [? ?] [? ?].
(* Goal: @eq X x y *)
(* Goal: @eq X x y *)
  subst.
(* Goal: @ex nat (fun n : nat => @eq Z (Z.max (two_power_nat x) (two_power_nat x0)) (two_power_nat n)) *)
  rewrite max_two_power_nat.
(* Goal: @ex nat (fun n : nat => @eq Z (two_power_nat (Nat.max x x0)) (two_power_nat n)) *)
  eexists; reflexivity.
Qed.

Lemma power_nat_divide: forall n m, two_power_nat n <= two_power_nat m -> Z.divide (two_power_nat n) (two_power_nat m).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: Z.divide (two_power_nat n) (two_power_nat m) *)
  repeat rewrite two_power_nat_two_p in *.
(* Goal: Z.divide (two_p (Z.of_nat n)) (two_p (Z.of_nat m)) *)
  unfold Z.divide.
(* Goal: @ex Z (fun z : Z => @eq Z (two_p (Z.of_nat m)) (Z.mul z (two_p (Z.of_nat n)))) *)
  exists (two_p (Z.of_nat m - Z.of_nat n)).
  assert ((Z.of_nat m) = (Z.of_nat m - Z.of_nat n) + Z.of_nat n) by omega.
(* Goal: @eq Z (two_p (Z.of_nat m)) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
  rewrite H0 at 1.
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
  assert (Z.of_nat m >= 0) by omega.
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
  assert (Z.of_nat n >= 0) by omega.
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
  assert (Z.of_nat n <= Z.of_nat m).
(* Goal: Z.le (Z.of_nat n) (Z.of_nat m) *)
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
    destruct (Z_le_gt_dec (Z.of_nat n) (Z.of_nat m)).
(* Goal: Z.le (Z.of_nat n) (Z.of_nat m) *)
(* Goal: Z.le (Z.of_nat n) (Z.of_nat m) *)
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
    exact l.
(* Goal: Z.le (Z.of_nat n) (Z.of_nat m) *)
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
    assert (Z.of_nat m < Z.of_nat n) by omega.
(* Goal: Z.le (Z.of_nat n) (Z.of_nat m) *)
(* Goal: @eq Z (two_p (Z.add (Z.sub (Z.of_nat m) (Z.of_nat n)) (Z.of_nat n))) (Z.mul (two_p (Z.sub (Z.of_nat m) (Z.of_nat n))) (two_p (Z.of_nat n))) *)
    assert (two_p (Z.of_nat m) < two_p (Z.of_nat n)) by (apply two_p_monotone_strict; omega).
(* Goal: le n n *)
    omega.
(* Goal: le n n *)
  apply (two_p_is_exp (Z.of_nat m - Z.of_nat n) (Z.of_nat n)); omega.
Qed.

Lemma power_nat_divide_ge: forall n m: Z,
  (exists N, n = two_power_nat N) ->
  (exists M, m = two_power_nat M) ->
  (n >= m <-> (m | n)).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
  destruct H, H0.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  split; intros.
  + subst.
    apply power_nat_divide.
(* Goal: le n n *)
    omega.
  + destruct H1 as [k ?].
    rewrite H1.
(* Goal: not (@eq Z x Z0) *)
    pose proof two_power_nat_pos x0.
    pose proof two_power_nat_pos x.
    assert (k > 0).
(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
    {
      eapply Zmult_gt_0_reg_l.
      + exact H2.
      + rewrite <- H0, Z.mul_comm; omega.
    } 
    rewrite <- (Z.mul_1_l m) at 2.
(* Goal: le n n *)
    apply Zmult_ge_compat_r; omega.
Qed.

Lemma power_nat_divide_le: forall n m: Z,
  (exists N, n = two_power_nat N) ->
  (exists M, m = two_power_nat M) ->
  (m <= n <-> (m | n)).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: iff (Z.le m n) (Z.divide m n) *)
  rewrite <- power_nat_divide_ge; auto.
(* Goal: le n n *)
  omega.
Qed.

Lemma two_p_max_divide: forall m1 m2 m, (exists n, m1 = two_power_nat n) -> (exists n, m2 = two_power_nat n) -> ((Z.max m1 m2 | m) <-> (m1 | m) /\ (m2 | m)).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: iff (Z.divide (Z.max m1 m2) m) (and (Z.divide m1 m) (Z.divide m2 m)) *)
  destruct (Z_le_dec m1 m2).
  + rewrite Z.max_r by omega.
(* Goal: iff (Z.divide m2 m) (and (Z.divide m1 m) (Z.divide m2 m)) *)
    rewrite power_nat_divide_le in l by auto.
(* Goal: iff (Z.divide m2 m) (and (Z.divide m1 m) (Z.divide m2 m)) *)
    pose proof Zdivides_trans m1 m2 m.
(* Goal: iff (@eq bool true true) (@eq (list A) (@nil A) (@nil A)) *)
    tauto.
  + rewrite Z.max_l by omega.
(* Goal: le n n *)
    assert (m2 <= m1) by omega.
(* Goal: iff (Z.divide m1 m) (and (Z.divide m1 m) (Z.divide m2 m)) *)
    rewrite power_nat_divide_le in H1 by auto.
(* Goal: iff (Z.divide m1 m) (and (Z.divide m1 m) (Z.divide m2 m)) *)
    pose proof Zdivides_trans m2 m1 m.
(* Goal: iff (@eq bool true true) (@eq (list A) (@nil A) (@nil A)) *)
    tauto.
Qed.

Lemma two_p_max_1: forall m1 m2, (exists n, m1 = two_power_nat n) -> (exists n, m2 = two_power_nat n) -> (Z.max m1 m2 = 1 <-> m1 = 1 /\ m2 = 1).
Proof.
(* Goal: forall (m1 m2 : Z) (_ : @ex nat (fun n : nat => @eq Z m1 (two_power_nat n))) (_ : @ex nat (fun n : nat => @eq Z m2 (two_power_nat n))), iff (@eq Z (Z.max m1 m2) (Zpos xH)) (and (@eq Z m1 (Zpos xH)) (@eq Z m2 (Zpos xH))) *)
  assert (forall x, (exists n : nat, x = two_power_nat n) -> (x = 1 <-> (x | 1))).
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  + intros.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
    split; intros.
(* Goal: @eq X x y *)
(* Goal: @eq X x y *)
    - subst.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
      exists 1; auto.
    - rewrite <- power_nat_divide_le in H0 by (auto; exists 0%nat; auto).
(* Goal: @eq Z x (Zpos xH) *)
      destruct H as [n ?]; subst x.
(* Goal: @eq Z (two_power_nat n) (Zpos xH) *)
      pose proof two_power_nat_pos n.
(* Goal: le n n *)
      omega.
  + intros m1 m2 Hm1 Hm2.
(* Goal: iff (@eq Z (Z.max m1 m2) (Zpos xH)) (and (@eq Z m1 (Zpos xH)) (@eq Z m2 (Zpos xH))) *)
    pose proof Z_max_two_p _ _ Hm1 Hm2 as Hmax.
(* Goal: iff (@eq Z (Z.max m1 m2) (Zpos xH)) (and (@eq Z m1 (Zpos xH)) (@eq Z m2 (Zpos xH))) *)
    rewrite (H _ Hm1), (H _ Hm2), (H _ Hmax).
(* Goal: iff (Z.divide (Z.max m1 m2) (Zpos xH)) (and (Z.divide m1 (Zpos xH)) (Z.divide m2 (Zpos xH))) *)
    apply two_p_max_divide; auto.
Qed.

Lemma two_power_nat_0: forall x, (exists n, x = two_power_nat n) -> x <> 0.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: not (@eq Z x Z0) *)
  destruct H.
(* Goal: not (@eq Z x Z0) *)
  pose proof two_power_nat_pos x0.
(* Goal: le n n *)
  omega.
Qed.

Hint Rewrite andb_true_iff: align.
Hint Rewrite <- Zle_is_le_bool: align.
Hint Rewrite Z.eqb_eq: align.
Hint Rewrite power_nat_divide_le using (auto with align): align.
Hint Rewrite Z.mod_divide using (apply two_power_nat_0; auto with align): align.
Hint Rewrite two_p_max_divide using (auto with align): align.
Hint Rewrite two_p_max_1 using (auto with align): align.
Hint Resolve Z_max_two_p: align.

Lemma Z_of_nat_ge_O: forall n, Z.of_nat n >= 0.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
Proof. intros.
(* Goal: Z.ge (Z.of_nat n) Z0 *)
change 0 with (Z.of_nat O).
(* Goal: le n n *)
apply inj_ge. clear; omega.
Qed.

Lemma nth_error_nth:
  forall A (al: list A) (z: A) i, (i < length al)%nat -> nth_error al i = Some (nth i al z).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros. revert al H; induction i; destruct al; simpl; intros; auto; try omega.
(* Goal: le n n *)
apply IHi. omega.
Qed.

Lemma nat_of_Z_eq: forall i, nat_of_Z (Z_of_nat i) = i.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.
(* Goal: @eq nat (nat_of_Z (Z.of_nat i)) i *)
apply inj_eq_rev.
(* Goal: @eq Z (Z.of_nat (nat_of_Z (Z.of_nat i))) (Z.of_nat i) *)
rewrite nat_of_Z_eq; auto.
(* Goal: le n n *)
omega.
Qed.

Lemma nth_error_length:
(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
  forall {A} i (l: list A), nth_error l i = None <-> (i >= length l)%nat.
Proof.
(* Goal: forall (A : Type) (i : nat) (l : list A), iff (@eq (option A) (@nth_error A l i) (@None A)) (ge i (@Datatypes.length A l)) *)
induction i; destruct l; simpl; intuition.
(* Goal: @eq (option A) (@Some A a) (@None A) *)
(* Goal: ge (S i) (S (@Datatypes.length A l)) *)
(* Goal: @eq (option A) (@nth_error A l i) (@None A) *)
inv H.
(* Goal: @eq (option A) (@Some A a) (@None A) *)
(* Goal: ge (S i) (S (@Datatypes.length A l)) *)
(* Goal: @eq (option A) (@nth_error A l i) (@None A) *)
inv H.
(* Goal: le n n *)
rewrite IHi in H. omega.
(* Goal: le n n *)
rewrite IHi. omega.
Qed.

Lemma prop_unext: forall P Q: Prop, P=Q -> (P<->Q).
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
Proof. intros. subst; split; auto. Qed.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Lemma list_norepet_In_In: forall {K X} a x y (l:list (K*X)),
  list_norepet (map (@fst K X) l) -> In (a, x) l -> In (a, y) l -> x = y.
Proof.
(* Goal: forall (K X : Type) (a : K) (x y : X) (l : list (prod K X)) (_ : @list_norepet K (@map (prod K X) K (@fst K X) l)) (_ : @In (prod K X) (@pair K X a x) l) (_ : @In (prod K X) (@pair K X a y) l), @eq X x y *)
  induction l; intros N Ix Iy.
   - inv Ix.
   - simpl in N; inv N.
(* Goal: @eq X x y *)
     destruct Ix.
     + subst.
(* Goal: @eq X x y *)
       simpl in Iy; destruct Iy as [|Iy]; [congruence|].
(* Goal: iff (@eq bool true true) (@eq (list A) (@nil A) (@nil A)) *)
       exfalso; apply (in_map (@fst K X)) in Iy; tauto.
     + simpl in Iy; destruct Iy as [|Iy].
(* Goal: @eq X x y *)
(* Goal: @eq X x y *)
       subst. exfalso; apply (in_map (@fst K X)) in H; tauto.
(* Goal: @eq X x y *)
       apply IHl; auto.
Qed.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Inductive sublist {A} : list A -> list A -> Prop :=
| sublist_nil : sublist nil nil
| sublist_cons a l1 l2 : sublist l1 l2 -> sublist (a :: l1) (a :: l2)
| sublist_drop a l1 l2 : sublist l1 l2 -> sublist l1 (a :: l2).

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Lemma sublist_In {A} (a : A) l1 l2 : sublist l1 l2 -> In a l1 -> In a l2.
Proof.
(* Goal: forall (_ : @sublist A l1 l2) (_ : @In A a l1), @In A a l2 *)
  intros S; induction S; intros I.
  - inversion I.
  - simpl in I; destruct I.
(* Goal: @In A a (@cons A a0 l2) *)
(* Goal: @In A a (@cons A a0 l2) *)
    subst; left; auto.
(* Goal: @In A a (@cons A a0 l2) *)
    right; auto.
  - right; auto.
Qed.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Lemma sublist_norepet {A} (l1 l2 : list A) : sublist l1 l2 -> list_norepet l2 -> list_norepet l1.
Proof.
(* Goal: forall (_ : @sublist A l1 l2) (_ : @list_norepet A l2), @list_norepet A l1 *)
  intros S; induction S; intros N; auto.
  - inversion N; subst; constructor; auto.
(* Goal: not (@In A a l1) *)
    pose proof sublist_In a l1 l2; auto.
  - inversion N; auto.
Qed.

Require Import Coq.Sets.Ensembles.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Definition Ensemble_join {A} (X Y Z: Ensemble A): Prop :=
  (forall a, Z a <-> X a \/ Y a) /\ (forall a, X a -> Y a -> False).

Require Coq.Logic.ConstructiveEpsilon.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Lemma decidable_countable_ex_sig {A} (f : nat -> A)
      (Hf : forall a, exists n, a = f n)
      (P : A -> Prop)
      (Pdec : forall x, {P x} + {~ P x}) :
(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
  (exists x : A, P x) -> {x : A | P x}.
Proof.
(* Goal: forall _ : @ex A (fun x : A => P x), @sig A (fun x : A => P x) *)
  intros E.
(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
  cut ({n | P (f n)}). intros [n Hn]; eauto.
(* Goal: @sig nat (fun n : nat => P (f n)) *)
  apply ConstructiveEpsilon.constructive_indefinite_ground_description_nat.
(* Goal: forall n : nat, sumbool (P (f n)) (not (P (f n))) *)
(* Goal: @ex nat (fun n : nat => P (f n)) *)
  intro; apply Pdec.
(* Goal: @ex nat (fun n : nat => P (f n)) *)
  destruct E as [x Hx].
  destruct (Hf x) as [n ->].
(* Goal: @ex nat (fun n : nat => P (f n)) *)
  eauto.
Qed.

(** Additions to [if_tac]: when mature, move these upstream *)

Tactic Notation "if_tac" "eq:" simple_intropattern(E) :=
  match goal with
    |- context [if ?a then _ else _] =>
    destruct a as [?H | ?H] eqn:E
  end.

Tactic Notation "if_tac" simple_intropattern(H) "eq:" simple_intropattern(E):=
  match goal with
    |- context [if ?a then _ else _] =>
    destruct a as H eqn:E
  end.

Tactic Notation "if_tac" "in" hyp(H0) "eq:" simple_intropattern(E) :=
  match type of H0 with
    context [if ?a then _ else _] =>
    destruct a as [?H  | ?H] eqn:E
  end.

Tactic Notation "if_tac" simple_intropattern(H) "in" hyp(H1) "eq:" simple_intropattern(E) :=
  match type of H1 with
    context [if ?a then _ else _] =>
    destruct a as H eqn:E
  end.

(** Specializing a hypothesis with a newly created goal *)

Tactic Notation "assert_specialize" hyp(H) :=
  match type of H with
    forall x : ?P, _ =>
    let Htemp := fresh "Htemp" in
    assert P as Htemp; [ | specialize (H Htemp); try clear Htemp ]
  end.

Tactic Notation "assert_specialize" hyp(H) "by" tactic1(tac) :=
  match type of H with
    forall x : ?P, _ =>
    let Htemp := fresh "Htemp" in
    assert P as Htemp by tac; specialize (H Htemp); try clear Htemp
  end.

Tactic Notation "assert_specialize" hyp(H) "as" simple_intropattern(Hnew) :=
  match type of H with
    forall x : ?P, _ =>
    assert P as Hnew; [ | specialize (H Hnew) ]
  end.

Tactic Notation "assert_specialize" hyp(H) "as" simple_intropattern(Hnew) "by" tactic1(tac) :=
  match type of H with
    forall x : ?P, _ =>
    assert P as Hnew by tac;
    specialize (H Hnew)
  end.

(** Auto-specializing a hypothesis *)

Ltac autospec H := specialize (H ltac:(solve [eauto])).

(** When a hypothesis/term is provably equal, but not convertible, to
    your goal *)

Ltac exact_eq H :=
  revert H;
  match goal with
    |- ?p -> ?q => cut (p = q); [intros ->; auto | ]
  end.

(** Auto rewriting of a term *)

Tactic Notation "rewr" :=
  match goal with
  | H : ?f = _ |- context [?f] => rewrite H
  | H : ?f _ = ?f _ |- _ => try (injection H; repeat intros ->)
  end.

Tactic Notation "rewr" constr(e) :=
  match goal with
    E : e = _ |- _ => rewrite E
  | E : _ = e |- _ => rewrite <-E
  end.

Tactic Notation "rewr" constr(e) "in" "*" :=
  match goal with
    E : e = _ |- _ => rewrite E in *
  | E : _ = e |- _ => rewrite <-E in *
  end.

Tactic Notation "rewr" constr(e) "in" hyp(H) :=
  match goal with
    E : e = _ |- _ => rewrite E in H
  | E : _ = e |- _ => rewrite <-E in H
  end.

Lemma perm_search:
(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
  forall {A} (a b: A) r s t,
     Permutation (a::t) s ->
     Permutation (b::t) r ->
     Permutation (a::r) (b::s).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.
eapply perm_trans.
apply perm_skip.
apply Permutation_sym.
(* Goal: P (Z.add l (Z.of_nat n)) *)
apply H0.
eapply perm_trans.
apply perm_swap.
apply perm_skip.
(* Goal: sumbool (P (Z.add l (Z.of_nat n))) (not (P (Z.add l (Z.of_nat n)))) *)
apply H.
Qed.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Lemma Permutation_concat: forall {A} (P Q: list (list A)),
  Permutation P Q ->
  Permutation (concat P) (concat Q).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: @Permutation A (@concat A P) (@concat A Q) *)
  induction H.
  + apply Permutation_refl.
  + simpl.
(* Goal: @Permutation A (@app A x (@concat A l)) (@app A x (@concat A l')) *)
    apply Permutation_app_head; auto.
  + simpl.
(* Goal: @Permutation A (@app A y (@app A x (@concat A l))) (@app A x (@app A y (@concat A l))) *)
    rewrite !app_assoc.
(* Goal: @Permutation A (@app A (@app A y x) (@concat A l)) (@app A (@app A x y) (@concat A l)) *)
    apply Permutation_app_tail.
(* Goal: @Permutation A (@app A y x) (@app A x y) *)
    apply Permutation_app_comm.
  + eapply Permutation_trans; eauto.
Qed.    

Lemma Permutation_app_comm_trans:
 forall (A: Type) (a b c : list A),
   Permutation (b++a) c ->
   Permutation (a++b) c.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.
eapply Permutation_trans.
(* Goal: @Permutation A (@app A y x) (@app A x y) *)
apply Permutation_app_comm.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n *)
auto.
Qed.

Ltac solve_perm :=
    (* solves goals of the form (R ++ ?i = S)
          where R and S are lists, and ?i is a unification variable *)
  try match goal with
       | |-  Permutation (?A ++ ?B) _ =>
            is_evar A; first [is_evar B; fail 1| idtac];
            apply Permutation_app_comm_trans
       end;
  repeat first [ apply Permutation_refl
       | apply perm_skip
       | eapply perm_search
       ].

Goal exists e, Permutation ((1::2::nil)++e) (3::2::1::5::nil).
eexists.
solve_perm.
Qed.

Lemma range_pred_dec: forall (P: nat -> Prop),
  (forall n, {P n} + {~ P n}) ->
  forall m,
    {forall n, (n < m)%nat -> P n} + {~ forall n, (n < m)%nat -> P n}.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: sumbool (forall (n : nat) (_ : lt n m), P n) (not (forall (n : nat) (_ : lt n m), P n)) *)
  induction m.
  + left.
(* Goal: le n n *)
    intros; omega.
  + destruct (H m); [destruct IHm |].
    - left.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
      intros.
(* Goal: P n *)
      destruct (eq_dec n m).
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n *)
      * subst; auto.
(* Goal: le n n *)
      * apply p0; omega.
    - right.
(* Goal: not (forall (n : nat) (_ : lt n (S m)), P n) *)
      intro.
(* Goal: False *)
      apply n; clear n.
(* Goal: le n n *)
      intros; apply H0; omega.
    - right.
(* Goal: not (forall (n : nat) (_ : lt n (S m)), P n) *)
      intro.
(* Goal: False *)
      apply n; clear n.
(* Goal: P (Z.add l (Z.of_nat n)) *)
      apply H0.
(* Goal: le n n *)
      omega.
Qed.

Lemma Z2Nat_neg: forall i, i < 0 -> Z.to_nat i = 0%nat.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: @eq nat (Z.to_nat i) O *)
  destruct i; try reflexivity.
(* Goal: le n n *)
  pose proof Zgt_pos_0 p; omega.
Qed.

Lemma Zrange_pred_dec: forall (P: Z -> Prop),
  (forall z, {P z} + {~ P z}) ->
  forall l r,  
    {forall z, l <= z < r -> P z} + {~ forall z, l <= z < r -> P z}.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
  assert ((forall n: nat, (n < Z.to_nat (r - l))%nat -> P (l + Z.of_nat n)) <-> (forall z : Z, l <= z < r -> P z)).
(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
  {
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
    split; intros.
    + specialize (H0 (Z.to_nat (z - l))).
(* Goal: le n n *)
      rewrite <- Z2Nat.inj_lt in H0 by omega.
(* Goal: P z *)
      spec H0; [omega |].
(* Goal: le n n *)
      rewrite Z2Nat.id in H0 by omega.
      replace (l + (z - l)) with z in H0 by omega.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n *)
      auto.
    + apply H0.
(* Goal: and (Z.le l (Z.add l (Z.of_nat n))) (Z.lt (Z.add l (Z.of_nat n)) r) *)
      rewrite Nat2Z.inj_lt in H1.
      destruct (zlt (r - l) 0).
(* Goal: le n n *)
      - rewrite Z2Nat_neg in H1 by omega.
(* Goal: and (Z.le l (Z.add l (Z.of_nat n))) (Z.lt (Z.add l (Z.of_nat n)) r) *)
        simpl in H1.
(* Goal: le n n *)
        omega.
(* Goal: le n n *)
      - rewrite Z2Nat.id in H1 by omega.
(* Goal: le n n *)
        omega.
  }
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
  eapply sumbool_dec_iff; [clear H0 | eassumption].
(* Goal: sumbool (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (not (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n)))) *)
  apply range_pred_dec.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: sumbool (P (Z.add l (Z.of_nat n))) (not (P (Z.add l (Z.of_nat n)))) *)
  apply H.
Qed.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Definition eqb_list {A: Type} (eqb_A: A -> A -> bool): list A -> list A -> bool :=
  fix eqb_list (l1 l2: list A): bool :=
    match l1, l2 with
    | nil, nil => true
    | a1 :: l1, a2 :: l2 => eqb_A a1 a2 && eqb_list l1 l2
    | _, _ => false
    end.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Lemma eqb_list_spec: forall {A: Type} (eqb_A: A -> A -> bool),
  (forall a1 a2, eqb_A a1 a2 = true <-> a1 = a2) ->
  (forall l1 l2, eqb_list eqb_A l1 l2 = true <-> l1 = l2).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: iff (@eq bool (@eqb_list A eqb_A l1 l2) true) (@eq (list A) l1 l2) *)
  revert l2; induction l1 as [| a1 l1]; intros; destruct l2 as [| a2 l2].
  + simpl.
(* Goal: iff (@eq bool true true) (@eq (list A) (@nil A) (@nil A)) *)
    tauto.
  + simpl.
(* Goal: iff (@eq bool false true) (@eq (list A) (@cons A a1 l1) (@nil A)) *)
    split; intros; congruence.
  + simpl.
(* Goal: iff (@eq bool false true) (@eq (list A) (@cons A a1 l1) (@nil A)) *)
    split; intros; congruence.
  + simpl.
(* Goal: iff (@eq bool (andb (eqb_A a1 a2) (@eqb_list A eqb_A l1 l2)) true) (@eq (list A) (@cons A a1 l1) (@cons A a2 l2)) *)
    rewrite andb_true_iff.
    rewrite  H.
(* Goal: iff (and (@eq A a1 a2) (@eq bool (@eqb_list A eqb_A l1 l2) true)) (@eq (list A) (@cons A a1 l1) (@cons A a2 l2)) *)
    rewrite IHl1.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
    split; intros.
    - destruct H0; subst; auto.
    - inv H0; auto.
Qed.


Lemma nat_ind2_Type:
forall P : nat -> Type,
((forall n, (forall j:nat, (j<n )%nat -> P j) ->  P n):Type) ->
(forall n, P n).
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.
assert (forall j , (j <= n)%nat -> P j).
(* Goal: forall (j : nat) (_ : le j n), P j *)
(* Goal: P n *)
induction n.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.
(* Goal: le n n *)
replace j with 0%nat ; try omega.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
apply X; intros.
(* Goal: le n n *)
elimtype False; omega.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.  apply X. intros.
(* Goal: P j0 *)
(* Goal: P n *)
apply IHn.
(* Goal: le n n *)
omega.
(* Goal: P n *)
apply X0.
(* Goal: le n n *)
omega.
Qed.

Lemma nat_ind2:
forall P : nat -> Prop,
(forall n, (forall j:nat, (j<n )%nat -> P j) ->  P n) ->
(forall n, P n).
Proof.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n *)
intros; apply Wf_nat.lt_wf_ind. auto.
Qed.

Lemma equiv_e2 : forall A B: Prop, A=B -> B -> A.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
intros.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n *)
rewrite H; auto.
Qed.
Arguments equiv_e2 [A B] _ _.

Definition opt2list (A: Type) (x: option A) :=
  match x with Some a => a::nil | None => nil end.
Arguments opt2list [A] _.

(* Goal: iff (forall (n : nat) (_ : lt n (Z.to_nat (Z.sub r l))), P (Z.add l (Z.of_nat n))) (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) *)
(* Goal: sumbool (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z) (not (forall (z : Z) (_ : and (Z.le l z) (Z.lt z r)), P z)) *)
Definition isSome {A} (o: option A) := match o with Some _ => True | None => False end.

Definition isSome_dec: forall {A} (P: option A), isSome P + ~ isSome P.
Proof.
(* Goal: forall (A : Type) (P : option A), sum (@isSome A P) (not (@isSome A P)) *)
  intros.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n *)
  destruct P; simpl; auto.
Defined.
