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.