Wf_nat.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Well-founded relations and natural numbers

Require Import PeanoNat Lt.

Local Open Scope nat_scope.

Implicit Types m n p : nat.

Section Well_founded_Nat.

Variable A : Type.

Variable f : A -> nat.
Definition ltof (a b:A) := f a < f b.
Definition gtof (a b:A) := f b > f a.

Theorem well_founded_ltof : well_founded ltof.A:Type
f:A -> nat
well_founded ltof
Proof.A:Type
f:A -> nat
well_founded ltof
  assert (H : forall n (a:A), f a < n -> Acc ltof a).A:Type
f:A -> nat
forall (n : nat) (a : A), f a < n -> Acc ltof a
A:Type
f:A -> nat
H:forall (n : nat) (a : A), f a < n -> Acc ltof a
well_founded ltof
  {A:Type
f:A -> nat
forall (n : nat) (a : A), f a < n -> Acc ltof a induction n.A:Type
f:A -> nat
forall a : A, f a < 0 -> Acc ltof a
A:Type
f:A -> nat
n:nat
IHn:forall a : A, f a < n -> Acc ltof a
forall a : A, f a < S n -> Acc ltof a
    -A:Type
f:A -> nat
forall a : A, f a < 0 -> Acc ltof a intros; absurd (f a < 0); auto with arith.
    -A:Type
f:A -> nat
n:nat
IHn:forall a : A, f a < n -> Acc ltof a
forall a : A, f a < S n -> Acc ltof a intros a Ha.A:Type
f:A -> nat
n:nat
IHn:forall a0 : A, f a0 < n -> Acc ltof a0
a:A
Ha:f a < S n
Acc ltof a apply Acc_intro.A:Type
f:A -> nat
n:nat
IHn:forall a0 : A, f a0 < n -> Acc ltof a0
a:A
Ha:f a < S n
forall y : A, ltof y a -> Acc ltof y unfold ltof at 1.A:Type
f:A -> nat
n:nat
IHn:forall a0 : A, f a0 < n -> Acc ltof a0
a:A
Ha:f a < S n
forall y : A, f y < f a -> Acc ltof y intros b Hb.A:Type
f:A -> nat
n:nat
IHn:forall a0 : A, f a0 < n -> Acc ltof a0
a:A
Ha:f a < S n
b:A
Hb:f b < f a
Acc ltof b
      apply IHn.A:Type
f:A -> nat
n:nat
IHn:forall a0 : A, f a0 < n -> Acc ltof a0
a:A
Ha:f a < S n
b:A
Hb:f b < f a
f b < n apply Nat.lt_le_trans with (f a); auto with arith. }A:Type
f:A -> nat
H:forall (n : nat) (a : A), f a < n -> Acc ltof a
well_founded ltof
  intros a.A:Type
f:A -> nat
H:forall (n : nat) (a0 : A), f a0 < n -> Acc ltof a0
a:A
Acc ltof a apply (H (S (f a))).A:Type
f:A -> nat
H:forall (n : nat) (a0 : A), f a0 < n -> Acc ltof a0
a:A
f a < S (f a) auto with arith.
Defined.

Theorem well_founded_gtof : well_founded gtof.A:Type
f:A -> nat
well_founded gtof
Proof.A:Type
f:A -> nat
well_founded gtof
  exact well_founded_ltof.
Defined.

It is possible to directly prove the induction principle going back to primitive recursion on natural numbers (induction_ltof1) or to use the previous lemmas to extract a program with a fixpoint (induction_ltof2)

the ML-like program for induction_ltof1 is :
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 :
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.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, ltof y x -> P y) -> P x) ->
forall a : A, P a
Proof.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, ltof y x -> P y) -> P x) ->
forall a : A, P a
  intros P F.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
forall a : A, P a
  assert (H : forall n (a:A), f a < n -> P a).A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
