diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /theories/Arith/Wf_nat.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Arith/Wf_nat.v')
-rw-r--r-- | theories/Arith/Wf_nat.v | 76 |
1 files changed, 71 insertions, 5 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 11fcd161..6ad640eb 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 9341 2006-11-06 13:08:10Z notin $ i*) +(*i $Id: Wf_nat.v 11072 2008-06-08 16:13:37Z herbelin $ i*) (** Well-founded relations and natural numbers *) @@ -50,10 +50,12 @@ Defined. 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)));; +let induction_ltof1 f F a = + let rec indrec n k = + match n with + | O -> error + | S m -> F k (indrec m) + in indrec (f a + 1) a ]] the ML-like program for [induction_ltof2] is : @@ -210,3 +212,67 @@ 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. Qed. + +(** A constructive proof that any non empty decidable subset of + natural numbers has a least element *) + +Set Implicit Arguments. + +Require Import Le. +Require Import Compare_dec. +Require Import Decidable. + +Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) := + exists! x, P x /\ forall x', P x' -> R x x'. + +Lemma dec_inh_nat_subset_has_unique_least_element : + forall P:nat->Prop, (forall n, P n \/ ~ P n) -> + (exists n, P n) -> has_unique_least_element le P. +Proof. + intros P Pdec (n0,HPn0). + assert + (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') + \/(forall n', P n' -> n<=n')). + induction n. + right. + intros n' Hn'. + apply le_O_n. + destruct IHn. + left; destruct H as (n', (Hlt', HPn')). + exists n'; split. + apply lt_S; assumption. + assumption. + destruct (Pdec n). + left; exists n; split. + apply lt_n_Sn. + split; assumption. + right. + intros n' Hltn'. + destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. + apply H; assumption. + assumption. + destruct H0. + rewrite Heqn; assumption. + destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; + repeat split; + assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. +Qed. + +Unset Implicit Arguments. + +(** [n]th iteration of the function [f] *) + +Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A := + match n with + | O => x + | S n' => f (iter_nat n' A f x) + end. + +Theorem iter_nat_plus : + forall (n m:nat) (A:Type) (f:A -> A) (x:A), + iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). +Proof. + simple induction n; + [ simpl in |- *; auto with arith + | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. +Qed. |