From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 4 Jul 2009 13:28:35 +0200 Subject: Imported Upstream version 8.2.pl1+dfsg --- theories/Classes/EquivDec.v | 15 +++++----- theories/Classes/Equivalence.v | 8 ++--- theories/Classes/Init.v | 11 ++----- theories/Classes/Morphisms.v | 50 +++++++++++-------------------- theories/Classes/Morphisms_Relations.v | 1 + theories/Classes/RelationClasses.v | 9 +++--- theories/Classes/SetoidAxioms.v | 4 +-- theories/Classes/SetoidClass.v | 4 +-- theories/Classes/SetoidTactics.v | 12 ++++---- theories/FSets/FMapFacts.v | 4 +-- theories/FSets/FSetFacts.v | 10 +++---- theories/Logic/ConstructiveEpsilon.v | 6 ++-- theories/Logic/FunctionalExtensionality.v | 2 -- theories/Program/Equality.v | 10 +++++-- theories/Program/Wf.v | 12 ++++---- theories/Setoids/Setoid.v | 4 ++- 16 files changed, 73 insertions(+), 89 deletions(-) (limited to 'theories') diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 157217ae..15cabf81 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -12,9 +12,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud * 91405 Orsay, France *) -(* $Id: EquivDec.v 11800 2009-01-18 18:34:15Z msozeau $ *) - -Set Manual Implicit Arguments. +(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *) (** Export notations. *) @@ -144,9 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := | _, _ => 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. - Proof. clear aux. red in H0. subst. - destruct y; intuition (discriminate || eauto). - Defined. + Next Obligation. destruct x ; destruct y ; intuition eauto. Defined. + + Solve Obligations using unfold equiv, complement in *; program_simpl; + intuition (discriminate || eauto). diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5e5895ab..7068bc6b 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -12,15 +12,15 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *) +(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *) -Require Export Coq.Program.Basics. +Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Classes.Init. Require Import Relation_Definitions. -Require Import Coq.Classes.RelationClasses. -Require Export Coq.Classes.Morphisms. +Require Export Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 5df7a4ed..762cc5c1 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -13,12 +13,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) -(* $Id: Init.v 11709 2008-12-20 11:42:15Z msozeau $ *) - -(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *) - -Tactic Notation "clapply" ident(c) := - eapply @c ; typeclasses eauto. +(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *) (** Hints for the proof search: these combinators should be considered rigid. *) @@ -29,12 +24,12 @@ Typeclasses Opaque id const flip compose arrow impl iff. (** The unconvertible typeclass, to test that two objects of the same type are actually different. *) -Class Unconvertible (A : Type) (a b : A). +Class Unconvertible (A : Type) (a b : A) := unconvertible : unit. Ltac unconvertible := match goal with | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible" - | |- _ => eapply Build_Unconvertible + | |- _ => exact tt end. Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances. \ No newline at end of file diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 86097a56..2b653e27 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* R' " := (@respectful _ _ (R%signature) (R'%signature)) - (right associativity, at level 55) : signature_scope. +Module MorphismNotations. -Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) - (right associativity, at level 55) : signature_scope. + Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) + (right associativity, at level 55) : signature_scope. -Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) - (right associativity, at level 55) : signature_scope. +End MorphismNotations. -Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. +Export MorphismNotations. Open Local Scope signature_scope. @@ -118,7 +121,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. (** And of course it is reflexive. *) -Instance morphisms_subrelation_refl : ! subrelation A R R | 10. +Instance morphisms_subrelation_refl : ! subrelation A R R. Proof. simpl_relation. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) @@ -151,10 +154,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) -Instance iff_impl_subrelation : subrelation iff impl. +Instance iff_impl_subrelation : subrelation iff impl | 2. Proof. firstorder. Qed. -Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). +Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2. Proof. firstorder. Qed. Instance pointwise_subrelation {A} `(sub : subrelation B R R') : @@ -372,25 +375,6 @@ Ltac partial_application_tactic := end end. -Section PartialAppTest. - Instance and_ar : Params and 0. - - Goal Morphism (iff) (and True True). - partial_application_tactic. - Admitted. - - Goal Morphism (iff) (or True True). - partial_application_tactic. - partial_application_tactic. - Admitted. - - Goal Morphism (iff ==> iff) (iff True). - partial_application_tactic. - (*partial_application_tactic. *) - Admitted. - -End PartialAppTest. - Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 24b8d636..4654e654 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -12,6 +12,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) +Require Import Relation_Definitions. Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Program. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index f95894be..e1de9ee9 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -13,12 +13,12 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) -(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. -Require Export Coq.Relations.Relation_Definitions. +Require Import Coq.Relations.Relation_Definitions. (** We allow to unfold the [relation] definition while doing morphism search. *) @@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q We give an equivalent definition, up-to an equivalence relation on the carrier. *) -Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := +Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). (** The equivalence proof is sufficient for proving that [R] must be a morphism @@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R. Proof with auto. - reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. + reduce_goal. + pose proof partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. Qed. diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index 305168ec..03bb9a80 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -12,7 +12,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud * 91405 Orsay, France *) -(* $Id: SetoidAxioms.v 11709 2008-12-20 11:42:15Z msozeau $ *) +(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *) Require Import Coq.Program.Program. @@ -22,7 +22,7 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. (* Application of the extensionality axiom to turn a goal on - Leibinz equality to a setoid equivalence (use with care!). *) + Leibniz equality to a setoid equivalence (use with care!). *) Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 47f92ada..d3da7d5a 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -12,14 +12,14 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: SetoidClass.v 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. Require Import Coq.Program.Program. -Require Import Coq.Classes.Init. +Require Import Relation_Definitions. Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. Require Import Coq.Classes.Functions. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index caacc9ec..36f05e31 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -13,13 +13,13 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: SetoidTactics.v 11709 2008-12-20 11:42:15Z msozeau $ *) +(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *) -Require Export Coq.Classes.RelationClasses. -Require Export Coq.Classes.Morphisms. -Require Export Coq.Classes.Morphisms_Prop. -Require Export Coq.Classes.Equivalence. -Require Export Coq.Relations.Relation_Definitions. +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. + +Export MorphismNotations. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index df12166e..d91eb87a 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *) +(* $Id: FMapFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *) (** * Finite maps library *) @@ -15,7 +15,7 @@ different styles: equivalence and boolean equalities. *) -Require Import Bool DecidableType DecidableTypeEx OrderedType. +Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms. Require Export FMapInterface. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 1e15d3a1..674caaac 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *) +(* $Id: FSetFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *) (** * Finite sets library *) @@ -17,7 +17,7 @@ *) Require Import DecidableTypeEx. -Require Export FSetInterface. +Require Export FSetInterface. Set Implicit Arguments. Unset Strict Implicit. @@ -424,14 +424,14 @@ Add Relation t Subset transitivity proved by Subset_trans as SubsetSetoid. -Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1. +Instance In_s_m : Morphisms.Morphism (E.eq ==> Subset ++> Basics.impl) In | 1. Proof. simpl_relation. eauto with set. Qed. -Add Morphism Empty with signature Subset --> impl as Empty_s_m. +Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m. Proof. -unfold Subset, Empty, impl; firstorder. +unfold Subset, Empty, Basics.impl; firstorder. Qed. Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 3753b97b..ff70c9fb 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ConstructiveEpsilon.v 11238 2008-07-19 09:34:03Z herbelin $ i*) +(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*) (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a @@ -14,8 +14,8 @@ predicate from the regular existence (i.e., [Prop]-existence). One requires that the underlying set is countable and that the predicate is decidable. *) -(** Coq does not allow case analysis on sort [Set] when the goal is in -[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to +(** Coq does not allow case analysis on sort [Prop] when the goal is in +[Set]. Therefore, one cannot eliminate [exists n, P n] in order to show [{n : nat | P n}]. However, one can perform a recursion on an inductive predicate in sort [Prop] so that the returning type of the recursion is in [Set]. This trick is described in Coq'Art book, Sect. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 4445b0e1..0dc82907 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -11,8 +11,6 @@ (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) -Set Manual Implicit Arguments. - (** The converse of functional extensionality. *) Lemma equal_f : forall {A B : Type} {f g : A -> B}, diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 99d54755..9681d543 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*) +(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -479,8 +479,12 @@ Ltac intro_prototypes := | _ => idtac end. -Ltac do_case p := destruct p || elim_case p || (case p ; clear p). -Ltac do_ind p := induction p || elim_ind p. +Ltac introduce p := + first [ match p with _ => idtac end (* Already there *) + | intros until p | intros ]. + +Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)). +Ltac do_ind p := introduce p ; (induction p || elim_ind p). Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 12bdf3a7..2083e530 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *) +(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -165,7 +165,7 @@ Section Measure_well_founded. (* Measure relations are well-founded if the underlying relation is well-founded. *) - Variables T M: Set. + Variables T M: Type. Variable R: M -> M -> Prop. Hypothesis wf: well_founded R. Variable m: T -> M. @@ -191,7 +191,7 @@ End Measure_well_founded. Section Fix_measure_rects. - Variable A: Set. + Variable A: Type. Variable m: A -> nat. Variable P: A -> Type. Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x. @@ -287,7 +287,7 @@ Section Fix_measure_rects. End Fix_measure_rects. -(** Tactic to fold a definitions based on [Fix_measure_sub]. *) +(** Tactic to fold a definition based on [Fix_measure_sub]. *) Ltac fold_sub f := match goal with @@ -312,8 +312,8 @@ Module WfExtensionality. (** For a function defined with Program using a well-founded order. *) Program Lemma fix_sub_eq_ext : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) + forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Type) (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index e7fe82b2..a187a7c6 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -6,10 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Setoid.v 11720 2008-12-28 07:12:15Z letouzey $: i*) +(*i $Id: Setoid.v 12187 2009-06-13 19:36:59Z msozeau $: i*) Require Export Coq.Classes.SetoidTactics. +Export Morphisms.MorphismNotations. + (** For backward compatibility *) Definition Setoid_Theory := @Equivalence. -- cgit v1.2.3