forall (n : nat) (a : A), f a < n -> P a
A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
H:forall (n : nat) (a : A), f a < n -> P a
forall a : A, P a
  {A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
forall (n : nat) (a : A), f a < n -> P a induction n.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
forall a : A, f a < 0 -> P a
A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a : A, f a < n -> P a
forall a : A, f a < S n -> P a
    -A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
forall a : A, f a < 0 -> P a intros; absurd (f a < 0); auto with arith.
    -A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a : A, f a < n -> P a
forall a : A, f a < S n -> P a intros a Ha.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a0 : A, f a0 < n -> P a0
a:A
Ha:f a < S n
P a apply F.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a0 : A, f a0 < n -> P a0
a:A
Ha:f a < S n
forall y : A, ltof y a -> P y unfold ltof.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a0 : A, f a0 < n -> P a0
a:A
Ha:f a < S n
forall y : A, f y < f a -> P y intros b Hb.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a0 : A, f a0 < n -> P a0
a:A
Ha:f a < S n
b:A
Hb:f b < f a
P b
      apply IHn.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
n:nat
IHn:forall a0 : A, f a0 < n -> P a0
a:A
Ha:f a < S n
b:A
Hb:f b < f a
f b < n apply Nat.lt_le_trans with (f a); auto with arith. }A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
H:forall (n : nat) (a : A), f a < n -> P a
forall a : A, P a
  intros a.A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
H:forall (n : nat) (a0 : A), f a0 < n -> P a0
a:A
P a apply (H (S (f a))).A:Type
f:A -> nat
P:A -> Set
F:forall x : A,
(forall y : A, ltof y x -> P y) -> P x
H:forall (n : nat) (a0 : A), f a0 < n -> P a0
a:A
f a < S (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.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, gtof y x -> P y) -> P x) ->
forall a : A, P a
Proof.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, gtof y x -> P y) -> P x) ->
forall a : A, P a
  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.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, ltof y x -> P y) -> P x) ->
forall a : A, P a
Proof.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, ltof y x -> P y) -> P x) ->
forall a : A, P a
  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.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, gtof y x -> P y) -> P x) ->
forall a : A, P a
Proof.A:Type
f:A -> nat
forall P : A -> Set,
(forall x : A, (forall y : A, gtof y x -> P y) -> P x) ->
forall a : A, P a
  exact induction_ltof2.
Defined.

If a relation R is compatible with lt i.e. if x R y ⇒ f(x) < f(y) then R is well-founded.

Variable R : A -> A -> Prop.

Hypothesis H_compat : forall x y:A, R x y -> f x < f y.

Theorem well_founded_lt_compat : well_founded R.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
well_founded R
Proof.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
well_founded R
  assert (H : forall n (a:A), f a < n -> Acc R a).A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
forall (n : nat) (a : A), f a < n -> Acc R a
A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
H:forall (n : nat) (a : A), f a < n -> Acc R a
well_founded R
  {A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
forall (n : nat) (a : A), f a < n -> Acc R a induction n.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
forall a : A, f a < 0 -> Acc R a
A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
n:nat
IHn:forall a : A, f a < n -> Acc R a
forall a : A, f a < S n -> Acc R a
    -A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
forall a : A, f a < 0 -> Acc R a intros; absurd (f a < 0); auto with arith.
    -A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
n:nat
IHn:forall a : A, f a < n -> Acc R a
forall a : A, f a < S n -> Acc R a intros a Ha.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
n:nat
IHn:forall a0 : A, f a0 < n -> Acc R a0
a:A
Ha:f a < S n
Acc R a apply Acc_intro.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
n:nat
IHn:forall a0 : A, f a0 < n -> Acc R a0
a:A
Ha:f a < S n
forall y : A, R y a -> Acc R y intros b Hb.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
n:nat
IHn:forall a0 : A, f a0 < n -> Acc R a0
a:A
Ha:f a < S n
b:A
Hb:R b a
Acc R b
      apply IHn.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
n:nat
IHn:forall a0 : A, f a0 < n -> Acc R a0
a:A
Ha:f a < S n
b:A
Hb:R b a
f b < n apply Nat.lt_le_trans with (f a); auto with arith. }A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
H:forall (n : nat) (a : A), f a < n -> Acc R a
well_founded R
  intros a.A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
H:forall (n : nat) (a0 : A), f a0 < n -> Acc R a0
a:A
Acc R a apply (H (S (f a))).A:Type
f:A -> nat
R:A -> A -> Prop
H_compat:forall x y : A, R x y -> f x < f y
H:forall (n : nat) (a0 : A), f a0 < n -> Acc R a0
a:A
f a < S (f a) auto with arith.
Defined.

End Well_founded_Nat.

Lemma lt_wf : well_founded lt.well_founded lt
Proof.well_founded lt
  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 : nat) (P : nat -> Set),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Set),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
  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 : nat) (P : nat -> Set),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Set),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
  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 : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall m : nat, m < n0 -> P m) -> P n0) -> P n
  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 : nat) (P : nat -> Set),
