Instructions : Le sujet comporte 6 parties indépendantes :

• Logique de base (calcul des propositions, sans tiers exclu)
• Entiers naturels et récurrence (sans tiers exclu)
• Calcul des prédicats (il existe, pour tout) et tiers exclu
• Réels, propriétés de base, sans automatisation
• Entiers naturels et relation d'ordre (sans tiers exclu)

Les tactiques autorisées sont celles du cours :

• intros
• exact
• apply et apply ... in
• split
• destruct
• exfalso
• exists
• reflexivity
• specialize
• rewrite, rewrite <-, rewrite ... in, rewrite ... <- in et toutes les variantes rewrite ... at numéro
• simpl
• induction
• unfold
• les tactiques pour le raissonnement vers l'avant :
• assert ... as ...
• replace ... with ...
• pose proof ... as ...

1. Logique de base

Section LogiqueBase.

Dans cette partie, il n'y a besoin d'aucun lemme, juste la logique de base et les tactiques liées à la logique ( intros, exact, apply, ...)

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma conj_and : forall (A B : Prop), A -> B -> A /\ B. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma imp_transitivity : forall (A B C : Prop), (A -> B) -> (B -> C) -> (A -> C). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma and_not_diag_falso : forall (A : Prop), A /\ ~A -> forall (B : Prop), B. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma or_induction : forall (A B C : Prop), (A -> C) -> (B -> C) -> A \/ B -> C. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma or_not_r_imp : forall (A B : Prop), B \/ ~A -> A -> B. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End LogiqueBase. From Coq.Arith Require Import PeanoNat.

2. entiers naturels, calcul, induction

Section NatBase. Import Nat(add, mul). Import (notations) Nat.

Dans cette partie, on travaille sur les entiers naturels de Peano, et on n'a besoin de rien d'autre que de la définition usuelle de l'addition et de la multiplication (qu'on rappelle ci-dessous). On n'utilisera donc aucun lemme (à part peut-être ceux de cette partie), mais on n'hésitera pas à utiliser les tactiques basées sur le calcul comme simpl et discriminate (bien sûr il peut y avoir des inductions, des rewrite, ...).

Print add. Print mul.

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma add_2_l (n : nat) : 2 + n = S (S n). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma add_2_r (n : nat) : n + 2 = S (S n). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

On définit maintenant une opération "ajouter 2 n fois" par récurrence :

Fixpoint two_mul (n : nat) := match n with | 0 => 0 | (S p) => 2 + (two_mul p) end.

Exercice (difficulté 20) : Prouver le théorème suivant.

Lemma two_mul_not_0 (n : nat) : n <> 0 <-> two_mul n <> 0. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma two_mul_mul_2_r (n : nat) : two_mul n = n * 2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End NatBase.

3. Logique des prédicats et logique classique

3.1 Calcul des prédicats sans tiers-exclus

Section Predicats.

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma not_exists_forall {T : Type} (P : T ->Prop) : ~(exists (x : T), P x) -> forall (x : T), ~ P x. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma forall_not_exists {T : Type} (P : T -> Prop) : (forall (x : T), ~ P x) -> ~(exists (x : T), P x). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End Predicats.

3.2 Logique avec tiers-exclus

From Coq Require Import Classical. Section LogiqueClassique.

Dans cette partie, il y a parfois besoin de l'axiome du tiers exclu. Rappel: celuis-ci dit

Check classic.

On l'utilise pour faire un raisonnement par cas sur la validité ou non d'une proposition plus ou moins élaborée avec destruct classic(...) as [H | H].

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma contrapose (P Q : Prop) : (~Q -> ~P) -> P -> Q. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 25) : Prouver le théorème suivant.

Lemma classical_equiv : forall (P Q : Prop), (P <-> Q) <-> ((P /\ Q) \/ (~ P /\ ~ Q)). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End LogiqueClassique.

4. Nombres réels, égalités et inégalités

From Coq Require RIneq. Section RéelsBase. Open Scope R_scope. Import Rdefinitions. Import Raxioms(Rplus_comm, Rplus_0_l, Rplus_assoc, Rplus_opp_r, Rplus_lt_compat_l, Rmult_lt_compat_l, Rmult_assoc, Rmult_comm, Rinv_l, Rmult_1_l, Rmult_lt_compat_l). Import RIneq(Rplus_eq_compat_l, Rplus_eq_compat_r, Rmult_eq_compat_l, Rmult_eq_compat_r, Rplus_opp_l, Rplus_0_r, Rplus_lt_compat_r, Rlt_0_1, Rmult_0_l, Rmult_0_r, Rinv_r, Rplus_lt_reg_l, Rplus_lt_reg_r, Rmult_1_r, Rmult_lt_compat_r, Rmult_lt_reg_l, Rmult_lt_reg_r).

Dans cette partie, vous utiliserez seulement les propriétés de base sur l'addition et la multiplication dans R :

