# Library CoursDeCoq.ex1_auto

Theorem trivial : A : Prop, AA.
auto with v62.
Qed.

Theorem and_commutative : A B : Prop, A BB A.
intros A B H'; elim H'; auto with v62.
Qed.

Theorem or_commutative : A B : Prop, A BB A.
intros A B H'; elim H'; auto with v62.
Qed.

Theorem mp : A B : Prop, A → (AB) → B.
auto with v62.
Qed.

Theorem S : A B C : Prop, (ABC) → (AB) → AC.
auto with v62.
Qed.

Theorem Praeclarum :
x y z t : Prop, (xz) (yt)x yz t.
intros x y z t H'; elim H'.
intros H'0 H'1 H'2; elim H'2.
auto with v62.
Qed.

Theorem resolution :
(p q : TypeProp) (a : Type),
p a → ( x : Type, p xq x) → q a.
auto with v62.
Qed.

Theorem Witnesses :
(a b : Type) (p : TypeProp), p a p b x : Type, p x.
intros a b p h; elim h;
[ intro H'; clear h; try exact H' | clear h; intro H' ].
a; try assumption.
b; try assumption.
Qed.

Theorem Simple :
(A : Set) (R : AAProp),
( x y z : A, R x y R y zR x z) →
( x y : A, R x yR y x) →
x : A, ( y : A, R x y) → R x x.
intros A R H' H'0 x H'1; try assumption.
elim H'1; intros y E; clear H'1; try exact E.
apply H' with y; auto with v62.
Qed.

Theorem not_not : a : Prop, a¬ ¬ a.
unfold not in |- *; auto with v62.
Qed.

Theorem mini_cases : x y : Prop, (x ¬ y) yx.
intros x y h; elim h; intros h0 H'; elim h0;
[ clear h h0; intro H'0 | intro H'0; elim H'0; clear h h0; try assumption ];
auto with v62.
Qed.

Require Import Classical.

Theorem not_not_converse : a : Prop, ¬ ¬ aa.
intros a H'; try assumption; auto 10 with v62.
generalize (classic a); intro h; elim h;
[ intro H'0; clear h; try exact H'0 | clear h; intro H'0 ].
elim H'; assumption.
Qed.

Theorem not_quite_classic : a : Prop, ¬ ¬ (a ¬ a).
unfold not in |- *; auto with v62.
Qed.

Theorem Peirce : A B : Prop, ((((AB) → A) → A) → B) → B.
auto with v62.
Qed.