diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-26 13:58:56 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-26 14:16:26 +0200 |
commit | 15999903f875f4b5dbb3d5240d2ca39acc3cd777 (patch) | |
tree | 9906d3cf7d95d4d3f0e996811aa429532b825f0d /theories | |
parent | d8176e6baaa33692ed82b9ac3c6e57e85f51dff0 (diff) |
- 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.
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Classes/CEquivalence.v | 4 | ||||
-rw-r--r-- | theories/Classes/CMorphisms.v | 43 |
2 files changed, 2 insertions, 45 deletions
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. @@ -301,16 +297,6 @@ Section GenericInstances. 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. @@ -323,15 +309,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. @@ -380,15 +357,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. |