diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/EquivDec.v | 4 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 4 | ||||
| -rw-r--r-- | theories/Classes/Init.v | 6 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 125 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 32 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 10 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 85 | ||||
| -rw-r--r-- | theories/Classes/RelationPairs.v | 34 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 6 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 19 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 4 |
11 files changed, 195 insertions, 134 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index ea1543e3..719a9a84 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: EquivDec.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Export notations. *) Require Export Coq.Classes.Equivalence. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index e562328d..d9e9fe25 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: Equivalence.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index eea16129..a001f2e9 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,8 +13,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: Init.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Hints for the proof search: these combinators should be considered rigid. *) Require Import Coq.Program.Basics. @@ -36,4 +34,4 @@ Ltac unconvertible := | |- _ => exact tt end. -Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file +Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index ea869a66..8e491b1b 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,8 +13,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: Morphisms.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. @@ -23,12 +21,6 @@ Require Export Coq.Classes.RelationClasses. Generalizable All Variables. Local Obligation Tactic := simpl_relation. -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - -Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. - (** * Morphisms. We now turn to the definition of [Proper] and declare standard instances. @@ -63,8 +55,8 @@ Definition respectful {A B : Type} Delimit Scope signature_scope with signature. -Arguments Scope Proper [type_scope signature_scope]. -Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. Module ProperNotations. @@ -83,17 +75,58 @@ Export ProperNotations. Open Local Scope signature_scope. +(** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f] + by repeated introductions and setoid rewrites. It should work + fine when [f] is a combination of already known morphisms and + quantifiers. *) + +Ltac solve_respectful t := + match goal with + | |- respectful _ _ _ _ => + let H := fresh "H" in + intros ? ? H; solve_respectful ltac:(setoid_rewrite H; t) + | _ => t; reflexivity + end. + +Ltac solve_proper := unfold Proper; solve_respectful ltac:(idtac). + +(** [f_equiv] is a clone of [f_equal] that handles setoid equivalences. + For example, if we know that [f] is a morphism for [E1==>E2==>E], + then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv] + into the subgoals [E1 x x'] and [E2 y y']. +*) + +Ltac f_equiv := + match goal with + | |- ?R (?f ?x) (?f' _) => + let T := type of x in + let Rx := fresh "R" in + evar (Rx : relation T); + let H := fresh in + assert (H : (Rx==>R)%signature f f'); + unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ] + | |- ?R ?f ?f' => + try reflexivity; + change (Proper R f); eauto with typeclass_instances; fail + | _ => idtac + end. + +(** [forall_def] reifies the dependent product as a definition. *) + +Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x. + (** Dependent pointwise lifting of a relation on the range. *) -Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) := - λ f g, Π a : A, sig a (f a) (g a). +Definition forall_relation {A : Type} {B : A -> Type} + (sig : forall a, relation (B a)) : relation (forall x, B x) := + fun f g => forall a, sig a (f a) (g a). -Arguments Scope forall_relation [type_scope type_scope signature_scope]. +Arguments forall_relation {A B}%type sig%signature _ _. (** Non-dependent pointwise lifting *) Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := - Eval compute in forall_relation (B:=λ _, B) (λ _, R). + Eval compute in forall_relation (B:=fun _ => B) (fun _ => R). Lemma pointwise_pointwise A B (R : relation B) : relation_equivalence (pointwise_relation A R) (@eq A ==> R). @@ -192,28 +225,34 @@ Hint Extern 4 (subrelation (inverse _) _) => (** The complement of a relation conserves its proper elements. *) -Program Instance complement_proper +Program Definition complement_proper `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement R). + Proper (RA ==> RA ==> iff) (complement R) := _. - Next Obligation. + Next Obligation. Proof. unfold complement. pose (mR x y H x0 y0 H0). intuition. Qed. + +Hint Extern 1 (Proper _ (complement _)) => + apply @complement_proper : typeclass_instances. (** The [inverse] too, actually the [flip] instance is a bit more general. *) -Program Instance flip_proper +Program Definition flip_proper `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : - Proper (RB ==> RA ==> RC) (flip f). + Proper (RB ==> RA ==> RC) (flip f) := _. Next Obligation. Proof. apply mor ; auto. Qed. +Hint Extern 1 (Proper _ (flip _)) => + apply @flip_proper : typeclass_instances. + (** Every Transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) @@ -369,41 +408,45 @@ Class PartialApplication. CoInductive normalization_done : Prop := did_normalization. Ltac partial_application_tactic := - let rec do_partial_apps H m := + let rec do_partial_apps H m cont := match m with - | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H] - | _ => idtac + | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; + [(do_partial_apps H m' ltac:idtac)|clear H] + | _ => cont end in - let rec do_partial H ar m := + let rec do_partial H ar m := match ar with - | 0 => do_partial_apps H m + | 0%nat => do_partial_apps H m ltac:(fail 1) | S ?n' => match m with ?m' ?x => do_partial H n' m' end end in - let on_morphism m := - let m' := fresh in head_of_constr m' m ; - let n := fresh in evar (n:nat) ; - let v := eval compute in n in clear n ; - let H := fresh in - assert(H:Params m' v) by typeclasses eauto ; - let v' := eval compute in v in subst m'; - do_partial H v' m - in + let params m sk fk := + (let m' := fresh in head_of_constr m' m ; + let n := fresh in evar (n:nat) ; + let v := eval compute in n in clear n ; + let H := fresh in + assert(H:Params m' v) by typeclasses eauto ; + let v' := eval compute in v in subst m'; + (sk H v' || fail 1)) + || fk + in + let on_morphism m cont := + params m ltac:(fun H n => do_partial H n m) + ltac:(cont) + in match goal with | [ _ : normalization_done |- _ ] => fail 1 | [ _ : @Params _ _ _ |- _ ] => fail 1 | [ |- @Proper ?T _ (?m ?x) ] => match goal with - | [ _ : PartialApplication |- _ ] => - class_apply @Reflexive_partial_app_morphism - | _ => - on_morphism (m x) || - (class_apply @Reflexive_partial_app_morphism ; - [ pose Build_PartialApplication | idtac ]) + | [ H : PartialApplication |- _ ] => + class_apply @Reflexive_partial_app_morphism; [|clear H] + | _ => on_morphism (m x) + ltac:(class_apply @Reflexive_partial_app_morphism) end end. @@ -432,7 +475,7 @@ Qed. Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) : Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature). -Proof. unfold Normalizes in *. intros. +Proof. unfold Normalizes in *. intros. rewrite NA, NB. firstorder. Qed. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 5a2482d4..256bcc37 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -107,3 +107,33 @@ Program Instance all_inverse_impl_morphism {A : Type} : unfold pointwise_relation, all in *. intuition ; specialize (H x0) ; intuition. Qed. + +(** Equivalent points are simultaneously accessible or not *) + +Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) + `(Equivalence _ E) `(Proper _ (E==>E==>iff) R) : + Proper (E==>iff) (Acc R). +Proof. + apply proper_sym_impl_iff; auto with *. + intros x y EQ WF. apply Acc_intro; intros z Hz. + rewrite <- EQ in Hz. now apply Acc_inv with x. +Qed. + +(** Equivalent relations have the same accessible points *) + +Instance Acc_rel_morphism {A:Type} : + Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A). +Proof. + apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry. + intros R R' EQ a a' Ha WF. subst a'. + induction WF as [x _ WF']. constructor. + intros y Ryx. now apply WF', EQ. +Qed. + +(** Equivalent relations are simultaneously well-founded or not *) + +Instance well_founded_morphism {A : Type} : + Proper (@relation_equivalence A ==> iff) (@well_founded A). +Proof. + unfold well_founded. solve_proper. +Qed. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index a8009f9e..7ac49eeb 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,11 +32,11 @@ Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> Require Import List. -Lemma predicate_equivalence_pointwise (l : list Type) : +Lemma predicate_equivalence_pointwise (l : Tlist) : Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id. Proof. do 2 red. unfold predicate_equivalence. auto. Qed. -Lemma predicate_implication_pointwise (l : list Type) : +Lemma predicate_implication_pointwise (l : Tlist) : Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. @@ -45,11 +45,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed. Instance relation_equivalence_pointwise : Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. -Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed. +Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed. Instance subrelation_pointwise : Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id. -Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed. +Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed. Lemma inverse_pointwise_relation A (R : relation A) : diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 94c51bf1..cf05d9d4 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** * Typeclass-based relations, tactics and standard instances +(** * Typeclass-based relations, tactics and standard instances This is the basic theory needed to formalize morphisms and setoids. @@ -15,8 +15,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. @@ -143,9 +141,9 @@ Program Instance impl_Transitive : Transitive impl. (** Logical equivalence. *) -Program Instance iff_Reflexive : Reflexive iff. -Program Instance iff_Symmetric : Symmetric iff. -Program Instance iff_Transitive : Transitive iff. +Instance iff_Reflexive : Reflexive iff := iff_refl. +Instance iff_Symmetric : Symmetric iff := iff_sym. +Instance iff_Transitive : Transitive iff := iff_trans. (** Leibniz equality. *) @@ -158,14 +156,14 @@ Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. (** A [PreOrder] is both Reflexive and Transitive. *) Class PreOrder {A} (R : relation A) : Prop := { - PreOrder_Reflexive :> Reflexive R ; - PreOrder_Transitive :> Transitive R }. + PreOrder_Reflexive :> Reflexive R | 2 ; + PreOrder_Transitive :> Transitive R | 2 }. (** A partial equivalence relation is Symmetric and Transitive. *) Class PER {A} (R : relation A) : Prop := { - PER_Symmetric :> Symmetric R ; - PER_Transitive :> Transitive R }. + PER_Symmetric :> Symmetric R | 3 ; + PER_Transitive :> Transitive R | 3 }. (** Equivalence relations. *) @@ -210,17 +208,21 @@ Local Open Scope list_scope. (** A compact representation of non-dependent arities, with the codomain singled-out. *) -Fixpoint arrows (l : list Type) (r : Type) : Type := +(* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) +Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist. +Local Infix "::" := Tcons. + +Fixpoint arrows (l : Tlist) (r : Type) : Type := match l with - | nil => r + | Tnil => r | A :: l' => A -> arrows l' r end. (** We can define abbreviations for operation and relation types based on [arrows]. *) -Definition unary_operation A := arrows (A::nil) A. -Definition binary_operation A := arrows (A::A::nil) A. -Definition ternary_operation A := arrows (A::A::A::nil) A. +Definition unary_operation A := arrows (A::Tnil) A. +Definition binary_operation A := arrows (A::A::Tnil) A. +Definition ternary_operation A := arrows (A::A::A::Tnil) A. (** We define n-ary [predicate]s as functions into [Prop]. *) @@ -228,23 +230,23 @@ Notation predicate l := (arrows l Prop). (** Unary predicates, or sets. *) -Definition unary_predicate A := predicate (A::nil). +Definition unary_predicate A := predicate (A::Tnil). (** Homogeneous binary relations, equivalent to [relation A]. *) -Definition binary_relation A := predicate (A::A::nil). +Definition binary_relation A := predicate (A::A::Tnil). (** We can close a predicate by universal or existential quantification. *) -Fixpoint predicate_all (l : list Type) : predicate l -> Prop := +Fixpoint predicate_all (l : Tlist) : predicate l -> Prop := match l with - | nil => fun f => f + | Tnil => fun f => f | A :: tl => fun f => forall x : A, predicate_all tl (f x) end. -Fixpoint predicate_exists (l : list Type) : predicate l -> Prop := +Fixpoint predicate_exists (l : Tlist) : predicate l -> Prop := match l with - | nil => fun f => f + | Tnil => fun f => f | A :: tl => fun f => exists x : A, predicate_exists tl (f x) end. @@ -253,30 +255,30 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop := For an operator on [Prop] this lifts the operator to a binary operation. *) Fixpoint pointwise_extension {T : Type} (op : binary_operation T) - (l : list Type) : binary_operation (arrows l T) := + (l : Tlist) : binary_operation (arrows l T) := match l with - | nil => fun R R' => op R R' + | Tnil => fun R R' => op R R' | A :: tl => fun R R' => fun x => pointwise_extension op tl (R x) (R' x) end. (** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *) -Fixpoint pointwise_lifting (op : binary_relation Prop) (l : list Type) : binary_relation (predicate l) := +Fixpoint pointwise_lifting (op : binary_relation Prop) (l : Tlist) : binary_relation (predicate l) := match l with - | nil => fun R R' => op R R' + | Tnil => fun R R' => op R R' | A :: tl => fun R R' => forall x, pointwise_lifting op tl (R x) (R' x) end. (** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *) -Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) := +Definition predicate_equivalence {l : Tlist} : binary_relation (predicate l) := pointwise_lifting iff l. (** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *) -Definition predicate_implication {l : list Type} := +Definition predicate_implication {l : Tlist} := pointwise_lifting impl l. (** Notations for pointwise equivalence and implication of predicates. *) @@ -297,15 +299,15 @@ Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_ (** The always [True] and always [False] predicates. *) -Fixpoint true_predicate {l : list Type} : predicate l := +Fixpoint true_predicate {l : Tlist} : predicate l := match l with - | nil => True + | Tnil => True | A :: tl => fun _ => @true_predicate tl end. -Fixpoint false_predicate {l : list Type} : predicate l := +Fixpoint false_predicate {l : Tlist} : predicate l := match l with - | nil => False + | Tnil => False | A :: tl => fun _ => @false_predicate tl end. @@ -315,6 +317,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l). + Next Obligation. induction l ; firstorder. Qed. @@ -343,18 +346,18 @@ Program Instance predicate_implication_preorder : from the general ones. *) Definition relation_equivalence {A : Type} : relation (relation A) := - @predicate_equivalence (_::_::nil). + @predicate_equivalence (_::_::Tnil). Class subrelation {A:Type} (R R' : relation A) : Prop := - is_subrelation : @predicate_implication (A::A::nil) R R'. + is_subrelation : @predicate_implication (A::A::Tnil) R R'. -Implicit Arguments subrelation [[A]]. +Arguments subrelation {A} R R'. Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_intersection (A::A::nil) R R'. + @predicate_intersection (A::A::Tnil) R R'. Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_union (A::A::nil) R R'. + @predicate_union (A::A::Tnil) R R'. (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) @@ -362,10 +365,10 @@ Set Automatic Introduction. Instance relation_equivalence_equivalence (A : Type) : Equivalence (@relation_equivalence A). -Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed. +Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed. Instance relation_implication_preorder A : PreOrder (@subrelation A). -Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed. +Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed. (** *** Partial Order. A partial order is a preorder which is additionally antisymmetric. @@ -393,7 +396,7 @@ Program Instance subrelation_partial_order : Next Obligation. Proof. - unfold relation_equivalence in *. firstorder. + unfold relation_equivalence in *. compute; firstorder. Qed. Typeclasses Opaque arrows predicate_implication predicate_equivalence @@ -420,7 +423,7 @@ Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA (** Strict Order *) -Class StrictOrder {A : Type} (R : relation A) := { +Class StrictOrder {A : Type} (R : relation A) : Prop := { StrictOrder_Irreflexive :> Irreflexive R ; StrictOrder_Transitive :> Transitive R }. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 7972c96c..2b010206 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -15,27 +15,25 @@ Require Import Relations Morphisms. fix the simpl tactic, since "simpl fst" would be refused for the moment. -Implicit Arguments fst [[A] [B]]. -Implicit Arguments snd [[A] [B]]. -Implicit Arguments pair [[A] [B]]. +Arguments fst {A B}. +Arguments snd {A B}. +Arguments pair {A B}. /NB *) Local Notation Fst := (@fst _ _). Local Notation Snd := (@snd _ _). -Arguments Scope relation_conjunction - [type_scope signature_scope signature_scope]. -Arguments Scope relation_equivalence - [type_scope signature_scope signature_scope]. -Arguments Scope subrelation [type_scope signature_scope signature_scope]. -Arguments Scope Reflexive [type_scope signature_scope]. -Arguments Scope Irreflexive [type_scope signature_scope]. -Arguments Scope Symmetric [type_scope signature_scope]. -Arguments Scope Transitive [type_scope signature_scope]. -Arguments Scope PER [type_scope signature_scope]. -Arguments Scope Equivalence [type_scope signature_scope]. -Arguments Scope StrictOrder [type_scope signature_scope]. +Arguments relation_conjunction A%type (R R')%signature _ _. +Arguments relation_equivalence A%type (_ _)%signature. +Arguments subrelation A%type (R R')%signature. +Arguments Reflexive A%type R%signature. +Arguments Irreflexive A%type R%signature. +Arguments Symmetric A%type R%signature. +Arguments Transitive A%type R%signature. +Arguments PER A%type R%signature. +Arguments Equivalence A%type R%signature. +Arguments StrictOrder A%type R%signature. Generalizable Variables A B RA RB Ri Ro f. @@ -88,10 +86,10 @@ Section RelCompFun_Instances. `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f). Proof. firstorder. Qed. - Global Instance RelCompFun_Equivalence + Global Program Instance RelCompFun_Equivalence `(Measure A B f, Equivalence _ R) : Equivalence (R@@f). - Global Instance RelCompFun_StrictOrder + Global Program Instance RelCompFun_StrictOrder `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f). End RelCompFun_Instances. @@ -108,7 +106,7 @@ Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). Proof. firstorder. Qed. -Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) +Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). Lemma FstRel_ProdRel {A B}(RA:relation A) : diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index e9da6874..591671d9 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: SetoidClass.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Set Implicit Arguments. Unset Strict Implicit. @@ -71,7 +69,7 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) Ltac clsubst H := - match type of H with + lazymatch type of H with ?x == ?y => substitute H ; clear H x end. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 4f70b244..6708220e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,16 +13,11 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: SetoidDec.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Set Implicit Arguments. Unset Strict Implicit. Generalizable Variables A B . -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - (** Export notations. *) Require Export Coq.Classes.SetoidClass. @@ -95,7 +90,7 @@ Program Instance bool_eqdec : EqDec (eq_setoid bool) := bool_dec. Program Instance unit_eqdec : EqDec (eq_setoid unit) := - λ x y, in_left. + fun x y => in_left. Next Obligation. Proof. @@ -103,8 +98,9 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := reflexivity. Qed. -Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) := - λ x y, +Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) + : EqDec (eq_setoid (prod A B)) := + fun x y => let '(x1, x2) := x in let '(y1, y2) := y in if x1 == y1 then @@ -117,8 +113,9 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq (** Objects of function spaces with countable domains like bool have decidable equality. *) -Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := - λ f g, +Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) + : EqDec (eq_setoid (bool -> A)) := + fun f g => if f true == g true then if f false == g false then in_left else in_right diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index a1a0c969..31a4f5f2 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: SetoidTactics.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. |