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 : Z → Z) (z:Z) := g (f z).
Compute Z_compose square double 2.
Compute Z_compose double square 2.
Definition compose (A B C: Type)(g : B → C)(f : A → B) (a:A) := g (f a).
Check compose.
SearchAbout (nat→Z).
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: nat→ A) := compose f S.
Compute compose_succ _ (fun n ⇒ square (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 P → Q.
Check (P → Q)->(Q → R) → (P → R).
Check (fun p:P ⇒ p).
Check fun (H : P → Q)(H0 : Q → R) (p:P) ⇒ H0 (H p).
Lemma imp_trans : (P → Q) → (Q → R) → P → R.
Proof fun (H : P → Q)(H0 : Q → R) (p:P) ⇒ H0 (H p).
Lemma imp_refl : P → P.
Proof fun p:P ⇒ p.
Lemma imp_trans' : (P → Q) → (Q → R) → P → R.
Proof.
intro H.
intro H0.
intro p.
apply H0.
apply H.
assumption.
Qed.
Lemma imp_trans'' : (P → Q) → (Q → R) → P → R.
Proof.
intros H H0 p.
apply H0.
apply H.
assumption.
Qed.
Lemma imp_trans''' : (P → Q) → (Q → R) → P → R.
Proof.
intros H H0 p;apply H0;apply H; trivial.
Qed.
Lemma imp_trans_4 : (P → Q) → (Q → R) → P → R.
Proof. auto. Qed.
proofs with various subgoals
Lemma imp_dist : (P → Q → R) → (P → Q) → P→ R.
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 : (P→ Q → R) → (Q → P → R).
auto.
Qed.
Lemma L2 : (((P→Q)->Q)->Q)-> P → Q.
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 : (P → Q) → ¬Q → ¬P.
auto.
Qed.
Falsehood (2) : Elimination
Lemma L23 : False → 2 = 3.
Proof.
intro H.
elim H.
Qed.
Lemma L4 : ¬P → P → Q.
Proof.
intros H H0.
Check (H H0).
elim (H H0).
Qed.
Lemma L4' : ¬P → P → Q.
Proof.
intros H H0.
unfold not in H.
destruct H.
assumption.
Qed.
Lemma L4'' : ¬P → P → Q.
Proof. tauto. Qed.
Proofs with sublemmas
Lemma L4''' : ¬P → P → Q.
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 : (P → Q) → (~P → Q) → ~~Q.
Proof.
tauto.
Qed.
Connectives
Lemma L7 : P → P ∨ Q.
Proof.
intro H;left.
trivial.
Qed.
Lemma L8 : (P → R) → (Q → R) → P ∨ Q → R.
Proof.
intros H H0 H1.
destruct H1. now apply H.
now apply H0.
Qed.
Lemma L8' : (P → R) → (Q → R) → P ∨ Q → R.
Proof.
intros H H0 H1.
destruct H1;[apply H|apply H0];trivial.
Qed.
Lemma L9 : P∨Q → Q ∨ P.
Proof. tauto. Qed.
Lemma L10 : P ∧ Q → P.
Proof.
intro H;destruct H. assumption.
Qed.
Lemma L11 : P → Q → P ∧ Q.
Proof.
intros p q;split.
assumption.
assumption.
Qed.
Lemma L12 : ~(P ∨ Q) → ¬P ∧ ¬Q.
Proof.
tauto.
Qed.
1 star exercise
Lemma L13 : ~(P ∧ Q) → ~~ (~P ∨ ¬Q).
Proof.
tauto.
Qed.
Lemma L14 : ~~(P ∨ ¬P).
Proof.
tauto.
Qed.
End Propositional_logic.
Proof.
tauto.
Qed.
Lemma L14 : ~~(P ∨ ¬P).
Proof.
tauto.
Qed.
End Propositional_logic.
Teasing
Lemma exm : (∀ P:Prop,~~P →P) → (∀ 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,~~P →P).
Admitted.
Lemma Peirce : (∀ P:Prop, P ∨ ¬P)->
∀ P Q:Prop, ((P → Q)-> P)->P.
Proof.
intros exm P Q.
destruct (exm P).
Admitted.
Lemma Peirce' : (∀ P Q:Prop, ((P → Q)-> 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_2Global 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