blob: 5c2b240508b5aabcccd833396e2766730b6c95c2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Well_Ordering.v,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ i*)
(** Author: Cristina Cornes.
From: Constructing Recursion Operators in Type Theory
L. Paulson JSC (1986) 2, 325-355 *)
Require Eqdep.
Section WellOrdering.
Variable A:Set.
Variable B:A->Set.
Inductive WO : Set :=
sup : (a:A)(f:(B a)->WO)WO.
Inductive le_WO : WO->WO->Prop :=
le_sup : (a:A)(f:(B a)->WO)(v:(B a)) (le_WO (f v) (sup a f)).
Theorem wf_WO : (well_founded WO le_WO ).
Proof.
Unfold well_founded ;Intro.
Apply Acc_intro.
Elim a.
Intros.
Inversion H0.
Apply Acc_intro.
Generalize H4 ;Generalize H1 ;Generalize f0 ;Generalize v.
Rewrite -> H3.
Intros.
Apply (H v0 y0).
Cut (eq ? f f1).
Intros E;Rewrite -> E;Auto.
Symmetry.
Apply (inj_pair2 A [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:Set.
Variable leA:A->A->Prop.
Definition B:= [a:A] {x:A | (leA x a)}.
Definition wof: (well_founded A leA)-> A-> (WO A B).
Proof.
Intros.
Apply (well_founded_induction A leA H [a:A](WO A B));Auto.
Intros.
Apply (sup A B x).
Unfold 1 B .
NewDestruct 1 as [x0].
Apply (H1 x0);Auto.
Qed.
End Characterisation_wf_relations.
|
