diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 17:59:15 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 17:59:15 +0000 |
commit | f093a07ab0289c632b3f5600e8ad03bad23c13c5 (patch) | |
tree | 57bbbb8ca58ddcbc647a99832aa5ba93936e8bec | |
parent | ecb17841e955ca888010d72876381a86cdcf09ad (diff) |
suppression d'axiomes dans Rstar, Newman et Integers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2187 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | theories/Relations/Newman.v | 14 | ||||
-rwxr-xr-x | theories/Relations/Rstar.v | 10 | ||||
-rwxr-xr-x | theories/Sets/Integers.v | 145 |
3 files changed, 62 insertions, 107 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index e7829b00e..2fe408543 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -10,6 +10,16 @@ Require Rstar. +Section Newman. + +Variable A: Type. +Variable R: A->A->Prop. + +Local Rstar := (Rstar A R). +Local Rstar_reflexive := (Rstar_reflexive A R). +Local Rstar_transitive := (Rstar_transitive A R). +Local Rstar_Rstar' := (Rstar_Rstar' A R). + Definition coherence := [x:A][y:A] (exT2 ? (Rstar x) (Rstar y)). Theorem coherence_intro : (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y). @@ -99,3 +109,7 @@ Theorem Newman : (x:A)(confluence x). Proof [x:A](Hyp1 x confluence Ind_proof). End Newman_section. + + +End Newman. + diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index a0aaed9ad..ff2e02a4b 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -10,8 +10,10 @@ (* Properties of a binary relation R on type A *) -Parameter A : Type. -Parameter R : A->A->Prop. +Section Rstar. + +Variable A : Type. +Variable R : A->A->Prop. (* Definition of the reflexive-transitive closure R* of R *) (* Smallest reflexive P containing R o P *) @@ -71,3 +73,7 @@ Theorem Rstar_Rstar': (x:A)(y:A)(Rstar x y)->(Rstar' x y). Definition commut := [A:Set][R1,R2:A->A->Prop] (x,y:A)(R1 y x)->(z:A)(R2 z y) ->(EX y':A |(R2 y' x) & (R1 z y')). + + +End Rstar. + diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 85d3b1c12..dbfc6b463 100755 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -46,128 +46,67 @@ Require Export Cpo. Section Integers_sect. -Inductive Nat : Type := - mkNat: nat -> Nat. - -Parameter nat_of_Nat: Nat -> nat. - -Axiom nat_of_nat_returns: (n: nat) (nat_of_Nat (mkNat n)) = n. - -Lemma mkNat_injective: (n1, n2: nat) (mkNat n1) == (mkNat n2) -> n1 = n2. -Proof. -Intros n1 n2 H'; Try Assumption. -Rewrite <- (nat_of_nat_returns n1). -Rewrite <- (nat_of_nat_returns n2). -Rewrite H'; Auto with sets arith. -Qed. - -Inductive Integers : (Ensemble Nat) := - Integers_defn: (x: Nat) (In Nat Integers x). +Inductive Integers : (Ensemble nat) := + Integers_defn: (x: nat) (In nat Integers x). Hints Resolve Integers_defn. -Inductive Le_Nat [x, y:Nat]: Prop := - Definition_of_Le_nat: - (n1, n2: nat) x == (mkNat n1) -> y == (mkNat n2) -> (le n1 n2) -> - (Le_Nat x y). - -Lemma Le_Nat_direct: (n1, n2: nat) (le n1 n2) -> (Le_Nat (mkNat n1) (mkNat n2)). +Lemma le_reflexive: (Reflexive nat le). Proof. -Intros n1 n2 H'. -Apply Definition_of_Le_nat with n1 := n1 n2 := n2; Auto with sets arith. +Red; Auto with arith. Qed. -Hints Resolve Le_Nat_direct. -Lemma Le_Nat_Reflexive: (Reflexive Nat Le_Nat). +Lemma le_antisym: (Antisymmetric nat le). Proof. -Red. -Intro x; Elim x; Auto with sets arith. +Red; Intros x y H H';Rewrite (le_antisym x y);Auto. Qed. -Hints Resolve Le_Nat_Reflexive. -Lemma Le_Nat_antisym: (Antisymmetric Nat Le_Nat). +Lemma le_trans: (Transitive nat le). Proof. -Red. -Intros x y H'; Elim H'. -Intros n1 n2 H'0 H'1 H'2 H'3; Elim H'3. -Intros n3 n4 H'4 H'5 H'6. -Cut n1 = n4 /\ n2 = n3. -Intro H'7. -Generalize H'6. -Elim H'7; Intros H'8 H'9; Rewrite <- H'8; Clear H'7. -Rewrite <- H'9. -Intro H'7. -Cut n1 = n2. -Rewrite H'0; Rewrite H'1. -Intro H'10; Rewrite <- H'10; Auto with sets arith. -Apply le_antisym; Auto with sets arith. -Split; Apply mkNat_injective. -Rewrite <- H'5; Rewrite H'0; Auto with sets arith. -Rewrite <- H'4; Rewrite H'1; Auto with sets arith. +Red; Intros; Apply le_trans with y;Auto. Qed. +Hints Resolve le_reflexive le_antisym le_trans. -Hints Resolve Le_Nat_antisym. - -Lemma Le_Nat_trans: (Transitive Nat Le_Nat). -Proof. -Red. -Intros x y z H'; Elim H'. -Intros n1 n2 H'0 H'1 H'2 H'3; Elim H'3. -Intros n3 n4 H'4 H'5 H'6. -Rewrite H'0; Rewrite H'5. -Apply Le_Nat_direct. -Apply le_trans with m := n3; Auto with sets arith. -Cut n2 = n3. -Intro H'7; Rewrite <- H'7; Auto with sets arith. -Apply mkNat_injective. -Rewrite <- H'4; Rewrite <- H'1; Auto with sets arith. -Qed. -Hints Resolve Le_Nat_trans. - -Lemma Le_Nat_Order: (Order Nat Le_Nat). +Lemma le_Order: (Order nat le). Proof. Auto with sets arith. Qed. -Hints Resolve Le_Nat_Order. +Hints Resolve le_Order. -Definition Nat_O := (mkNat O). - -Lemma triv_Nat: (n: nat) (In Nat Integers (mkNat n)). +Lemma triv_nat: (n: nat) (In nat Integers n). Proof. Auto with sets arith. Qed. -Hints Resolve triv_Nat. +Hints Resolve triv_nat. -Definition Nat_po: (PO Nat). -Apply Definition_of_PO with Carrier_of := Integers Rel_of := Le_Nat; Auto with sets arith. -Apply Inhabited_intro with x := Nat_O; Auto with sets arith. +Definition nat_po: (PO nat). +Apply Definition_of_PO with Carrier_of := Integers Rel_of := le; Auto with sets arith. +Apply Inhabited_intro with x := O; Auto with sets arith. Defined. -Hints Unfold Nat_po. +Hints Unfold nat_po. -Lemma Le_Nat_total_order: (Totally_ordered Nat Nat_po Integers). +Lemma le_total_order: (Totally_ordered nat nat_po Integers). Proof. Apply Totally_ordered_definition. Simpl. -Intros H' x; Elim x. -Intros n y; Elim y. -Intros n0 H'0. -Specialize 2 le_or_lt with n := n m := n0; Intro H'2; Elim H'2. +Intros H' x y H'0. +Specialize 2 le_or_lt with n := x m := y; Intro H'2; Elim H'2. Intro H'1; Left; Auto with sets arith. Intro H'1; Right. -Cut (le n0 n); Auto with sets arith. +Cut (le y x); Auto with sets arith. Qed. -Hints Resolve Le_Nat_total_order. +Hints Resolve le_total_order. Lemma Finite_subset_has_lub: - (X: (Ensemble Nat)) (Finite Nat X) -> - (EXT m: Nat | (Upper_Bound Nat Nat_po X m)). + (X: (Ensemble nat)) (Finite nat X) -> + (EXT m: nat | (Upper_Bound nat nat_po X m)). Proof. Intros X H'; Elim H'. -Exists Nat_O. +Exists O. Apply Upper_Bound_definition; Auto with sets arith. Intros y H'0; Elim H'0; Auto with sets arith. Intros A H'0 H'1 x H'2; Try Assumption. Elim H'1; Intros x0 H'3; Clear H'1. -Elim Le_Nat_total_order. +Elim le_total_order. Simpl. Intro H'1; Try Assumption. LApply H'1; [Intro H'4; Idtac | Try Assumption]; Auto with sets arith. @@ -181,7 +120,7 @@ Intro H'1; LApply H'1; Exists x. Apply Upper_Bound_definition; Auto with sets arith; Simpl. Intros y H'1; Elim H'1. -Generalize Le_Nat_trans. +Generalize le_trans. Intro H'4; Red in H'4. Intros x1 H'6; Try Assumption. Apply H'4 with y := x0; Auto with sets arith. @@ -197,30 +136,21 @@ Red. Intros x1 H'1; Elim H'1; Auto with sets arith. Qed. -Lemma Integers_has_no_ub: ~ (EXT m:Nat | (Upper_Bound Nat Nat_po Integers m)). +Lemma Integers_has_no_ub: ~ (EXT m:nat | (Upper_Bound nat nat_po Integers m)). Proof. Red; Intro H'; Elim H'. -Intro x; Elim x. -Intros n H'0; Elim H'0. -Intros H'1 H'2; Try Assumption. -Cut (In Nat Integers (mkNat (S n))). -Intro H'3; Try Assumption. -Specialize 1 H'2 with y := (mkNat (S n)); Intro H'4; LApply H'4; +Intros x H'0. +Elim H'0; Intros H'1 H'2. +Cut (In nat Integers (S x)). +Intro H'3. +Specialize 1 H'2 with y := (S x); Intro H'4; LApply H'4; [Intro H'5; Clear H'4 | Try Assumption; Clear H'4]. Simpl in H'5. -Elim H'5. -Intros n1 n2 H'4 H'6; Try Assumption. -Specialize 2 mkNat_injective with n1 := (S n) n2 := n1; Intro H'8; LApply H'8; - [Intro H'9; Rewrite <- H'9; Clear H'8 | Clear H'8]; Auto with sets arith. -Specialize 2 mkNat_injective with n1 := n n2 := n2; Intro H'8; LApply H'8; - [Intro H'10; Rewrite <- H'10; Clear H'8 | Clear H'8]; Auto with sets arith. -Intro H'7; Try Assumption. -Specialize 1 le_Sn_n with n := n; Intro H'8; Elim H'8. -Auto with sets arith. +Absurd (le (S x) x); Auto with arith. Auto with sets arith. Qed. -Lemma Integers_infinite: ~ (Finite Nat Integers). +Lemma Integers_infinite: ~ (Finite nat Integers). Proof. Generalize Integers_has_no_ub. Intro H'; Red; Intro H'0; Try Exact H'0. @@ -229,3 +159,8 @@ Apply Finite_subset_has_lub; Auto with sets arith. Qed. End Integers_sect. + + + + + |