(* Mini projet pour la premiere partie du cours de Logique: Regle du jeu : Le fichier qui suit contient un certain nombre d'Admitted. Il s'agit de remplacer ces Admitted par des preuves completes *) (* Exercices sur la logique du second ordre *) Theorem triple_neg : forall P:Prop, ~ ~ ~ P -> ~ P. Proof. intros P H p. (* 1 subgoal P : Prop H : ~ ~ ~ P p : P ============================ False *) destruct H. (* 1 subgoal P : Prop p : P ============================ ~ ~ P la suite de la preuve est facile. Voici une solution parmi d'autres: *) unfold not;auto. Qed. Theorem ex_eq : forall (A:Set) (a b:A), (exists m:A, a = m /\ m=b) -> a = b. Proof. intros A a b H. (* on elimine l'existentiel, ce qui declare une variable x *) destruct H. (* il suffit d'eliminer la conjonction, puis de se servir de l'egalite a=x *) destruct H. rewrite H;assumption. Qed. (* Voici une variante qui utilise un style plus direct (utilise par certains binomes) *) Theorem ex_eq' : forall (A:Set) (a b:A), (exists m:A, a = m /\ m=b) -> a = b. Proof. intros A a b (m,(H1,H2));subst m;assumption. Qed. Theorem thm_42 : forall (A:Set) (a:A), (forall b:A, ~ a=b) -> 1=42. Proof. intros A a H. (* A tout moment on peut introduire un lemme d'énoncé E dans une preuve par la commande 'assert E'. Si le but courant est G, deux buts sont crées a) prouver E b) montrer que E sert à prouver G *) (* on peut montrer que le contexte courant implique a<>a, ce qui est absurde L'enonce suggere la tactique "assert (a <> a) ", qui fonctionne bien. une autre solution, plus courte utilise "absurd". *) absurd (a=a). (* 2 subgoals A : Set a : A H : forall b : A, a <> b ============================ a <> a subgoal 2 is: a = a *) apply H. reflexivity. Qed. (* Exercice sur le tiers exclu *) Section Klas1. Hypothesis tiers_exclu : forall P : Prop, P \/ ~ P. Lemma L1 : forall P Q R: Prop, ((P -> Q) -> R) -> ((Q -> P) -> R) -> R. Proof. intros P Q R H H0. (* tiers_exclu : forall P : Prop, P \/ ~ P P : Prop Q : Prop R : Prop H : (P -> Q) -> R H0 : (Q -> P) -> R ============================ R *) destruct (tiers_exclu P). (* tiers_exclu : forall P : Prop, P \/ ~ P P : Prop Q : Prop R : Prop H : (P -> Q) -> R H0 : (Q -> P) -> R H1 : P ============================ R subgoal 2 is: R *) apply H0;auto. (* 1 subgoal tiers_exclu : forall P : Prop, P \/ ~ P P : Prop Q : Prop R : Prop H : (P -> Q) -> R H0 : (Q -> P) -> R H1 : ~ P ============================ R facile ! H1 nous permettra de prouver (P -> Q), donc R *) apply H;intro p. destruct H1; assumption. Qed. Lemma L2 : forall P Q:Prop, (P -> Q) \/ (Q -> P). Proof. (* a peu pres le meme raisonnement que L1 *) intros P Q; destruct (tiers_exclu P). right;auto. left;intro H0;destruct H;assumption. Qed. End Klas1. Section Klas2. Hypothesis Hyp1 : forall P Q R: Prop, ((P -> Q) -> R) -> ((Q -> P) -> R) -> R. (* La c'est interessant : sous l'hypothese Hyp1, on a plus que la logique intuitionniste, mais pas tout à fait la logique classique (car on montre une regle plus faible que le tiers exclu *) Lemma presque_le_tiers_exclu : forall P:Prop, ~P \/ ~~P. Proof. intros; apply Hyp1 with P (not P). (* 1er sous-but P : Prop ============================ (P -> ~ P) -> ~ P \/ ~ ~ P Facile ! si on a (P -> ~P), alors on a forcement ~ P *) left;intro H0. apply H;assumption. (* second sous-but : P : Prop ============================ (~ P -> P) -> ~ P \/ ~ ~ P *) right. intro H0. (* P : Prop H : ~ P -> P H0 : ~ P ============================ False *) absurd (P);auto. Qed. End Klas2. Section Klas3. Hypothesis Hyp2 : forall P Q: Prop, (P -> Q) \/ (Q -> P). Lemma encore_presque_le_tiers_exclu : forall P:Prop, ~P \/ ~~P. Proof. intros. (* la commande suivante nous permet d'engendrer deux sous-buts, l'un avec l'hypothese P -> ~P (qui nous permettra de deduire ~P) l'autre avec l'hypothese ~P -> P, qui permet de montrer ~ (~P) *) destruct (Hyp2 P (not P)). left. intro H0. destruct (H H0). assumption. right. intro H1. absurd P;auto. Qed. End Klas3. (* Etude d'une axiomatique de l'arithmetique *) (************************************************* Note : ceci est une illustration de notions vues en cours. En Coq les entiers naturels, l'addition et la multiplications sont traitées sans axiomes et d'une maniere beaucoup plus efficace, ainsi que les inégalités <= et < De même, ce fichier utilise volontairement des tactiques 'de base'. Il peut sans nul doute être beaucoup plus concis. *******************************************************) Parameter Nat : Set. Parameter zero : Nat. Parameter S : Nat -> Nat. Parameter plus : Nat -> Nat -> Nat. Parameter mult : Nat -> Nat -> Nat. Notation "n + p" := (plus n p). Notation "n * p" := (mult n p). (* Axiomes (sont des théorèmes dans la bibliotheque standard de Coq) *) Axiom zero_not_S : forall n:Nat, S n <> zero. Axiom S_injective : forall n p, S n = S p -> n = p. Axiom zero_plus_n : forall n:Nat, zero + n = n. Axiom S_plus_n : forall n p:Nat, S n + p = S (n + p). Axiom zero_mult_n : forall n:Nat, zero * n = zero. Axiom S_mult_n : forall n p: Nat, (S n)*p = p + (n * p). (* axiome de recurrence *) Axiom Nat_ind : forall (P:Nat->Prop), P zero -> (forall p:Nat, P p -> P (S p)) -> forall n:Nat, P n. Hint Resolve zero_not_S S_injective zero_plus_n S_plus_n. Lemma fib_ind : forall (P:Nat->Prop), P zero -> P (S zero) -> (forall p : Nat, P p -> P (S (S p))) -> forall n : Nat, P n. Proof. intros P H0 H1 H n. assert (P n /\ P (S n)). destruct n using Nat_ind. auto. destruct IHn;auto. destruct H2. auto. Qed. Lemma zero_or_S : forall n:Nat, n=zero \/ exists p:Nat, n = S p. Proof. intro n; induction n using Nat_ind. auto. right;exists n;auto. Qed. (* Le prédicat 'inférieur ou égal' est axiomatisé, à la différence du cours et de la bibliiothèque standard de Coq (où il est défini) *) Parameter Le : Nat -> Nat -> Prop. Notation "n <= p" := (Le n p). Axiom Le_n : forall n:Nat, n<=n. Axiom Le_S : forall n p:Nat, n <= p -> n <= S p. (* Permet aux tactiques "auto" et "auto" d'utiliser ces axiomes *) Hint Resolve Le_n Le_S. (* Le_ind exprime la "récurrence complète": Pour prouver que n <= q -> P q il suffit de prouver P n et que si n <= p et P p, alors P(S p) *) Axiom Le_ind : forall n:Nat, forall P:Nat -> Prop, P n -> (forall p : Nat, n <= p -> P p -> P (S p)) -> forall q:Nat, n<= q -> P q. (* Cette preuve utilise Le_ind *) Lemma Le_Sn_p : forall n p, S n <= p -> n <= p. Proof. intros n p H. induction H using Le_ind. auto. auto. Qed. (* on place Ce résultat dans la base de théorèmes pour auto *) Hint Resolve Le_Sn_p. Theorem Le_trans : forall n p q:Nat, n <= p -> p <= q -> n <= q. Proof. intros n p q H;induction H using Le_ind;auto. Qed. Lemma Le_inv : forall n p : Nat, n <= p -> n= p \/ exists q:Nat, p = S q /\ n <= q. Proof. intros n p H;induction H using Le_ind. auto. destruct IHLe. right;exists p;auto. destruct H0. destruct H0. right;exists (S x). split. rewrite H0;trivial. auto. Qed. Lemma Le_n_zero : forall n:Nat, n<=zero -> n=zero. Proof. intros n H. (* 1 subgoal n : Nat H : n <= zero ============================ n = zero Ici, on veut appliquer Le_inv Cette fonction prend trois arguments : un entier n un entier p une preuve H : n<= p Si on veut faire une preuve par cas, il suffit d'utiliser destruct sur le terme (Le_inv n zero H) dont le type est n= zero \/ exists q:Nat, zero = S q /\ n <= q. *) destruct (Le_inv n zero H). auto. destruct H0. destruct H0. destruct (zero_not_S x). rewrite H0;auto. Qed. Lemma Le_n_Sn : forall n, n <= S n. Proof. info auto. (* intro n; simple apply Le_S; simple apply Le_n. *) Qed. Lemma Le_zero_n : forall n:Nat, zero <= n. Proof. (* on peut proceder par recurrence sur n *) intro n;induction n using Nat_ind. (* cas de base : ============================ zero <= zero *) apply Le_n. (* pas de recurrence 1 subgoal n : Nat IHn : zero <= n ============================ zero <= S n *) apply Le_S;assumption. Qed. (* en fait, cette preuve pouvait se faire en une ligne : Lemma Le_zero_n : forall n:Nat, zero <= n. Proof. intro n; induction n using Nat_ind;auto. Qed. *) Hint Resolve Le_zero_n. Definition Lt n p := S n <= p. Notation "n < p" := (Lt n p). (* A tout moment, on peut transformer un but contenant (a < b) par 'unfold lt' (qui le remplace par ((S a) <= b) On peut faire ce remplacement dans une hypothèse H avec 'unfold lt in H' *) Lemma Lt_trans : forall n p q:Nat, n < p -> p < q -> n < q. Proof. unfold Lt;intros n p q H H0. (* 1 subgoal n : Nat p : Nat q : Nat H : S n <= p H0 : S p <= q ============================ S n <= q *) apply Le_trans with p;auto. Qed. Lemma Le_cases : forall n p, n <= p -> n < p \/ n = p. Proof. (* Ici, on choisit la "recurrence a partir de n (Le_ind) *) intros n p H; induction H using Le_ind;auto. (* 1 subgoal n : Nat p : Nat H : n <= p IHLe : n < p \/ n = p ============================ n < S p \/ n = S p *) (* L'hypothese de recurrence est une disjonction. dans le premier cas la transitivite de Lt sera facile a utiliser. dans le second, si on remplace n par p, il sera facile de prouver p < S p *) destruct IHLe. left; eapply Lt_trans with p;auto. unfold Lt;auto. left; rewrite H0;unfold Lt;auto. Qed. Lemma Lt_Le : forall n p, n < p -> n <= p. Proof. intros n p H. auto. Qed. Lemma Le_S_S : forall n p, n <= p -> S n <= S p. Proof. (* La encore, il s'agit d'une recurrence "a partir de n" *) intros n p H;induction H using Le_ind; info auto. Qed. Lemma Le_n_S_p : forall n p, n <= S p -> n = S p \/ n <= p. Proof. (* Le_inv donne deux cas pour l'hypothese n <= S p : a) n = S P (preuve triviale b) il existe q tel que S p = S q et n <= q *) intros n p H; destruct (Le_inv _ _ H). auto. destruct H0. destruct H0. (* n : Nat p : Nat H : n <= S p x : Nat H0 : S p = S x H1 : n <= x ============================ n = S p \/ n <= p *) assert (H2 : p = x). apply S_injective; assumption. rewrite H2;auto. Qed. Lemma Le_S_SR : forall n p, S n <= S p -> n <= p. Proof. (* rien de nouveau ... *) intros n p H; destruct (Le_n_S_p _ _ H). assert (H1 : n=p). apply S_injective;assumption. rewrite H1;auto. (* 1 subgoal n : Nat p : Nat H : S n <= S p H0 : S n <= p ============================ n <= p *) apply Le_trans with (S n);auto. Qed. Lemma not_le_Sn_n : forall n:Nat,~ S n <= n. Proof. intro n. induction n using Nat_ind. intro. destruct (Le_inv _ _ H). destruct (zero_not_S zero);auto. destruct H0. destruct H0. destruct (zero_not_S x);auto. intro H;destruct IHn. apply Le_S_SR. assumption. Qed. Lemma Lt_irreflexive : forall n, ~ n < n. Proof. unfold Lt. apply not_le_Sn_n. Qed. Lemma not_lt_S_n_n : forall n, ~ (S n < n). Proof. intros n H. destruct (not_le_Sn_n n). auto. Qed. Lemma Le_antisym : forall n p, n <= p -> p <= n -> n = p. Proof. (* Apparemment, c'est cette preuve qui a le plus fait souffrir ... *) intro n; induction n using Nat_ind. intros p Hp Hp'. symmetry;apply Le_n_zero. assumption. intros p H0 H1. destruct (Le_cases _ _ H0);destruct (Le_cases _ _ H1);auto. destruct (not_lt_S_n_n (S n)). unfold Lt. apply Le_S_S. apply Le_trans with p;auto. apply Le_S_SR. trivial. Qed. (* Proprietes de l'addition *) Lemma n_plus_zero : forall n:Nat, n + zero =n. Proof. intro n; induction n using Nat_ind. auto. rewrite S_plus_n. rewrite IHn;trivial. Qed. (* La commande suivante permet d'utiliser les égalités ci-dessous avec la commande 'autorewrite with peano' Attention aux bouclages éventuels !!!!!!! *) Hint Rewrite n_plus_zero zero_plus_n S_plus_n: peano. Lemma n_plus_S : forall n p:Nat, n+ S p = S(n+p). Proof. intro n; induction n using Nat_ind. intro p. autorewrite with peano;trivial. intros p . autorewrite with peano. rewrite IHn. trivial. Qed. Hint Rewrite n_plus_S :peano. Hint Resolve n_plus_S n_plus_zero. Theorem plus_comm : forall n p:Nat, n + p = p + n. Proof. intro n; induction n using Nat_ind. intro; autorewrite with peano;trivial. intros p . transitivity (S (n + p));auto. rewrite IHn. auto. Qed. Hint Rewrite zero_mult_n S_mult_n : peano. Theorem plus_assoc : forall n p q:Nat, (n+p)+q = n+(p+q). Proof. intro n. induction n using Nat_ind. intros;autorewrite with peano. trivial. intros p q. autorewrite with peano. rewrite IHn;auto. Qed. Hint Rewrite plus_assoc :peano. Lemma plus_zero : forall n p:Nat, n+p=zero -> n=zero /\ p=zero. Proof. intro n; induction n using Nat_ind. auto. intros. autorewrite with peano in H. split;auto. intros p H. autorewrite with peano in H. destruct (zero_not_S (n + p)). auto. Qed. Theorem mult_n_zero : forall n:Nat, n* zero = zero. (* A faire *) Proof. intro n; induction n using Nat_ind. autorewrite with peano. trivial. autorewrite with peano. trivial. Qed. Hint Rewrite mult_n_zero : peano. Theorem mult_n_Sp : forall n p:Nat, n * (S p) = n + (n * p). Proof. intro n; induction n using Nat_ind. intros;autorewrite with peano. trivial. intros p;autorewrite with peano. rewrite IHn. (* ici, autorewrite ne permet pas d'automatiser la fin de la preuve *) rewrite <- plus_assoc. rewrite <- plus_assoc. (* On veut utiliser la commutativite de l'addition pour remplacer p0 + p par p + p0 Pour specifier à rewrite ces arguments, on les donne comme arguments de plus_comm *) rewrite (plus_comm p n). trivial. Qed. Hint Rewrite mult_n_Sp:peano. Lemma mult_comm: forall n p:Nat, n*p = p*n. Proof. (* Comme pour l'addition, on procede par recurrence sur n *) intro n; induction n using Nat_ind;intros;autorewrite with peano. trivial. (* 1 subgoal n : Nat IHn : forall p : Nat, n * p = p * n p : Nat ============================ p + n * p = p + p * n *) rewrite (IHn p). trivial. Qed. Lemma one_mult_n : forall n, (S zero)*n = n. Proof. (* meme pas besoin de recurrence *) intro n; autorewrite with peano. trivial. Qed. (* A faire *) Lemma n_mult_one : forall n, n*(S zero) = n. Proof. intro n; autorewrite with peano. trivial. Qed. Lemma mult_zero : forall n p:Nat, n*p=zero -> n=zero \/ p=zero. Proof. (* strategie, une recurrence sur n, qui aura un cas de base facile *) intro n; induction n using Nat_ind;auto. (* passons aux choses serieuses : n : Nat IHn : forall p : Nat, n * p = zero -> n = zero \/ p = zero ============================ forall p : Nat, S n * p = zero -> S n = zero \/ p = zero *) intros p H. (* 1 subgoal n : Nat IHn : forall p : Nat, n * p = zero -> n = zero \/ p = zero p : Nat H : S n * p = zero ============================ S n = zero \/ p = zero Dans H, il suffit de faire apparaitre une addition. *) autorewrite with peano in H. (* 1 subgoal n : Nat IHn : forall p : Nat, n * p = zero -> n = zero \/ p = zero p : Nat H : p + n * p = zero ============================ S n = zero \/ p = zero *) generalize (plus_zero p (n * p) H). (* 1 subgoal n : Nat IHn : forall p : Nat, n * p = zero -> n = zero \/ p = zero p : Nat H : p + n * p = zero ============================ p = zero /\ n * p = zero -> S n = zero \/ p = zero *) tauto. Qed. Lemma Le_plus : forall n p:Nat, n <= p -> exists q:Nat, p = n+q. Proof. (* La encore, induction a partir de n *) intros n p H. induction H using Le_ind. (* cas de base: n : Nat ============================ exists q : Nat, n = n + q *) exists zero; autorewrite with peano; trivial. (* pas de recurrence : 1 subgoal n : Nat p : Nat H : n <= p IHLe : exists q : Nat, p = n + q ============================ exists q : Nat, S p = n + q *) destruct IHLe. exists (S x). (* 1 subgoal n : Nat p : Nat H : n <= p x : Nat H0 : p = n + x ============================ S p = n + S x *) autorewrite with peano. rewrite H0;auto. Qed . Theorem plus_le : forall n p, n <= n + p. Proof. (* choix strategique; une recurrence sur p *) intros n p; induction p using Nat_ind. autorewrite with peano;auto. (* 1 subgoal n : Nat p : Nat IHp : n <= n + p ============================ n <= n + S p *) apply Le_trans with (n + p). auto. autorewrite with peano. auto. Qed. Definition decidable (P:Nat -> Prop) := forall n, P n \/ ~ P n. Theorem zero_dec : decidable (fun n:Nat => n=zero). Proof. intro n. destruct (zero_or_S n). auto. destruct H. right;rewrite H. intro H0. destruct (zero_not_S x);auto. Qed. Theorem le_dec : forall n:Nat, decidable (fun p:Nat => n <= p). Proof. intros n ;induction n using Nat_ind. intro p. auto. intro q. destruct (IHn q). destruct (Le_cases _ _ H). left;auto. rewrite H0. right;apply not_le_Sn_n. right. intro H0;destruct H. auto. Qed. Theorem decidable_negation : forall P:Nat->Prop, decidable P -> decidable (fun n : Nat => ~ (P n)). Proof. intros P H n. destruct (H n);tauto. Qed. Theorem decidable_or : forall P Q:Nat->Prop, decidable P -> decidable Q -> decidable (fun n : Nat => P n \/ Q n). Proof. intros P Q H H0 n. destruct (H n); auto. destruct (H0 n);auto. right;tauto. Qed. Theorem bounded_ex_dec : forall P:Nat->Prop, decidable P -> decidable (fun n:Nat => exists p:Nat, p <= n /\ P p). Proof. intros P H n. induction n using Nat_ind. (* 2 subgoals P : Nat -> Prop H : decidable P ============================ (exists p : Nat, p <= zero /\ P p) \/ ~ (exists p : Nat, p <= zero /\ P p) par H, on sait que deux cas se présentent : P zero ou ~ (P zero): *) destruct (H zero). left;exists zero. auto. right;intro H2. (* P : Nat -> Prop H : decidable P H0 : ~ P zero H2 : exists p : Nat, p <= zero /\ P p ============================ False par H2, on va considerer x tel que x <= zero /\ P x. *) destruct H2. destruct H1. (* Mais x = zero, donc on a P zero et une contradiction *) assert (x=zero). apply Le_n_zero; assumption. destruct H0. rewrite <- H3;auto. (* Le pas de recurrence est plus long, mais on y arrive ... *) destruct IHn. (* P : Nat -> Prop H : decidable P n : Nat H0 : exists p : Nat, p <= n /\ P p ============================ (exists p : Nat, p <= S n /\ P p) \/ ~ (exists p : Nat, p <= S n /\ P p) Bon, si p <= n, alors p <= S n ... *) left;destruct H0. exists x;destruct H0;split;auto. (* P : Nat -> Prop H : decidable P n : Nat H0 : ~ (exists p : Nat, p <= n /\ P p) ============================ (exists p : Nat, p <= S n /\ P p) \/ ~ (exists p : Nat, p <= S n /\ P p) La, ca depend : comme il n'existe aucun p <= n tel que P p, il faut considerer les deux cas : P (S n) puis ~P(S n) : *) destruct (H (S n)). left;exists (S n);auto. (* dernier cas : on va montrer qu'il n'y a aucun p <= S n tel que P p P : Nat -> Prop H : decidable P n : Nat H0 : ~ (exists p : Nat, p <= n /\ P p) H1 : ~ P (S n) ============================ (exists p : Nat, p <= S n /\ P p) \/ ~ (exists p : Nat, p <= S n /\ P p) *) right;intro H2. destruct H2. destruct H2. (* On en est la : P : Nat -> Prop H : decidable P n : Nat H0 : ~ (exists p : Nat, p <= n /\ P p) H1 : ~ P (S n) x : Nat H2 : x <= S n H3 : P x ============================ False Mais soit x <= n, et ça contredit H0, soit x = S n, et ca contredit H1 *) destruct (Le_inv _ _ H2). destruct H1; rewrite <- H4;auto. (* Argh ... 1 subgoal P : Nat -> Prop H : decidable P n : Nat H0 : ~ (exists p : Nat, p <= n /\ P p) H1 : ~ P (S n) x : Nat H2 : x <= S n H3 : P x H4 : exists q : Nat, S n = S q /\ x <= q ============================ False de H4, on va déduire que x<= n *) assert (x <= n). destruct H4. destruct H4. rewrite (S_injective n x0 H4);assumption. (* voila, c'est fait 1 subgoal P : Nat -> Prop H : decidable P n : Nat H0 : ~ (exists p : Nat, p <= n /\ P p) H1 : ~ P (S n) x : Nat H2 : x <= S n H3 : P x H4 : exists q : Nat, S n = S q /\ x <= q H5 : x <= n ============================ False L'affirmation H0 est contradictoire avec H3 et H5 *) destruct H0;exists x;split;assumption. Qed. Theorem bounded_all_dec : forall P:Nat->Prop, decidable P -> decidable (fun n:Nat => forall p:Nat, p<= n -> P p). Proof. (* meme demarche que le precedent *) intros P H n. induction n using Nat_ind. destruct (H zero). left;intros p Hp. assert (p=zero). apply Le_n_zero. auto. rewrite H1;auto. right. intro H1. destruct H0. auto. destruct IHn. destruct (H (S n)). left. intro q. intro. destruct (Le_inv _ _ H2). rewrite H3;auto. destruct H3. destruct H3. rewrite <- (S_injective _ _ H3) in H4. auto. right. intro H2. destruct H1. auto. right. intro H2. destruct H0;auto. Qed. (* A partir de cette limite les déclarations et axiomes peuvent entrainer des incoherences *) (* Comme quoi on a raison de se mefier des axiomes ... *) (* Ensembles d'entiers *) Definition Nats := Nat -> Prop. Definition In (n:Nat)(X: Nats) := X n. Definition Empty: Nats := fun n:Nat => False. Parameter Inf : Nats -> Nat. Axiom Inf_1: forall (X : Nats) (n:Nat), In n X -> Inf X <= n. Axiom Inf_2 : forall (X : Nats)(p:Nat), (forall n:Nat, In n X -> p <= n) -> p <= Inf X. Lemma Vers_le_paradoxe : forall p:Nat, p <= Inf Empty. Proof. intros; apply Inf_2. intros n H. (* 1 subgoal p : Nat n : Nat H : In n Empty ============================ p <= n *) destruct H. Qed. Lemma paradox : False. Proof. destruct (not_le_Sn_n (Inf Empty)). (*1 subgoal ============================ S (Inf Empty) <= Inf Empty *) apply Vers_le_paradoxe. Qed.