Library Escuela_2

Petite Ecole : Cours N° 2
Rappel du cours N° 1

Check 3.

Check 3+5.

Compute 3+5.
Require Import ZArith.
Open Scope Z_scope.
Compute leb (5*7) (9*4).

Definition double (n:Z) := n*2.

Definition square (n:Z) := n×n.

Definition Z_compose (g f : ZZ) (z:Z) := g (f z).

Compute Z_compose square double 2.

Compute Z_compose double square 2.

Definition compose (A B C: Type)(g : BC)(f : AB) (a:A) := g (f a).

Check compose.

SearchAbout (natZ).

Compute compose _ _ _ square Z.of_nat (3%nat).

Arguments compose [A B C] g f a.

Compute compose square Z.of_nat (3%nat).

Definition compose_succ (A:Type)(f: natA) := compose f S.

Compute compose_succ _ (fun nsquare (Z.of_nat n)) 4.

Fin des rappels
Un peu de logique

Check 3=3.

Check 2=3.

Check True.

Check False.

Check true.

Check Prop.

Section Propositional_logic.

 Variables P Q R S : Prop.

 Check PQ.

 Check (PQ)->(QR) → (PR).

 Check (fun p:Pp).

 Check fun (H : PQ)(H0 : QR) (p:P) ⇒ H0 (H p).

 Lemma imp_trans : (PQ) → (QR) → PR.
 Proof fun (H : PQ)(H0 : QR) (p:P) ⇒ H0 (H p).

 Lemma imp_refl : PP.
 Proof fun p:Pp.

 Lemma imp_trans' : (PQ) → (QR) → PR.
 Proof.
   intro H.
   intro H0.
   intro p.
   apply H0.
   apply H.
   assumption.
Qed.

Lemma imp_trans'' : (PQ) → (QR) → PR.
 Proof.
   intros H H0 p.
   apply H0.
   apply H.
   assumption.
Qed.

Lemma imp_trans''' : (PQ) → (QR) → PR.
Proof.
  intros H H0 p;apply H0;apply H; trivial.
Qed.

Lemma imp_trans_4 : (PQ) → (QR) → PR.
Proof. auto. Qed.

proofs with various subgoals

Lemma imp_dist : (PQR) → (PQ) → PR.
Proof.
 intros H H0 p.
 apply H.
 assumption.
 apply H0;assumption.
Qed.

Print imp_dist.

Exercise: Remove the "auto" in the following proofs and use only the tactics intros, apply and assumption

Lemma L1 : (PQR) → (QPR).
auto.
Qed.

Lemma L2 : (((PQ)->Q)->Q)-> PQ.
auto.
Qed.

Falsehood and negation
The negation of a proposition is defined by
Definition not (P:Prop) := P -> False.
The notation ~P is usable for (not P)
Replacing a negation by an implication is esaily done
in the conclusion of the goal by "unfold not" in a hypothesis H by "unfold not in H"

Lemma double_neg_i : P → ~(~ P).
Proof.
 intros p H.
 unfold not in H .
 apply H; trivial.
Qed.

Lemma triple_neg : ~(~(~P)) → ¬P.
Proof.
 auto.
Qed.

Lemma contraposee : (PQ) → ¬Q → ¬P.
auto.
Qed.

Falsehood (2) : Elimination

Lemma L23 : False → 2 = 3.
Proof.
 intro H.
 elim H.
Qed.

Lemma L4 : ¬PPQ.
Proof.
 intros H H0.
 Check (H H0).
 elim (H H0).
Qed.

Lemma L4' : ¬PPQ.
Proof.
 intros H H0.
 unfold not in H.
  destruct H.
 assumption.
Qed.

Lemma L4'' : ¬PPQ.
Proof. tauto. Qed.

Proofs with sublemmas

Lemma L4''' : ¬PPQ.
Proof.
 intros H H0.
 assert (H1 : False).
 now apply H.
 destruct H1.
Qed.

Remove the tauto tactic !

Lemma L5 : (P → ¬P) → ¬P.
tauto.
Qed.

Lemma L6 : (PQ) → (~PQ) → ~~Q.
Proof.
 tauto.
Qed.

Connectives

Lemma L7 : PPQ.
Proof.
 intro H;left.
trivial.
Qed.

Lemma L8 : (PR) → (QR) → PQR.
Proof.
 intros H H0 H1.

 destruct H1.  now apply H.
 now apply H0.
Qed.

Lemma L8' : (PR) → (QR) → PQR.
Proof.
 intros H H0 H1.
 destruct H1;[apply H|apply H0];trivial.
Qed.

Lemma L9 : PQQP.
Proof. tauto. Qed.

Lemma L10 : PQP.
Proof.
 intro H;destruct H. assumption.
Qed.

Lemma L11 : PQPQ.
Proof.
 intros p q;split.
 assumption.
 assumption.
Qed.

Lemma L12 : ~(PQ) → ¬P ∧ ¬Q.
Proof.
 tauto.
Qed.

1 star exercise
Lemma L13 : ~(PQ) → ~~ (~P ∨ ¬Q).
Proof.
tauto.
Qed.

Lemma L14 : ~~(P ∨ ¬P).
Proof.
 tauto.
Qed.

End Propositional_logic.

Teasing

Lemma exm : ( P:Prop,~~PP) → ( P:Prop, P ∨ ¬P).
Proof.
 intros H P.
 apply H.
 intro H0.
 apply H0.
 right.
 intro H1.
 apply H0;left.
 assumption.
Qed.

Lemma exm' : ( P:Prop, P ∨ ¬P) → ( P:Prop,~~PP).
Admitted.

Lemma Peirce : ( P:Prop, P ∨ ¬P)->
                 P Q:Prop, ((PQ)-> P)->P.
Proof.
 intros exm P Q.
 destruct (exm P).
 Admitted.

Lemma Peirce' : ( P Q:Prop, ((PQ)-> P)->P) →
                ( P:Prop, P ∨ ¬P).
Proof.
intro H.
 apply exm.
 intros P.
 intro.
 generalize (H P False).
Admitted.
Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)

Global Index

E

Escuela_2 [library]



Library Index

E

Escuela_2



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)

This page has been generated by coqdoc