Require Import Coq.Sets.Ensembles.
Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.
Require Import Coq.Logic.ClassicalFacts.

Lemma prop_ext: prop_extensionality.
Proof.
(* Goal: prop_extensionality *)
  hnf; intros.
(* Goal: @eq Prop A B *)
  set (A0 := fun x: unit => A).
(* Goal: @eq Prop A B *)
  set (B0 := fun x: unit => B).
(* Goal: @eq Prop A B *)
  assert (A0 = B0).
  + apply Extensionality_Ensembles.
(* Goal: Same_set unit A0 B0 *)
    split; subst A0 B0; unfold Included, Ensembles.In; intros; tauto.
  + change A with (A0 tt).
(* Goal: @eq Prop (A0 tt) B *)
    change B with (B0 tt).
(* Goal: @eq Prop (A0 tt) (B0 tt) *)
    rewrite H0; auto.
Qed.

Lemma fin_subset_match {A B: Type} {P: A -> B -> Prop}: forall (X: Ensemble A) (Y: Ensemble B),
  (forall x, X x -> exists y, P x y /\ Y y) ->
  forall xs, Forall (fun x => X x) xs -> exists ys, Forall2 P xs ys /\ Forall (fun y => Y y) ys.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: @ex (list B) (fun ys : list B => and (@Forall2 A B P xs ys) (@Forall B (fun y : B => Y y) ys)) *)
  induction xs as [| x0 xs].
  + exists nil; split; constructor.
  + inversion H0; subst.
(* Goal: @ex (list B) (fun ys : list B => and (@Forall2 A B P (@cons A x0 xs) ys) (@Forall B (fun y : B => Y y) ys)) *)
    specialize (IHxs H4).
(* Goal: @ex (list B) (fun ys : list B => and (@Forall2 A B P (@cons A x0 xs) ys) (@Forall B (fun y : B => Y y) ys)) *)
    destruct IHxs as [ys [? ?]].
(* Goal: @ex (list B) (fun ys : list B => and (@Forall2 A B P (@cons A x0 xs) ys) (@Forall B (fun y : B => Y y) ys)) *)
    specialize (H x0 H3).
(* Goal: @ex (list B) (fun ys : list B => and (@Forall2 A B P (@cons A x0 xs) ys) (@Forall B (fun y : B => Y y) ys)) *)
    destruct H as [y0 [? ?]].
(* Goal: @ex (list B) (fun ys : list B => and (@Forall2 A B P (@cons A x0 xs) ys) (@Forall B (fun y : B => Y y) ys)) *)
    exists (y0 :: ys).
(* Goal: and (@Forall2 A B P (@cons A x0 xs) (@cons B y0 ys)) (@Forall B (fun y : B => Y y) (@cons B y0 ys)) *)
    split; constructor; auto.
Qed.

Lemma Forall2_lr_rev {A B: Type} {P: A -> B -> Prop}: forall xs ys,
  Forall2 (fun y x => P x y) ys xs ->
  Forall2 P xs ys.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: @Forall2 A B P xs ys *)
  induction H; auto.
Qed.

(* This one copy from RamifyCoq *)
Lemma Forall_app_iff: forall {A : Type} (P : A -> Prop) (l1 l2 : list A), Forall P (l1 ++ l2) <-> Forall P l1 /\ Forall P l2.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros; induction l1; intros.
  + simpl.
(* Goal: iff (@Forall A P l2) (and (@Forall A P (@nil A)) (@Forall A P l2)) *)
    assert (Forall P nil) by constructor; tauto.
  + simpl; split; intros.
    - inversion H; subst; split; try tauto.
(* Goal: @Forall A P (@cons A a (@app A l1 l2)) *)
      constructor; auto; tauto.
    - destruct H.
(* Goal: @Forall A P (@cons A a (@app A l1 l2)) *)
      inversion H; subst.
(* Goal: @Forall A P (@cons A a (@app A l1 l2)) *)
      constructor; auto; tauto.
Qed.

Inductive remove_rel {A: Type}: A -> list A -> list A -> Prop :=
| remove_rel_nil: forall a, remove_rel a nil nil
| remove_rel_cons_eq: forall a xs ys, remove_rel a xs ys -> remove_rel a (a :: xs) ys
| remove_rel_cons_neq: forall a b xs ys, a <> b -> remove_rel a xs ys -> remove_rel a (b :: xs) (b :: ys).

Lemma remove_rel_In: forall (A : Type) (l1 l2 : list A) (x : A), remove_rel x l1 l2 -> ~ In x l2.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: @Forall A (fun y : A => @In A y l1) l2 *)
  induction H.
  + intros [].
  + auto.
  + intros [|]; auto.
