diff options
Diffstat (limited to 'theories/ZArith/Zwf.v')
| -rw-r--r-- | theories/ZArith/Zwf.v | 92 |
1 files changed, 46 insertions, 46 deletions
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 4ff663fb..bd617204 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zwf.v 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: Zwf.v 9245 2006-10-17 12:53:34Z notin $ *) Require Import ZArith_base. Require Export Wf_nat. @@ -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. |