aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zwf.v
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
commit28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch)
tree63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/ZArith/Zwf.v
parent744e7f6a319f4d459a3cc2309f575d43041d75aa (diff)
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zwf.v')
-rw-r--r--theories/ZArith/Zwf.v90
1 files changed, 45 insertions, 45 deletions
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 2052ae9a1..650c79745 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -26,35 +26,35 @@ Definition Zwf (c x y:Z) := c <= y /\ x < y.
Section wf_proof.
-Variable c : Z.
-
-(** The proof of well-foundness is classic: we do the proof by induction
- on a measure in nat, which is here [|x-c|] *)
-
-Let f (z:Z) := Zabs_nat (z - c).
-
-Lemma Zwf_well_founded : well_founded (Zwf c).
-red in |- *; intros.
-assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
-clear a; simple induction n; intros.
-(** n= 0 *)
-case H; intros.
-case (lt_n_O (f a)); auto.
-apply Acc_intro; unfold Zwf in |- *; intros.
-assert False; omega || contradiction.
-(** inductive case *)
-case H0; clear H0; intro; auto.
-apply Acc_intro; intros.
-apply H.
-unfold Zwf in H1.
-case (Zle_or_lt c y); intro; auto with zarith.
-left.
-red in H0.
-apply lt_le_trans with (f a); auto with arith.
-unfold f in |- *.
-apply Zabs.Zabs_nat_lt; omega.
-apply (H (S (f a))); auto.
-Qed.
+ Variable c : Z.
+
+ (** The proof of well-foundness is classic: we do the proof by induction
+ on a measure in nat, which is here [|x-c|] *)
+
+ Let f (z:Z) := Zabs_nat (z - c).
+
+ Lemma Zwf_well_founded : well_founded (Zwf c).
+ red in |- *; intros.
+ assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
+ clear a; simple induction n; intros.
+ (** n= 0 *)
+ case H; intros.
+ case (lt_n_O (f a)); auto.
+ apply Acc_intro; unfold Zwf in |- *; intros.
+ assert False; omega || contradiction.
+ (** inductive case *)
+ case H0; clear H0; intro; auto.
+ apply Acc_intro; intros.
+ apply H.
+ unfold Zwf in H1.
+ case (Zle_or_lt c y); intro; auto with zarith.
+ left.
+ red in H0.
+ apply lt_le_trans with (f a); auto with arith.
+ unfold f in |- *.
+ apply Zabs.Zabs_nat_lt; omega.
+ apply (H (S (f a))); auto.
+ Qed.
End wf_proof.
@@ -72,25 +72,25 @@ Definition Zwf_up (c x y:Z) := y < x <= c.
Section wf_proof_up.
-Variable c : Z.
+ Variable c : Z.
-(** The proof of well-foundness is classic: we do the proof by induction
- on a measure in nat, which is here [|c-x|] *)
+ (** The proof of well-foundness is classic: we do the proof by induction
+ on a measure in nat, which is here [|c-x|] *)
-Let f (z:Z) := Zabs_nat (c - z).
+ Let f (z:Z) := Zabs_nat (c - z).
-Lemma Zwf_up_well_founded : well_founded (Zwf_up c).
-Proof.
-apply well_founded_lt_compat with (f := f).
-unfold Zwf_up, f in |- *.
-intros.
-apply Zabs.Zabs_nat_lt.
-unfold Zminus in |- *. split.
-apply Zle_left; intuition.
-apply Zplus_lt_compat_l; unfold Zlt in |- *; rewrite <- Zcompare_opp;
- intuition.
-Qed.
+ Lemma Zwf_up_well_founded : well_founded (Zwf_up c).
+ Proof.
+ apply well_founded_lt_compat with (f := f).
+ unfold Zwf_up, f in |- *.
+ intros.
+ apply Zabs.Zabs_nat_lt.
+ unfold Zminus in |- *. split.
+ apply Zle_left; intuition.
+ apply Zplus_lt_compat_l; unfold Zlt in |- *; rewrite <- Zcompare_opp;
+ intuition.
+ Qed.
End wf_proof_up.
-Hint Resolve Zwf_up_well_founded: datatypes v62. \ No newline at end of file
+Hint Resolve Zwf_up_well_founded: datatypes v62.