From 15999903f875f4b5dbb3d5240d2ca39acc3cd777 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 26 May 2014 13:58:56 +0200 Subject: - Fix in kernel conversion not folding the universe constraints correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes. --- theories/Classes/CEquivalence.v | 4 ++-- theories/Classes/CMorphisms.v | 43 ----------------------------------------- 2 files changed, 2 insertions(+), 45 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index b540feabf..8610f18c3 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -107,11 +107,11 @@ Section Respecting. Definition respecting `(eqa : Equivalence A (R : crelation A), eqb : Equivalence B (R' : crelation B)) : Type := - { morph : A -> B | respectful R R' morph morph }. + { 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)). + forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)). Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 4b031f949..b1c2842f7 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -192,10 +192,6 @@ Section Relations. 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. @@ -300,16 +296,6 @@ Section GenericInstances. (** 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. @@ -322,15 +308,6 @@ Section GenericInstances. (** 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. @@ -379,15 +356,6 @@ Section GenericInstances. (** 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. @@ -669,17 +637,6 @@ Qed. (** A [PartialOrder] is compatible with its underlying equivalence. *) Require Import Relation_Definitions. -Instance PartialOrder_proper `(PartialOrder A eqA (R : crelation 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. -- cgit v1.2.3