Require Import Arith List.

(* When you want to force the acceptation of a proof without proving it,
  Finish the proof with "Admitted." .
  On the other hand, if you empty the goal-list of a proof, you should
  finish it using "Qed." *)

Section very_simple_programming.

(* Write a function that maps any x to x^2 + 3x + 1, name this function
f *)

(* If your function, then the following proof should workd without question:
  any problem. *)

Lemma f_correct : forall x y, y* (f x + 2) = (x * (x+3) +3)*y.
intros; unfold f; ring.
Qed.

End very_simple_programming.


Section Propositional_minimal.
 Variables P Q R S : Prop.

 Lemma id_P : P -> P.

 Lemma id_PP : (P->P)->(P->P).

 Lemma imp_trans : (P->Q)->(Q->R)->P->R.

 Lemma imp_perm : (P->Q->R)->(Q->P->R).

 Lemma ignore_Q : (P->R)->P->Q->R.

 Lemma delta_imp  : (P->P->Q)->P->Q.

 Lemma delta_impR : (P->Q)->(P->P->Q).

 Lemma diamond : (P->Q)->(P->R)->(Q->R->S)->P->S.

 Lemma weak_peirce : ((((P->Q)->P)->P)->Q)->Q.

End Propositional_minimal.

Section Predicate_minimal.
Variables (A:Type)(P Q:A->Prop) (R : A -> A -> Prop).
Lemma pc1 : (forall a b:A, R a b) -> forall a b:A, R b a.

Lemma pc2 :  (forall a:A, P a -> Q a) -> (forall a:A, P a) -> forall a:A, Q a.

Lemma pc3 : (forall a b:A, R a b) -> forall a:A, R a a.

End Predicate_minimal.

Section intuitionistic_predicate.

Lemma and_assoc : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.

Lemma and_imp_dist : forall A B C D:Prop,
                     (A -> B) /\ (C -> D) -> A /\ C -> B /\ D.

Lemma not_contrad : forall A : Prop, ~(A /\ ~A).

Lemma or_and_not : forall A B : Prop, (A\/B)/\~A -> B.

Lemma and_permute : forall a b c, a/\ (b /\ c) -> b /\ (a /\ c).

Lemma or_permute : forall a b c, a \/ (b \/ c) -> b \/ (a \/ c).

(* This lemma is taken from a proof of correctness for an algorithm in 
  geometry. *)

Lemma rotate3 : forall (A:Type), forall R : A -> A -> A -> Prop,
  (forall x y z, R x y z -> R y z x) ->
  forall a b c, R a b c -> R c a b.
End intuitionistic_predicate.