Set Implicit Arguments.

Require Import Logic.
Require Import Specif.

Section Proof_Irrelevence.

(* The Axiom: justified by the proof-irrelevent model of Miquel.
   There exists an object that belong to any true proposition
 *)
Axiom impl_PI : forall [A:Prop], [A] -> A.

Lemma proof_irrelevance : forall [P:Prop] [x y:P], x = y.
intros.
pose (px := impl_PI (existT (fun z => x=z:>P) x (refl_equal x))). 
pose (py := impl_PI (existT (fun z => z=y:>P) y (refl_equal y))).
(* px and py are convertable *)
transitivity (projT1 px).
 apply (projT2 px).
 apply (projT2 py).
Qed.

Lemma False_rect': forall [P:Type], [False] -> P.
intros.
apply False_rect.
apply (@impl_PI False); trivial.
Defined.
Lemma impl_neg : forall [A : Prop], [~A] -> [A] -> False.
intros.
apply False_rect';auto.
Qed.

Lemma eq_rect':
  forall [A:Type] [x:A] [P:A->Type], P x -> forall [y : A], [x = y] -> P y.
intros.
apply eq_rect with (1:=X).
apply (@impl_PI (x=y)); trivial.
Defined.

Definition proj2_sig [A] [P:A->Prop] (x:sig P) : P (proj1_sig x) :=
  match x as s return P (proj1_sig s) with
    exist x H => impl_PI H
  end.


(* With surjective pairing, s could be implicit *)
Lemma sig2_ext : forall [A] [P:A->Prop] s,
  s = exist P (proj1_sig s) (proj2_sig s).
Proof.
destruct s; trivial.
Qed.

(* With surjective pairing, impl_PI would not be needed *)
Lemma sig_rect' : forall [A] [P] [P0 : sig P -> Type],
       (forall [x : A] [p : P x], P0 (exist [P] x [p])) ->
       forall [s : sig P], P0 s.
intros.
rewrite (@impl_PI (_=_) (sig2_ext s)).
trivial.
Defined.

  Lemma Choice : forall S S' R,
   (forall x:S, sig (fun y:S' => R x y)) ->
   sig (fun f:S -> S' => forall z:S, R z (f z)).
Proof.
intros S S' R H.
exists (fun z => proj1_sig (H z)).
intro z; destruct (H z); simpl.
apply (@impl_PI (R z x)); trivial.
Qed.

  Lemma sumbool_or : forall [A B:Prop], {A}+{B} -> A \/ B.
destruct 1; apply impl_PI; auto.
Qed.

  Lemma sumbool_ind' : forall [A B:Prop] [P:{A}+{B}->Prop],
    (forall a:A, P (left B a)) ->
    (forall b:B, P (right A b)) ->
    forall s:{A}+{B}, P s.
destruct s; apply impl_PI; trivial.
Qed.


End Proof_Irrelevence.

Section Smash.

Inductive smash (A:Prop) : Prop := Smash [_:A].
Scheme smash_indd := Induction for smash Sort Type.


Lemma smash_unit : forall A (p1 p2 : smash A), p1=p2.
intros.
elim p1 using smash_indd; intros.
elim p2 using smash_indd; intros.
reflexivity.
Qed.

Hint Resolve Smash : core.

Lemma smash_impl : forall A B:Prop, (A->B) -> smash A -> smash B.
destruct 2; auto.
Qed.

Lemma smash_choice : forall (A:Type) (B:A->Prop),
  (forall x:A, smash (B x)) -> smash (forall x:A, B x).
constructor; intros.
elim (H x); intros.
apply (@impl_PI (B x)); trivial.
Qed.
End Smash.