(* ZADANIE 1: *)

Lemma jeden: forall A: Prop, A -> A.
intros.
assumption.
Qed.

Lemma dwa: forall A B C: Prop, (A -> B) -> (B -> C) -> A -> C.
intros.
assert B.
exact(H H1).
clear H.

assert C.
exact (H0 H2).
clear H0.
assumption.
Qed.

Lemma trzy: forall A B: Prop, A /\ B <-> B /\ A.
intros.
split.
intros.
elim H.
intros.
clear H.
split.
assumption.
assumption.

intros.
elim H.
intros.
clear H.
split.
assumption.
assumption.
Qed.

Lemma cztery: forall A B: Prop, A \/ B <-> B \/ A.
intros.

split.
intros.
elim H.
intro.
clear H.
right.
assumption.

intro.
left.
assumption.

intros.
elim H.
intro.
clear H.
right.
assumption.
intro.
left.
assumption.
Qed.

Lemma piec: forall A: Prop, A -> ~~A.
intros.
intro.
apply H0.
assumption.
Qed.

Lemma szesc: forall A B: Prop, (A -> B) -> ~B -> ~A.
intros.
unfold not at 1 in |- *.
intro.
unfold not at 1 in H0.
assert B.
exact (H H1).
clear H.
assert False.
exact (H0 H2).
clear H0.
elimtype False.
assumption.
Qed.

Lemma siedem: forall A: Prop, ~~(A \/ ~ A).
intros.
intro.
unfold not in H; cut ((A -> False) -> False).
cut (A -> False).
intro; intros; clear H; assert False.
exact (H1 H0).

clear H1; elimtype False; assumption.

intro; cut (A \/ (A -> False)).
exact H.

left; assumption.

intro; cut (A \/ (A -> False)).
exact H.

right; assumption.
Qed.

Lemma osiem: forall A B C : Prop, (A /\ B) \/ C <-> (A \/ C) /\ (B \/ C).
intros; unfold iff in |- *; split.
intro; elim H.
intro; clear H; elim H0; intro; intro; clear H0;
split.

left; assumption.
left; assumption.

intro; clear H; split.
right; assumption.
right; assumption.

intro; elim H; intro; intro; clear H; elim H0.
intro; clear H0; elim H1.
intro; clear H1; left; split.
assumption.
assumption.

intro; clear H1; right; assumption.

intro; clear H0; elim H1.
intro; clear H1; right; assumption.
intro; clear H1; right; assumption.
Qed.

(* Zadanie 2: *)

Parameter X Y : Set.
Parameter A B : X -> Prop.

Lemma jeden : (forall x : X, A x /\ B x) <-> (forall x : X, A x) /\ (forall x : X, B x).
unfold iff in |- *; split.
    intro; split.
    intro.
    auto with *.
    destruct (H x).
    assumption.
    intro; auto with *.
    destruct (H x).
    assumption.
    intro; elim H; intro; intro; clear H; intro;
       split.
    apply H0.
apply H1.
Qed.

(* brakuje B *)

(* Zadanie 3: *)

Axiom not_not_elim : forall A : Prop, ~~A -> A.
Lemma jeden: forall A : Prop, A \/ ~A.

intro; unfold not, iff in |- *; auto with *.
apply not_not_elim.

unfold not in |-*; intro; cut ((A -> False) -> False).
cut (A -> False).
intro; intros; clear H; assert False.
exact (H1 H0).

clear H1; elimtype False; assumption.

intro; cut (A \/ (A -> False)).
exact H.

left; assumption.

intro; cut (A \/ (A -> False)).
exact H.

right; assumption.
Qed.

(* Zadanie 4: *)
Parameter E : Set.
  Parameter R : E -> E -> Prop.
  Axiom refl :     forall (x : E),      R x x.
  Axiom trans :    forall (x y z : E),  R x y -> R y z -> R x z.
  Axiom antisym :  forall (x y : E),    R x y -> R y x -> x = y.
  Definition smallest (x0 : E) := forall (x : E), R x0 x.
  Definition minimal (x0 : E) := forall (x : E),  R x x0 -> x = x0.
Lemma jeden: forall (x1 x2 : E), smallest x1 -> smallest x2 -> x1 = x2.

intros.
apply antisym.
apply H.
apply H0.
Qed.

(* ZADANIE 5: *)
Lemma plus_n_0 :  forall n, n + 0 = n.

Proof.
intro.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.

Lemma plus_n_Sm :  forall n m, S (n + m) = n + S m.

Proof.
intros.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.

Lemma plus_commut : forall n m, n + m = m + n.

Proof.
intros.
induction n.
apply plus_n_O.
simpl.
rewrite -> IHn.
apply (plus_n_Sm m n).
Qed.