(* Une théorie *) Parameter D : Set. (* D est un type de donnee *) Axiom D_not_empty : exists d:D, True. (* Il existe un élément d de D tel que vrai *) Parameter lt : D -> D -> Prop. (* "lt" pour "Lower Than" : "strictement plus petit que" *) Parameter max : D -> D -> D. (* La commande suivante permet d'employer la notation " t1 < t2 " au lieu de " (lt t1 t2) " *) Notation "x < y" := (lt x y). Axiom lt_irreflexive : forall d:D, ~( d < d). Axiom lt_transitive : forall d d' d'':D, d < d' -> d' < d'' -> d < d''. Axiom lt_cases : forall d d', d < d' \/ d = d' \/ d' < d. Axiom D_not_bounded : forall x:D, exists y:D, x < y. Definition le x y := lt x y \/ x = y. (* "le" pour "Lower or Equal" : "plus petit ou égal" *) Notation "x <= y" := (le x y). Axiom max_1 : forall x y:D, x <= max x y. Axiom max_2 : forall x y:D, y <= max x y. Axiom max_3 : forall x y m, x <= m -> y <= m -> max x y <= m. Theorem lt_not_gt : forall x y:D, x < y -> ~ y < x. Proof. intros x y. (* NOUVEAU : cas forall *) intros H. (* cas -> *) intro H0. (* cas ~ *) absurd (x < x). (* NOUVEAU *) apply lt_irreflexive. apply lt_transitive with (d':= y). (* NOUVEAU *) trivial. trivial. Qed. Theorem le_reflexive : forall d, d <= d. Proof. intro d. unfold le. (* NOUVEAU *) right. reflexivity. (* trivial. *) Qed. Theorem le_transitive : forall x y z:D, x <= y -> y <= z -> x <= z. Proof. intros x y z H H0. elim H;elim H0;intros. left. apply lt_transitive with y;auto. Admitted. Theorem le_antisym : forall x y, x <= y -> y <= x -> x =y. Proof. intros x y H H0. elim H;elim H0;intros;trivial. elim (lt_irreflexive x). apply lt_transitive with y;auto. symmetry;trivial. Qed. Theorem le_lt_trans : forall x y z, x <= y -> y < z -> x < z. Proof. Admitted. Theorem lt_le_trans : forall x y z, x < y -> y <= z -> x < z. Proof. Admitted. Theorem le_not_gt : forall x y:D, x <= y -> ~ y < x. Proof. Admitted. (* A propos de max *) Theorem max_eq : forall x :D, max x x = x. Proof. Admitted. (* Un peu d'aide pour auto : "Hint Resolve" *) Hint Resolve max_1 max_2 max_3 le_reflexive le_antisym le_transitive lt_transitive lt_irreflexive le_not_gt lt_not_gt lt_le_trans le_lt_trans. Theorem le_total : forall x y, x <= y \/ y <= x. Proof. intros x y. elim (lt_cases x y) (* NOUVEAU *). Admitted. Theorem max_comm : forall x y, max x y = max y x. Proof. Admitted. Theorem le_max : forall x y, x <= y -> max x y = y. Proof. auto. Admitted. Theorem ge_max : forall x y, y <= x -> max x y = x. Proof. auto. Qed. Hint Resolve le_max ge_max. Theorem max_or : forall x y, max x y = x \/ max x y = y. Proof. Admitted. Theorem max_le : forall x y, max x y = y -> x <= y. Proof. Admitted. (* autre possibilité *) Theorem max_le' : forall x y, max x y = y -> x <= y. Proof. intros x y H; elim (le_total x y);auto. intro H0. generalize (ge_max x y H0). Admitted. Theorem max_ge : forall x y, max x y = x -> y <= x. Proof. Admitted. Theorem max_assoc : forall x y z, max x (max y z)=max (max x y) z. Proof. intros x y z; elim (le_total x y);elim (le_total y z); intros H H0. rewrite (le_max _ _ H0). rewrite (le_max _ _ H). eauto. Admitted. Section Top_absurd. Variable top: D. Hypothesis top_top : forall d:D, d <= top. Lemma super_top : exists x:D, top < x. Proof. Admitted. Lemma no_top : False. Proof. Admitted. End Top_absurd. (* La partie ci-dessous n'est à faire que lorsque les Admitted de la section Top_absurd ont été levés *) Check no_top. Lemma pas_d_element_absorbant_pour_max : ~ exists e:D, forall x, max e x = e. Admitted.