← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Classes/Equivalence.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/Classes/Equivalence.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
(* Typeclass-based setoids. Definitions on [Equivalence].
 
10
 
 
11
   Author: Matthieu Sozeau
 
12
   Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
 
13
   91405 Orsay, France *) 
 
14
 
 
15
(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
16
 
 
17
Require Import Coq.Program.Basics.
 
18
Require Import Coq.Program.Tactics.
 
19
 
 
20
Require Import Coq.Classes.Init.
 
21
Require Import Relation_Definitions.
 
22
Require Export Coq.Classes.RelationClasses.
 
23
Require Import Coq.Classes.Morphisms.
 
24
 
 
25
Set Implicit Arguments.
 
26
Unset Strict Implicit.
 
27
 
 
28
Open Local Scope signature_scope.
 
29
 
 
30
Definition equiv `{Equivalence A R} : relation A := R.
 
31
 
 
32
(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
33
 
 
34
Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
35
 
 
36
Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
 
37
  
 
38
Open Local Scope equiv_scope.
 
39
 
 
40
(** Overloading for [PER]. *)
 
41
 
 
42
Definition pequiv `{PER A R} : relation A := R.
 
43
 
 
44
(** Overloaded notation for partial equivalence. *)
 
45
 
 
46
Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
47
 
 
48
(** Shortcuts to make proof search easier. *)
 
49
 
 
50
Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
 
51
 
 
52
Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
 
53
 
 
54
Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
55
 
 
56
  Next Obligation.
 
57
  Proof.
 
58
    transitivity y ; auto.
 
59
  Qed.
 
60
 
 
61
(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
62
 
 
63
Ltac setoid_subst H := 
 
64
  match type of H with
 
65
    ?x === ?y => substitute H ; clear H x
 
66
  end.
 
67
 
 
68
Ltac setoid_subst_nofail :=
 
69
  match goal with
 
70
    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
 
71
    | _ => idtac
 
72
  end.
 
73
  
 
74
(** [subst*] will try its best at substituting every equality in the goal. *)
 
75
 
 
76
Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
 
77
 
 
78
(** Simplify the goal w.r.t. equivalence. *)
 
79
 
 
80
Ltac equiv_simplify_one :=
 
81
  match goal with
 
82
    | [ H : ?x === ?x |- _ ] => clear H
 
83
    | [ H : ?x === ?y |- _ ] => setoid_subst H
 
84
    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
 
85
    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
 
86
  end.
 
87
 
 
88
Ltac equiv_simplify := repeat equiv_simplify_one.
 
89
 
 
90
(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
 
91
   for easy recognition in tactics. *)
 
92
 
 
93
Ltac equivify_tac :=
 
94
  match goal with
 
95
    | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
 
96
    | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
 
97
  end.
 
98
 
 
99
Ltac equivify := repeat equivify_tac.
 
100
 
 
101
Section Respecting.
 
102
 
 
103
  (** Here we build an equivalence instance for functions which relates respectful ones only, 
 
104
     we do not export it. *)
 
105
 
 
106
  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := 
 
107
    { morph : A -> B | respectful R R' morph morph }.
 
108
  
 
109
  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
 
110
    Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
111
  
 
112
  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
 
113
 
 
114
  Next Obligation.
 
115
  Proof. 
 
116
    unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
 
117
  Qed.
 
118
 
 
119
End Respecting.
 
120
 
 
121
(** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
122
 
 
123
Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
 
124
  Equivalence (pointwise_relation A eqB) | 9.
 
125
 
 
126
  Next Obligation.
 
127
  Proof.
 
128
    transitivity (y a) ; auto.
 
129
  Qed.