summaryrefslogtreecommitdiff
path: root/theories/Arith/Wf_nat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Wf_nat.v')
-rw-r--r--theories/Arith/Wf_nat.v185
1 files changed, 94 insertions, 91 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index e1bbfad9..11fcd161 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Wf_nat.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Wf_nat.v 9341 2006-11-06 13:08:10Z notin $ i*)
(** Well-founded relations and natural numbers *)
@@ -18,7 +18,7 @@ Implicit Types m n p : nat.
Section Well_founded_Nat.
-Variable A : Set.
+Variable A : Type.
Variable f : A -> nat.
Definition ltof (a b:A) := f a < f b.
@@ -26,21 +26,21 @@ Definition gtof (a b:A) := f b > f a.
Theorem well_founded_ltof : well_founded ltof.
Proof.
-red in |- *.
-cut (forall n (a:A), f a < n -> Acc ltof a).
-intros H a; apply (H (S (f a))); auto with arith.
-induction n.
-intros; absurd (f a < 0); auto with arith.
-intros a ltSma.
-apply Acc_intro.
-unfold ltof in |- *; intros b ltfafb.
-apply IHn.
-apply lt_le_trans with (f a); auto with arith.
+ red in |- *.
+ cut (forall n (a:A), f a < n -> Acc ltof a).
+ intros H a; apply (H (S (f a))); auto with arith.
+ induction n.
+ intros; absurd (f a < 0); auto with arith.
+ intros a ltSma.
+ apply Acc_intro.
+ unfold ltof in |- *; intros b ltfafb.
+ apply IHn.
+ apply lt_le_trans with (f a); auto with arith.
Defined.
Theorem well_founded_gtof : well_founded gtof.
Proof.
-exact well_founded_ltof.
+ exact well_founded_ltof.
Defined.
(** It is possible to directly prove the induction principle going
@@ -48,52 +48,55 @@ Defined.
or to use the previous lemmas to extract a program with a fixpoint
([induction_ltof2])
-the ML-like program for [induction_ltof1] is : [[
+the ML-like program for [induction_ltof1] is :
+[[
let induction_ltof1 F a = indrec ((f a)+1) a
where rec indrec =
function 0 -> (function a -> error)
|(S m) -> (function a -> (F a (function y -> indrec y m)));;
]]
-the ML-like program for [induction_ltof2] is : [[
+the ML-like program for [induction_ltof2] is :
+[[
let induction_ltof2 F a = indrec a
where rec indrec a = F a indrec;;
-]] *)
+]]
+*)
Theorem induction_ltof1 :
- forall P:A -> Set,
- (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
-Proof.
-intros P F; cut (forall n (a:A), f a < n -> P a).
-intros H a; apply (H (S (f a))); auto with arith.
-induction n.
-intros; absurd (f a < 0); auto with arith.
-intros a ltSma.
-apply F.
-unfold ltof in |- *; intros b ltfafb.
-apply IHn.
-apply lt_le_trans with (f a); auto with arith.
+ forall P:A -> Set,
+ (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
+Proof.
+ intros P F; cut (forall n (a:A), f a < n -> P a).
+ intros H a; apply (H (S (f a))); auto with arith.
+ induction n.
+ intros; absurd (f a < 0); auto with arith.
+ intros a ltSma.
+ apply F.
+ unfold ltof in |- *; intros b ltfafb.
+ apply IHn.
+ apply lt_le_trans with (f a); auto with arith.
Defined.
Theorem induction_gtof1 :
- forall P:A -> Set,
- (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
+ forall P:A -> Set,
+ (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
-exact induction_ltof1.
+ exact induction_ltof1.
Defined.
Theorem induction_ltof2 :
- forall P:A -> Set,
- (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
+ forall P:A -> Set,
+ (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
-exact (well_founded_induction well_founded_ltof).
+ exact (well_founded_induction well_founded_ltof).
Defined.
Theorem induction_gtof2 :
- forall P:A -> Set,
- (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
+ forall P:A -> Set,
+ (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Proof.
-exact induction_ltof2.
+ exact induction_ltof2.
Defined.
(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
@@ -105,105 +108,105 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
Theorem well_founded_lt_compat : well_founded R.
Proof.
-red in |- *.
-cut (forall n (a:A), f a < n -> Acc R a).
-intros H a; apply (H (S (f a))); auto with arith.
-induction n.
-intros; absurd (f a < 0); auto with arith.
-intros a ltSma.
-apply Acc_intro.
-intros b ltfafb.
-apply IHn.
-apply lt_le_trans with (f a); auto with arith.
+ red in |- *.
+ cut (forall n (a:A), f a < n -> Acc R a).
+ intros H a; apply (H (S (f a))); auto with arith.
+ induction n.
+ intros; absurd (f a < 0); auto with arith.
+ intros a ltSma.
+ apply Acc_intro.
+ intros b ltfafb.
+ apply IHn.
+ apply lt_le_trans with (f a); auto with arith.
Defined.
End Well_founded_Nat.
Lemma lt_wf : well_founded lt.
Proof.
-exact (well_founded_ltof nat (fun m => m)).
+ exact (well_founded_ltof nat (fun m => m)).
Defined.
Lemma lt_wf_rec1 :
- forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+ forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
-exact (fun p P F => induction_ltof1 nat (fun m => m) P F p).
+ exact (fun p P F => induction_ltof1 nat (fun m => m) P F p).
Defined.
Lemma lt_wf_rec :
- forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+ forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
-exact (fun p P F => induction_ltof2 nat (fun m => m) P F p).
+ exact (fun p P F => induction_ltof2 nat (fun m => m) P F p).
Defined.
Lemma lt_wf_ind :
- forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+ forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.
-intro p; intros; elim (lt_wf p); auto with arith.
+ intro p; intros; elim (lt_wf p); auto with arith.
Qed.
Lemma gt_wf_rec :
- forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
+ forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Proof.
-exact lt_wf_rec.
+ exact lt_wf_rec.
Defined.
Lemma gt_wf_ind :
- forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
+ forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Proof lt_wf_ind.
Lemma lt_wf_double_rec :
forall P:nat -> nat -> Set,
(forall n m,
- (forall p q, p < n -> P p q) ->
- (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
+ (forall p q, p < n -> P p q) ->
+ (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
-intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
-intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
+ intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
+ intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
Defined.
Lemma lt_wf_double_ind :
- forall P:nat -> nat -> Prop,
- (forall n m,
+ forall P:nat -> nat -> Prop,
+ (forall n m,
(forall p (q:nat), p < n -> P p q) ->
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
-intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
-intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
+ intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
+ intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
Qed.
Hint Resolve lt_wf: arith.
Hint Resolve well_founded_lt_compat: arith.
Section LT_WF_REL.
-Variable A : Set.
-Variable R : A -> A -> Prop.
-
-(* Relational form of inversion *)
-Variable F : A -> nat -> Prop.
-Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m).
-
-Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
-Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
-Proof.
-intros x [n fxn]; generalize dependent x.
-pattern n in |- *; apply lt_wf_ind; intros.
-constructor; intros.
-destruct (F_compat y x) as (x0,H1,H2); trivial.
-apply (H x0); auto.
-Qed.
-
-Theorem well_founded_inv_lt_rel_compat : well_founded R.
-Proof.
-constructor; intros.
-case (F_compat y a); trivial; intros.
-apply acc_lt_rel; trivial.
-exists x; trivial.
-Qed.
+ Variable A : Set.
+ Variable R : A -> A -> Prop.
+
+ (* Relational form of inversion *)
+ Variable F : A -> nat -> Prop.
+ Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m).
+
+ Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
+ Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
+ Proof.
+ intros x [n fxn]; generalize dependent x.
+ pattern n in |- *; apply lt_wf_ind; intros.
+ constructor; intros.
+ destruct (F_compat y x) as (x0,H1,H2); trivial.
+ apply (H x0); auto.
+ Qed.
+
+ Theorem well_founded_inv_lt_rel_compat : well_founded R.
+ Proof.
+ constructor; intros.
+ case (F_compat y a); trivial; intros.
+ apply acc_lt_rel; trivial.
+ exists x; trivial.
+ Qed.
End LT_WF_REL.
Lemma well_founded_inv_rel_inv_lt_rel :
- forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
-intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
+ forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
+ intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 05:15:49 +0000