(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                                  ex1.v                                   *)
(****************************************************************************)


Theorem trivial : forall A : Prop, A -> A.
(* Goal: forall (A : Prop) (_ : A), A *)
intros A H'; exact H'.
Qed.

Theorem and_commutative : forall A B : Prop, A /\ B -> B /\ A.
(* Goal: forall (A B : Prop) (_ : and A B), and B A *)
intros A B H'; split.
(* Goal: B *)
(* Goal: A *)
elim H'; intros H'0 H'1; clear H'; exact H'1.
(* Goal: A *)
elim H'; intros H'0 H'1; clear H'; exact H'0.
Qed.

Theorem or_commutative : forall A B : Prop, A \/ B -> B \/ A.
(* Goal: forall (A B : Prop) (_ : or A B), or B A *)
intros A B h; elim h; [ intro H'; clear h; try exact H' | clear h; intro H' ].
(* Goal: or B A *)
(* Goal: or B A *)
right; assumption.
(* Goal: or B A *)
left; assumption.
Qed.

Theorem mp : forall A B : Prop, A -> (A -> B) -> B.
(* Goal: forall (A B : Prop) (_ : A) (_ : forall _ : A, B), B *)
intros A B H' H'0.
(* Goal: q a *)
apply H'0.
(* Goal: p a *)
exact H'.
Qed.

Theorem S : forall A B C : Prop, (A -> B -> C) -> (A -> B) -> A -> C.
(* Goal: forall (A B C : Prop) (_ : forall (_ : A) (_ : B), C) (_ : forall _ : A, B) (_ : A), C *)
intros A B C H' H'0 H'1.
(* Goal: C *)
apply H'.
(* Goal: A *)
exact H'1.
(* Goal: q a *)
apply H'0.
(* Goal: A *)
exact H'1.
Qed.

Theorem Praeclarum :
 forall x y z t : Prop, (x -> z) /\ (y -> t) -> x /\ y -> z /\ t.
(* Goal: forall (x y z t : Prop) (_ : and (forall _ : x, z) (forall _ : y, t)) (_ : and x y), and z t *)
intros x y z t h; elim h; intros H' H'0; clear h.
(* Goal: forall _ : and x y, and z t *)
intro h; elim h; intros H'1 H'2; clear h.
(* Goal: and z t *)
split.
(* Goal: z *)
(* Goal: t *)
apply H'; assumption.
(* Goal: R y x *)
apply H'0; assumption.
Qed.

Theorem resolution :
 forall (p q : Type -> Prop) (a : Type),
 p a -> (forall x : Type, p x -> q x) -> q a.
(* Goal: forall (p q : forall _ : Type, Prop) (a : Type) (_ : p a) (_ : forall (x : Type) (_ : p x), q x), q a *)
intros p q a H' H'0.
(* Goal: q a *)
apply H'0.
(* Goal: p a *)
exact H'.
Qed.

Theorem Witnesses :
 forall (a b : Type) (p : Type -> Prop), p a \/ p b -> exists x : Type, p x.
(* Goal: forall (a b : Type) (p : forall _ : Type, Prop) (_ : or (p a) (p b)), @ex Type (fun x : Type => p x) *)
intros a b p h; elim h; intro H'; clear h.
(* Goal: @ex Type (fun x : Type => p x) *)
(* Goal: @ex Type (fun x : Type => p x) *)
exists a; assumption.
(* Goal: @ex Type (fun x : Type => p x) *)
exists b; assumption.
Qed.

Theorem Simple :
 forall (A : Set) (R : A -> A -> Prop),
 (forall x y z : A, R x y /\ R y z -> R x z) ->
 (forall x y : A, R x y -> R y x) ->
 forall x : A, (exists y : A, R x y) -> R x x.
(* Goal: forall (A : Set) (R : forall (_ : A) (_ : A), Prop) (_ : forall (x y z : A) (_ : and (R x y) (R y z)), R x z) (_ : forall (x y : A) (_ : R x y), R y x) (x : A) (_ : @ex A (fun y : A => R x y)), R x x *)
intros A R H' H'0 x h; elim h; intros y E; clear h.
(* Goal: R x x *)
apply H' with y.
(* Goal: and (R x y) (R y x) *)
split; [ assumption | idtac ].
(* Goal: R y x *)
apply H'0; assumption.
Qed.

Theorem not_not : forall a : Prop, a -> ~ ~ a.
(* Goal: forall (a : Prop) (_ : a), not (not a) *)
intros a H'; red in |- *; intro H'0; elim H'0; assumption.
Qed.

Theorem mini_cases : forall x y : Prop, (x \/ ~ y) /\ y -> x.
intros x y h; elim h; intros h0 H'; elim h0;
 [ intro H'0; clear h h0; try exact H'0 | clear h h0; intro H'0 ].
(* Goal: x *)
elim H'0; try assumption.
Qed.

Require Import Classical.
(*This theorem needs classical logic*)

Theorem not_not_converse : forall a : Prop, ~ ~ a -> a.
(* Goal: forall (a : Prop) (_ : not (not a)), a *)
intros a H'.
generalize (classic a); intro h; elim h;
 [ intro H'0; clear h; try exact H'0 | clear h; intro H'0 ].
(* Goal: a *)
elim H'; assumption.
Qed.

Theorem not_quite_classic : forall a : Prop, ~ ~ (a \/ ~ a).
(* Goal: forall a : Prop, not (not (or a (not a))) *)
intro a; red in |- *; intro H'; elim H'; right; red in |- *; intro H'0.
(* Goal: False *)
elim H'; left; try assumption.
Qed.