Check Rlt_0_1. Check Rplus_0_l. Check Rplus_0_r. Check Rplus_assoc. Check Rplus_comm. Check Rplus_eq_compat_l. Check Rplus_eq_compat_r. Check Rplus_lt_compat_l. Check Rplus_lt_compat_r. Check Rplus_lt_reg_l. Check Rplus_lt_reg_r. Check Rplus_opp_l. Check Rplus_opp_r. Check Rmult_0_l. Check Rmult_0_r. Check Rmult_1_l. Check Rmult_1_r. Check Rmult_assoc. Check Rmult_comm. Check Rinv_l. Check Rinv_r. Check Rmult_eq_compat_l. Check Rmult_eq_compat_r. Check Rmult_lt_compat_l. Check Rmult_lt_compat_l. Check Rmult_lt_compat_r. Check Rmult_lt_reg_l. Check Rmult_lt_reg_r.

Dans toute cette partie, on considère 2 réels a et b fixés. Ils seront dans le contexte de tous les lemmes.

Context {a b : R}.

La définition de "fonction strictement croissante" est la suivante :

Definition increasing (f : R -> R) := forall (x y : R), x < y -> f x < f y.

N'hésitez pas à unfold increasing en cas de besoin.

On considère la fonction affine aff suivante :

Definition aff (x : R) := a * x + b.

De la même manière, n'hésitez pas à unfold aff

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma a_pos_aff_incr : 0 < a -> increasing aff. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 20) : Prouver le théorème suivant.

Lemma aff_incr_a_pos : increasing aff -> 0 < a. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 25) : Prouver le théorème suivant.

Lemma aff_eq_0 : a <> 0 -> (forall (x : R), (aff x = 0) -> x = - b * / a). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 20) : Prouver le théorème suivant.

Lemma eq_0_aff : a <> 0 -> (forall (x : R), x = - b * / a -> aff x = 0). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End RéelsBase.

5. Entiers naturels et relations

Section LeBizarre. Import Nat(add, mul, le_refl, le_trans, le_antisymm, leb_le, nle_succ_diag_l, le_ge_cases, le_0_l). Import (notations) Nat.

On commence par définir un type pair_ou_impair à deux éléments qui sont pair et impair.

Inductive pair_ou_impair := | pair : pair_ou_impair | impair : pair_ou_impair.

Rappel : pair ou impair est un type à deux constructeurs constants qui sont pair et impair, donc avec un hypothèse du type H : pair = impair, il suffit de discriminate H pour prouver False (et donc n'importe quoi).

On calcule maintenant par récurrence la parité d'un entier naturel n :

• la parité de 0 est "pair"
• la parité de 1 est "impair"
• la parité de n + 2 est la même que la parité de n.

Fixpoint parité (n : nat) := match n with | 0 => pair | 1 => impair | S (S p) => parité p end.

Noter que notre fonction parité calcule :

Compute (parité 5). Compute (parité 42). Eval simpl in (fun n => parité (4 + n)).

Pour faire des raisonnements par cas, on pourra se servir du lemme suivant. Indice, on peut utiliser destruct (parité n) eqn:parn pour faire un raisonnement par cas sur la valeur de (parité n).

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma nat_pair_ou_impair : forall n, parité n = pair \/ parité n = impair. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 10) : Prouver le théorème suivant.

Lemma non_pair_et_impair : forall n, ~(parité n = pair /\ parité n = impair). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 20) : Prouver le théorème suivant.

Lemma parité_succ (n : nat) : (parité n = pair -> parité (S n) = impair) /\ (parité n = impair -> parité (S n) = pair). Proof. induction n as [| n IH]. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Maintenant on définit la relation << (ici appelée le_bizarre, où le est l'abbréviation de "less than or equal to") :

Definition le_bizarre (x y : nat) := (parité x = parité y /\ x <= y) \/ (parité x = impair /\ parité y = pair). Notation "x << y" := (le_bizarre x y) (at level 70).

Intuitivement, on a 1 << 3 << 5 << ... << 0 << 2 << 4 << ...

On va prouver que << est un ordre total sur nat. On aura besoin des propriétés correspondantes sur <=.

Check le_refl. Check le_antisymm. Check le_trans. Check le_ge_cases.

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma le_bizarre_refl (x : nat) : x << x. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 20) : Prouver le théorème suivant.

Lemma le_bizarre_antisymm (x y : nat) : x << y -> y << x -> x = y. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 20) : Prouver le théorème suivant.

Lemma le_bizarre_trans (x y z : nat) : x << y -> y << z -> x << z. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 10) : Prouver le théorème suivant.

Indications : vous pourrez utiliser :

Check le_n_S. Check le_0_l.

ou passer par l'opération leb qui calcule avec leb_le :

Check leb_le. Lemma le_1_S (x : nat) : 1 <= S x. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 15) : Prouver le théorème suivant.

Lemma le_bizarre_1_min : forall x, 1 << x. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 15) : Prouver le théorème suivant.

Voici quelques lemmes qui peuvent vous aider (pas la peine de tous les utiliser) en plus de ceux déjà proposés plus hauts.

Check le_S. Check le_n_S. Check le_S_n. Check nle_succ_diag_l. Lemma not_succ_succ_le (n : nat) : ~(S (S n) <= n). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 30) : Prouver le théorème suivant.

Lemma le_bizarre_pas_de_max : ~ (exists M, forall x, x << M). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice (difficulté 30) : Prouver le théorème suivant.

Lemma le_bizarre_total (x y : nat) : x << y \/ y << x. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End LeBizarre.