Zad3-1.V

Require Import ProofWeb.

Section ZadanieOne.

Variables A B C D : Prop. 

Theorem impl_rozdz : (A -> B) -> (A -> C) -> A -> B -> C.
 Proof.
 imp_i H1.
 imp_i H2.
 imp_i H3.
 imp_i H4.
 imp_e A.
 exact H2.
 exact H3.
 Qed.

Theorem impl_komp : (A -> B) -> (B -> C) -> A -> C.
 Proof.
 imp_i H1.
 imp_i H2.
 imp_i H3.
 imp_e B.
 exact H2.
 imp_e A.
 exact H1.
 exact H3.
 Qed.

Theorem impl_perm : (A -> B -> C) -> B -> A -> C. 
 Proof.
 imp_i H1.
 imp_i H2.
 imp_i H3.
 imp_e B.
 imp_e A.
 exact H1.
 exact H3.
 exact H2.
 Qed.

Theorem impl_conj : A -> B -> A /\ B. 
 Proof.
 imp_i H1.
 imp_i H2.
 con_i.
 exact H1.
 exact H2.
 Qed.

Theorem conj_elim_l : A /\ B -> A. 
 Proof.
 imp_i H1.
 con_e1 B.
 exact H1.
 Qed.

Theorem disj_intro_l : A -> A \/ B.
 Proof.
 imp_i H1.
 dis_i1.
 exact H1.
 Qed.

Theorem rozl_elim : A \/ B -> (A -> C) -> (B -> C) -> C. 
 Proof.
 imp_i H1.
 imp_i H2.
 imp_i H3.
 dis_e (A\/B) H4 H5.
 exact H1.
 imp_e A.
 exact H2.
 exact H4.
 imp_e B.
 exact H3.
 exact H5.
 Qed.

Theorem diamencik : (A -> B) -> (A -> C) -> (B -> C -> D) -> A -> D.
 Proof.
 imp_i H1.
 imp_i H2.
 imp_i H3.
 imp_i H4.
 imp_e C.
 imp_e B.
 exact H3.
 imp_e A.
 exact H1.
 exact H4.
 imp_e A.
 exact H2.
 exact H4. 
 Qed.

Theorem slaby_peirce : ((((A -> B) -> A) -> A) -> B) -> B.
 Proof.
 imp_i H1.
 imp_e (((A->B)->A)->A).
 exact H1.
 imp_i H2.
 imp_e (A->B).
 exact H2.
 imp_i H3.
 imp_e (((A->B)->A)->A).
 exact H1.
 imp_i H4.
 exact H3.
 Qed.

Theorem rozl_impl_rozdz : (A \/ B -> C) -> (A -> C) /\ (B -> C).
 Proof.
 imp_i H1.
 con_i.
 imp_i H2.
 imp_e (A\/B).
 exact H1.
 dis_i1.
 exact H2.
 imp_i H2.
 imp_e (A\/B).
 exact H1.
 dis_i2.
 exact H2.
 Qed.
 
Theorem rozl_impl_rozdz_odw : (A -> C) /\ (B -> C) -> A \/ B -> C.
 Proof.
 imp_i H1.
 imp_i H2.
 dis_e (A\/B) H3 H4.
 exact H2.
 imp_e A.
 con_e1 (B->C).
 exact H1.
 exact H3.
 imp_e B.
 con_e2 (A->C).
 exact H1.
 exact H4.
 Qed.

Theorem curry : (A /\ B -> C) -> A -> B -> C.
Proof.
imp_i H1.
imp_i H2.
imp_i H3.
imp_e (A/\B).
exact H1.
con_i.
exact H2.
exact H3.
Qed.

Theorem uncurry : (A -> B -> C) -> A /\ B -> C.
Proof.
imp_i H1.
imp_i H2.
imp_e B.
imp_e A.
exact H1.
con_e1 B.
exact H2.
con_e2 A.
exact H2.
Qed.

End ZadanieOne.