Require ZArith.
Require Export Wf_nat.
Require Omega.
| Well-founded relations on Z. |
We define the following family of relations on Z x Z:
|
Definition Zwf := [c:Z][x,y:Z] `c <= y` /\ `x < y`.
and we prove that (Zwf c) is well founded
|
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|
|
Local f := [z:Z](absolu (Zminus z c)).
Lemma Zwf_well_founded : (well_founded Z (Zwf c)).
Red; Intros.
Assert (n:nat)(a:Z)(lt (f a) n)\/(`a<c`) -> (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.
Hints Resolve Zwf_well_founded : datatypes v62.
|
We also define the other family of relations:
|
Definition Zwf_up := [c:Z][x,y:Z] `y < x <= c`.
and we prove that (Zwf_up c) is well founded
|
Section wf_proof_up.
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|
|
Local f := [z:Z](absolu (Zminus c z)).
Lemma Zwf_up_well_founded : (well_founded Z (Zwf_up c)).
Proof.
Apply well_founded_lt_compat with f:=f.
Unfold Zwf_up f.
Intros.
Apply absolu_lt.
Unfold Zminus. Split.
Apply Zle_left; Intuition.
Apply Zlt_reg_l; Unfold Zlt; Rewrite <- Zcompare_Zopp; Intuition.
Save.
End wf_proof_up.
Hints Resolve Zwf_up_well_founded : datatypes v62.
Require Export Compare_dec.
Require Export Peano_dec.
Require Sumbool.
Any decidability function in type sumbool can be turned into a function returning a boolean with the corresponding specification:
|
Definition bool_of_sumbool :
(A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
Proof.
Intros A B H.
Elim H; [ Intro; Exists true; Assumption
| Intro; Exists false; Assumption ].
Save.
Implicits bool_of_sumbool.
The decidability of equality and order relations over type nat give some boolean functions with the adequate specification.
|
Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)).
Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} :=
[n,m:nat] (sumbool_not ? ? (le_lt_dec m n)).
Definition nat_lt_ge_bool :=
[x,y:nat](bool_of_sumbool (lt_ge_dec x y)).
Definition nat_ge_lt_bool :=
[x,y:nat](bool_of_sumbool (sumbool_not ? ? (lt_ge_dec x y))).
Definition nat_le_gt_bool :=
[x,y:nat](bool_of_sumbool (le_gt_dec x y)).
Definition nat_gt_le_bool :=
[x,y:nat](bool_of_sumbool (sumbool_not ? ? (le_gt_dec x y))).
Definition nat_eq_bool :=
[x,y:nat](bool_of_sumbool (eq_nat_dec x y)).
Definition nat_noteq_bool :=
[x,y:nat](bool_of_sumbool (sumbool_not ? ? (eq_nat_dec x y))).
Definition zerop_bool := [x:nat](bool_of_sumbool (zerop x)).
Definition notzerop_bool := [x:nat](bool_of_sumbool (notzerop x)).