diff options
Diffstat (limited to 'theories')
75 files changed, 2260 insertions, 919 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index a90a9ce996..76132aed03 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -201,7 +201,7 @@ Qed. Lemma nat_compare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y). Proof. - intros. + intros. destruct (nat_compare x y) eqn:?; constructor. apply nat_compare_eq; auto. apply <- nat_compare_lt; auto. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 1febb76b66..c3386787dd 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -54,7 +54,7 @@ Hint Resolve le_0_n le_Sn_0: arith v62. Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n. Proof. - induction n; auto with arith. + induction n. auto with arith. idtac. auto with arith. intro; contradiction le_Sn_0 with n. Qed. Hint Immediate le_n_0_eq: arith v62. diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v new file mode 100644 index 0000000000..68a6dcd632 --- /dev/null +++ b/theories/Classes/CEquivalence.v @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Typeclass-based setoids. Definitions on [Equivalence]. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. + +Require Import Coq.Classes.Init. +Require Import Relation_Definitions. +Require Export Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. + +Set Implicit Arguments. +Unset Strict Implicit. + +Generalizable Variables A R eqA B S eqB. +Local Obligation Tactic := try solve [simpl_crelation]. + +Local Open Scope signature_scope. + +Definition equiv `{Equivalence A R} : crelation A := R. + +(** Overloaded notations for setoid equivalence and inequivalence. + Not to be confused with [eq] and [=]. *) + +Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. + +Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. + +Local Open Scope equiv_scope. + +(** Overloading for [PER]. *) + +Definition pequiv `{PER A R} : crelation A := R. + +(** Overloaded notation for partial equivalence. *) + +Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. + +(** Shortcuts to make proof search easier. *) + +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. + +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. + +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. + + Next Obligation. + Proof. intros A R sa x y z Hxy Hyz. + now transitivity y. + Qed. + +(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) + +Ltac setoid_subst H := + match type of H with + ?x === ?y => substitute H ; clear H x + end. + +Ltac setoid_subst_nofail := + match goal with + | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail + | _ => idtac + end. + +(** [subst*] will try its best at substituting every equality in the goal. *) + +Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail. + +(** Simplify the goal w.r.t. equivalence. *) + +Ltac equiv_simplify_one := + match goal with + | [ H : ?x === ?x |- _ ] => clear H + | [ H : ?x === ?y |- _ ] => setoid_subst H + | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name + | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name + end. + +Ltac equiv_simplify := repeat equiv_simplify_one. + +(** "reify" relations which are equivalences to applications of the overloaded [equiv] method + for easy recognition in tactics. *) + +Ltac equivify_tac := + match goal with + | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H + | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y) + end. + +Ltac equivify := repeat equivify_tac. + +Section Respecting. + + (** Here we build an equivalence instance for functions which relates respectful ones only, + we do not export it. *) + + Definition respecting `(eqa : Equivalence A (R : crelation A), + eqb : Equivalence B (R' : crelation B)) : Type := + { morph : A -> B | respectful R R' morph morph }. + + Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') : + Equivalence (fun (f g : respecting eqa eqb) => + forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). + + Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl. + + Next Obligation. + Proof. + intros. intros f g h H H' x y Rxy. + unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder. + Qed. + +End Respecting. + +(** The default equivalence on function spaces, with higher-priority than [eq]. *) + +Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : + Reflexive (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) : + Symmetric (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_transitive {A} `(transb : Transitive B eqB) : + Transitive (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) : + Equivalence (pointwise_relation A eqB) | 9. +Proof. split; apply _. Qed. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v new file mode 100644 index 0000000000..5737c88b5e --- /dev/null +++ b/theories/Classes/CMorphisms.v @@ -0,0 +1,799 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Typeclass-based morphism definition and standard, minimal instances + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. +Require Export Coq.Classes.RelationClasses. + +Generalizable Variables A eqA B C D R RA RB RC m f x y. +Local Obligation Tactic := simpl_crelation. + +Set Universe Polymorphism. + +(** * Morphisms. + + We now turn to the definition of [Proper] and declare standard instances. + These will be used by the [setoid_rewrite] tactic later. *) + +(** A morphism for a relation [R] is a proper element of the relation. + The relation [R] will be instantiated by [respectful] and [A] by an arrow + type for usual morphisms. *) +Section Proper. + Let U := Type. + Context {A B : U}. + + Class Proper (R : crelation A) (m : A) := + proper_prf : R m m. + + (** Every element in the carrier of a reflexive relation is a morphism + for this relation. We use a proxy class for this case which is used + internally to discharge reflexivity constraints. The [Reflexive] + instance will almost always be used, but it won't apply in general to + any kind of [Proper (A -> B) _ _] goal, making proof-search much + slower. A cleaner solution would be to be able to set different + priorities in different hint bases and select a particular hint + database for resolution of a type class constraint. *) + + Class ProperProxy (R : crelation A) (m : A) := + proper_proxy : R m m. + + Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x. + Proof. firstorder. Qed. + + Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. + Proof. firstorder. Qed. + + Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x. + Proof. firstorder. Qed. + + (** Respectful morphisms. *) + + (** The fully dependent version, not used yet. *) + + Definition respectful_hetero + (A B : Type) + (C : A -> Type) (D : B -> Type) + (R : A -> B -> Type) + (R' : forall (x : A) (y : B), C x -> D y -> Type) : + (forall x : A, C x) -> (forall x : B, D x) -> Type := + fun f g => forall x y, R x y -> R' x y (f x) (g y). + + (** The non-dependent version is an instance where we forget dependencies. *) + + Definition respectful (R : crelation A) (R' : crelation B) : crelation (A -> B) := + Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). + +End Proper. + +(** We favor the use of Leibniz equality or a declared reflexive crelation + when resolving [ProperProxy], otherwise, if the crelation is given (not an evar), + we fall back to [Proper]. *) +Hint Extern 1 (ProperProxy _ _) => + class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. + +Hint Extern 2 (ProperProxy ?R _) => + not_evar R; class_apply @proper_proper_proxy : typeclass_instances. + +(** Notations reminiscent of the old syntax for declaring morphisms. *) +Delimit Scope signature_scope with signature. + +Module ProperNotations. + + 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 _ _ (flip (R%signature)) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +End ProperNotations. + +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. + +Export ProperNotations. + +Local Open 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 : crelation 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' => + solve [change (Proper R f); eauto with typeclass_instances | reflexivity ] + | _ => idtac + end. + +Section Relations. + Let U := Type. + Context {A B : U}. + + (** [forall_def] reifies the dependent product as a definition. *) + + Definition forall_def (P : A -> U) : Type := forall x : A, P x. + + (** Dependent pointwise lifting of a crelation on the range. *) + + Definition forall_relation (P : A -> U) + (sig : forall a, crelation (P a)) : crelation (forall x, P x) := + fun f g => forall a, sig a (f a) (g a). + + (** Non-dependent pointwise lifting *) + Definition pointwise_relation (R : crelation B) : crelation (A -> B) := + fun f g => forall a, R (f a) (g a). + + Lemma pointwise_pointwise (R : crelation B) : + relation_equivalence (pointwise_relation R) (@eq A ==> R). + Proof. intros. split. simpl_crelation. firstorder. Qed. + + (** Subcrelations induce a morphism on the identity. *) + + Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id. + Proof. firstorder. Qed. + + (** The subrelation property goes through products as usual. *) + + Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') : + subrelation (RA ==> RB) (RA' ==> RB'). + Proof. simpl_crelation. Qed. + + (** And of course it is reflexive. *) + + Lemma subrelation_refl R : @subrelation A R R. + Proof. simpl_crelation. Qed. + + (** [Proper] is itself a covariant morphism for [subrelation]. + We use an unconvertible premise to avoid looping. + *) + + Lemma subrelation_proper `(mor : Proper A R' m) + `(unc : Unconvertible (crelation A) R R') + `(sub : subrelation A R' R) : Proper R m. + Proof. + intros. apply sub. apply mor. + Qed. + + Global Instance proper_subrelation_proper : + Proper (subrelation ++> eq ==> impl) (@Proper A). + Proof. reduce. subst. firstorder. Qed. + + Global Instance proper_subrelation_proper_arrow : + Proper (subrelation ++> eq ==> arrow) (@Proper A). + Proof. reduce. subst. firstorder. Qed. + + Global Instance pointwise_subrelation `(sub : subrelation B R R') : + subrelation (pointwise_relation R) (pointwise_relation R') | 4. + Proof. reduce. unfold pointwise_relation in *. apply sub. auto. Qed. + + (** For dependent function types. *) + Lemma forall_subrelation (P : A -> U) (R S : forall x : A, crelation (P x)) : + (forall a, subrelation (R a) (S a)) -> + subrelation (forall_relation P R) (forall_relation P S). + Proof. reduce. firstorder. Qed. +End Relations. + +Typeclasses Opaque respectful pointwise_relation forall_relation. +Arguments forall_relation {A P}%type sig%signature _ _. +Arguments pointwise_relation A%type {B}%type R%signature _ _. + +Hint Unfold Reflexive : core. +Hint Unfold Symmetric : core. +Hint Unfold Transitive : core. + +(** Resolution with subrelation: favor decomposing products over applying reflexivity + for unconstrained goals. *) +Ltac subrelation_tac T U := + (is_ground T ; is_ground U ; class_apply @subrelation_refl) || + class_apply @subrelation_respectful || class_apply @subrelation_refl. + +Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. + +CoInductive apply_subrelation : Prop := do_subrelation. + +Ltac proper_subrelation := + match goal with + [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper + end. + +Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. + +(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) + +Instance iff_impl_subrelation : subrelation iff impl | 2. +Proof. firstorder. Qed. + +Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2. +Proof. firstorder. Qed. + +(** Essential subrelation instances for [iffT] and [arrow]. *) + +Instance iffT_arrow_subrelation : subrelation iffT arrow | 2. +Proof. firstorder. Qed. + +Instance iffT_flip_arrow_subrelation : subrelation iffT (flip arrow) | 2. +Proof. firstorder. Qed. + +(** We use an extern hint to help unification. *) + +Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => + apply (@forall_subrelation A B R S) ; intro : typeclass_instances. + +Section GenericInstances. + (* Share universes *) + Let U := Type. + Context {A B C : U}. + + (** We can build a PER on the Coq function space if we have PERs on the domain and + codomain. *) + + Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). + + Next Obligation. + Proof with auto. + assert(R x0 x0). + transitivity y0... symmetry... + transitivity (y x0)... + Qed. + + (** The complement of a crelation conserves its proper elements. *) + + Program Definition complement_proper + `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : + Proper (RA ==> RA ==> iff) (complement R) := _. + + Next Obligation. + Proof. + unfold complement. + pose (mR x y X x0 y0 X0). + intuition. + Qed. + + (** The [flip] too, actually the [flip] instance is a bit more general. *) + + Program Definition flip_proper + `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : + Proper (RB ==> RA ==> RC) (flip f) := _. + + Next Obligation. + Proof. + apply mor ; auto. + Qed. + + + (** Every Transitive crelation gives rise to a binary morphism on [impl], + contravariant in the first argument, covariant in the second. *) + + Global Program + Instance trans_contra_co_morphism + `(Transitive A R) : Proper (R --> R ++> impl) R. + + Next Obligation. + Proof with auto. + transitivity x... + transitivity x0... + Qed. + + Global Program + Instance trans_contra_co_type_morphism + `(Transitive A R) : Proper (R --> R ++> arrow) R. + + Next Obligation. + Proof with auto. + transitivity x... + transitivity x0... + Qed. + + (** Proper declarations for partial applications. *) + + Global Program + Instance trans_contra_inv_impl_morphism + `(Transitive A R) : Proper (R --> flip impl) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + + Global Program + Instance trans_contra_inv_impl_type_morphism + `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + + Global Program + Instance trans_co_impl_morphism + `(Transitive A R) : Proper (R ++> impl) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity x0... + Qed. + + Global Program + Instance trans_co_impl_type_morphism + `(Transitive A R) : Proper (R ++> arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity x0... + Qed. + + Global Program + Instance trans_sym_co_inv_impl_morphism + `(PER A R) : Proper (R ++> flip impl) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity y... symmetry... + Qed. + + Global Program + Instance trans_sym_co_inv_impl_type_morphism + `(PER A R) : Proper (R ++> flip arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity y... symmetry... + Qed. + + Global Program Instance trans_sym_contra_impl_morphism + `(PER A R) : Proper (R --> impl) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity x0... symmetry... + Qed. + + Global Program Instance trans_sym_contra_arrow_morphism + `(PER A R) : Proper (R --> arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity x0... symmetry... + Qed. + + Global Program Instance per_partial_app_morphism + `(PER A R) : Proper (R ==> iff) (R x) | 2. + + Next Obligation. + Proof with auto. + split. intros ; transitivity x0... + intros. + transitivity y... + symmetry... + Qed. + + Global Program Instance per_partial_app_type_morphism + `(PER A R) : Proper (R ==> iffT) (R x) | 2. + + Next Obligation. + Proof with auto. + split. intros ; transitivity x0... + intros. + transitivity y... + symmetry... + Qed. + + (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) + + Global Program + Instance trans_co_eq_inv_impl_morphism + `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + + Global Program + Instance trans_co_eq_inv_arrow_morphism + `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + + (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *) + + Global Program + Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. + + Next Obligation. + Proof with auto. + split ; intros. + transitivity x0... transitivity x... symmetry... + + transitivity y... transitivity y0... symmetry... + Qed. + + (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *) + + Global Program + Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1. + + Next Obligation. + Proof with auto. + split ; intros. + transitivity x0... transitivity x... symmetry... + + transitivity y... transitivity y0... symmetry... + Qed. + + Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). + Proof. firstorder. Qed. + + Global Program Instance compose_proper RA RB RC : + Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C). + + Next Obligation. + Proof. + simpl_crelation. + unfold compose. firstorder. + Qed. + + (** Coq functions are morphisms for Leibniz equality, + applied only if really needed. *) + + Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') : + Reflexive (@Logic.eq A ==> R'). + Proof. simpl_crelation. Qed. + + (** [respectful] is a morphism for crelation equivalence. *) + + Global Instance respectful_morphism : + Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) + (@respectful A B). + Proof. + intros R R' HRR' S S' HSS' f g. + unfold respectful, relation_equivalence in * ; simpl in *. + split ; intros H x y Hxy. + setoid_rewrite <- HSS'. apply H. now rewrite HRR'. + rewrite HSS'. apply H. now rewrite <- HRR'. + Qed. + + (** [R] is Reflexive, hence we can build the needed proof. *) + + Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : + Proper R' (m x). + Proof. simpl_crelation. Qed. + + Class Params (of : A) (arity : nat). + + Lemma flip_respectful (R : crelation A) (R' : crelation B) : + relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). + Proof. + intros. + unfold flip, respectful. + split ; intros ; intuition. + Qed. + + + (** Treating flip: can't make them direct instances as we + need at least a [flip] present in the goal. *) + + Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R. + Proof. firstorder. Qed. + + Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')). + Proof. firstorder. Qed. + + (** That's if and only if *) + + Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. + Proof. simpl_crelation. Qed. + + (** Once we have normalized, we will apply this instance to simplify the problem. *) + + Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor. + + (** Every reflexive crelation gives rise to a morphism, + only for immediately solving goals without variables. *) + + Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x. + Proof. firstorder. Qed. + + Lemma proper_eq (x : A) : Proper (@eq A) x. + Proof. intros. apply reflexive_proper. Qed. + +End GenericInstances. + +Class PartialApplication. + +CoInductive normalization_done : Prop := did_normalization. + +Ltac partial_application_tactic := + let rec do_partial_apps H m cont := + match m with + | ?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 := + match ar with + | 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 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 + | [ H : PartialApplication |- _ ] => + class_apply @Reflexive_partial_app_morphism; [|clear H] + | _ => on_morphism (m x) + ltac:(class_apply @Reflexive_partial_app_morphism) + end + end. + +(** Bootstrap !!! *) + +Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A). +Proof. + intros A R R' HRR' x y <-. red in HRR'. + split ; red ; intros. + now setoid_rewrite <- HRR'. + now setoid_rewrite HRR'. +Qed. + +Ltac proper_reflexive := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | _ => class_apply proper_eq || class_apply @reflexive_proper + end. + + +Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. +Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. + +Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper + : typeclass_instances. +Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper + : typeclass_instances. +Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper + : typeclass_instances. +Hint Extern 4 (@Proper _ _ _) => partial_application_tactic + : typeclass_instances. +Hint Extern 7 (@Proper _ _ _) => proper_reflexive + : typeclass_instances. + +(** Special-purpose class to do normalization of signatures w.r.t. flip. *) + +Section Normalize. + Context (A : Type). + + Class Normalizes (m : crelation A) (m' : crelation A) : Prop := + normalizes : relation_equivalence m m'. + + (** Current strategy: add [flip] everywhere and reduce using [subrelation] + afterwards. *) + + Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. + Proof. + red in H, H0. red in H. + setoid_rewrite H. + assumption. + Qed. + + Lemma flip_atom R : Normalizes R (flip (flip R)). + Proof. + firstorder. + Qed. + +End Normalize. + +Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : + Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature). +Proof. + unfold Normalizes in *. intros. + rewrite NA, NB. firstorder. +Qed. + +Ltac normalizes := + match goal with + | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow + | _ => class_apply @flip_atom + end. + +Ltac proper_normalization := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : apply_subrelation |- @Proper _ ?R _ ] => + let H := fresh "H" in + set(H:=did_normalization) ; class_apply @proper_normalizes_proper + end. + +Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances. +Hint Extern 6 (@Proper _ _ _) => proper_normalization + : typeclass_instances. + +(** When the crelation on the domain is symmetric, we can + flip the crelation on the codomain. Same for binary functions. *) + +Lemma proper_sym_flip : + forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), + Proper (R1==>flip R2) f. +Proof. +intros A R1 Sym B R2 f Hf. +intros x x' Hxx'. apply Hf, Sym, Hxx'. +Qed. + +Lemma proper_sym_flip_2 : + forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), + Proper (R1==>R2==>flip R3) f. +Proof. +intros A R1 Sym1 B R2 Sym2 C R3 f Hf. +intros x x' Hxx' y y' Hyy'. apply Hf; auto. +Qed. + +(** When the crelation on the domain is symmetric, a predicate is + compatible with [iff] as soon as it is compatible with [impl]. + Same with a binary crelation. *) + +Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f), + Proper (R==>iff) f. +Proof. +intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_arrow_iffT : forall `(Symmetric A R)`(Proper _ (R==>arrow) f), + Proper (R==>iffT) f. +Proof. +intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_impl_iff_2 : + forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f), + Proper (R==>R'==>iff) f. +Proof. +intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. +repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_arrow_iffT_2 : + forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>arrow) f), + Proper (R==>R'==>iffT) f. +Proof. +intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. +repeat red in Hf. split; eauto. +Qed. + +(** A [PartialOrder] is compatible with its underlying equivalence. *) +Require Import Relation_Definitions. +Instance PartialOrder_proper `(PartialOrder A eqA (R : relation A)) : + Proper (eqA==>eqA==>iff) R. +Proof. +intros. +apply proper_sym_impl_iff_2; auto with *. +intros x x' Hx y y' Hy Hr. +transitivity x. +generalize (partial_order_equivalence x x'); compute; intuition. +transitivity y; auto. +generalize (partial_order_equivalence y y'); compute; intuition. +Qed. + +Instance PartialOrder_proper_type `(PartialOrder A eqA R) : + Proper (eqA==>eqA==>iffT) R. +Proof. +intros. +apply proper_sym_arrow_iffT_2; auto with *. +intros x x' Hx y y' Hy Hr. +transitivity x. +generalize (partial_order_equivalence x x'); compute; intuition. +transitivity y; auto. +generalize (partial_order_equivalence y y'); compute; intuition. +Qed. + +(** From a [PartialOrder] to the corresponding [StrictOrder]: + [lt = le /\ ~eq]. + If the order is total, we could also say [gt = ~le]. *) + +Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : + StrictOrder (relation_conjunction R (complement eqA)). +Proof. +split; compute. +intros x (_,Hx). apply Hx, Equivalence_Reflexive. +intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. +apply PreOrder_Transitive with y; assumption. +intro Hxz. +apply Hxy'. +apply partial_order_antisym; auto. +rewrite Hxz. auto. +Qed. + +(** From a [StrictOrder] to the corresponding [PartialOrder]: + [le = lt \/ eq]. + If the order is total, we could also say [ge = ~lt]. *) + +Lemma StrictOrder_PreOrder + `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) : + PreOrder (relation_disjunction R eqA). +Proof. +split. +intros x. right. reflexivity. +intros x y z [Hxy|Hxy] [Hyz|Hyz]. +left. transitivity y; auto. +left. rewrite <- Hyz; auto. +left. rewrite Hxy; auto. +right. transitivity y; auto. +Qed. + +Hint Extern 4 (PreOrder (relation_disjunction _ _)) => + class_apply StrictOrder_PreOrder : typeclass_instances. + +Lemma StrictOrder_PartialOrder + `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) : + PartialOrder eqA (relation_disjunction R eqA). +Proof. +intros. intros x y. compute. intuition. +elim (StrictOrder_Irreflexive x). +transitivity y; auto. +Qed. + +Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => + class_apply PartialOrder_StrictOrder : typeclass_instances. + +Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => + class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v new file mode 100644 index 0000000000..ca38ac5b43 --- /dev/null +++ b/theories/Classes/CRelationClasses.v @@ -0,0 +1,354 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \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 + + This is the basic theory needed to formalize morphisms and setoids. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +Require Export Coq.Classes.Init. +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. + +Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. + +Set Universe Polymorphism. + +Definition crelation (A : Type) := A -> A -> Type. + +Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type. + +(** We allow to unfold the [crelation] definition while doing morphism search. *) + +Section Defs. + Context {A : Type}. + + (** We rebind crelational properties in separate classes to be able to overload each proof. *) + + Class Reflexive (R : crelation A) := + reflexivity : forall x : A, R x x. + + Definition complement (R : crelation A) : crelation A := + fun x y => R x y -> False. + + (** Opaque for proof-search. *) + Typeclasses Opaque complement iffT. + + (** These are convertible. *) + Lemma complement_inverse R : complement (flip R) = flip (complement R). + Proof. reflexivity. Qed. + + Class Irreflexive (R : crelation A) := + irreflexivity : Reflexive (complement R). + + Class Symmetric (R : crelation A) := + symmetry : forall {x y}, R x y -> R y x. + + Class Asymmetric (R : crelation A) := + asymmetry : forall {x y}, R x y -> (complement R y x : Type). + + Class Transitive (R : crelation A) := + transitivity : forall {x y z}, R x y -> R y z -> R x z. + + (** Various combinations of reflexivity, symmetry and transitivity. *) + + (** A [PreOrder] is both Reflexive and Transitive. *) + + Class PreOrder (R : crelation A) := { + PreOrder_Reflexive :> Reflexive R | 2 ; + PreOrder_Transitive :> Transitive R | 2 }. + + (** A [StrictOrder] is both Irreflexive and Transitive. *) + + Class StrictOrder (R : crelation A) := { + StrictOrder_Irreflexive :> Irreflexive R ; + StrictOrder_Transitive :> Transitive R }. + + (** By definition, a strict order is also asymmetric *) + Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R. + Proof. firstorder. Qed. + + (** A partial equivalence crelation is Symmetric and Transitive. *) + + Class PER (R : crelation A) := { + PER_Symmetric :> Symmetric R | 3 ; + PER_Transitive :> Transitive R | 3 }. + + (** Equivalence crelations. *) + + Class Equivalence (R : crelation A) := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. + + (** An Equivalence is a PER plus reflexivity. *) + + Global Instance Equivalence_PER {R} `(Equivalence R) : PER R | 10 := + { PER_Symmetric := Equivalence_Symmetric ; + PER_Transitive := Equivalence_Transitive }. + + (** We can now define antisymmetry w.r.t. an equivalence crelation on the carrier. *) + + Class Antisymmetric eqA `{equ : Equivalence eqA} (R : crelation A) := + antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. + + Class subrelation (R R' : crelation A) := + is_subrelation : forall {x y}, R x y -> R' x y. + + (** Any symmetric crelation is equal to its inverse. *) + + Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R. + Proof. hnf. intros x y H'. red in H'. apply symmetry. assumption. Qed. + + Section flip. + + Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R). + Proof. tauto. Qed. + + Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) := + irreflexivity (R:=R). + + Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) := + fun x y H => symmetry (R:=R) H. + + Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) := + fun x y H H' => asymmetry (R:=R) H H'. + + Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) := + fun x y z H H' => transitivity (R:=R) H' H. + + Program Definition flip_Antisymmetric `(Antisymmetric eqA R) : + Antisymmetric eqA (flip R). + Proof. firstorder. Qed. + + (** Inversing the larger structures *) + + Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_PER `(PER R) : PER (flip R). + Proof. firstorder. Qed. + + Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R). + Proof. firstorder. Qed. + + End flip. + + Section complement. + + Definition complement_Irreflexive `(Reflexive R) + : Irreflexive (complement R). + Proof. firstorder. Qed. + + Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R). + Proof. firstorder. Qed. + End complement. + + + (** Rewrite crelation on a given support: declares a crelation as a rewrite + crelation for use by the generalized rewriting tactic. + It helps choosing if a rewrite should be handled + by the generalized or the regular rewriting tactic using leibniz equality. + Users can declare an [RewriteRelation A RA] anywhere to declare default + crelations. This is also done automatically by the [Declare Relation A RA] + commands. *) + + Class RewriteRelation (RA : crelation A). + + (** Any [Equivalence] declared in the context is automatically considered + a rewrite crelation. *) + + Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA. + + (** Leibniz equality. *) + Section Leibniz. + Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A. + Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A. + Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A. + + (** Leibinz equality [eq] is an equivalence crelation. + The instance has low priority as it is always applicable + if only the type is constrained. *) + + Global Program Instance eq_equivalence : Equivalence (@eq A) | 10. + End Leibniz. + +End Defs. + +(** Default rewrite crelations handled by [setoid_rewrite]. *) +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. + +(** Hints to drive the typeclass resolution avoiding loops + due to the use of full unification. *) +Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. + +Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. + +Hint Extern 4 (subrelation (flip _) _) => + class_apply @subrelation_symmetric : typeclass_instances. + +Hint Resolve irreflexivity : ord. + +Unset Implicit Arguments. + +(** A HintDb for crelations. *) + +Ltac solve_crelation := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H + end. + +Hint Extern 4 => solve_crelation : crelations. + +(** We can already dualize all these properties. *) + +(** * Standard instances. *) + +Ltac reduce_hyp H := + match type of H with + | context [ _ <-> _ ] => fail 1 + | _ => red in H ; try reduce_hyp H + end. + +Ltac reduce_goal := + match goal with + | [ |- _ <-> _ ] => fail 1 + | _ => red ; intros ; try reduce_goal + end. + +Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid. + +Ltac reduce := reduce_goal. + +Tactic Notation "apply" "*" constr(t) := + first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) | + refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ]. + +Ltac simpl_crelation := + unfold flip, impl, arrow ; try reduce ; program_simpl ; + try ( solve [ dintuition ]). + +Local Obligation Tactic := simpl_crelation. + +(** Logical implication. *) + +Program Instance impl_Reflexive : Reflexive impl. +Program Instance impl_Transitive : Transitive impl. + +(** Logical equivalence. *) + +Instance iff_Reflexive : Reflexive iff := iff_refl. +Instance iff_Symmetric : Symmetric iff := iff_sym. +Instance iff_Transitive : Transitive iff := iff_trans. + +(** Logical equivalence [iff] is an equivalence crelation. *) + +Program Instance iff_equivalence : Equivalence iff. + +Program Instance arrow_Reflexive : Reflexive arrow. +Program Instance arrow_Transitive : Transitive arrow. + +Instance iffT_Reflexive : Reflexive iffT. +Proof. firstorder. Defined. +Instance iffT_Symmetric : Symmetric iffT. +Proof. firstorder. Defined. +Instance iffT_Transitive : Transitive iffT. +Proof. firstorder. Defined. + +(** We now develop a generalization of results on crelations for arbitrary predicates. + The resulting theory can be applied to homogeneous binary crelations but also to + arbitrary n-ary predicates. *) + +Local Open Scope list_scope. + +(** A compact representation of non-dependent arities, with the codomain singled-out. *) + +(** We define the various operations which define the algebra on binary crelations *) +Section Binary. + Context {A : Type}. + + Definition relation_equivalence : crelation (crelation A) := + fun R R' => forall x y, iffT (R x y) (R' x y). + + Global Instance: RewriteRelation relation_equivalence. + + Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A := + fun x y => prod (R x y) (R' x y). + + Definition relation_disjunction (R : crelation A) (R' : crelation A) : crelation A := + fun x y => sum (R x y) (R' x y). + + (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + + Set Automatic Introduction. + + Global Instance relation_equivalence_equivalence : + Equivalence relation_equivalence. + Proof. split; red; unfold relation_equivalence, iffT. firstorder. + firstorder. + intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. + Qed. + + Global Instance relation_implication_preorder : PreOrder (@subrelation A). + Proof. firstorder. Qed. + + (** *** Partial Order. + A partial order is a preorder which is additionally antisymmetric. + We give an equivalent definition, up-to an equivalence crelation + on the carrier. *) + + Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := + partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)). + + (** The equivalence proof is sufficient for proving that [R] must be a + morphism for equivalence (see Morphisms). It is also sufficient to + show that [R] is antisymmetric w.r.t. [eqA] *) + + Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Proof with auto. + reduce_goal. + apply H. firstorder. + Qed. + + Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). + Proof. firstorder. Qed. +End Binary. + +Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. + +(** The partial order defined by subrelation and crelation equivalence. *) + +Program Instance subrelation_partial_order : + ! PartialOrder (crelation A) relation_equivalence subrelation. + +Next Obligation. +Proof. + unfold relation_equivalence in *. compute; firstorder. +Qed. + +Typeclasses Opaque relation_equivalence. + + diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 6e6ba68a24..3b4ba786a4 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -44,7 +44,7 @@ Qed. (** The generic function that should be used to program, together with some useful tactics. *) -Definition decide P {H : Decidable P} := @Decidable_witness P H. +Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). Ltac _decide_ P H := let b := fresh "b" in diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 39d7cdaa01..dcaf057b01 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -56,6 +56,7 @@ Local Open Scope program_scope. Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y). + (** Overloaded notation for inequality. *) Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 233e97c195..db04fbe39c 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -24,7 +24,7 @@ Set Implicit Arguments. Unset Strict Implicit. Generalizable Variables A R eqA B S eqB. -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [simpl_relation]. Local Open Scope signature_scope. @@ -56,8 +56,8 @@ Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. Next Obligation. - Proof. - transitivity y ; auto. + Proof. intros A R sa x y z Hxy Hyz. + now transitivity y. Qed. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) @@ -116,8 +116,9 @@ Section Respecting. Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl. Next Obligation. - Proof. - unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity. + Proof. + intros. intros f g h H H' x y Rxy. + unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder. Qed. End Respecting. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 617ff19061..921f212338 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -18,7 +18,7 @@ Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. -Generalizable All Variables. +Generalizable Variables A eqA B C D R RA RB RC m f x y. Local Obligation Tactic := simpl_relation. (** * Morphisms. @@ -29,15 +29,39 @@ Local Obligation Tactic := simpl_relation. (** A morphism for a relation [R] is a proper element of the relation. The relation [R] will be instantiated by [respectful] and [A] by an arrow type for usual morphisms. *) - -Class Proper {A} (R : relation A) (m : A) : Prop := - proper_prf : R m m. - -(** Respectful morphisms. *) - -(** The fully dependent version, not used yet. *) - -Definition respectful_hetero +Section Proper. + Let U := Type. + Context {A B : U}. + + Class Proper (R : relation A) (m : A) : Prop := + proper_prf : R m m. + + (** Every element in the carrier of a reflexive relation is a morphism + for this relation. We use a proxy class for this case which is used + internally to discharge reflexivity constraints. The [Reflexive] + instance will almost always be used, but it won't apply in general to + any kind of [Proper (A -> B) _ _] goal, making proof-search much + slower. A cleaner solution would be to be able to set different + priorities in different hint bases and select a particular hint + database for resolution of a type class constraint. *) + + Class ProperProxy (R : relation A) (m : A) : Prop := + proper_proxy : R m m. + + Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x. + Proof. firstorder. Qed. + + Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. + Proof. firstorder. Qed. + + Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x. + Proof. firstorder. Qed. + + (** Respectful morphisms. *) + + (** The fully dependent version, not used yet. *) + + Definition respectful_hetero (A B : Type) (C : A -> Type) (D : B -> Type) (R : A -> B -> Prop) @@ -45,18 +69,24 @@ Definition respectful_hetero (forall x : A, C x) -> (forall x : B, D x) -> Prop := fun f g => forall x y, R x y -> R' x y (f x) (g y). -(** The non-dependent version is an instance where we forget dependencies. *) + (** The non-dependent version is an instance where we forget dependencies. *) + + Definition respectful (R : relation A) (R' : relation B) : relation (A -> B) := + Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). -Definition respectful {A B : Type} - (R : relation A) (R' : relation B) : relation (A -> B) := - Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). +End Proper. -(** Notations reminiscent of the old syntax for declaring morphisms. *) +(** We favor the use of Leibniz equality or a declared reflexive relation + when resolving [ProperProxy], otherwise, if the relation is given (not an evar), + we fall back to [Proper]. *) +Hint Extern 1 (ProperProxy _ _) => + class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. -Delimit Scope signature_scope with signature. +Hint Extern 2 (ProperProxy ?R _) => + not_evar R; class_apply @proper_proper_proxy : typeclass_instances. -Arguments Proper {A}%type R%signature m. -Arguments respectful {A B}%type (R R')%signature _ _. +(** Notations reminiscent of the old syntax for declaring morphisms. *) +Delimit Scope signature_scope with signature. Module ProperNotations. @@ -66,11 +96,14 @@ Module ProperNotations. Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) (right associativity, at level 55) : signature_scope. - Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) + Notation " R --> R' " := (@respectful _ _ (flip (R%signature)) (R'%signature)) (right associativity, at level 55) : signature_scope. End ProperNotations. +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. + Export ProperNotations. Local Open Scope signature_scope. @@ -106,80 +139,89 @@ Ltac f_equiv := 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 + solve [change (Proper R f); eauto with typeclass_instances | reflexivity ] | _ => 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 : forall a, relation (B a)) : relation (forall x, B x) := - fun f g => forall a, sig a (f a) (g a). - -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:=fun _ => B) (fun _ => R). +Section Relations. + Let U := Type. + Context {A B : U} (P : A -> U). + + (** [forall_def] reifies the dependent product as a definition. *) + + Definition forall_def : Type := forall x : A, P x. + + (** Dependent pointwise lifting of a relation on the range. *) + + Definition forall_relation + (sig : forall a, relation (P a)) : relation (forall x, P x) := + fun f g => forall a, sig a (f a) (g a). + + (** Non-dependent pointwise lifting *) + Definition pointwise_relation (R : relation B) : relation (A -> B) := + fun f g => forall a, R (f a) (g a). + + Lemma pointwise_pointwise (R : relation B) : + relation_equivalence (pointwise_relation R) (@eq A ==> R). + Proof. intros. split; reduce; subst; firstorder. Qed. + + (** Subrelations induce a morphism on the identity. *) + + Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id. + Proof. firstorder. Qed. + + (** The subrelation property goes through products as usual. *) + + Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') : + subrelation (RA ==> RB) (RA' ==> RB'). + Proof. unfold subrelation in *; firstorder. Qed. + + (** And of course it is reflexive. *) + + Lemma subrelation_refl R : @subrelation A R R. + Proof. unfold subrelation; firstorder. Qed. + + (** [Proper] is itself a covariant morphism for [subrelation]. + We use an unconvertible premise to avoid looping. + *) + + Lemma subrelation_proper `(mor : Proper A R' m) + `(unc : Unconvertible (relation A) R R') + `(sub : subrelation A R' R) : Proper R m. + Proof. + intros. apply sub. apply mor. + Qed. -Lemma pointwise_pointwise A B (R : relation B) : - relation_equivalence (pointwise_relation A R) (@eq A ==> R). -Proof. intros. split. simpl_relation. firstorder. Qed. + Global Instance proper_subrelation_proper : + Proper (subrelation ++> eq ==> impl) (@Proper A). + Proof. reduce. subst. firstorder. Qed. -(** We can build a PER on the Coq function space if we have PERs on the domain and - codomain. *) + Global Instance pointwise_subrelation `(sub : subrelation B R R') : + subrelation (pointwise_relation R) (pointwise_relation R') | 4. + Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. + + (** For dependent function types. *) + Lemma forall_subrelation (R S : forall x : A, relation (P x)) : + (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S). + Proof. reduce. apply H. apply H0. Qed. +End Relations. +Typeclasses Opaque respectful pointwise_relation forall_relation. +Arguments forall_relation {A P}%type sig%signature _ _. +Arguments pointwise_relation A%type {B}%type R%signature _ _. + Hint Unfold Reflexive : core. Hint Unfold Symmetric : core. Hint Unfold Transitive : core. -Typeclasses Opaque respectful pointwise_relation forall_relation. - -Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). - - Next Obligation. - Proof with auto. - assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... - Qed. - -(** Subrelations induce a morphism on the identity. *) - -Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id. -Proof. firstorder. Qed. - -(** The subrelation property goes through products as usual. *) - -Lemma subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) : - subrelation (R₁ ==> S₁) (R₂ ==> S₂). -Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. - -(** And of course it is reflexive. *) - -Lemma subrelation_refl A R : @subrelation A R R. -Proof. simpl_relation. Qed. - +(** Resolution with subrelation: favor decomposing products over applying reflexivity + for unconstrained goals. *) Ltac subrelation_tac T U := (is_ground T ; is_ground U ; class_apply @subrelation_refl) || class_apply @subrelation_respectful || class_apply @subrelation_refl. Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. -(** [Proper] is itself a covariant morphism for [subrelation]. *) - -Lemma subrelation_proper `(mor : Proper A R₁ m, unc : Unconvertible (relation A) R₁ R₂, - sub : subrelation A R₁ R₂) : Proper R₂ m. -Proof. - intros. apply sub. apply mor. -Qed. - CoInductive apply_subrelation : Prop := do_subrelation. Ltac proper_subrelation := @@ -189,117 +231,112 @@ Ltac proper_subrelation := Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. -Instance proper_subrelation_proper : - Proper (subrelation ++> eq ==> impl) (@Proper A). -Proof. reduce. subst. firstorder. Qed. - (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) Instance iff_impl_subrelation : subrelation iff impl | 2. Proof. firstorder. Qed. -Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2. +Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2. Proof. firstorder. Qed. -Instance pointwise_subrelation {A} `(sub : subrelation B R R') : - subrelation (pointwise_relation A R) (pointwise_relation A R') | 4. -Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. - -(** For dependent function types. *) -Lemma forall_subrelation A (B : A -> Type) (R S : forall x : A, relation (B x)) : - (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S). -Proof. reduce. apply H. apply H0. Qed. - (** We use an extern hint to help unification. *) Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => apply (@forall_subrelation A B R S) ; intro : typeclass_instances. -(** Any symmetric relation is equal to its inverse. *) +Section GenericInstances. + (* Share universes *) + Let U := Type. + Context {A B C : U}. -Lemma subrelation_symmetric A R `(Symmetric A R) : subrelation (inverse R) R. -Proof. reduce. red in H0. symmetry. assumption. Qed. - -Hint Extern 4 (subrelation (inverse _) _) => - class_apply @subrelation_symmetric : typeclass_instances. - -(** The complement of a relation conserves its proper elements. *) + (** We can build a PER on the Coq function space if we have PERs on the domain and + codomain. *) + + Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). -Program Definition complement_proper - `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement R) := _. + Next Obligation. + Proof with auto. + assert(R x0 x0). + transitivity y0... symmetry... + transitivity (y x0)... + Qed. - Next Obligation. + (** The complement of a relation conserves its proper elements. *) + + Program Definition complement_proper + `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : + Proper (RA ==> RA ==> iff) (complement R) := _. + + 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 Definition flip_proper - `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : - Proper (RB ==> RA ==> RC) (flip f) := _. + (** The [flip] too, actually the [flip] instance is a bit more general. *) + Program Definition flip_proper + `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) 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], + (** Every Transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) - -Program Instance trans_contra_co_morphism - `(Transitive A R) : Proper (R --> R ++> impl) R. - + + Global Program + Instance trans_contra_co_morphism + `(Transitive A R) : Proper (R --> R ++> impl) R. + Next Obligation. Proof with auto. transitivity x... transitivity x0... Qed. -(** Proper declarations for partial applications. *) + (** Proper declarations for partial applications. *) -Program Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3. + Global Program + Instance trans_contra_inv_impl_morphism + `(Transitive A R) : Proper (R --> flip impl) (R x) | 3. Next Obligation. Proof with auto. transitivity y... Qed. -Program Instance trans_co_impl_morphism - `(Transitive A R) : Proper (R ++> impl) (R x) | 3. + Global Program + Instance trans_co_impl_morphism + `(Transitive A R) : Proper (R ++> impl) (R x) | 3. Next Obligation. Proof with auto. transitivity x0... Qed. -Program Instance trans_sym_co_inv_impl_morphism - `(PER A R) : Proper (R ++> inverse impl) (R x) | 3. + Global Program + Instance trans_sym_co_inv_impl_morphism + `(PER A R) : Proper (R ++> flip impl) (R x) | 3. Next Obligation. Proof with auto. transitivity y... symmetry... Qed. -Program Instance trans_sym_contra_impl_morphism - `(PER A R) : Proper (R --> impl) (R x) | 3. + Global Program Instance trans_sym_contra_impl_morphism + `(PER A R) : Proper (R --> impl) (R x) | 3. Next Obligation. Proof with auto. transitivity x0... symmetry... Qed. -Program Instance per_partial_app_morphism + Global Program Instance per_partial_app_morphism `(PER A R) : Proper (R ==> iff) (R x) | 2. Next Obligation. @@ -310,20 +347,21 @@ Program Instance per_partial_app_morphism symmetry... Qed. -(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof - to get an [R y z] goal. *) + (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) -Program Instance trans_co_eq_inv_impl_morphism - `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2. + Global Program + Instance trans_co_eq_inv_impl_morphism + `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2. Next Obligation. Proof with auto. transitivity y... Qed. -(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) + (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. + Global Program + Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. @@ -333,11 +371,11 @@ Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. transitivity y... transitivity y0... symmetry... Qed. -Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R). -Proof. firstorder. Qed. + Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). + Proof. firstorder. Qed. -Program Instance compose_proper A B C R₀ R₁ R₂ : - Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C). + Global Program Instance compose_proper RA RB RC : + Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C). Next Obligation. Proof. @@ -345,63 +383,79 @@ Program Instance compose_proper A B C R₀ R₁ R₂ : unfold compose. apply H. apply H0. apply H1. Qed. -(** Coq functions are morphisms for Leibniz equality, - applied only if really needed. *) + (** Coq functions are morphisms for Leibniz equality, + applied only if really needed. *) -Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') : - Reflexive (@Logic.eq A ==> R'). -Proof. simpl_relation. Qed. - -(** [respectful] is a morphism for relation equivalence. *) - -Instance respectful_morphism : - Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). -Proof. - reduce. - unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. - split ; intros. + Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') : + Reflexive (@Logic.eq A ==> R'). + Proof. simpl_relation. Qed. + (** [respectful] is a morphism for relation equivalence. *) + + Global Instance respectful_morphism : + Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) + (@respectful A B). + Proof. + reduce. + unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. + split ; intros. + rewrite <- H0. apply H1. rewrite H. assumption. - + rewrite H0. apply H1. rewrite <- H. assumption. -Qed. - -(** Every element in the carrier of a reflexive relation is a morphism for this relation. - We use a proxy class for this case which is used internally to discharge reflexivity constraints. - The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of - [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able - to set different priorities in different hint bases and select a particular hint database for - resolution of a type class constraint.*) - -Class ProperProxy {A} (R : relation A) (m : A) : Prop := - proper_proxy : R m m. - -Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x. -Proof. firstorder. Qed. - -Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. -Proof. firstorder. Qed. - -Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x. -Proof. firstorder. Qed. - -Hint Extern 1 (ProperProxy _ _) => - class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. -Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. + Qed. -(** [R] is Reflexive, hence we can build the needed proof. *) + (** [R] is Reflexive, hence we can build the needed proof. *) -Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : - Proper R' (m x). -Proof. simpl_relation. Qed. + Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : + Proper R' (m x). + Proof. simpl_relation. Qed. + + Class Params (of : A) (arity : nat). + + Lemma flip_respectful (R : relation A) (R' : relation B) : + relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). + Proof. + intros. + unfold flip, respectful. + split ; intros ; intuition. + Qed. -Class Params {A : Type} (of : A) (arity : nat). + + (** Treating flip: can't make them direct instances as we + need at least a [flip] present in the goal. *) + + Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R. + Proof. firstorder. Qed. + + Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')). + Proof. firstorder. Qed. + + (** That's if and only if *) + + Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. + Proof. simpl_relation. Qed. + + (** Once we have normalized, we will apply this instance to simplify the problem. *) + + Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor. + + (** Every reflexive relation gives rise to a morphism, + only for immediately solving goals without variables. *) + + Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x. + Proof. firstorder. Qed. + + Lemma proper_eq (x : A) : Proper (@eq A) x. + Proof. intros. apply reflexive_proper. Qed. + +End GenericInstances. Class PartialApplication. @@ -450,68 +504,6 @@ Ltac partial_application_tactic := end end. -Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances. - -Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), - relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R'). -Proof. - intros. - unfold flip, respectful. - split ; intros ; intuition. -Qed. - -(** Special-purpose class to do normalization of signatures w.r.t. inverse. *) - -Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := - normalizes : relation_equivalence m m'. - -(** Current strategy: add [inverse] everywhere and reduce using [subrelation] - afterwards. *) - -Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)). -Proof. - firstorder. -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. - rewrite NA, NB. firstorder. -Qed. - -Ltac inverse := - match goal with - | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow - | _ => class_apply @inverse_atom - end. - -Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances. - -(** Treating inverse: can't make them direct instances as we - need at least a [flip] present in the goal. *) - -Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R. -Proof. firstorder. Qed. - -Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')). -Proof. firstorder. Qed. - -Hint Extern 1 (subrelation (flip _) _) => class_apply @inverse1 : typeclass_instances. -Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances. - -(** That's if and only if *) - -Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. -Proof. simpl_relation. Qed. - -(* Hint Extern 3 (subrelation eq ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *) - -(** Once we have normalized, we will apply this instance to simplify the problem. *) - -Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor. - -Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances. - (** Bootstrap !!! *) Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). @@ -525,46 +517,83 @@ Proof. apply H0. Qed. -Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m. -Proof. - red in H, H0. - setoid_rewrite H. - assumption. -Qed. - -Ltac proper_normalization := +Ltac proper_reflexive := match goal with | [ _ : normalization_done |- _ ] => fail 1 - | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in - set(H:=did_normalization) ; class_apply @proper_normalizes_proper + | _ => class_apply proper_eq || class_apply @reflexive_proper end. -Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances. -(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *) +Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. +Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. -Lemma reflexive_proper `{Reflexive A R} (x : A) - : Proper R x. -Proof. firstorder. Qed. +Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper + : typeclass_instances. +Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper + : typeclass_instances. +Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper + : typeclass_instances. +Hint Extern 4 (@Proper _ _ _) => partial_application_tactic + : typeclass_instances. +Hint Extern 7 (@Proper _ _ _) => proper_reflexive + : typeclass_instances. -Lemma proper_eq A (x : A) : Proper (@eq A) x. -Proof. intros. apply reflexive_proper. Qed. +(** Special-purpose class to do normalization of signatures w.r.t. flip. *) -Ltac proper_reflexive := +Section Normalize. + Context (A : Type). + + Class Normalizes (m : relation A) (m' : relation A) : Prop := + normalizes : relation_equivalence m m'. + + (** Current strategy: add [flip] everywhere and reduce using [subrelation] + afterwards. *) + + Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. + Proof. + red in H, H0. + rewrite H. + assumption. + Qed. + + Lemma flip_atom R : Normalizes R (flip (flip R)). + Proof. + firstorder. + Qed. + +End Normalize. + +Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : + Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature). +Proof. + unfold Normalizes in *. intros. + rewrite NA, NB. firstorder. +Qed. + +Ltac normalizes := match goal with - | [ _ : normalization_done |- _ ] => fail 1 - | _ => class_apply proper_eq || class_apply @reflexive_proper + | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow + | _ => class_apply @flip_atom end. -Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. +Ltac proper_normalization := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : apply_subrelation |- @Proper _ ?R _ ] => + let H := fresh "H" in + set(H:=did_normalization) ; class_apply @proper_normalizes_proper + end. +Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances. +Hint Extern 6 (@Proper _ _ _) => proper_normalization + : typeclass_instances. (** When the relation on the domain is symmetric, we can - inverse the relation on the codomain. Same for binary functions. *) + flip the relation on the codomain. Same for binary functions. *) Lemma proper_sym_flip : forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), - Proper (R1==>inverse R2) f. + Proper (R1==>flip R2) f. Proof. intros A R1 Sym B R2 f Hf. intros x x' Hxx'. apply Hf, Sym, Hxx'. @@ -572,7 +601,7 @@ Qed. Lemma proper_sym_flip_2 : forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), - Proper (R1==>R2==>inverse R3) f. + Proper (R1==>R2==>flip R3) f. Proof. intros A R1 Sym1 B R2 Sym2 C R3 f Hf. intros x x' Hxx' y y' Hyy'. apply Hf; auto. @@ -627,8 +656,6 @@ apply partial_order_antisym; auto. rewrite Hxz; auto. Qed. -Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => - class_apply PartialOrder_StrictOrder : typeclass_instances. (** From a [StrictOrder] to the corresponding [PartialOrder]: [le = lt \/ eq]. @@ -659,5 +686,8 @@ elim (StrictOrder_Irreflexive x). transitivity y; auto. Qed. +Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => + class_apply PartialOrder_StrictOrder : typeclass_instances. + Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 6f02ac9f57..4f80a67ae6 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -16,7 +16,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [simpl_relation | firstorder auto]. (** Standard instances for [not], [iff] and [impl]. *) @@ -52,49 +52,20 @@ Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl. Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A). - Next Obligation. - Proof. - unfold pointwise_relation in H. - split ; intros. - destruct H0 as [x1 H1]. - exists x1. rewrite H in H1. assumption. - - destruct H0 as [x1 H1]. - exists x1. rewrite H. assumption. - Qed. - Program Instance ex_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@ex A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance ex_inverse_impl_morphism {A : Type} : - Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1. - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. +Program Instance ex_flip_impl_morphism {A : Type} : + Proper (pointwise_relation A (flip impl) ==> flip impl) (@ex A) | 1. Program Instance all_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@all A). - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - Program Instance all_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@all A) | 1. -Program Instance all_inverse_impl_morphism {A : Type} : - Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1. +Program Instance all_flip_impl_morphism {A : Type} : + Proper (pointwise_relation A (flip impl) ==> flip impl) (@all A) | 1. (** Equivalent points are simultaneously accessible or not *) @@ -104,13 +75,13 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) 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. +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). + Proper (relation_equivalence ==> 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'. @@ -121,7 +92,7 @@ Qed. (** Equivalent relations are simultaneously well-founded or not *) Instance well_founded_morphism {A : Type} : - Proper (@relation_equivalence A ==> iff) (@well_founded A). + Proper (relation_equivalence ==> 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 ea2afb3063..dc46b4bbb8 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -30,8 +30,6 @@ Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> (* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *) -Require Import List. - Lemma predicate_equivalence_pointwise (l : Tlist) : Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id. Proof. do 2 red. unfold predicate_equivalence. auto. Qed. @@ -52,6 +50,6 @@ Instance subrelation_pointwise : Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed. -Lemma inverse_pointwise_relation A (R : relation A) : - relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)). +Lemma flip_pointwise_relation A (R : relation A) : + relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)). Proof. intros. split; firstorder. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index b8fdac8c9d..61edb2b981 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -20,41 +20,187 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. -(** We allow to unfold the [relation] definition while doing morphism search. *) - -Notation inverse R := (flip (R:relation _) : relation _). - -Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. - -(** Opaque for proof-search. *) -Typeclasses Opaque complement. - -(** These are convertible. *) - -Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). -Proof. reflexivity. Qed. +Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. -(** We rebind relations in separate classes to be able to overload each proof. *) +(** We allow to unfold the [relation] definition while doing morphism search. *) -Set Implicit Arguments. -Unset Strict Implicit. +Section Defs. + Context {A : Type}. + + (** We rebind relational properties in separate classes to be able to overload each proof. *) + + Class Reflexive (R : relation A) := + reflexivity : forall x : A, R x x. + + Definition complement (R : relation A) : relation A := fun x y => R x y -> False. + + (** Opaque for proof-search. *) + Typeclasses Opaque complement. + + (** These are convertible. *) + Lemma complement_inverse R : complement (flip R) = flip (complement R). + Proof. reflexivity. Qed. + + Class Irreflexive (R : relation A) := + irreflexivity : Reflexive (complement R). + + Class Symmetric (R : relation A) := + symmetry : forall {x y}, R x y -> R y x. + + Class Asymmetric (R : relation A) := + asymmetry : forall {x y}, R x y -> R y x -> False. + + Class Transitive (R : relation A) := + transitivity : forall {x y z}, R x y -> R y z -> R x z. + + (** Various combinations of reflexivity, symmetry and transitivity. *) + + (** A [PreOrder] is both Reflexive and Transitive. *) + + Class PreOrder (R : relation A) : Prop := { + PreOrder_Reflexive :> Reflexive R | 2 ; + PreOrder_Transitive :> Transitive R | 2 }. + + (** A [StrictOrder] is both Irreflexive and Transitive. *) + + Class StrictOrder (R : relation A) : Prop := { + StrictOrder_Irreflexive :> Irreflexive R ; + StrictOrder_Transitive :> Transitive R }. + + (** By definition, a strict order is also asymmetric *) + Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R. + Proof. firstorder. Qed. + + (** A partial equivalence relation is Symmetric and Transitive. *) + + Class PER (R : relation A) : Prop := { + PER_Symmetric :> Symmetric R | 3 ; + PER_Transitive :> Transitive R | 3 }. + + (** Equivalence relations. *) + + Class Equivalence (R : relation A) : Prop := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. + + (** An Equivalence is a PER plus reflexivity. *) + + Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 := + { }. + + (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) + + Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) := + antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. + + Class subrelation (R R' : relation A) : Prop := + is_subrelation : forall {x y}, R x y -> R' x y. + + (** Any symmetric relation is equal to its inverse. *) + + Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R. + Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed. + + Section flip. + + Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R). + Proof. tauto. Qed. + + Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) := + irreflexivity (R:=R). + + Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) := + fun x y H => symmetry (R:=R) H. + + Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) := + fun x y H H' => asymmetry (R:=R) H H'. + + Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) := + fun x y z H H' => transitivity (R:=R) H' H. + + Program Definition flip_Antisymmetric `(Antisymmetric eqA R) : + Antisymmetric eqA (flip R). + Proof. firstorder. Qed. + + (** Inversing the larger structures *) + + Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_PER `(PER R) : PER (flip R). + Proof. firstorder. Qed. + + Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R). + Proof. firstorder. Qed. + + End flip. + + Section complement. + + Definition complement_Irreflexive `(Reflexive R) + : Irreflexive (complement R). + Proof. firstorder. Qed. + + Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R). + Proof. firstorder. Qed. + End complement. + + + (** Rewrite relation on a given support: declares a relation as a rewrite + relation for use by the generalized rewriting tactic. + It helps choosing if a rewrite should be handled + by the generalized or the regular rewriting tactic using leibniz equality. + Users can declare an [RewriteRelation A RA] anywhere to declare default + relations. This is also done automatically by the [Declare Relation A RA] + commands. *) -Class Reflexive {A} (R : relation A) := - reflexivity : forall x, R x x. + Class RewriteRelation (RA : relation A). -Class Irreflexive {A} (R : relation A) := - irreflexivity : Reflexive (complement R). + (** Any [Equivalence] declared in the context is automatically considered + a rewrite relation. *) + + Global Instance equivalence_rewrite_relation `(Equivalence eqA) : RewriteRelation eqA. + + (** Leibniz equality. *) + Section Leibniz. + Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A. + Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A. + Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A. + + (** Leibinz equality [eq] is an equivalence relation. + The instance has low priority as it is always applicable + if only the type is constrained. *) + + Global Program Instance eq_equivalence : Equivalence (@eq A) | 10. + End Leibniz. + +End Defs. + +(** Default rewrite relations handled by [setoid_rewrite]. *) +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. +(** Hints to drive the typeclass resolution avoiding loops + due to the use of full unification. *) Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. -Class Symmetric {A} (R : relation A) := - symmetry : forall x y, R x y -> R y x. - -Class Asymmetric {A} (R : relation A) := - asymmetry : forall x y, R x y -> R y x -> False. +Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. -Class Transitive {A} (R : relation A) := - transitivity : forall x y z, R x y -> R y z -> R x z. +Hint Extern 4 (subrelation (flip _) _) => + class_apply @subrelation_symmetric : typeclass_instances. Hint Resolve irreflexivity : ord. @@ -72,40 +218,6 @@ Hint Extern 4 => solve_relation : relations. (** We can already dualize all these properties. *) -Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. - -Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R). -Proof. tauto. Qed. - -Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. - -Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := - irreflexivity (R:=R). - -Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) := - fun x y H => symmetry (R:=R) H. - -Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) := - fun x y H H' => asymmetry (R:=R) H H'. - -Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) := - fun x y z H H' => transitivity (R:=R) H' H. - -Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. -Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. -Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. -Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. - -Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) - : Irreflexive (complement R). -Proof. firstorder. Qed. - -Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). -Proof. firstorder. Qed. - -Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. -Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances. - (** * Standard instances. *) Ltac reduce_hyp H := @@ -145,54 +257,6 @@ Instance iff_Reflexive : Reflexive iff := iff_refl. Instance iff_Symmetric : Symmetric iff := iff_sym. Instance iff_Transitive : Transitive iff := iff_trans. -(** Leibniz equality. *) - -Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A. -Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A. -Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. - -(** Various combinations of reflexivity, symmetry and transitivity. *) - -(** A [PreOrder] is both Reflexive and Transitive. *) - -Class PreOrder {A} (R : relation A) : Prop := { - 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 | 3 ; - PER_Transitive :> Transitive R | 3 }. - -(** Equivalence relations. *) - -Class Equivalence {A} (R : relation A) : Prop := { - Equivalence_Reflexive :> Reflexive R ; - Equivalence_Symmetric :> Symmetric R ; - Equivalence_Transitive :> Transitive R }. - -(** An Equivalence is a PER plus reflexivity. *) - -Instance Equivalence_PER `(Equivalence A R) : PER R | 10 := - { PER_Symmetric := Equivalence_Symmetric ; - PER_Transitive := Equivalence_Transitive }. - -(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) - -Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) := - antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. - -Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) : - Antisymmetric A eqA (flip R). -Proof. firstorder. Qed. - -(** Leibinz equality [eq] is an equivalence relation. - The instance has low priority as it is always applicable - if only the type is constrained. *) - -Program Instance eq_equivalence : Equivalence (@eq A) | 10. - (** Logical equivalence [iff] is an equivalence relation. *) Program Instance iff_equivalence : Equivalence iff. @@ -203,9 +267,6 @@ Program Instance iff_equivalence : Equivalence iff. Local Open Scope list_scope. -(* Notation " [ ] " := nil : list_scope. *) -(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) - (** A compact representation of non-dependent arities, with the codomain singled-out. *) (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) @@ -346,106 +407,66 @@ Program Instance predicate_implication_preorder : (** We define the various operations which define the algebra on binary relations, from the general ones. *) -Definition relation_equivalence {A : Type} : relation (relation A) := - @predicate_equivalence (_::_::Tnil). - -Class subrelation {A:Type} (R R' : relation A) : Prop := - is_subrelation : @predicate_implication (A::A::Tnil) R R'. - -Arguments subrelation {A} R R'. - -Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_intersection (A::A::Tnil) R R'. - -Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_union (A::A::Tnil) R R'. - -(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) - -Set Automatic Introduction. - -Instance relation_equivalence_equivalence (A : Type) : - Equivalence (@relation_equivalence A). -Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed. - -Instance relation_implication_preorder A : PreOrder (@subrelation A). -Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed. - -(** *** Partial Order. +Section Binary. + Context {A : Type}. + + Definition relation_equivalence : relation (relation A) := + @predicate_equivalence (_::_::Tnil). + + Global Instance: RewriteRelation relation_equivalence. + + Definition relation_conjunction (R : relation A) (R' : relation A) : relation A := + @predicate_intersection (A::A::Tnil) R R'. + + Definition relation_disjunction (R : relation A) (R' : relation A) : relation A := + @predicate_union (A::A::Tnil) R R'. + + (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + + Set Automatic Introduction. + + Global Instance relation_equivalence_equivalence : + Equivalence relation_equivalence. + Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed. + + Global Instance relation_implication_preorder : PreOrder (@subrelation A). + Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed. + + (** *** Partial Order. A partial order is a preorder which is additionally antisymmetric. 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} := - partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). + Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := + partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)). + + (** The equivalence proof is sufficient for proving that [R] must be a + morphism for equivalence (see Morphisms). It is also sufficient to + show that [R] is antisymmetric w.r.t. [eqA] *) + + Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Proof with auto. + reduce_goal. + pose proof partial_order_equivalence as poe. do 3 red in poe. + apply <- poe. firstorder. + Qed. -(** The equivalence proof is sufficient for proving that [R] must be a morphism - for equivalence (see Morphisms). - It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) -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. - apply <- poe. firstorder. -Qed. + Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). + Proof. firstorder. Qed. +End Binary. + +Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. (** The partial order defined by subrelation and relation equivalence. *) Program Instance subrelation_partial_order : ! PartialOrder (relation A) relation_equivalence subrelation. - Next Obligation. - Proof. - unfold relation_equivalence in *. compute; firstorder. - Qed. +Next Obligation. +Proof. + unfold relation_equivalence in *. compute; firstorder. +Qed. Typeclasses Opaque arrows predicate_implication predicate_equivalence - relation_equivalence pointwise_lifting. - -(** Rewrite relation on a given support: declares a relation as a rewrite - relation for use by the generalized rewriting tactic. - It helps choosing if a rewrite should be handled - by the generalized or the regular rewriting tactic using leibniz equality. - Users can declare an [RewriteRelation A RA] anywhere to declare default - relations. This is also done automatically by the [Declare Relation A RA] - commands. *) - -Class RewriteRelation {A : Type} (RA : relation A). - -Instance: RewriteRelation impl. -Instance: RewriteRelation iff. -Instance: RewriteRelation (@relation_equivalence A). - -(** Any [Equivalence] declared in the context is automatically considered - a rewrite relation. *) - -Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA. - -(** Strict Order *) - -Class StrictOrder {A : Type} (R : relation A) : Prop := { - StrictOrder_Irreflexive :> Irreflexive R ; - StrictOrder_Transitive :> Transitive R -}. - -Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R. -Proof. firstorder. Qed. - -(** Inversing a [StrictOrder] gives another [StrictOrder] *) - -Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R). -Proof. firstorder. Qed. - -(** Same for [PartialOrder]. *) - -Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R). -Proof. firstorder. Qed. - -Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances. -Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances. - -Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R). -Proof. firstorder. Qed. - -Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances. + relation_equivalence pointwise_lifting. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 2b010206c4..73be830a48 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -9,8 +9,8 @@ (** * Relations over pairs *) +Require Import SetoidList. Require Import Relations Morphisms. - (* NB: This should be system-wide someday, but for that we need to fix the simpl tactic, since "simpl fst" would be refused for the moment. @@ -40,7 +40,7 @@ Generalizable Variables A B RA RB Ri Ro f. (** Any function from [A] to [B] allow to obtain a relation over [A] out of a relation over [B]. *) -Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A := +Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. @@ -62,13 +62,13 @@ Instance snd_measure : @Measure (A * B) B Snd. (** We define a product relation over [A*B]: each components should satisfy the corresponding initial relation. *) -Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) := - relation_conjunction (RA @@1) (RB @@2). +Polymorphic Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) := + relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2). Infix "*" := RelProd : signature_scope. Section RelCompFun_Instances. - Context {A B : Type} (R : relation B). + Context {A : Type} {B : Type} (R : relation B). Global Instance RelCompFun_Reflexive `(Measure A B f, Reflexive _ R) : Reflexive (R@@f). @@ -94,57 +94,61 @@ Section RelCompFun_Instances. End RelCompFun_Instances. -Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B) - `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB). -Proof. firstorder. Qed. - -Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B) - `(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB). -Proof. firstorder. Qed. - -Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) - `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). -Proof. firstorder. Qed. - -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) : - relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)). -Proof. firstorder. Qed. - -Lemma SndRel_ProdRel {A B}(RB:relation B) : - relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB). -Proof. firstorder. Qed. - -Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (RA*RB) (RA @@1). -Proof. firstorder. Qed. - -Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (RA*RB) (RB @@2). -Proof. firstorder. Qed. - -Instance pair_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA==>RB==> RA*RB) (@pair _ _). -Proof. firstorder. Qed. - -Instance fst_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA*RB ==> RA) Fst. -Proof. -intros (x,y) (x',y') (Hx,Hy); compute in *; auto. -Qed. - -Instance snd_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA*RB ==> RB) Snd. -Proof. -intros (x,y) (x',y') (Hx,Hy); compute in *; auto. -Qed. - -Instance RelCompFun_compat {A B}(f:A->B)(R : relation B) - `(Proper _ (Ri==>Ri==>Ro) R) : - Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature. -Proof. unfold RelCompFun; firstorder. Qed. +Section RelProd_Instances. + + Context {A : Type} {B : Type} (RA : relation A) (RB : relation B). + + Global Instance RelProd_Reflexive `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB). + Proof. firstorder. Qed. + + Global Instance RelProd_Symmetric `(Symmetric _ RA, Symmetric _ RB) + : Symmetric (RA*RB). + Proof. firstorder. Qed. + + Global Instance RelProd_Transitive + `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). + Proof. firstorder. Qed. + + Global Program Instance RelProd_Equivalence + `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). + + Lemma FstRel_ProdRel : + relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)). + Proof. firstorder. Qed. + + Lemma SndRel_ProdRel : + relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB). + Proof. firstorder. Qed. + + Global Instance FstRel_sub : + subrelation (RA*RB) (RA @@1). + Proof. firstorder. Qed. + + Global Instance SndRel_sub : + subrelation (RA*RB) (RB @@2). + Proof. firstorder. Qed. + + Global Instance pair_compat : + Proper (RA==>RB==> RA*RB) (@pair _ _). + Proof. firstorder. Qed. + + Global Instance fst_compat : + Proper (RA*RB ==> RA) Fst. + Proof. + intros (x,y) (x',y') (Hx,Hy); compute in *; auto. + Qed. + + Global Instance snd_compat : + Proper (RA*RB ==> RB) Snd. + Proof. + intros (x,y) (x',y') (Hx,Hy); compute in *; auto. + Qed. + + Global Instance RelCompFun_compat (f:A->B) + `(Proper _ (Ri==>Ri==>Ro) RB) : + Proper (Ri@@f==>Ri@@f==>Ro) (RB@@f)%signature. + Proof. unfold RelCompFun; firstorder. Qed. +End RelProd_Instances. Hint Unfold RelProd RelCompFun. Hint Extern 2 (RelProd _ _ _ _) => split. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 7bc208c45d..3ea8fe10e5 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) else in_right else in_right. - Solve Obligations with try red ; unfold equiv, complement ; program_simpl. + Solve Obligations with try red ; unfold complement ; program_simpl. Next Obligation. Proof. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 5d34a4bf50..bee922c6fc 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1247,11 +1247,11 @@ Proof. intros m1 m2; functional induction (concat m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. apply join_bst; auto. - change (bst (m2',xd)#1); rewrite <-e1; eauto. + change (bst (m2',xd)#1). rewrite <-e1; eauto. intros y Hy. apply H1; auto. rewrite remove_min_in, e1; simpl; auto. - change (gt_tree (m2',xd)#2#1 (m2',xd)#1); rewrite <-e1; eauto. + change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. Hint Resolve concat_bst. @@ -1930,7 +1930,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'. Proof. - intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition. + intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. generalize (H0 k); do 2 rewrite In_alt; intuition. generalize (H0 k); do 2 rewrite In_alt; intuition. generalize (H0 k); do 2 rewrite <- In_alt; intuition. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 85b7242b5c..0e3b5cef1c 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -437,12 +437,6 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. -Definition option_map (A B:Type)(f:A->B)(o:option A) : option B := - match o with - | Some a => Some (f a) - | None => None - end. - Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = option_map f (find x m). Proof. @@ -678,7 +672,7 @@ Qed. Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. -unfold Empty; intros m m' Hm; intuition. +unfold Empty; intros m m' Hm. split; intros; intro. rewrite <-Hm in H0; eapply H, H0. rewrite Hm in H0; eapply H, H0. Qed. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index f15ab222ce..64d5b1c9a4 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -527,7 +527,7 @@ Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := | nil => nil | (k,e)::m' => (k,f k e) :: mapi f m' end. - + End Elt. Section Elt2. (* A new section is necessary for previous definitions to work @@ -543,14 +543,13 @@ Proof. intros m x e f. (* functional induction map elt elt' f m. *) (* Marche pas ??? *) induction m. - inversion 1. + inversion 1. destruct a as (x',e'). simpl. - inversion_clear 1. + inversion_clear 1. constructor 1. unfold eqke in *; simpl in *; intuition congruence. - constructor 2. unfold MapsTo in *; auto. Qed. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 792b88717c..253800a458 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -8,7 +8,7 @@ (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) -Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface. +Require Import Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface. Set Implicit Arguments. Local Open Scope positive_scope. @@ -69,7 +69,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. Module ME:=KeyOrderedType E. - Definition key := positive. + Definition key := positive : Type. Inductive tree (A : Type) := | Leaf : tree A @@ -93,7 +93,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | _ => false end. - Fixpoint find (i : positive) (m : t A) : option A := + Fixpoint find (i : key) (m : t A) : option A := match m with | Leaf => None | Node l o r => @@ -104,7 +104,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint mem (i : positive) (m : t A) : bool := + Fixpoint mem (i : key) (m : t A) : bool := match m with | Leaf => false | Node l o r => @@ -115,7 +115,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (v : A) (m : t A) : t A := + Fixpoint add (i : key) (v : A) (m : t A) : t A := match m with | Leaf => match i with @@ -131,7 +131,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint remove (i : positive) (m : t A) : t A := + Fixpoint remove (i : key) (m : t A) : t A := match i with | xH => match m with @@ -163,7 +163,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** [elements] *) - Fixpoint xelements (m : t A) (i : positive) : list (positive * A) := + Fixpoint xelements (m : t A) (i : key) : list (key * A) := match m with | Leaf => nil | Node l None r => @@ -190,33 +190,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section CompcertSpec. Theorem gempty: - forall (i: positive), find i empty = None. + forall (i: key), find i empty = None. Proof. destruct i; simpl; auto. Qed. Theorem gss: - forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x. + forall (i: key) (x: A) (m: t A), find i (add i x m) = Some x. Proof. induction i; destruct m; simpl; auto. Qed. - Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None. + Lemma gleaf : forall (i : key), find i (Leaf : t A) = None. Proof. exact gempty. Qed. Theorem gso: - forall (i j: positive) (x: A) (m: t A), + forall (i j: key) (x: A) (m: t A), i <> j -> find i (add j x m) = find i m. Proof. induction i; intros; destruct j; destruct m; simpl; try rewrite <- (gleaf i); auto; try apply IHi; congruence. Qed. - Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf. + Lemma rleaf : forall (i : key), remove i (Leaf : t A) = Leaf. Proof. destruct i; simpl; auto. Qed. Theorem grs: - forall (i: positive) (m: t A), find i (remove i m) = None. + forall (i: key) (m: t A), find i (remove i m) = None. Proof. induction i; destruct m. simpl; auto. @@ -236,7 +236,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gro: - forall (i j: positive) (m: t A), + forall (i j: key) (m: t A), i <> j -> find i (remove j m) = find i m. Proof. induction i; intros; destruct j; destruct m; @@ -265,11 +265,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_correct: - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), find i m = Some v -> List.In (append j i, v) (xelements m j). Proof. induction m; intros. - rewrite (gleaf i) in H; congruence. + rewrite (gleaf i) in H; discriminate. destruct o; destruct i; simpl; simpl in H. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. @@ -282,14 +282,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem elements_correct: - forall (m: t A) (i: positive) (v: A), + forall (m: t A) (i: key) (v: A), find i m = Some v -> List.In (i, v) (elements m). Proof. intros m i v H. exact (xelements_correct m i xH H). Qed. - Fixpoint xfind (i j : positive) (m : t A) : option A := + Fixpoint xfind (i j : key) (m : t A) : option A := match i, j with | _, xH => find i m | xO ii, xO jj => xfind ii jj m @@ -298,7 +298,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end. Lemma xfind_left : - forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A), + forall (j i : key) (m1 m2 : t A) (o : option A) (v : A), xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v. Proof. induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. @@ -306,7 +306,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ii : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j). Proof. induction m. @@ -322,7 +322,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_io : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), ~List.In (xI i, v) (xelements m (xO j)). Proof. induction m. @@ -337,7 +337,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oo : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j). Proof. induction m. @@ -353,7 +353,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oi : - forall (m: t A) (i j : positive) (v: A), + forall (m: t A) (i j : key) (v: A), ~List.In (xO i, v) (xelements m (xI j)). Proof. induction m. @@ -368,7 +368,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ih : - forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH). Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). @@ -381,7 +381,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_oh : - forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH). Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). @@ -394,7 +394,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_hi : - forall (m: t A) (i : positive) (v: A), + forall (m: t A) (i : key) (v: A), ~List.In (xH, v) (xelements m (xI i)). Proof. induction m; intros. @@ -409,7 +409,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma xelements_ho : - forall (m: t A) (i : positive) (v: A), + forall (m: t A) (i : key) (v: A), ~List.In (xH, v) (xelements m (xO i)). Proof. induction m; intros. @@ -424,13 +424,13 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma find_xfind_h : - forall (m: t A) (i: positive), find i m = xfind i xH m. + forall (m: t A) (i: key), find i m = xfind i xH m. Proof. destruct i; simpl; auto. Qed. Lemma xelements_complete: - forall (i j : positive) (m: t A) (v: A), + forall (i j : key) (m: t A) (v: A), List.In (i, v) (xelements m j) -> xfind i j m = Some v. Proof. induction i; simpl; intros; destruct j; simpl. @@ -458,7 +458,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem elements_complete: - forall (m: t A) (i: positive) (v: A), + forall (m: t A) (i: key) (v: A), List.In (i, v) (elements m) -> find i m = Some v. Proof. intros m i v H. @@ -479,18 +479,18 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End CompcertSpec. - Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v. + Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v. - Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m. + Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m. - Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m. + Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m. - Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p'). + Definition eq_key (p p':key*A) := E.eq (fst p) (fst p'). - Definition eq_key_elt (p p':positive*A) := + Definition eq_key_elt (p p':key*A) := E.eq (fst p) (fst p') /\ (snd p) = (snd p'). - Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). + Definition lt_key (p p':key*A) := E.lt (fst p) (fst p'). Global Instance eqk_equiv : Equivalence eq_key := _. Global Instance eqke_equiv : Equivalence eq_key_elt := _. @@ -715,8 +715,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Lemma elements_3w : NoDupA eq_key (elements m). Proof. - change eq_key with (@ME.eqk A). - apply ME.Sort_NoDupA; apply elements_3; auto. + apply ME.Sort_NoDupA. + apply elements_3. Qed. End FMapSpec. @@ -727,9 +727,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section Mapi. - Variable f : positive -> A -> B. + Variable f : key -> A -> B. - Fixpoint xmapi (m : t A) (i : positive) : t B := + Fixpoint xmapi (m : t A) (i : key) : t B := match m with | Leaf => @Leaf B | Node l o r => Node (xmapi l (append i (xO xH))) @@ -746,7 +746,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End A. Lemma xgmapi: - forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), + forall (A B: Type) (f: key -> A -> B) (i j : key) (m: t A), find i (xmapi f m j) = option_map (f (append j i)) (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -756,7 +756,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gmapi: - forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), + forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A), find i (mapi f m) = option_map (f i) (find i m). Proof. intros. @@ -820,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r) end. - Lemma xgmap2_l : forall (i : positive) (m : t A), + Lemma xgmap2_l : forall (i : key) (m : t A), f None None = None -> find i (xmap2_l m) = f (find i m) None. Proof. induction i; intros; destruct m; simpl; auto. @@ -832,7 +832,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r) end. - Lemma xgmap2_r : forall (i : positive) (m : t B), + Lemma xgmap2_r : forall (i : key) (m : t B), f None None = None -> find i (xmap2_r m) = f None (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -848,7 +848,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B), + Lemma gmap2: forall (i: key)(m1:t A)(m2: t B), f None None = None -> find i (_map2 m1 m2) = f (find i m1) (find i m2). Proof. @@ -896,9 +896,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section Fold. Variables A B : Type. - Variable f : positive -> A -> B -> B. + Variable f : key -> A -> B -> B. - Fixpoint xfoldi (m : t A) (v : B) (i : positive) := + Fixpoint xfoldi (m : t A) (v : B) (i : key) := match m with | Leaf _ => v | Node l (Some x) r => @@ -1070,7 +1070,7 @@ Module PositiveMapAdditionalFacts. (* Derivable from the Map interface *) Theorem gsspec: - forall (A:Type)(i j: positive) (x: A) (m: t A), + forall (A:Type)(i j: key) (x: A) (m: t A), find i (add j x m) = if E.eq_dec i j then Some x else find i m. Proof. intros. @@ -1079,7 +1079,7 @@ Module PositiveMapAdditionalFacts. (* Not derivable from the Map interface *) Theorem gsident: - forall (A:Type)(i: positive) (m: t A) (v: A), + forall (A:Type)(i: key) (m: t A) (v: A), find i m = Some v -> add i v m = m. Proof. induction i; intros; destruct m; simpl; simpl in H; try congruence. @@ -1118,4 +1118,3 @@ Module PositiveMapAdditionalFacts. Qed. End PositiveMapAdditionalFacts. - diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 670d091546..efd49f54e3 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -27,7 +27,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. - Definition elt := positive. + Definition elt := positive : Type. Inductive tree := | Leaf : tree @@ -35,9 +35,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Scheme tree_ind := Induction for tree Sort Prop. - Definition t := tree. + Definition t := tree : Type. - Definition empty := Leaf. + Definition empty : t := Leaf. Fixpoint is_empty (m : t) : bool := match m with @@ -45,7 +45,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | Node l b r => negb b &&& is_empty l &&& is_empty r end. +<<<<<<< HEAD Fixpoint mem (i : positive) (m : t) {struct m} : bool := +======= + Fixpoint mem (i : elt) (m : t) : bool := +>>>>>>> This commit adds full universe polymorphism and fast projections to Coq. match m with | Leaf => false | Node l o r => @@ -56,7 +60,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (m : t) : t := + Fixpoint add (i : elt) (m : t) : t := match m with | Leaf => match i with @@ -76,13 +80,17 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** helper function to avoid creating empty trees that are not leaves *) - Definition node l (b: bool) r := + Definition node (l : t) (b: bool) (r : t) : t := if b then Node l b r else match l,r with | Leaf,Leaf => Leaf | _,_ => Node l false r end. +<<<<<<< HEAD Fixpoint remove (i : positive) (m : t) {struct m} : t := +======= + Fixpoint remove (i : elt) (m : t) : t := +>>>>>>> This commit adds full universe polymorphism and fast projections to Coq. match m with | Leaf => Leaf | Node l o r => @@ -93,7 +101,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint union (m m': t) := + Fixpoint union (m m': t) : t := match m with | Leaf => m' | Node l o r => @@ -103,7 +111,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint inter (m m': t) := + Fixpoint inter (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -113,7 +121,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint diff (m m': t) := + Fixpoint diff (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -145,7 +153,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** reverses [y] and concatenate it with [x] *) - Fixpoint rev_append y x := + Fixpoint rev_append (y x : elt) : elt := match y with | 1 => x | y~1 => rev_append y x~1 @@ -156,8 +164,8 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Section Fold. - Variables B : Type. - Variable f : positive -> B -> B. + Variable B : Type. + Variable f : elt -> B -> B. (** the additional argument, [i], records the current path, in reverse order (this should be more efficient: we reverse this argument @@ -165,7 +173,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. we also use this convention in all functions below *) - Fixpoint xfold (m : t) (v : B) (i : positive) := + Fixpoint xfold (m : t) (v : B) (i : elt) := match m with | Leaf => v | Node l true r => @@ -179,9 +187,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Section Quantifiers. - Variable f : positive -> bool. + Variable f : elt -> bool. - Fixpoint xforall (m : t) (i : positive) := + Fixpoint xforall (m : t) (i : elt) := match m with | Leaf => true | Node l o r => @@ -189,21 +197,21 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end. Definition for_all m := xforall m 1. - Fixpoint xexists (m : t) (i : positive) := + Fixpoint xexists (m : t) (i : elt) := match m with | Leaf => false | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0 end. Definition exists_ m := xexists m 1. - Fixpoint xfilter (m : t) (i : positive) := + Fixpoint xfilter (m : t) (i : elt) : t := match m with | Leaf => Leaf | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1) end. Definition filter m := xfilter m 1. - Fixpoint xpartition (m : t) (i : positive) := + Fixpoint xpartition (m : t) (i : elt) : t * t := match m with | Leaf => (Leaf,Leaf) | Node l o r => @@ -221,7 +229,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** uses [a] to accumulate values rather than doing a lot of concatenations *) - Fixpoint xelements (m : t) (i : positive) (a: list positive) := + Fixpoint xelements (m : t) (i : elt) (a: list elt) := match m with | Leaf => a | Node l false r => xelements l i~0 (xelements r i~1 a) @@ -245,7 +253,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** would it be more efficient to use a path like in the above functions ? *) - Fixpoint choose (m: t) := + Fixpoint choose (m: t) : option elt := match m with | Leaf => None | Node l o r => if o then Some 1 else @@ -255,7 +263,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint min_elt (m: t) := + Fixpoint min_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -265,7 +273,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint max_elt (m: t) := + Fixpoint max_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -750,7 +758,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Proof. intros. rewrite diff_spec. split; assumption. Qed. (** Specification of [fold] *) - + Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i. Proof. @@ -798,15 +806,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. rewrite <- andb_lazy_alt. apply andb_true_iff. Qed. - Lemma filter_1 : forall s x f, compat_bool E.eq f -> + Lemma filter_1 : forall s x f, @compat_bool elt E.eq f -> In x (filter f s) -> In x s. Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. - Lemma filter_2 : forall s x f, compat_bool E.eq f -> + Lemma filter_2 : forall s x f, @compat_bool elt E.eq f -> In x (filter f s) -> f x = true. Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. - Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s -> + Lemma filter_3 : forall s x f, @compat_bool elt E.eq f -> In x s -> f x = true -> In x (filter f s). Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. @@ -831,11 +839,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. apply H. assumption. Qed. - Lemma for_all_1 : forall s f, compat_bool E.eq f -> + Lemma for_all_1 : forall s f, @compat_bool elt E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed. - Lemma for_all_2 : forall s f, compat_bool E.eq f -> + Lemma for_all_2 : forall s f, @compat_bool elt E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed. @@ -858,11 +866,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. intros [[x|x|] H]; eauto. Qed. - Lemma exists_1 : forall s f, compat_bool E.eq f -> + Lemma exists_1 : forall s f, @compat_bool elt E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed. - Lemma exists_2 : forall s f, compat_bool E.eq f -> + Lemma exists_2 : forall s f, @compat_bool elt E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed. @@ -878,11 +886,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o; simpl; rewrite IHl, IHr; reflexivity. Qed. - Lemma partition_1 : forall s f, compat_bool E.eq f -> + Lemma partition_1 : forall s f, @compat_bool elt E.eq f -> Equal (fst (partition f s)) (filter f s). Proof. intros. rewrite partition_filter. apply eq_refl. Qed. - Lemma partition_2 : forall s f, compat_bool E.eq f -> + Lemma partition_2 : forall s f, @compat_bool elt E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). Proof. intros. rewrite partition_filter. apply eq_refl. Qed. @@ -990,7 +998,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. constructor. intros x H. apply E.lt_not_eq in H. apply H. reflexivity. intro. apply E.lt_trans. - intros ? ? <- ? ? <-. reflexivity. + solve_proper. apply elements_3. Qed. @@ -1101,7 +1109,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct (min_elt r). injection H. intros <-. clear H. destruct y as [z|z|]. - apply (IHr p z); trivial. + apply (IHr e z); trivial. elim (Hp _ H'). discriminate. discriminate. @@ -1155,7 +1163,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. injection H. intros <-. clear H. destruct y as [z|z|]. elim (Hp _ H'). - apply (IHl p z); trivial. + apply (IHl e z); trivial. discriminate. discriminate. Qed. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index a956954544..cc46fe617f 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -143,6 +143,8 @@ Arguments S _%nat. (********************************************************************) (** * Container datatypes *) +Set Universe Polymorphism. + (** [option A] is the extension of [A] with an extra element [None] *) Inductive option (A:Type) : Type := @@ -182,7 +184,8 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Arguments pair {A B} _ _. Section projections. - Variables A B : Type. + Context {A : Type} {B : Type}. + Definition fst (p:A * B) := match p with | (x, y) => x end. @@ -244,8 +247,10 @@ Definition app (A : Type) : list A -> list A -> list A := | a :: l1 => a :: app l1 m end. + Infix "++" := app (right associativity, at level 60) : list_scope. +Unset Universe Polymorphism. (********************************************************************) (** * The comparison datatype *) @@ -310,6 +315,7 @@ Defined. Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := CompareSpec (eq x y) (lt x y) (lt y x). + Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := CompareSpecT (eq x y) (lt x y) (lt y x). Hint Unfold CompSpec CompSpecT. @@ -336,8 +342,11 @@ Arguments identity_rect [A] a P f y i. (** Identity type *) -Definition ID := forall A:Type, A -> A. -Definition id : ID := fun A x => x. +Polymorphic Definition ID := forall A:Type, A -> A. +Polymorphic Definition id : ID := fun A x => x. + +Definition IDProp := forall A:Prop, A -> A. +Definition idProp : IDProp := fun A x => x. (* begin hide *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9251d00ff3..f994b4ca64 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -15,6 +15,7 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. (** * Propositional connectives *) (** [True] is the always true proposition *) + Inductive True : Prop := I : True. @@ -232,7 +233,6 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) P x] is in fact equivalent to [ex (fun x => P x)] which may be not convertible to [ex P] if [P] is not itself an abstraction *) - Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. @@ -301,7 +301,8 @@ Arguments eq_ind [A] x P _ y _. Arguments eq_rec [A] x P _ y _. Arguments eq_rect [A] x P _ y _. -Hint Resolve I conj or_introl or_intror eq_refl: core. +Hint Resolve I conj or_introl or_intror : core. +Hint Resolve eq_refl: core. Hint Resolve ex_intro ex_intro2: core. Section Logic_lemmas. @@ -341,7 +342,7 @@ Section Logic_lemmas. Definition eq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. - intros A x P H y H0; elim eq_sym with (1 := H0); assumption. + intros A x P H y H0. elim eq_sym with (1 := H0); assumption. Defined. Definition eq_rec_r : diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index f58c21f488..f534dd6c6f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -21,19 +21,19 @@ Require Import Logic. Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset of elements of the type [A] which satisfy both [P] and [Q]. *) -Inductive sig (A:Type) (P:A -> Prop) : Type := +Polymorphic Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. -Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := +Polymorphic Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := exist2 : forall x:A, P x -> Q x -> sig2 P Q. (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) -Inductive sigT (A:Type) (P:A -> Type) : Type := +Polymorphic Inductive sigT (A:Type) (P:A -> Type) : Type := existT : forall x:A, P x -> sigT P. -Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := +Polymorphic Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := existT2 : forall x:A, P x -> Q x -> sigT2 P Q. (* Notations *) @@ -65,7 +65,7 @@ Add Printing Let sigT2. [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the proof of [(P a)] *) - +Set Universe Polymorphism. Section Subset_projections. Variable A : Type. @@ -123,6 +123,8 @@ End Subset_projections2. [(projT1 x)] is the first projection and [(projT2 x)] is the second projection, the type of which depends on the [projT1]. *) + + Section Projections. Variable A : Type. @@ -131,6 +133,7 @@ Section Projections. Definition projT1 (x:sigT P) : A := match x with | existT _ a _ => a end. + Definition projT2 (x:sigT P) : P (projT1 x) := match x return P (projT1 x) with | existT _ _ h => h @@ -212,6 +215,8 @@ Add Printing If sumor. Arguments inleft {A B} _ , [A] B _. Arguments inright {A B} _ , A [B] _. +Unset Universe Polymorphism. + (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. @@ -257,10 +262,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. @@ -273,11 +278,13 @@ End Dependent_choice_lemmas. [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)]. It is implemented using the option type. *) +Section Exc. + Variable A : Type. -Definition Exc := option. -Definition value := Some. -Definition error := @None. - + Definition Exc := option A. + Definition value := @Some A. + Definition error := @None A. +End Exc. Arguments error [A]. Definition except := False_rec. (* for compatibility with previous versions *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d282fe8c31..f6a0382c26 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -10,7 +10,7 @@ Require Import Le Gt Minus Bool. Require Setoid. Set Implicit Arguments. - +Set Universe Polymorphism. (******************************************************************) (** * Basics: definition of polymorphic lists and some operations *) @@ -65,8 +65,6 @@ End ListNotations. Import ListNotations. -(** ** Facts about lists *) - Section Facts. Variable A : Type. @@ -131,7 +129,7 @@ Section Facts. subst a; auto. exists [], l; auto. destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1), l2; simpl; f_equal; auto. + exists (a::l1), l2; simpl. apply f_equal. auto. Qed. (** Inversion *) @@ -174,7 +172,7 @@ Section Facts. Qed. Theorem app_nil_r : forall l:list A, l ++ [] = l. - Proof. + Proof. induction l; simpl; f_equal; auto. Qed. @@ -654,8 +652,6 @@ Section Elts. End Elts. - - (*******************************) (** * Manipulating whole lists *) (*******************************) @@ -858,7 +854,7 @@ End ListOps. (************) Section Map. - Variables A B : Type. + Variables (A : Type) (B : Type). Variable f : A -> B. Fixpoint map (l:list A) : list B := @@ -983,7 +979,7 @@ Qed. (************************************) Section Fold_Left_Recursor. - Variables A B : Type. + Variables (A : Type) (B : Type). Variable f : A -> B -> A. Fixpoint fold_left (l:list B) (a0:A) : A := @@ -1021,7 +1017,7 @@ Qed. (************************************) Section Fold_Right_Recursor. - Variables A B : Type. + Variables (A : Type) (B : Type). Variable f : B -> A -> A. Variable a0 : A. @@ -1211,7 +1207,7 @@ End Fold_Right_Recursor. (******************************************************) Section ListPairs. - Variables A B : Type. + Variables (A : Type) (B : Type). (** [split] derives two lists from a list of pairs *) @@ -2039,3 +2035,5 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) Hint Resolve app_nil_end : datatypes v62. (* end hide *) + +Unset Universe Polymorphism. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 8fd2299171..d75eb384f6 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -11,7 +11,7 @@ Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. - +Set Universe Polymorphism. (** * Logical relations over lists with respect to a setoid equality or ordering. *) @@ -34,7 +34,7 @@ Hint Constructors InA. of the previous one. Having [InA = Exists eqA] raises too many compatibility issues. For now, we only state the equivalence: *) -Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. +Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. Proof. split; induction 1; auto. Qed. Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l. @@ -104,7 +104,7 @@ Hypothesis eqA_equiv : Equivalence eqA. Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). - + Hint Resolve eqarefl eqatrans. Hint Immediate eqasym. @@ -151,7 +151,7 @@ Qed. Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. Proof. - intros l x y H H'. rewrite <- H; auto. + intros l x y H H'. rewrite <- H. auto. Qed. Hint Immediate InA_eqA. @@ -498,7 +498,7 @@ Proof. apply Hrec; auto. inv; auto. eapply NoDupA_split; eauto. - invlist ForallOrdPairs; auto. + invlist ForallOrdPairs; auto. eapply equivlistA_NoDupA_split; eauto. transitivity (f y (fold_right f i (s1++s2))). apply Comp; auto. reflexivity. @@ -819,7 +819,6 @@ intros. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. - Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index b0657b63aa..05f03ea561 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -7,6 +7,7 @@ (***********************************************************************) Require Import SetoidList. +Set Universe Polymorphism. Set Implicit Arguments. Unset Strict Implicit. @@ -88,7 +89,7 @@ Lemma PermutationA_cons_app l l₁ l₂ x : PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂). Proof. intros E. rewrite E. - now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc. + now rewrite app_comm_cons, (PermutationA_cons_append l₁ x), <- app_assoc. Qed. Lemma PermutationA_middle l₁ l₂ x : diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 3837757357..cb61e8f009 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -67,18 +67,13 @@ Variables A B : Prop. Record retract : Prop := {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. - Record retract_cond : Prop := {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. - (** The dependent elimination above implies the axiom of choice: *) -Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. -Proof. -intros r. -case r; simpl. -trivial. -Qed. + +Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a. +Proof. intros r. exact r.(inv2). Qed. End Retracts. @@ -114,7 +109,7 @@ Proof. exists g f. intro a. unfold f, g; simpl. -apply AC. +apply AC. exists (fun x:pow U => x) (fun x:pow U => x). trivial. Qed. @@ -132,9 +127,10 @@ Lemma not_has_fixpoint : R R = Not_b (R R). Proof. unfold R at 1. unfold g. -rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). +rewrite AC. +trivial. +exists (fun x:pow U => x) (fun x:pow U => x). trivial. -exists (fun x:pow U => x) (fun x:pow U => x); trivial. Qed. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index b22f58dadd..57a82161d6 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -96,6 +96,12 @@ Local Unset Intuition Negation Unfolding. (** Choice, reification and description schemes *) +(** We make them all polymorphic. most of them have existentials as conclusion + so they require polymorphism otherwise their first application (e.g. to an + existential in [Set]) will fix the level of [A]. +*) +Set Universe Polymorphism. + Section ChoiceSchemes. Variables A B :Type. @@ -217,39 +223,39 @@ End ChoiceSchemes. (** Generalized schemes *) Notation RelationalChoice := - (forall A B, RelationalChoice_on A B). + (forall A B : Type, RelationalChoice_on A B). Notation FunctionalChoice := - (forall A B, FunctionalChoice_on A B). + (forall A B : Type, FunctionalChoice_on A B). Definition FunctionalDependentChoice := - (forall A, FunctionalDependentChoice_on A). + (forall A : Type, FunctionalDependentChoice_on A). Definition FunctionalCountableChoice := - (forall A, FunctionalCountableChoice_on A). + (forall A : Type, FunctionalCountableChoice_on A). Notation FunctionalChoiceOnInhabitedSet := - (forall A B, inhabited B -> FunctionalChoice_on A B). + (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := - (forall A B, FunctionalRelReification_on A B). + (forall A B : Type, FunctionalRelReification_on A B). Notation GuardedRelationalChoice := - (forall A B, GuardedRelationalChoice_on A B). + (forall A B : Type, GuardedRelationalChoice_on A B). Notation GuardedFunctionalChoice := - (forall A B, GuardedFunctionalChoice_on A B). + (forall A B : Type, GuardedFunctionalChoice_on A B). Notation GuardedFunctionalRelReification := - (forall A B, GuardedFunctionalRelReification_on A B). + (forall A B : Type, GuardedFunctionalRelReification_on A B). Notation OmniscientRelationalChoice := - (forall A B, OmniscientRelationalChoice_on A B). + (forall A B : Type, OmniscientRelationalChoice_on A B). Notation OmniscientFunctionalChoice := - (forall A B, OmniscientFunctionalChoice_on A B). + (forall A B : Type, OmniscientFunctionalChoice_on A B). Notation ConstructiveDefiniteDescription := - (forall A, ConstructiveDefiniteDescription_on A). + (forall A : Type, ConstructiveDefiniteDescription_on A). Notation ConstructiveIndefiniteDescription := - (forall A, ConstructiveIndefiniteDescription_on A). + (forall A : Type, ConstructiveIndefiniteDescription_on A). Notation IotaStatement := - (forall A, IotaStatement_on A). + (forall A : Type, IotaStatement_on A). Notation EpsilonStatement := - (forall A, EpsilonStatement_on A). + (forall A : Type, EpsilonStatement_on A). (** Subclassical schemes *) @@ -293,7 +299,7 @@ Proof. Qed. Lemma funct_choice_imp_rel_choice : - forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B. + forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B FunCh R H. destruct (FunCh R H) as (f,H0). @@ -306,7 +312,7 @@ Proof. Qed. Lemma funct_choice_imp_description : - forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B. + forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. intros A B FunCh R H. destruct (FunCh R) as [f H0]. @@ -319,10 +325,10 @@ Proof. Qed. Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : - forall A B, FunctionalChoice_on A B <-> + forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. - intros A B; split. + intros A B. split. intro H; split; [ exact (funct_choice_imp_rel_choice H) | exact (funct_choice_imp_description H) ]. @@ -363,7 +369,7 @@ Proof. Qed. Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : - forall A B, inhabited B -> RelationalChoice_on A B -> + forall A B : Type, inhabited B -> RelationalChoice_on A B -> IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B. Proof. intros A B Inh AC_rel IndPrem P R H. @@ -375,7 +381,7 @@ Proof. Qed. Lemma guarded_rel_choice_imp_rel_choice : - forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B. + forall A B : Type, GuardedRelationalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B GAC_rel R H. destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)). @@ -794,12 +800,13 @@ be applied on the same Type universes on both sides of the first Require Import Setoid. Theorem constructive_definite_descr_excluded_middle : - ConstructiveDefiniteDescription -> + (forall A : Type, ConstructiveDefiniteDescription_on A) -> (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}). Proof. intros Descr EM P. pose (select := fun b:bool => if b then P else ~P). assert { b:bool | select b } as ([|],HP). + red in Descr. apply Descr. rewrite <- unique_existence; split. destruct (EM P). @@ -815,14 +822,13 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : (forall P:Prop, P \/ ~ P) -> forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. Proof. - intros FunReify EM C; intuition auto using + intros FunReify EM C H. intuition auto using constructive_definite_descr_excluded_middle, (relative_non_contradiction_of_definite_descr (C:=C)). Qed. (**********************************************************************) (** * Choice => Dependent choice => Countable choice *) - (* The implications below are standard *) Require Import Arith. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 87b279877f..0eba49a7e0 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -99,7 +99,7 @@ Lemma AC_bool_subset_to_bool : Proof. destruct (guarded_rel_choice _ _ (fun Q:bool -> Prop => exists y : _, Q y) - (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). + (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). exact (fun _ H => H). exists R; intros P HP. destruct (HR P HP) as (y,(Hy,Huni)). @@ -172,7 +172,7 @@ Variables a1 a2 : A. (** We build the subset [A'] of [A] made of [a1] and [a2] *) -Definition A' := sigT (fun x => x=a1 \/ x=a2). +Definition A' := @sigT A (fun x => x=a1 \/ x=a2). Definition a1':A'. exists a1 ; auto. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 0e9f39f6b4..2c971ec24e 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -52,6 +52,8 @@ Table of contents: Import EqNotations. +Set Universe Polymorphism. + Section Dependent_Equality. Variable U : Type. @@ -117,7 +119,7 @@ Lemma eq_sigT_eq_dep : existT P p x = existT P q y -> eq_dep p x q y. Proof. intros. - dependent rewrite H. + dependent rewrite H. apply eq_dep_intro. Qed. @@ -162,11 +164,12 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent to a dependent pair of equalities *) +(** Dependent equality is equivalent tco a dependent pair of equalities *) Set Implicit Arguments. -Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}. +Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> + {H:x1=x2 | rew H in H1 = H2}. Proof. intros; split; intro H. - change x2 with (projT1 (existT P x2 H2)). @@ -191,7 +194,7 @@ Lemma eq_sigT_snd : forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2. Proof. intros. - unfold eq_sigT_fst. + unfold eq_sigT_fst. change x2 with (projT1 (existT P x2 H2)). change H2 with (projT2 (existT P x2 H2)) at 3. destruct H. @@ -271,8 +274,8 @@ Section Equivalences. Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. Proof. intros eq_rect_eq; red; intros. - apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial. - Qed. + apply (eq_rect_eq__eq_dep1_eq eq_rect_eq). apply eq_dep_dep1; trivial. + Qed. (** Uniqueness of Identity Proofs (UIP) is a consequence of *) (** Injectivity of Dependent Equality *) diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 53b25d4a86..e4db81fafe 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -35,6 +35,7 @@ Table of contents: (** * Streicher's K and injectivity of dependent pair hold on decidable types *) Set Implicit Arguments. +Set Universe Polymorphism. Section EqdepDec. @@ -203,7 +204,7 @@ Unset Implicit Arguments. Module Type DecidableType. - Parameter U:Type. + Monomorphic Parameter U:Type. Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. End DecidableType. @@ -271,7 +272,7 @@ End DecidableEqDep. Module Type DecidableSet. - Parameter U:Type. + Parameter U:Set. Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. End DecidableSet. @@ -294,23 +295,23 @@ Module DecidableEqDepSet (M:DecidableSet). Theorem eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y. - Proof N.eq_dep_eq. + Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). (** Uniqueness of Identity Proofs (UIP) *) Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2. - Proof N.UIP. + Proof (eq_dep_eq__UIP U eq_dep_eq). (** Uniqueness of Reflexive Identity Proofs *) Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x. - Proof N.UIP_refl. + Proof (UIP__UIP_refl U UIP). (** Streicher's axiom K *) Lemma Streicher_K : forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. - Proof N.Streicher_K. + Proof (K_dec_type eq_dec). (** Proof-irrelevance on subsets of decidable sets *) @@ -350,7 +351,7 @@ Qed. Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt. Proof. - change (match tt as b return tt = b -> Type with + change (match tt as b return tt = b -> Prop with | tt => fun x => x = eq_refl tt end x). destruct x; reflexivity. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 530e05559d..b557a78672 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -28,9 +28,11 @@ Arguments JMeq_refl {A x} , [A] x. Hint Resolve JMeq_refl. +Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. + Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. -Proof. -destruct 1; trivial. +Proof. +intros; destruct H; trivial. Qed. Hint Immediate JMeq_sym. diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 4f0d93fb9b..843b9aaa7b 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -856,7 +856,7 @@ intros. rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto. -intros; do 3 (rewrite fold_add; auto with *). +intros. do 3 (rewrite fold_add; auto with *). do 3 rewrite fold_empty;auto. Qed. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index bd88116899..a61ef8bcd9 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -595,7 +595,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O. (** Specification of [lt] *) Instance lt_strorder : StrictOrder lt. Proof. constructor ; unfold lt; red. - unfold complement. red. intros. apply (irreflexivity H). + unfold complement. red. intros. apply (irreflexivity _ H). intros. transitivity y; auto. Qed. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index b0e09b719d..5c232f3400 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -472,7 +472,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. equal s s' = true <-> Equal s s'. Proof. induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl. - intuition. + intuition reflexivity. split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv. split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv. inv. @@ -820,7 +820,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s'). Proof. - induction s as [|x s IH]; intros [|x' s']; simpl; intuition. + induction s as [|x s IH]; intros [|x' s']; simpl; intuition. elim_compare x x'; auto. Qed. diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index f3a1d39c9b..25a8c16292 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -93,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Module E:=PositiveOrderedTypeBits. - Definition elt := positive. + Definition elt := positive : Type. Inductive tree := | Leaf : tree @@ -101,9 +101,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Scheme tree_ind := Induction for tree Sort Prop. - Definition t := tree. + Definition t := tree : Type. - Definition empty := Leaf. + Definition empty : t := Leaf. Fixpoint is_empty (m : t) : bool := match m with @@ -142,7 +142,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** helper function to avoid creating empty trees that are not leaves *) - Definition node l (b: bool) r := + Definition node (l : t) (b: bool) (r : t) : t := if b then Node l b r else match l,r with | Leaf,Leaf => Leaf @@ -159,7 +159,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint union (m m': t) := + Fixpoint union (m m': t) : t := match m with | Leaf => m' | Node l o r => @@ -169,7 +169,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint inter (m m': t) := + Fixpoint inter (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -179,7 +179,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint diff (m m': t) := + Fixpoint diff (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -211,7 +211,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** reverses [y] and concatenate it with [x] *) - Fixpoint rev_append y x := + Fixpoint rev_append (y x : elt) : elt := match y with | 1 => x | y~1 => rev_append y x~1 @@ -262,14 +262,14 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end. Definition exists_ m := xexists m 1. - Fixpoint xfilter (m : t) (i : positive) := + Fixpoint xfilter (m : t) (i : positive) : t := match m with | Leaf => Leaf | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1) end. Definition filter m := xfilter m 1. - Fixpoint xpartition (m : t) (i : positive) := + Fixpoint xpartition (m : t) (i : positive) : t * t := match m with | Leaf => (Leaf,Leaf) | Node l o r => @@ -311,7 +311,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** would it be more efficient to use a path like in the above functions ? *) - Fixpoint choose (m: t) := + Fixpoint choose (m: t) : option elt := match m with | Leaf => None | Node l o r => if o then Some 1 else @@ -321,7 +321,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint min_elt (m: t) := + Fixpoint min_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -331,7 +331,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint max_elt (m: t) := + Fixpoint max_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -805,7 +805,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. rewrite <- andb_lazy_alt. apply andb_true_iff. Qed. - Lemma filter_spec: forall s x f, compat_bool E.eq f -> + Lemma filter_spec: forall s x f, @compat_bool elt E.eq f -> (In x (filter f s) <-> In x s /\ f x = true). Proof. intros. apply xfilter_spec. Qed. @@ -830,7 +830,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. apply H. assumption. Qed. - Lemma for_all_spec: forall s f, compat_bool E.eq f -> + Lemma for_all_spec: forall s f, @compat_bool elt E.eq f -> (for_all f s = true <-> For_all (fun x => f x = true) s). Proof. intros. apply xforall_spec. Qed. @@ -852,7 +852,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. intros [[x|x|] H]; eauto. Qed. - Lemma exists_spec : forall s f, compat_bool E.eq f -> + Lemma exists_spec : forall s f, @compat_bool elt E.eq f -> (exists_ f s = true <-> Exists (fun x => f x = true) s). Proof. intros. apply xexists_spec. Qed. @@ -868,11 +868,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o; simpl; rewrite IHl, IHr; reflexivity. Qed. - Lemma partition_spec1 : forall s f, compat_bool E.eq f -> + Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f -> Equal (fst (partition f s)) (filter f s). Proof. intros. rewrite partition_filter. reflexivity. Qed. - Lemma partition_spec2 : forall s f, compat_bool E.eq f -> + Lemma partition_spec2 : forall s f, @compat_bool elt E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). Proof. intros. rewrite partition_filter. reflexivity. Qed. @@ -1079,7 +1079,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct (min_elt r). injection H. intros <-. clear H. destruct y as [z|z|]. - apply (IHr p z); trivial. + apply (IHr e z); trivial. elim (Hp _ H'). discriminate. discriminate. @@ -1133,7 +1133,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. injection H. intros <-. clear H. destruct y as [z|z|]. elim (Hp _ H'). - apply (IHl p z); trivial. + apply (IHl e z); trivial. discriminate. discriminate. Qed. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f0cddcc387..d8f675ade7 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -1047,7 +1047,7 @@ Qed. (** ** Filter *) -Lemma filter_app A f (l l':list A) : +Polymorphic Lemma filter_app A f (l l':list A) : List.filter f (l ++ l') = List.filter f l ++ List.filter f l'. Proof. induction l as [|x l IH]; simpl; trivial. @@ -1196,7 +1196,7 @@ Lemma INV_rev l1 l2 acc : Proof. intros. rewrite rev_append_rev. apply SortA_app with X.eq; eauto with *. - intros x y. inA. eapply l1_lt_acc; eauto. + intros x y. inA. eapply @l1_lt_acc; eauto. Qed. (** ** union *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 39e086c311..17c69d226f 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -93,7 +93,7 @@ Module ZnZ. lor : t -> t -> t; land : t -> t -> t; lxor : t -> t -> t }. - + Section Specs. Context {t : Type}{ops : Ops t}. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index 809169a4df..a6bc446823 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -809,7 +809,7 @@ refine refine (@spec_ww_sqrt t w_is_even w_0 w_1 w_Bm1 w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits w_sqrt2 pred add_mul_div head0 compare - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. + _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto. exact ZnZ.spec_zdigits. exact ZnZ.spec_more_than_1_digit. exact ZnZ.spec_is_even. @@ -846,7 +846,7 @@ refine intros (Hn,Hn'). assert (E : ZnZ.to_Z y = [|WW x y|] mod wB). { simpl; symmetry. - rewrite Z.add_comm, Z.mod_add; auto with zarith. + rewrite Z.add_comm, Z.mod_add; auto with zarith nocore. apply Z.mod_small; eauto with ZnZ zarith. } rewrite E. unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto. @@ -923,6 +923,7 @@ refine End Z_2nZ. + Section MulAdd. Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 8525b0e13e..dddae7db50 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -211,8 +211,7 @@ Section DoubleDiv32. Variable w_div21 : w -> w -> w -> w*w. Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w). - Definition w_div32 a1 a2 a3 b1 b2 := - Eval lazy beta iota delta [ww_add_c_cont ww_add] in + Definition w_div32_body a1 a2 a3 b1 b2 := match w_compare a1 b1 with | Lt => let (q,r) := w_div21 a1 a2 b1 in @@ -233,6 +232,10 @@ Section DoubleDiv32. | Gt => (w_0, W0) (* cas absurde *) end. + Definition w_div32 a1 a2 a3 b1 b2 := + Eval lazy beta iota delta [ww_add_c_cont ww_add w_div32_body] in + w_div32_body a1 a2 a3 b1 b2. + (* Proof *) Variable w_digits : positive. @@ -312,26 +315,8 @@ Section DoubleDiv32. assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits). Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2. rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r. - change (w_div32 a1 a2 a3 b1 b2) with - match w_compare a1 b1 with - | Lt => - let (q,r) := w_div21 a1 a2 b1 in - match ww_sub_c (w_WW r a3) (w_mul_c q b2) with - | C0 r1 => (q,r1) - | C1 r1 => - let q := w_pred q in - ww_add_c_cont w_WW w_add_c w_add_carry_c - (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2))) - (fun r2 => (q,r2)) - r1 (WW b1 b2) - end - | Eq => - ww_add_c_cont w_WW w_add_c w_add_carry_c - (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2))) - (fun r => (w_Bm1,r)) - (WW (w_sub a2 b2) a3) (WW b1 b2) - | Gt => (w_0, W0) (* cas absurde *) - end. + change (w_div32 a1 a2 a3 b1 b2) with (w_div32_body a1 a2 a3 b1 b2). + unfold w_div32_body. rewrite spec_compare. case Z.compare_spec; intro Hcmp. simpl in Hlt. rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index df5d42bbce..7894363345 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v @@ -692,7 +692,7 @@ intros x; case x; simpl ww_is_even. intros x y H; unfold ww_sqrt2. repeat match goal with |- context[split ?x] => generalize (spec_split x); case (split x) - end; simpl fst; simpl snd. + end; simpl @fst; simpl @snd. intros w0 w1 Hw0 w2 w3 Hw1. assert (U: wB/4 <= [|w2|]). case (Z.le_gt_cases (wB / 4) [|w2|]); auto; intros H1. @@ -1193,7 +1193,7 @@ Qed. rewrite <- wwB_4_wB_4; auto. generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith. case (w_sqrt2 w0 w1); intros w2 c. - simpl ww_to_Z; simpl fst. + simpl ww_to_Z; simpl @fst. case c; unfold interp_carry; autorewrite with rm10. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3);auto with zarith. @@ -1256,7 +1256,7 @@ Qed. generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith. case (w_sqrt2 w0 w1); intros w2 c. case (spec_to_Z w2); intros HH1 HH2. - simpl ww_to_Z; simpl fst. + simpl ww_to_Z; simpl @fst. assert (Hv3: [[ww_pred ww_zdigits]] = Zpos (xO w_digits) - 1). rewrite spec_ww_pred; rewrite spec_ww_zdigits. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 03fc58c55f..634ff7d636 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -623,7 +623,7 @@ Section Basics. rewrite i2l_length; omega. generalize (firstn_length (size-n) (i2l x)). rewrite i2l_length. - intros H0 H1; rewrite H1 in H0. + intros H0 H1. rewrite H1 in H0. rewrite min_l in H0 by omega. simpl length in H0. omega. @@ -882,16 +882,16 @@ Section Basics. destruct p; simpl snd. specialize IHn with p. - destruct (p2ibis n p). simpl snd in *. -rewrite nshiftr_S_tail. + destruct (p2ibis n p). simpl @snd in *. + rewrite nshiftr_S_tail. destruct (le_lt_dec size n). rewrite nshiftr_above_size; auto. assert (H:=nshiftr_0_firstl _ _ l IHn). replace (shiftr (twice_plus_one i)) with i; auto. - destruct i; simpl in *; rewrite H; auto. + destruct i; simpl in *. rewrite H; auto. specialize IHn with p. - destruct (p2ibis n p); simpl snd in *. + destruct (p2ibis n p); simpl @snd in *. rewrite nshiftr_S_tail. destruct (le_lt_dec size n). rewrite nshiftr_above_size; auto. @@ -945,7 +945,7 @@ rewrite nshiftr_S_tail. intros. simpl p2ibis; destruct p; [ | | red; auto]; specialize IHn with p; - destruct (p2ibis n p); simpl snd in *; simpl phi_inv_positive; + destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive; rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice; replace (S (size - S n))%nat with (size - n)%nat by omega; apply IHn; omega. @@ -1629,7 +1629,7 @@ Section Int31_Specs. Lemma spec_pos_mod : forall w p, [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]). Proof. - unfold ZnZ.pos_mod, int31_ops, compare31. + unfold int31_ops, ZnZ.pos_mod, compare31. change [|31|] with 31%Z. assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p). intros. @@ -1959,7 +1959,7 @@ Section Int31_Specs. Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|]. intros Hj; generalize (spec_div i j Hj). - case div31; intros q r; simpl fst. + case div31; intros q r; simpl @fst. intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith. rewrite H1; ring. Qed. @@ -2094,7 +2094,7 @@ Section Int31_Specs. generalize (spec_div21 ih il j Hj Hj1). case div3121; intros q r (Hq, Hr). apply Zdiv_unique with (phi r); auto with zarith. - simpl fst; apply eq_trans with (1 := Hq); ring. + simpl @fst; apply eq_trans with (1 := Hq); ring. Qed. Lemma sqrt312_step_correct rec ih il j: @@ -2215,6 +2215,9 @@ Section Int31_Specs. apply Nat2Z.is_nonneg. Qed. + (* Avoid expanding [iter312_sqrt] before variables in the context. *) + Strategy 1 [iter312_sqrt]. + Lemma spec_sqrt2 : forall x y, wB/ 4 <= [|x|] -> let (s,r) := sqrt312 x y in diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 0e9323789a..1e6593b101 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -95,7 +95,7 @@ Proof. intros. generalize (Even_or_Odd n) (Even_Odd_False n). rewrite <- even_spec, <- odd_spec. - destruct (odd n), (even n); simpl; intuition. + destruct (odd n), (even n) ; simpl; intuition. Qed. Lemma negb_even : forall n, negb (even n) = odd n. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 8146fd014f..6b6c853104 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -438,7 +438,7 @@ Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. - intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx. + intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. Qed. (** The spec of [sqrt_up] indeed determines it *) diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 621a2ed9c8..adbbc5ea01 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -133,7 +133,6 @@ Proof. intros m n; unfold ltb at 1. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. (* Above, we rewrite applications of function. Is it possible to rewrite diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 67cab5507b..f98e8da9a7 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -13,7 +13,7 @@ and proves its properties *) Require Export NSub. -Ltac f_equiv' := repeat (f_equiv; try intros ? ? ?; auto). +Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto). Module NStrongRecProp (Import N : NAxiomsRecSig'). Include NSubProp N. @@ -82,7 +82,6 @@ Proof. intros. unfold strong_rec0. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. Lemma strong_rec_0 : forall a, diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 93ae858d85..bfbcb9465e 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -242,8 +242,8 @@ Module Make (W0:CyclicType) <: NType. Definition comparen_m n : forall m, word (dom_t n) (S m) -> dom_t n -> comparison := let op := dom_op n in - let zero := @ZnZ.zero _ op in - let compare := @ZnZ.compare _ op in + let zero := ZnZ.zero (Ops:=op) in + let compare := ZnZ.compare (Ops:=op) in let compare0 := compare zero in fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m). @@ -273,7 +273,7 @@ Module Make (W0:CyclicType) <: NType. Local Notation compare_folded := (iter_sym _ - (fun n => @ZnZ.compare _ (dom_op n)) + (fun n => ZnZ.compare (Ops:=dom_op n)) comparen_m comparenm CompOpp). @@ -358,13 +358,13 @@ Module Make (W0:CyclicType) <: NType. Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t := let op := dom_op n in - let zero := @ZnZ.zero _ op in - let succ := @ZnZ.succ _ op in - let add_c := @ZnZ.add_c _ op in - let mul_c := @ZnZ.mul_c _ op in + let zero := ZnZ.zero in + let succ := ZnZ.succ (Ops:=op) in + let add_c := ZnZ.add_c (Ops:=op) in + let mul_c := ZnZ.mul_c (Ops:=op) in let ww := @ZnZ.WW _ op in let ow := @ZnZ.OW _ op in - let eq0 := @ZnZ.eq0 _ op in + let eq0 := ZnZ.eq0 in let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in fun m x y => @@ -464,13 +464,13 @@ Module Make (W0:CyclicType) <: NType. Definition wn_divn1 n := let op := dom_op n in let zd := ZnZ.zdigits op in - let zero := @ZnZ.zero _ op in - let ww := @ZnZ.WW _ op in - let head0 := @ZnZ.head0 _ op in - let add_mul_div := @ZnZ.add_mul_div _ op in - let div21 := @ZnZ.div21 _ op in - let compare := @ZnZ.compare _ op in - let sub := @ZnZ.sub _ op in + let zero := ZnZ.zero in + let ww := ZnZ.WW in + let head0 := ZnZ.head0 in + let add_mul_div := ZnZ.add_mul_div in + let div21 := ZnZ.div21 in + let compare := ZnZ.compare in + let sub := ZnZ.sub in let ddivn1 := DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v). @@ -633,12 +633,12 @@ Module Make (W0:CyclicType) <: NType. Definition wn_modn1 n := let op := dom_op n in let zd := ZnZ.zdigits op in - let zero := @ZnZ.zero _ op in - let head0 := @ZnZ.head0 _ op in - let add_mul_div := @ZnZ.add_mul_div _ op in - let div21 := @ZnZ.div21 _ op in - let compare := @ZnZ.compare _ op in - let sub := @ZnZ.sub _ op in + let zero := ZnZ.zero in + let head0 := ZnZ.head0 in + let add_mul_div := ZnZ.add_mul_div in + let div21 := ZnZ.div21 in + let compare := ZnZ.compare in + let sub := ZnZ.sub in let dmodn1 := DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in fun m x y => reduce n (dmodn1 (S m) x y). diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index b28ce15b99..8df4b7c645 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -324,8 +324,13 @@ pr " Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z. Proof. - do_size (destruct n; [exact ZnZ.spec_0|]). - destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0. + do_size (destruct n; + [match goal with + |- @eq Z (_ (zeron ?n)) _ => + apply (ZnZ.spec_0 (Specs:=dom_spec n)) + end|]). + destruct n; auto. simpl. rewrite make_op_S. fold word. + apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))). Qed. (** * Digits *) diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 167be6d70c..d9f4b04297 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -627,7 +627,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. assert (Hz := spec_irred_zero nx dy). assert (Hz':= spec_irred_zero ny dx). destruct irred as (n1,d1); destruct irred as (n2,d2). - simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. + simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. rewrite spec_norm_denum. qsimpl. @@ -665,7 +665,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. assert (Hgc := strong_spec_irred nx dy). assert (Hgc' := strong_spec_irred ny dx). destruct irred as (n1,d1); destruct irred as (n2,d2). - simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. + simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. unfold norm_denum; qsimpl. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index aed4fef05e..22f3dcd64e 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -375,7 +375,7 @@ Fixpoint gcdn (n : nat) (a b : positive) : positive := Definition gcd (a b : positive) := gcdn (size_nat a + size_nat b)%nat a b. (** Generalized Gcd, also computing the division of a and b by the gcd *) - +Set Printing Universes. Fixpoint ggcdn (n : nat) (a b : positive) : (positive*(positive*positive)) := match n with | O => (1,(a,b)) diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 22436de690..ab1eccee20 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -15,6 +15,8 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) +Set Universe Polymorphism. + (** The polymorphic identity function is defined in [Datatypes]. *) Arguments id {A} x. @@ -45,7 +47,7 @@ Definition const {A B} (a : A) := fun _ : B => a. (** The [flip] combinator reverses the first two arguments of a function. *) -Definition flip {A B C} (f : A -> B -> C) x y := f y x. +Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x. (** Application as a combinator. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 323e80cc39..96345e1547 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -263,7 +263,7 @@ Class DependentEliminationPackage (A : Type) := Ltac elim_tac tac p := let ty := type of p in - let eliminator := eval simpl in (elim (A:=ty)) in + let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in tac p eliminator. (** Specialization to do case analysis or induction. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index f6d795b94e..d82fa602aa 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -153,7 +153,7 @@ Section Fix_rects. Hypothesis equiv_lowers: forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)), - (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) -> + (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) -> f g = f h. (* From equiv_lowers, it follows that @@ -231,10 +231,10 @@ Module WfExtensionality. Program Lemma fix_sub_eq_ext : forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Type) - (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x), + (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y). + F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)). Proof. intros ; apply Fix_eq ; auto. intros. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index e395e4d035..e777c74d37 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -460,13 +460,13 @@ Proof. induction n; simpl; auto with qarith. rewrite IHn; auto with qarith. Qed. - +Transparent Qred. Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. Proof. destruct n; simpl. destruct 1; auto. intros. - now apply Qc_is_canon. + now apply Qc_is_canon. Qed. Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 4a826f6910..f363fd7c28 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -167,14 +167,13 @@ Qed. Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R. Proof. -unfold Qinv, Q2R, Qeq; intros (x1, x2); unfold Qden, Qnum. -case x1. +unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. -intros; field; auto. +intros; field; auto. intros; change (IZR (Zneg x2)) with (- IZR (' x2))%R; change (IZR (Zneg p)) with (- IZR (' p))%R; - field; (*auto 8 with real.*) + simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 3c15a30532..b2d9c749fd 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -442,7 +442,7 @@ Proof. apply (Rabs_pos_lt _ H0). ring. assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro. - intro; rewrite <- H7; unfold dist, R_met; unfold R_dist; + intro; rewrite <- H7. unfold R_met, dist; unfold R_dist; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rabs_pos_lt. unfold Rdiv; apply prod_neq_R0; diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index d876b5d8e0..0614f39982 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -695,7 +695,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. exists deltatemp ; exact Htemp. elim (Hf_deriv eps eps_pos). intros deltatemp Htemp. - red in Hlinv ; red in Hlinv ; simpl dist in Hlinv ; unfold R_dist in Hlinv. + red in Hlinv ; red in Hlinv ; unfold dist in Hlinv ; unfold R_dist in Hlinv. assert (Hlinv' := Hlinv (fun h => (f (y+h) - f y)/h) (fun h => h <>0) l 0). unfold limit1_in, limit_in, dist in Hlinv' ; simpl in Hlinv'. unfold R_dist in Hlinv'. assert (Premisse : (forall eps : R, diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 658ffd12f4..3d52a98cd0 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -164,7 +164,7 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X') eps > 0 -> exists alp : R, alp > 0 /\ - (forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps). + (forall x:Base X, D x /\ X.(dist) x x0 < alp -> X'.(dist) (f x) l < eps). (*******************************) (** ** R is a metric space *) @@ -191,9 +191,9 @@ Lemma tech_limit : Proof. intros f D l x0 H H0. case (Rabs_pos (f x0 - l)); intros H1. - absurd (dist R_met (f x0) l < dist R_met (f x0) l). + absurd (R_met.(@dist) (f x0) l < R_met.(@dist) (f x0) l). apply Rlt_irrefl. - case (H0 (dist R_met (f x0) l)); auto. + case (H0 (R_met.(@dist) (f x0) l)); auto. intros alpha1 [H2 H3]; apply H3; auto; split; auto. case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto. case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto. @@ -345,8 +345,9 @@ Lemma single_limit : adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'. Proof. unfold limit1_in; unfold limit_in; intros. + simpl in *. cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps). - clear H0 H1; unfold dist; unfold R_met; unfold R_dist; + clear H0 H1; simpl @dist; unfold R_met; unfold R_dist, dist; unfold Rabs; case (Rcase_abs (l - l')); intros. cut (forall eps:R, eps > 0 -> - (l - l') < eps). intro; generalize (prop_eps (- (l - l')) H1); intro; @@ -356,7 +357,7 @@ Proof. intros; cut (eps * / 2 > 0). intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). - elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. + elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro; unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3); intro; elim (Rplus_ne 1); intros a b; rewrite a in H4; diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index f05539379f..7e020dd414 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -339,7 +339,7 @@ Proof. unfold neighbourhood in H4; elim H4; intros del H5. exists (pos del); split. apply (cond_pos del). - intros; unfold included in H5; apply H5; elim H6; intros; apply H8. + intros. unfold included in H5; apply H5; elim H6; intros; apply H8. unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. apply disc_P1. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 5140c29c19..6ff3fa8b8e 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -361,7 +361,7 @@ Proof with trivial. replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with (sum_f_R0 (fun k:nat => An k * Bn k) n + sum_f_R0 (fun k:nat => An k * - l) n)... - rewrite <- (scal_sum An n (- l)); field... + rewrite <- (scal_sum An n (- l)); field... rewrite <- plus_sum; apply sum_eq; intros; ring... Qed. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 058eec3da3..5ab6f38245 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -32,9 +32,9 @@ Section Bounds. Variable U : Type. Variable D : PO U. - Let C := Carrier_of U D. + Let C := @Carrier_of U D. - Let R := Rel_of U D. + Let R := @Rel_of U D. Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop := Upper_Bound_definition : @@ -103,6 +103,6 @@ Section Specific_orders. Record Chain : Type := Definition_of_chain {PO_of_chain : PO U; - Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}. + Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}. End Specific_orders. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 054164da57..8d97e32084 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -61,7 +61,7 @@ Section Partial_order_facts. Lemma Strict_Rel_Transitive_with_Rel : forall x y z:U, - Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z. + Strict_Rel_of U D x y -> @Rel_of U D y z -> Strict_Rel_of U D x z. Proof. unfold Strict_Rel_of at 1. red. @@ -77,7 +77,7 @@ Section Partial_order_facts. Lemma Strict_Rel_Transitive_with_Rel_left : forall x y z:U, - Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z. + @Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z. Proof. unfold Strict_Rel_of at 1. red. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index acad98e5fe..899acfc648 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -16,6 +16,7 @@ Require Import List Setoid Compare_dec Morphisms FinFun. Import ListNotations. (* For notations [] and [a;b;c] *) Set Implicit Arguments. +Set Universe Polymorphism. Section Permutation. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 03952c95a3..a89b90238e 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -20,6 +20,8 @@ Require Import List Relations Relations_1. +Set Universe Polymorphism. + (** Preambule *) Set Implicit Arguments. diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 79e817717a..f85222dfb4 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -80,13 +80,13 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. - unfold eqke; induction 1; intuition. + unfold eqke; induction 1; intuition. Qed. Hint Resolve InA_eqke_eqk. Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto with *. + intros; apply InA_eqA with p; auto with *. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index eb53738591..747d03f8a0 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -126,14 +126,14 @@ Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation. [EqualityType] and [DecidableType] *) Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E. - Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv. - Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv. - Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv. + Definition eq_refl := F.eq_equiv.(@Equivalence_Reflexive _ _). + Definition eq_sym := F.eq_equiv.(@Equivalence_Symmetric _ _). + Definition eq_trans := F.eq_equiv.(@Equivalence_Transitive _ _). End BackportEq. Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E. Instance eq_equiv : Equivalence E.eq. - Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed. + Proof. exact (Build_Equivalence _ F.eq_refl F.eq_sym F.eq_trans). Qed. End UpdateEq. Module Backport_ET (E:EqualityType) <: EqualityTypeBoth diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index ffd0649afc..a0ee4caaa5 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -440,7 +440,7 @@ Qed. Lemma max_min_antimono f : Proper (eq==>eq) f -> - Proper (le==>inverse le) f -> + Proper (le==>flip le) f -> forall x y, max (f x) (f y) == f (min x y). Proof. intros Eqf Lef x y. @@ -452,7 +452,7 @@ Qed. Lemma min_max_antimono f : Proper (eq==>eq) f -> - Proper (le==>inverse le) f -> + Proper (le==>flip le) f -> forall x y, min (f x) (f y) == f (max x y). Proof. intros Eqf Lef x y. @@ -557,11 +557,11 @@ Module UsualMinMaxLogicalProperties forall x y, min (f x) (f y) = f (min x y). Proof. intros; apply min_mono; auto. congruence. Qed. - Lemma min_max_antimonotone f : Proper (le ==> inverse le) f -> + Lemma min_max_antimonotone f : Proper (le ==> flip le) f -> forall x y, min (f x) (f y) = f (max x y). Proof. intros; apply min_max_antimono; auto. congruence. Qed. - Lemma max_min_antimonotone f : Proper (le ==> inverse le) f -> + Lemma max_min_antimonotone f : Proper (le ==> flip le) f -> forall x y, max (f x) (f y) = f (min x y). Proof. intros; apply max_min_antimono; auto. congruence. Qed. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index fa08f93666..fb28e0cfcb 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -328,7 +328,7 @@ Module KeyOrderedType(O:OrderedType). Proof. split; eauto. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. + Proof. constructor; eauto. intros x; apply (irreflexivity (fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 2e9c0cf562..88fbd8c11c 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -31,7 +31,7 @@ Module Type CompareFacts (Import O:DecStrOrder'). Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y. Proof. - case compare_spec; intro H; split; try easy; intro LT; + case compare_spec; intro H; split; try easy; intro LT; contradict LT; rewrite H; apply irreflexivity. Qed. @@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). Instance le_order : PartialOrder eq le. Proof. compute; iorder. Qed. - Instance le_antisym : Antisymmetric _ eq le. + Instance le_antisym : Antisymmetric eq le. Proof. apply partial_order_antisym; auto with *. Qed. Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 68ffc379d1..475a25a413 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -29,7 +29,7 @@ Set Implicit Arguments. [le x y -> le y z -> le x z]. *) -Inductive ord := OEQ | OLT | OLE. +Inductive ord : Set := OEQ | OLT | OLE. Definition trans_ord o o' := match o, o' with | OEQ, _ => o' @@ -70,7 +70,7 @@ Lemma le_refl : forall x, x<=x. Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed. Lemma lt_irrefl : forall x, ~ x<x. -Proof. intros; apply StrictOrder_Irreflexive. Qed. +Proof. intros. apply StrictOrder_Irreflexive. Qed. (** Symmetry rules *) @@ -100,8 +100,9 @@ Local Notation "#" := interp_ord. Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. Proof. -destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition; - subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. +destruct o, o'; simpl; intros x y z; +rewrite ?P.le_lteq; intuition auto; +subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z. diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index f57726bea7..1c4c16cc11 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -24,7 +24,7 @@ Inductive t : nat -> Set := Section SCHEMES. Definition case0 P (p: t 0): P p := - match p with | F1 | FS _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end. + match p with | F1 | FS _ => fun devil => False_rect (@IDProp) devil (* subterm !!! *) end. Definition caseS (P: forall {n}, t (S n) -> Type) (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p)) diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 8f672dedad..f12aa0b871 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -21,6 +21,8 @@ Require Vectors.Fin. Import EqNotations. Local Open Scope nat_scope. +Set Universe Polymorphism. + (** A vector is a list of size n whose elements belong to a set A. *) @@ -43,10 +45,10 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type) |@cons _ a 0 v => match v with |nil _ => bas a - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end |@cons _ a (S nn') v => rect a v (rectS_fix v) - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end. (** An induction scheme for 2 vectors of same length *) @@ -60,13 +62,13 @@ match v1 as v1' in t _ n1 |[] => fun v2 => match v2 with |[] => bas - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end |h1 :: t1 => fun v2 => match v2 with |h2 :: t2 => fun t1' => rect (rect2_fix t1' t2) h1 h2 - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end t1 end. @@ -74,7 +76,7 @@ end. Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v := match v with |[] => H - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end. (** A vector of length [S _] is [cons] *) @@ -82,7 +84,7 @@ Definition caseS {A} (P : forall {n}, t A (S n) -> Type) (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v := match v with |h :: t => H h t - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end. End SCHEMES. @@ -245,11 +247,11 @@ fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A := match v in t _ n0 return t C n0 -> A with |[] => fun w => match w with |[] => a - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end |@cons _ vh vn vt => fun w => match w with |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt - |_ => fun devil => False_rect (@ID) devil (* subterm !!! *) + |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *) end vt end. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index ed2b56d1f8..3e8c1175ff 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -105,7 +105,7 @@ Proof. assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). induction v0. now simpl. - intros; simpl. rewrite<- IHv0. now f_equal. + intros; simpl. rewrite<- IHv0, assoc. now f_equal. induction v. reflexivity. simpl. intros; now rewrite<- (IHv). diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 24f5d308aa..28288c0cb5 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -130,7 +130,7 @@ Section Wf_Lexicographic_Exponentiation. match goal with [ |- clos_refl_trans ?A ?R ?x ?y ] => cut (clos_refl A R x y) end. intros; inversion H8; subst; [apply rt_step|apply rt_refl]; assumption. generalize H1. - rewrite H4; intro. + setoid_rewrite H4; intro. generalize (app_inj_tail _ _ _ _ H8); simple induction 1. intros. @@ -182,7 +182,8 @@ Section Wf_Lexicographic_Exponentiation. Descl x0 /\ Descl y0). intro. - generalize (app_nil_end x1); simple induction 1; simple induction 1. + generalize (app_nil_end x1). + simple induction 1; simple induction 1. split. apply d_conc; auto with sets. apply d_nil. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 3935e12489..f1bfb027f1 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -151,9 +151,7 @@ Section Efficient_Rec. forall P:Z -> Prop, (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) -> forall x:Z, 0 <= x -> P x. - Proof. - exact Zlt_0_rec. - Qed. + Proof. intros; now apply Zlt_0_rec. Qed. (** Obsolete version of [Z.lt] induction principle on non-negative numbers *) @@ -170,7 +168,7 @@ Section Efficient_Rec. (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) -> forall x:Z, 0 <= x -> P x. Proof. - exact Z_lt_rec. + intros; now apply Z_lt_rec. Qed. (** An even more general induction principle using [Z.lt]. *) @@ -196,7 +194,7 @@ Section Efficient_Rec. (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) -> forall x:Z, z <= x -> P x. Proof. - exact Zlt_lower_bound_rec. + intros; now apply Zlt_lower_bound_rec with z. Qed. End Efficient_Rec. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index b4163ef996..a5e7105041 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -53,10 +53,11 @@ Theorem Z_lt_abs_rec : forall n:Z, P n. Proof. intros P HP p. - set (Q := fun z => 0 <= z -> P z * P (- z)) in *. - cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q; clear Q; intros. + set (Q := fun z => 0 <= z -> P z * P (- z)). + cut (Q (Z.abs p)); [ intros H | apply (Z_lt_rec Q); auto with zarith ]. + elim (Zabs_dec p); intro eq; rewrite eq; + elim H; auto with zarith. + intros x H; subst Q. split; apply HP. rewrite Z.abs_eq; auto; intros. elim (H (Z.abs m)); intros; auto with zarith. |