Require Export VST.msl.Axioms.

(* NO AXIOMS AFTER THIS POINT *)

Require Import Coq.Logic.EqdepFacts.

(* From EqdepTh we obtain inj_pair and inj_pairT2 without
   use of excluded middle:
 *)
Module EqdepElim: EqdepElimination.
Lemma eq_rect_eq :
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
      x = eq_rect p Q x p h.
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
  intros.
(* Goal: @eq (Q p) x (@eq_rect U p Q x p h) *)
  apply Streicher_K__eq_rect_eq.
(* Goal: Streicher_K_ U *)
  apply UIP_refl__Streicher_K.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
  hnf; intros; hnf; intros.
(* Goal: @eq (@eq U x0 x0) p0 (@eq_refl U x0) *)
  apply proof_irr.
Qed.
End EqdepElim.

Module EqdepTh := EqdepTheory EqdepElim.
Export EqdepTh.

(* Generalize the extensionality tactic from the Coq library. *)
Tactic Notation "extensionality" :=
 let x := fresh "x" in extensionality x.

Tactic Notation "extensionality" ident(x0) ident(x1) :=
  extensionality x0; extensionality x1.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) :=
  extensionality x0; extensionality x1; extensionality x2.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3)
  ident(x4) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3;
  extensionality x4.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3)
  ident(x4) ident(x5) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3;
  extensionality x4; extensionality x5.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3)
  ident(x4) ident(x5) ident(x6) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3;
  extensionality x4; extensionality x5; extensionality x6.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3)
  ident(x4) ident(x5) ident(x6) ident(x7) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3;
  extensionality x4; extensionality x5; extensionality x6; extensionality x7.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3)
  ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3;
  extensionality x4; extensionality x5; extensionality x6; extensionality x7;
  extensionality x8.

Tactic Notation "extensionality" ident(x0) ident(x1) ident(x2) ident(x3)
  ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) :=
  extensionality x0; extensionality x1; extensionality x2; extensionality x3;
  extensionality x4; extensionality x5; extensionality x6; extensionality x7;
  extensionality x8; extensionality x9.

Lemma imp_ext: forall (A A' B B' : Prop), (A=A') -> (A -> (B=B')) -> ((A->B)=(A'->B')).
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: @eq Prop (forall _ : A, B) (forall _ : A', B') *)
subst A'.
(* Goal: @eq Prop (forall _ : A, B) (forall _ : A, B') *)
apply prop_ext; split; intros; auto.
(* Goal: B' *)
(* Goal: B *)
rewrite <- H0; auto. rewrite H0; auto.
Qed.

Lemma exists_ext: forall (A: Type) F G, (forall x: A, F x = G x) -> (Logic.ex F = Logic.ex G).
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: @eq Prop (@ex A F) (@ex A G) *)
apply prop_ext; split; intro; destruct H0; exists x.
(* Goal: G x *)
(* Goal: F x *)
rewrite <- H; auto.
(* Goal: F x *)
rewrite H; auto.
Qed.


Lemma and_ext: forall A B C D, A=B -> C=D -> (A /\ C) = (B /\ D).
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: B *)
rewrite H; rewrite H0; auto.
Qed.

Lemma and_ext': forall (A: Prop) B C D, A=B -> (A -> (C=D)) -> (A /\ C) = (B /\ D).
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: @eq Prop (and A C) (and B D) *)
subst B.
(* Goal: @eq Prop (forall x : A, F x) (forall x : A, G x) *)
apply prop_ext.
(* Goal: iff (and A C) (and A D) *)
intuition; subst; auto.
Qed.

Lemma or_ext: forall A B C D, A=B -> C=D -> (A \/ C) = (B \/ D).
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: B *)
rewrite H; rewrite H0; auto.
Qed.

Lemma forall_ext: forall (A: Type) (F: A -> Prop) G, (forall x:A, F x = G x) -> (forall x, F x) = (forall x, G x).
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
apply prop_ext. split; intros. rewrite <- H; auto. rewrite H; auto.
Qed.

Lemma existT_ext:
  forall (A: Type) (P: A -> Prop) (x y: A) (Hx: P x) (Hy: P y),
     x = y -> existT _ x Hx = existT _ y Hy.
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: @eq (@sig A P) (@exist A P x Hx) (@exist A P y Hy) *)
subst.
(* Goal: @eq (@sig A P) (@exist A P y Hx) (@exist A P y Hy) *)
rewrite (proof_irr Hx Hy); auto.
Qed.

Lemma exist_ext:
  forall (A: Type) (P: A -> Prop) (x y: A) (Hx: P x) (Hy: P y),
     x = y -> exist _ x Hx = exist _ y Hy.
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
intros.
(* Goal: @eq (@sig A P) (@exist A P x Hx) (@exist A P y Hy) *)
subst.
(* Goal: @eq (@sig A P) (@exist A P y Hx) (@exist A P y Hy) *)
rewrite (proof_irr Hx Hy); auto.
Qed.

Lemma exist_ext' : forall A F (x y:@sig A F),
  proj1_sig x = proj1_sig y -> x = y.
Proof.
(* Goal: forall (A : Type) (F : forall _ : A, Prop) (x y : @sig A F) (_ : @eq A (@proj1_sig A F x) (@proj1_sig A F y)), @eq (@sig A F) x y *)
  intros.
(* Goal: @eq (@sig A F) x y *)
  destruct x; destruct y; simpl in *.
(* Goal: @eq (@sig A F) (@exist A F x f) (@exist A F x0 f0) *)
  subst x0.
(* Goal: @eq (@sig A F) (@exist A F x f) (@exist A F x f0) *)
  replace f0 with f by apply proof_irr; auto.
Qed.
