← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Wellfounded/Well_Ordering.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Wellfounded/Well_Ordering.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Well_Ordering.v 9598 2007-02-06 19:45:52Z herbelin $ i*)
 
10
 
 
11
(** Author: Cristina Cornes.
 
12
    From: Constructing Recursion Operators in Type Theory
 
13
    L. Paulson  JSC (1986) 2, 325-355 *)
 
14
 
 
15
Require Import Eqdep.
 
16
 
 
17
Section WellOrdering.
 
18
  Variable A : Type.
 
19
  Variable B : A -> Type. 
 
20
  
 
21
  Inductive WO : Type :=
 
22
    sup : forall (a:A) (f:B a -> WO), WO.
 
23
 
 
24
 
 
25
  Inductive le_WO : WO -> WO -> Prop :=
 
26
    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
 
27
 
 
28
  Theorem wf_WO : well_founded le_WO.
 
29
  Proof.
 
30
    unfold well_founded in |- *; intro.
 
31
    apply Acc_intro.
 
32
    elim a.
 
33
    intros.
 
34
    inversion H0.
 
35
    apply Acc_intro.
 
36
    generalize H4; generalize H1; generalize f0; generalize v.
 
37
    rewrite H3.
 
38
    intros.
 
39
    apply (H v0 y0).
 
40
    cut (f = f1).
 
41
    intros E; rewrite E; auto.
 
42
    symmetry  in |- *.
 
43
    apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
 
44
  Qed.
 
45
 
 
46
End WellOrdering.
 
47
 
 
48
 
 
49
Section Characterisation_wf_relations.
 
50
 
 
51
  (** Wellfounded relations are the inverse image of wellordering types *)
 
52
  (*  in course of development                                          *)
 
53
 
 
54
 
 
55
  Variable A : Type.
 
56
  Variable leA : A -> A -> Prop.
 
57
 
 
58
  Definition B (a:A) := {x : A | leA x a}.
 
59
 
 
60
  Definition wof : well_founded leA -> A -> WO A B.
 
61
  Proof.
 
62
    intros.
 
63
    apply (well_founded_induction_type H (fun a:A => WO A B)); auto.
 
64
    intros x H1.
 
65
    apply (sup A B x).
 
66
    unfold B at 1 in |- *.
 
67
    destruct 1 as [x0].
 
68
    apply (H1 x0); auto.
 
69
Qed.
 
70
 
 
71
End Characterisation_wf_relations.