Qed.

Lemma remove_rel_exist: forall (A : Type) (l1 : list A) (x : A) (DEC: forall y, x = y \/ x <> y), exists l2, remove_rel x l1 l2.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: @ex (list A) (fun l2 : list A => @remove_rel A x l1 l2) *)
  induction l1.
  + exists nil.
(* Goal: @remove_rel A x (@nil A) (@nil A) *)
    apply remove_rel_nil.
  + destruct IHl1 as [l2 ?].
(* Goal: @ex (list A) (fun l2 : list A => @remove_rel A x (@cons A a l1) l2) *)
    destruct (DEC a).
    - exists l2; subst.
(* Goal: @Forall A (fun y : A => @In A y (@nil A)) (@nil A) *)
      apply remove_rel_cons_eq; auto.
    - exists (a :: l2); subst.
(* Goal: @Forall A (fun y : A => @In A y (@nil A)) (@nil A) *)
      apply remove_rel_cons_neq; auto.
Qed.

Lemma remove_rel_result_belong: forall (A : Type) (l1 l2 : list A) (x : A), remove_rel x l1 l2 -> Forall (fun y => In y l1) l2.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: @Forall A (fun y : A => @In A y l1) l2 *)
  induction H.
  + auto.
  + simpl.
(* Goal: @Forall A (fun y : A => or (@eq A b y) (@In A y xs)) ys *)
    revert IHremove_rel; apply Forall_impl.
(* Goal: @Forall A (fun y : A => @In A y (@nil A)) (@nil A) *)
    intros; auto.
  + constructor; simpl; auto.
(* Goal: @Forall A (fun y : A => or (@eq A b y) (@In A y xs)) ys *)
    revert IHremove_rel; apply Forall_impl.
(* Goal: @Forall A (fun y : A => @In A y (@nil A)) (@nil A) *)
    intros; auto.
Qed.

Definition isSome {A} (o: option A) := match o with Some _ => True | None => False end.

(* These three lemmas are copied from veric/assert_lemmas.v and veric/initial_world.v *)
Lemma nth_error_in_bounds: forall {A} (l: list A) i, (O <= i < length l)%nat
  -> exists x, nth_error l i = value x.
Proof.
(* Goal: forall (A : Type) (l : list A) (i : nat) (_ : and (le O i) (lt i (@length A l))), @ex A (fun x : A => @eq (option A) (@nth_error A l i) (@value A x)) *)
intros until i; intros H.
(* Goal: @ex A (fun x : A => @eq (option A) (@nth_error A l i) (@value A x)) *)
revert i l H.
induction i; destruct l; intros; simpl in *;
  try solve [eauto | omega].
(* Goal: @ex A (fun x : A => @eq (option A) (@nth_error A l i) (@value A x)) *)
apply IHi; omega.
Qed.

Lemma nth_error_app: forall {T} (al bl : list T) (j: nat),
     nth_error (al++bl) (length al + j) = nth_error bl j.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
 intros. induction al; simpl; auto.
Qed.

Lemma nth_error_app1: forall {T} (al bl : list T) (j: nat),
     (j < length al)%nat ->
     nth_error (al++bl) j = nth_error al j.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros. revert al H; induction j; destruct al; simpl; intros; auto; try omega.
(* Goal: @eq (option T) (@nth_error T (@app T al bl) j) (@nth_error T al j) *)
   apply IHj. omega.
Qed.

Lemma nth_error_None_iff: forall {A} (l: list A) n, nth_error l n = None <-> n >= length l.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: @Forall A (fun y : A => @In A y (@cons A a xs)) ys *)
  revert n; induction l; intros; destruct n; simpl.
  + split; [intros _; omega | auto].
  + split; [intros _; omega | auto].
  + split; [intros; inversion H | omega].
  + rewrite IHl.
(* Goal: iff (ge n (@length A l)) (ge (S n) (S (@length A l))) *)
    omega.
Qed.

Lemma Forall_rev: forall {A} (P: A -> Prop) (l: list A), Forall P (rev l) <-> Forall P l.
Proof.
(* Goal: forall (A : Type) (P : forall _ : A, Prop) (l : list A), iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  intros.
(* Goal: iff (@Forall A P (@rev A l)) (@Forall A P l) *)
  rewrite !Forall_forall.
(* Goal: iff (forall (x : A) (_ : @In A x (@rev A l)), P x) (forall (x : A) (_ : @In A x l), P x) *)
  pose proof in_rev l.
(* Goal: iff (forall (x : A) (_ : @In A x (@rev A l)), P x) (forall (x : A) (_ : @In A x l), P x) *)
  firstorder.
Qed.