(forall n0 : nat,
 (forall m : nat, n0 > m -> P m) -> P n0) -> P n
Proof.forall (n : nat) (P : nat -> Set),
(forall n0 : nat,
 (forall m : nat, n0 > m -> P m) -> P n0) -> P n
  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 : nat) (P : nat -> Prop),
(forall n0 : nat,
 (forall m : nat, n0 > m -> P m) -> P n0) -> 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 : nat -> nat -> Set,
(forall n m : nat,
 (forall p q : nat, p < n -> P p q) ->
 (forall p : nat, p < m -> P n p) -> P n m) ->
forall n m : nat, P n m
Proof.forall P : nat -> nat -> Set,
(forall n m : nat,
 (forall p q : nat, p < n -> P p q) ->
 (forall p : nat, p < m -> P n p) -> P n m) ->
forall n m : nat, P n m
  intros P Hrec p; pattern p; apply lt_wf_rec.P:nat -> nat -> Set
Hrec:forall n m : nat,
(forall p0 q : nat, p0 < n -> P p0 q) ->
(forall p0 : nat, p0 < m -> P n p0) -> P n m
p:nat
forall n : nat,
(forall m : nat, m < n -> forall m0 : nat, P m m0) ->
forall m : nat, P n m
  intros n H q; pattern q; apply lt_wf_rec; auto with arith.
Defined.

Lemma lt_wf_double_ind :
  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.forall P : nat -> nat -> Prop,
(forall n m : nat,
 (forall p q : nat, p < n -> P p q) ->
 (forall p : nat, p < m -> P n p) -> P n m) ->
forall n m : nat, P n m
Proof.forall P : nat -> nat -> Prop,
(forall n m : nat,
 (forall p q : nat, p < n -> P p q) ->
 (forall p : nat, p < m -> P n p) -> P n m) ->
forall n m : nat, P n m
  intros P Hrec p; pattern p; apply lt_wf_ind.P:nat -> nat -> Prop
Hrec:forall n m : nat,
(forall p0 q : nat, p0 < n -> P p0 q) ->
(forall p0 : nat, p0 < m -> P n p0) -> P n m
p:nat
forall n : nat,
(forall m : nat, m < n -> forall m0 : nat, P m m0) ->
forall m : nat, P n m
  intros n H q; pattern q; 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.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x y : A, R x y -> inv_lt_rel x y
forall x : A, (exists n : nat, F x n) -> Acc R x
  Proof.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x y : A, R x y -> inv_lt_rel x y
forall x : A, (exists n : nat, F x n) -> Acc R x
    intros x [n fxn]; generalize dependent x.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x y : A, R x y -> inv_lt_rel x y
n:nat
forall x : A, F x n -> Acc R x
    pattern n; apply lt_wf_ind; intros.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x0 y : A, R x0 y -> inv_lt_rel x0 y
n, n0:nat
H:forall m : nat,
m < n0 -> forall x0 : A, F x0 m -> Acc R x0
x:A
fxn:F x n0
Acc R x
    constructor; intros.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x0 y0 : A,
R x0 y0 -> inv_lt_rel x0 y0
n, n0:nat
H:forall m : nat,
m < n0 -> forall x0 : A, F x0 m -> Acc R x0
x:A
fxn:F x n0
y:A
H0:R y x
Acc R y
    destruct (F_compat y x) as (x0,H1,H2); trivial.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x1 y0 : A,
R x1 y0 -> inv_lt_rel x1 y0
n, n0:nat
H:forall m : nat,
m < n0 -> forall x1 : A, F x1 m -> Acc R x1
x:A
fxn:F x n0
y:A
H0:R y x
x0:nat
H1:F y x0
H2:forall m : nat, F x m -> x0 < m
Acc R y
    apply (H x0); auto.
  Qed.

  Theorem well_founded_inv_lt_rel_compat : well_founded R.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x y : A, R x y -> inv_lt_rel x y
well_founded R
  Proof.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x y : A, R x y -> inv_lt_rel x y
well_founded R
    constructor; intros.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x y0 : A, R x y0 -> inv_lt_rel x y0
a, y:A
H:R y a
Acc R y
    case (F_compat y a); trivial; intros.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x0 y0 : A,
R x0 y0 -> inv_lt_rel x0 y0
a, y:A
H:R y a
x:nat
H0:F y x
H1:forall m : nat, F a m -> x < m
Acc R y
    apply acc_lt_rel; trivial.A:Set
