(* Une théorie *) Parameter D : Set. Axiom D_not_empty : exists d:D, True. Parameter lt : D -> D -> Prop. Parameter max : D -> D -> D. 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. 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 H H0. absurd (x < x) . (* NOUVEAU *) apply lt_irreflexive. apply lt_transitive with (d':= y) (* NOUVEAU *) ; trivial. Qed. Theorem le_reflexive : forall d, d <= d. Proof. intro d. (* unfold le. *) 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. (* NOUVEAU *) rewrite <- H1;assumption. rewrite H2;assumption. right; subst x (* NOUVEAU *);auto. Qed. 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. intros x y z H; elim H;intros H0 H1. apply lt_transitive with y;trivial. rewrite H0;trivial. Qed. Theorem lt_le_trans : forall x y z, x < y -> y <= z -> x < z. Proof. intros x y z H H0; elim H0;intros H1. apply lt_transitive with y;trivial. subst y;trivial. Qed. Theorem le_not_gt : forall x y:D, x <= y -> ~ y < x. Proof. intros x y H ;elim H. intro H0. apply lt_not_gt;trivial. intro H0;subst y;apply lt_irreflexive. Qed. (* A propos de max *) Theorem max_eq : forall x :D, max x x = x. Proof. intro x. apply le_antisym. apply max_3. apply le_reflexive. apply le_reflexive. apply max_1. Qed. 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 *). intros. left;left;trivial. intro H;elim H. intro H1;subst x;left;trivial. intro H1;right;left;trivial. Qed. Theorem max_comm : forall x y, max x y = max y x. Proof. intros x y; apply le_antisym;auto. Qed. Theorem le_max : forall x y, x <= y -> max x y = y. Proof. auto. Qed. 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. intros x y;elim (le_total x y);auto. Qed. 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. assert (max x y = x). apply ge_max;auto. right. transitivity (max x y);auto. Qed. (* 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). intro; rewrite <- H;auto. Qed. Theorem max_ge : forall x y, max x y = x -> y <= x. Proof. intros x y H; elim (le_total x y);auto. intro H0. generalize (le_max x y H0). intro; rewrite <- H;auto. Qed. 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. rewrite (le_max _ _ H0). rewrite (ge_max _ _ H). eauto. rewrite (le_max _ _ H). rewrite (ge_max _ _ H0). auto. rewrite (ge_max _ _ H). rewrite (ge_max _ _ H0). eauto. Qed. Section Top_absurd. Variable top: D. Hypothesis top_top : forall d:D, d <= top. Lemma super_top : exists x:D, top < x. Proof. apply D_not_bounded. Qed. Lemma no_top : False. Proof. elim super_top. intros top' H. assert (top < top). eauto. apply lt_irreflexive with top. trivial. Qed. End Top_absurd. Check no_top. (* no_top : forall top : D, (forall d : D, d <= top) -> False *) Lemma pas_d_element_absorbant_pour_max : ~ exists e:D, forall x, max e x = e. Proof. intro H;elim H;intros e He. apply no_top with e. intro;apply max_ge. auto. Qed.