From 62712cda8380f03c6d60c5987f9ff08b866127a8 Mon Sep 17 00:00:00 2001 From: mohring Date: Wed, 25 Sep 2002 10:41:34 +0000 Subject: Affaiblissement de l'ordre sur Z on demande x < y et seulement que y (et pas x) soit plus garnd que c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3032 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zwf.v | 35 +++++++++++++++++++++++------------ 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 2994bac31..56baf1782 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -10,16 +10,16 @@ Require ZArith_base. Require Export Wf_nat. +Require Omega. (** Well-founded relations on Z. *) (** We define the following family of relations on [Z x Z]: - [x (Zwf c) y] iff [c <= x < y] + [x (Zwf c) y] iff [x < y & c <= y] *) -Definition Zwf := [c:Z][x,y:Z] `c <= x` /\ `c <= y` /\ `x < y`. - +Definition Zwf := [c:Z][x,y:Z] `c <= y` /\ `x < y`. (** and we prove that [(Zwf c)] is well founded *) @@ -33,15 +33,26 @@ Variable c : Z. Local f := [z:Z](absolu (Zminus z c)). Lemma Zwf_well_founded : (well_founded Z (Zwf c)). -Proof. -Apply well_founded_lt_compat with f:=f. -Unfold Zwf f. -Intros. -Apply absolu_lt. -Unfold Zminus. Split. -Apply Zle_left; Intuition. -Rewrite (Zplus_sym x `-c`). Rewrite (Zplus_sym y `-c`). -Apply Zlt_reg_l; Intuition. +Red; Intros. +Assert (n:nat)(a:Z)(lt (f a) n)\/(`a (Acc Z (Zwf c) a). +Clear a; Induction n; Intros. +(** n= 0 *) +Case H; Intros. +Case (lt_n_O (f a)); Auto. +Apply Acc_intro; Unfold Zwf; Intros. +Assert False;Omega Orelse 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. +Apply absolu_lt; Omega. +Apply (H (S (f a))); Auto. Save. End wf_proof. -- cgit v1.2.3