R:A -> A -> Prop
F:A -> nat -> Prop
F_compat:forall x0 y0 : A,
R x0 y0 -> inv_lt_rel x0 y0
a, y:A
H:R y a
x:nat
H0:F y x
H1:forall m : nat, F a m -> x < m
exists n : nat, F y n
    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).forall (A : Set) (F : A -> nat -> Prop),
well_founded (inv_lt_rel A F)
Proof.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.forall P : nat -> Prop,
(forall n : nat, P n \/ ~ P n) ->
(exists n : nat, P n) -> has_unique_least_element le P
Proof.forall P : nat -> Prop,
(forall n : nat, P n \/ ~ P n) ->
(exists n : nat, P n) -> has_unique_least_element le P
  intros P Pdec (n0,HPn0).P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
has_unique_least_element le P
  assert
    (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
               \/ (forall n', P n' -> n<=n')).P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
forall n : nat,
(exists n' : nat,
   n' < n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> n <= n')
P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
H:forall n : nat,
(exists n' : nat,
   n' < n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> n <= n')
has_unique_least_element le P
  {P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
forall n : nat,
(exists n' : nat,
   n' < n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> n <= n') induction n.P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
(exists n' : nat,
   n' < 0 /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> 0 <= n')
P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IHn:(exists n' : nat,
   n' < n /\
   P n' /\
   (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> n <= n')
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n')
    -P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
(exists n' : nat,
   n' < 0 /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> 0 <= n') right.P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
forall n' : nat, P n' -> 0 <= n' intros.P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
n':nat
H:P n'
0 <= n' apply Nat.le_0_l.
    -P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IHn:(exists n' : nat,
   n' < n /\
   P n' /\
   (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> n <= n')
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n') destruct IHn as [(n' & IH1 & IH2)|IH].P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n, n':nat
IH1:n' < n
IH2:P n' /\ (forall n'' : nat, P n'' -> n' <= n'')
(exists n'0 : nat,
   n'0 < S n /\
   P n'0 /\ (forall n'' : nat, P n'' -> n'0 <= n'')) \/
(forall n'0 : nat, P n'0 -> S n <= n'0)
P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n')
      +P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n, n':nat
IH1:n' < n
IH2:P n' /\ (forall n'' : nat, P n'' -> n' <= n'')
(exists n'0 : nat,
   n'0 < S n /\
   P n'0 /\ (forall n'' : nat, P n'' -> n'0 <= n'')) \/
(forall n'0 : nat, P n'0 -> S n <= n'0) left.P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n, n':nat
IH1:n' < n
IH2:P n' /\ (forall n'' : nat, P n'' -> n' <= n'')
exists n'0 : nat,
  n'0 < S n /\
  P n'0 /\ (forall n'' : nat, P n'' -> n'0 <= n'') exists n'; auto with arith.
      +P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n') destruct (Pdec n) as [HP|HP].P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:P n
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n')
P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:~ P n
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n')
        *P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:P n
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n') left.P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:P n
exists n' : nat,
  n' < S n /\
  P n' /\ (forall n'' : nat, P n'' -> n' <= n'') exists n; auto with arith.
        *P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:~ P n
(exists n' : nat,
   n' < S n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> S n <= n') right.P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:~ P n
forall n' : nat, P n' -> S n <= n' intros n' Hn'.P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n'0 : nat, P n'0 -> n <= n'0
HP:~ P n
n':nat
Hn':P n'
S n <= n'
          apply Nat.le_neq; split; auto.P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n'0 : nat, P n'0 -> n <= n'0
HP:~ P n
n':nat
Hn':P n'
n <> n' intros <-.P:nat -> Prop
Pdec:forall n1 : nat, P n1 \/ ~ P n1
n0:nat
HPn0:P n0
n:nat
IH:forall n' : nat, P n' -> n <= n'
HP:~ P n
Hn':P n
False auto. }P:nat -> Prop
Pdec:forall n : nat, P n \/ ~ P n
n0:nat
HPn0:P n0
H:forall n : nat,
(exists n' : nat,
   n' < n /\
   P n' /\ (forall n'' : nat, P n'' -> n' <= n'')) \/
(forall n' : nat, P n' -> n <= n')
has_unique_least_element le P
  destruct (H n0) as [(n & H1 & H2 & H3)|H0]; [exists n | exists n0];
   repeat split; trivial;
   intros n' (HPn',Hn'); apply Nat.le_antisymm; auto.
Qed.

Unset Implicit Arguments.

Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n) (only parsing).