Well_Ordering.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)         *)
(************************************************************************)

Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355

Require Import Eqdep.

#[universes(template)]
Inductive WO (A : Type) (B : A -> Type) : Type :=
  sup : forall (a:A) (f:B a -> WO A B), WO A B.

Section WellOrdering.
  Variable A : Type.
  Variable B : A -> Type.

  Notation WO := (WO A B).

  Inductive le_WO : WO -> WO -> Prop :=
    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup _ _ a f).

  Theorem wf_WO : well_founded le_WO.A:Type
B:A -> Type
well_founded le_WO
  Proof.A:Type
B:A -> Type
well_founded le_WO
    unfold well_founded; intro.A:Type
B:A -> Type
a:WO
Acc le_WO a
    apply Acc_intro.A:Type
B:A -> Type
a:WO
forall y : WO, le_WO y a -> Acc le_WO y
    elim a.A:Type
B:A -> Type
a:WO
forall (a0 : A) (f : B a0 -> WO),
(forall (b : B a0) (y : WO),
 le_WO y (f b) -> Acc le_WO y) ->
forall y : WO, le_WO y (sup A B a0 f) -> Acc le_WO y
    intros.A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y0 : WO),
le_WO y0 (f b) -> Acc le_WO y0
y:WO
H0:le_WO y (sup A B a0 f)
Acc le_WO y
    inversion H0.A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y0 : WO),
le_WO y0 (f b) -> Acc le_WO y0
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
Acc le_WO (f1 v0)
    apply Acc_intro.A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y0 : WO),
le_WO y0 (f b) -> Acc le_WO y0
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
forall y0 : WO, le_WO y0 (f1 v0) -> Acc le_WO y0
    generalize H4; generalize H1; generalize f0; generalize v.A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y0 : WO),
le_WO y0 (f b) -> Acc le_WO y0
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
forall (v1 : B a1) (f2 : B a1 -> WO),
f2 v1 = y ->
existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f ->
forall y0 : WO, le_WO y0 (f1 v0) -> Acc le_WO y0
    rewrite H3.A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y0 : WO),
le_WO y0 (f b) -> Acc le_WO y0
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
forall (v1 : B a0) (f2 : B a0 -> WO),
f2 v1 = y ->
existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f ->
forall y0 : WO, le_WO y0 (f1 v0) -> Acc le_WO y0
    intros.A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
Acc le_WO y0
    apply (H v0 y0).A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
le_WO y0 (f v0)
    cut (f = f1).A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
f = f1 -> le_WO y0 (f v0)
A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
f = f1
    -A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
f = f1 -> le_WO y0 (f v0) intros E; rewrite E; auto.
    -A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
f = f1 symmetry .A:Type
B:A -> Type
a:WO
a0:A
f:B a0 -> WO
H:forall (b : B a0) (y1 : WO),
le_WO y1 (f b) -> Acc le_WO y1
y:WO
H0:le_WO y (sup A B a0 f)
a1:A
f0:B a1 -> WO
v:B a1
H1:f0 v = y
H3:a1 = a0
f1:B a0 -> WO
v0:B a0
H4:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
v1:B a0
f2:B a0 -> WO
H2:f2 v1 = y
H5:existT (fun a2 : A => B a2 -> WO) a0 f1 =
existT (fun a2 : A => B a2 -> WO) a0 f
y0:WO
H6:le_WO y0 (f1 v0)
f1 = f
      apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
  Qed.

End WellOrdering.


Section Characterisation_wf_relations.

Wellfounded relations are the inverse image of wellordering types

  (*  in course of development                                          *)


  Variable A : Type.
  Variable leA : A -> A -> Prop.

  Definition B (a:A) := {x : A | leA x a}.

  Definition wof : well_founded leA -> A -> WO A B.A:Type
leA:A -> A -> Prop
well_founded leA -> A -> WO A B
  Proof.A:Type
leA:A -> A -> Prop
well_founded leA -> A -> WO A B
    intros.A:Type
leA:A -> A -> Prop
H:well_founded leA
X:A
WO A B
    apply (well_founded_induction_type H (fun a:A => WO A B)); auto.A:Type
leA:A -> A -> Prop
H:well_founded leA
X:A
forall x : A,
(forall y : A, leA y x -> WO A B) -> WO A B
    intros x H1.A:Type
leA:A -> A -> Prop
H:well_founded leA
X, x:A
H1:forall y : A, leA y x -> WO A B
WO A B
    apply (sup A B x).A:Type
leA:A -> A -> Prop
H:well_founded leA
X, x:A
H1:forall y : A, leA y x -> WO A B
B x -> WO A B
    unfold B at 1.A:Type
leA:A -> A -> Prop
H:well_founded leA
X, x:A
H1:forall y : A, leA y x -> WO A B
{x0 : A | leA x0 x} -> WO A B
    destruct 1 as [x0].A:Type
leA:A -> A -> Prop
H:well_founded leA
X, x:A
H1:forall y : A, leA y x -> WO A B
x0:A
l:leA x0 x
WO A B
    apply (H1 x0); auto.
Qed.

End Characterisation_wf_relations.