(*** Exercice 1 ***) Section Exo1. Variable P Q R : Prop. Variable A : Set. Variable a : A. Variable B : Set. Variable p : A -> Prop. Variable q : A -> Prop. Variable r : B -> Prop. Lemma a1 : (P /\ (Q \/ R)) -> (P /\ Q) \/ (P /\ R). Proof. intro H. destruct H as (H1,H2). destruct H2. left. split. assumption. assumption. right. split. assumption. assumption. Qed. Lemma a2 : (P \/ (Q /\ R)) -> (P \/ Q) /\ (P \/ R). Proof. intro H. destruct H as [H1|H2]. split. left. assumption. left. assumption. destruct H2. split. right. assumption. right. assumption. Qed. Lemma a3 : (P -> Q) -> (P -> Q -> R) -> (P -> R). Proof. intros H1 H2 H3. apply H2. assumption. apply H1. assumption. Qed. Lemma a4 : ((P -> Q) -> R) -> (P -> R) -> (R -> Q) -> R. Proof. intros H1 H2 H3. apply H1. intro H4. apply H3. apply H2. apply H4. Qed. Lemma a6 : (forall x:A, p x) -> (exists x:A, p x). Proof. intro H. exists a. apply H. Qed. Lemma a7 : ((forall x, p x) /\ (forall x, q x)) -> (forall x, p x /\ q x). intros H x. destruct H as (H1,H2). split. apply H1. apply H2. Qed. End Exo1. (*** Exercice 2 ***) Section Exo2. Variable A : Set. Definition semi_inverse (f1 : A->A) (f2 : A->A) := forall x, f1 (f2 x) = x. Definition injective (f: A -> A) := forall x y, f x = f y -> x = y. Definition surjective (f: A -> A) := forall y, exists x, y = f x. Theorem semi_inverse_surj : forall f1 f2, semi_inverse f1 f2 -> surjective f1. Proof. intros f1 f2. unfold semi_inverse. unfold surjective. intros H y. assert (f1 (f2 y) = y). apply H. exists (f2 y). symmetry. assumption. Qed. Theorem semi_inverse_inj_inv : forall f1 f2, semi_inverse f1 f2 -> injective f1 -> semi_inverse f2 f1. Proof. intros f1 f2. unfold semi_inverse. unfold injective. intros H1 H2 x. apply H2. apply H1. Qed. Theorem semi_inverse_inj : forall f1 f2, semi_inverse f1 f2 -> injective f2. Proof. intros f1 f2. unfold semi_inverse. unfold injective. intros H1 a b H2. rewrite <- H1 with (x:=a). rewrite <- H1 with (x:=b). rewrite H2. reflexivity. Qed. Definition bijective (f:A->A) : Prop := injective f /\ surjective f. Definition inverse (f1:A->A) (f2:A->A) : Prop := semi_inverse f1 f2 /\ semi_inverse f2 f1. Theorem inverse_bij : forall f1 f2, inverse f1 f2 -> bijective f1. Proof. intros g h. unfold inverse. unfold bijective. intro H. destruct H as (H1,H2). split. apply semi_inverse_inj with (f1:=h). assumption. apply semi_inverse_surj with (f2:=h). assumption. Qed. Definition comp (f : A->A) (g : A->A) := fun x => f (g x). Theorem semi_inverse_comp : forall f1 f2 g1 g2, semi_inverse f1 f2 -> semi_inverse g1 g2 -> exists h, semi_inverse (comp f1 g1) h. Proof. unfold semi_inverse. unfold comp. intros f1 f2 g1 g2 H1 H2. exists (comp g2 f2). intro x. unfold comp. rewrite H2. apply H1. Qed. End Exo2. (*** Eercice 3 ***) Section Exo3. Inductive p0 : nat -> Prop := | p0S : forall x, p0 x -> p0 (S x). Inductive p1 : nat -> Prop := | p1_0 : p1 0 | p1_s : forall x, p1 (S x) -> p1 x. Inductive p2 : nat -> Prop := | p2_0 : p2 0 | p2_2 : p2 2 | p2_s : forall x, p2 (x) -> p2 (S(S(S(S x)))). Theorem th0 : forall x, ~(p0 x). Proof. intros x H. induction H. assumption. Qed. Theorem th1 : forall x, p1 x -> x = 0. Proof. intros x H. induction H. reflexivity. discriminate IHp1. Qed. Inductive even : nat -> Prop := | e_0 : even 0 | e_s2 : forall x, even x -> even(S (S x)). Theorem th2 : forall x, p2 x -> even x. intros x H. induction H. apply e_0. apply e_s2. apply e_0. apply e_s2. apply e_s2. assumption. Qed. End Exo3. (*** Exercice 4 ***) Section Exo4. Inductive div : nat -> nat -> nat -> nat -> Prop := | div0 : forall n p, n < p -> div n p 0 n | divp : forall n p q r, div n p q r -> div (n+p) p (S q) r. Theorem r_correct : forall n q p r, div n p q r -> r < p. Proof. intros n p q r H. induction H. assumption. assumption. Qed. Require Import Omega. Theorem q_correct : forall n p q r, div n p q r -> n = q * p + r. Proof. intros n p q r H. induction H. simpl. reflexivity. simpl. rewrite IHdiv. omega. Qed. End Exo4. Require Import Omega. Variable f : nat -> nat. Axiom H_f : forall x y, f (x+y) = f x + f y. Theorem f_0 : f 0 = 0. assert (f (0+0) = f 0 + f 0). apply H_f. simpl in H. omega. Qed. Theorem lineaire : forall x, f x = x * f 1. Proof. intro x. induction x. rewrite f_0. omega. simpl. rewrite <- IHx. rewrite <- H_f. assert (S x = 1 + x). omega. reflexivity. Qed. (*** Exo 3 ***) Variable Char : Set. Require Import List. Definition mot := list Char. Inductive palindrome : mot -> Prop := | pal_nil : palindrome nil | pal_cons : forall w:mot, forall x:Char, palindrome w -> palindrome (x::(w++(x::nil))). Theorem palindrome_rev : forall w, palindrome w -> palindrome (rev w). Proof. intros w H. induction H. simpl. apply pal_nil. assert ((x :: w ++ x :: nil) = (x :: w) ++ (x :: nil)) as H1. simpl. reflexivity. rewrite H1. rewrite distr_rev. simpl. apply pal_cons. assumption. Qed. (*** Exo 4 ***) Inductive p0 : nat -> Prop := | p0S : forall x, p0 x -> p0 (S x). Inductive p1 : nat -> Prop := | p1_0 : p1 0 | p1_s : forall x, p1 (S x) -> p1 x. Inductive p2 : nat -> Prop := | p2_0 : p2 0 | p2_2 : p2 2 | p2_s : forall x, p2 (x) -> p2 (S(S(S(S x)))). Theorem th0 : forall x, ~(p0 x). Proof. intros x H. induction H. assumption. Qed. Theorem th1 : forall x, p1 x -> x = 0. Proof. intros x H. induction H. reflexivity. discriminate IHp1. Qed. Inductive even : nat -> Prop := | e_0 : even 0 | e_s2 : forall x, even x -> even(S (S x)). Theorem th2 : forall x, p2 x -> even x. intros x H. induction H. apply e_0. apply e_s2. apply e_0. apply e_s2. apply e_s2. assumption. Qed. Inductive exp : nat -> nat -> Prop := | exp_0 : exp 0 1 | exp_s : forall x y, exp x y -> exp (S x) (2*y). Theorem exp_tot : forall n, exists e, exp n e. Proof. intro n. induction n. exists 1. apply exp_0. destruct IHn. exists (2*x). apply exp_s. assumption. Qed. Theorem exp_func : forall n e, exp n e -> forall e1, exp n e1 -> e=e1. Proof. intros n e H1. induction H1; intros e2 H2. inversion H2. reflexivity. inversion H2. assert (y = y0). apply IHexp. assumption. rewrite H4. reflexivity. Qed. apply IHexp. End dm.