diff options
Diffstat (limited to 'theories/Classes/EquivDec.v')
| -rw-r--r-- | theories/Classes/EquivDec.v | 80 |
1 files changed, 38 insertions, 42 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 15cabf81..0a35ef45 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -6,46 +6,51 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable equivalences. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable equivalences. -(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +(* $Id$ *) (** Export notations. *) Require Export Coq.Classes.Equivalence. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. +Require Import Coq.Bool.Bool. +Require Import Coq.Arith.Peano_dec. +Require Import Coq.Program.Program. + +Generalizable Variables A B R. Open Scope equiv_scope. Class DecidableEquivalence `(equiv : Equivalence A) := setoid_decidable : forall x y : A, decidable (x === y). -(** The [EqDec] class gives a decision procedure for a particular setoid equality. *) +(** The [EqDec] class gives a decision procedure for a particular + setoid equality. *) Class EqDec A R {equiv : Equivalence R} := equiv_dec : forall x y : A, { x === y } + { x =/= y }. -(** We define the [==] overloaded notation for deciding equality. It does not take precedence - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } := match x with - | left H => @right _ _ H - | right H => @left _ _ H + | left H => @right _ _ H + | right H => @left _ _ H end. -Require Import Coq.Program.Program. - Open Local Scope program_scope. (** Invert the branches. *) @@ -69,17 +74,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -Require Import Coq.Arith.Peano_dec. - -(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) +(** The equiv is burried inside the setoid, but we can recover it by specifying + which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. -Require Import Coq.Bool.Bool. - Program Instance bool_eqdec : EqDec bool eq := bool_dec. -Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left. +Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. @@ -87,41 +89,37 @@ Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left. reflexivity. Qed. +Obligation Tactic := unfold complement, equiv ; program_simpl. + Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) : ! EqDec (prod A B) eq := { equiv_dec x y := - let '(x1, x2) := x in - let '(y1, y2) := y in - if x1 == y1 then + let '(x1, x2) := x in + let '(y1, y2) := y in + if x1 == y1 then if x2 == y2 then in_left else in_right else in_right }. - Solve Obligations using unfold complement, equiv ; program_simpl. - Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : EqDec (sum A B) eq := { - equiv_dec x y := + equiv_dec x y := match x, y with | inl a, inl b => if a == b then in_left else in_right | inr a, inr b => if a == b then in_left else in_right | inl _, inr _ | inr _, inl _ => in_right end }. - Solve Obligations using unfold complement, equiv ; program_simpl. - -(** Objects of function spaces with countable domains like bool have decidable equality. - Proving the reflection requires functional extensionality though. *) +(** Objects of function spaces with countable domains like bool have decidable + equality. Proving the reflection requires functional extensionality though. *) Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := - { equiv_dec f g := + { equiv_dec f g := if f true == g true then if f false == g false then in_left else in_right else in_right }. - Solve Obligations using try red ; unfold equiv, complement ; program_simpl. - Next Obligation. Proof. extensionality x. @@ -131,21 +129,19 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := Require Import List. Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := - { equiv_dec := - fix aux (x : list A) y { struct x } := + { equiv_dec := + fix aux (x y : list A) := match x, y with | nil, nil => in_left - | cons hd tl, cons hd' tl' => + | cons hd tl, cons hd' tl' => if hd == hd' then if aux tl tl' then in_left else in_right else in_right | _, _ => in_right end }. - Solve Obligations using unfold equiv, complement in *; program_simpl; - intuition (discriminate || eauto). + Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). - Next Obligation. destruct x ; destruct y ; intuition eauto. Defined. + Next Obligation. destruct y ; intuition eauto. Defined. - Solve Obligations using unfold equiv, complement in *; program_simpl; - intuition (discriminate || eauto). + Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). |