← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Classes/EquivDec.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/EquivDec.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
(* Decidable equivalences.
 
10
 *
 
11
 * Author: Matthieu Sozeau
 
12
 * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
 
13
 *              91405 Orsay, France *)
 
14
 
 
15
(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *)
 
16
 
 
17
(** Export notations. *)
 
18
 
 
19
Require Export Coq.Classes.Equivalence.
 
20
 
 
21
(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
 
22
   classically. *)
 
23
 
 
24
Require Import Coq.Logic.Decidable.
 
25
 
 
26
Open Scope equiv_scope.
 
27
 
 
28
Class DecidableEquivalence `(equiv : Equivalence A) :=
 
29
  setoid_decidable : forall x y : A, decidable (x === y).
 
30
 
 
31
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
32
 
 
33
Class EqDec A R {equiv : Equivalence R} :=
 
34
  equiv_dec : forall x y : A, { x === y } + { x =/= y }.
 
35
 
 
36
(** We define the [==] overloaded notation for deciding equality. It does not take precedence
 
37
   of [==] defined in the type scope, hence we can have both at the same time. *)
 
38
 
 
39
Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
 
40
 
 
41
Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
 
42
  match x with
 
43
    | left H => @right _ _ H 
 
44
    | right H => @left _ _ H 
 
45
  end.
 
46
 
 
47
Require Import Coq.Program.Program.
 
48
 
 
49
Open Local Scope program_scope.
 
50
 
 
51
(** Invert the branches. *)
 
52
 
 
53
Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
 
54
 
 
55
(** Overloaded notation for inequality. *)
 
56
 
 
57
Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
 
58
 
 
59
(** Define boolean versions, losing the logical information. *)
 
60
 
 
61
Definition equiv_decb `{EqDec A} (x y : A) : bool :=
 
62
  if x == y then true else false.
 
63
 
 
64
Definition nequiv_decb `{EqDec A} (x y : A) : bool :=
 
65
  negb (equiv_decb x y).
 
66
 
 
67
Infix "==b" := equiv_decb (no associativity, at level 70).
 
68
Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
69
 
 
70
(** Decidable leibniz equality instances. *)
 
71
 
 
72
Require Import Coq.Arith.Peano_dec.
 
73
 
 
74
(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
 
75
 
 
76
Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
 
77
 
 
78
Require Import Coq.Bool.Bool.
 
79
 
 
80
Program Instance bool_eqdec : EqDec bool eq := bool_dec.
 
81
 
 
82
Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left.
 
83
 
 
84
  Next Obligation.
 
85
  Proof.
 
86
    destruct x ; destruct y.
 
87
    reflexivity.
 
88
  Qed.
 
89
 
 
90
Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
 
91
  ! EqDec (prod A B) eq :=
 
92
  { equiv_dec x y :=
 
93
    let '(x1, x2) := x in 
 
94
    let '(y1, y2) := y in 
 
95
    if x1 == y1 then 
 
96
      if x2 == y2 then in_left
 
97
      else in_right
 
98
    else in_right }.
 
99
 
 
100
  Solve Obligations using unfold complement, equiv ; program_simpl.
 
101
 
 
102
Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
 
103
  EqDec (sum A B) eq := {
 
104
  equiv_dec x y := 
 
105
    match x, y with
 
106
      | inl a, inl b => if a == b then in_left else in_right
 
107
      | inr a, inr b => if a == b then in_left else in_right
 
108
      | inl _, inr _ | inr _, inl _ => in_right
 
109
    end }.
 
110
 
 
111
  Solve Obligations using unfold complement, equiv ; program_simpl.
 
112
 
 
113
(** Objects of function spaces with countable domains like bool have decidable equality. 
 
114
   Proving the reflection requires functional extensionality though. *)
 
115
 
 
116
Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
 
117
  { equiv_dec f g := 
 
118
    if f true == g true then
 
119
      if f false == g false then in_left
 
120
      else in_right
 
121
    else in_right }.
 
122
 
 
123
  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
 
124
 
 
125
  Next Obligation.
 
126
  Proof.
 
127
    extensionality x.
 
128
    destruct x ; auto.
 
129
  Qed.
 
130
 
 
131
Require Import List.
 
132
 
 
133
Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
 
134
  { equiv_dec := 
 
135
    fix aux (x : list A) y { struct x } :=
 
136
    match x, y with
 
137
      | nil, nil => in_left
 
138
      | cons hd tl, cons hd' tl' => 
 
139
        if hd == hd' then
 
140
          if aux tl tl' then in_left else in_right
 
141
          else in_right
 
142
      | _, _ => in_right
 
143
    end }.
 
144
 
 
145
  Solve Obligations using unfold equiv, complement in *; program_simpl;
 
146
    intuition (discriminate || eauto).
 
147
 
 
148
  Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
 
149
 
 
150
  Solve Obligations using unfold equiv, complement in *; program_simpl;
 
151
    intuition (discriminate || eauto).