You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
From HB RequireImport structures.
From Coq RequireImport Relations Morphisms.
HB.mixin Record hasEquiv A := { equiv : relation A }.
HB.structure Definition Equiv := { A of hasEquiv A }.
HB.mixin Record Equiv_isSetoid A of Equiv A := {
equivP : Equivalence (@equiv A)
}.
HB.structure DefinitionSetoid := {A of hasEquiv A & Equiv_isSetoid A}.
#[global] ExistingInstance equivP.
HB.mixin Record isFoo A of Setoid A := {}.
HB.structure Definition Foo := {A of isFoo A & Setoid A}.
Lemma not_breaking (A : Setoid.type) : @Equivalence A (@equiv A).
Proof. apply @equivP. Qed.
Lemma not_breaking2 (A : Foo.type) : @Equivalence _ (@equiv A).
Proof. apply @equivP. Qed.
Lemma breaking (A : Foo.type) : @Equivalence A (@equiv A).
Proof.
Set Debug "all".
Set Printing All.
(* Check @equivP. *)
Fail apply @equivP.
Set Typeclasses Debug.
Fail typeclasses eauto.
Succeed refine (@equivP _).
Abort.
Lemma breaking (A : Foo.type) : @Equivalence A (@equiv A).
Proof.
Set Debug "all".
Set Printing All.
(*@Equivalence (Foo.sort A) (@equiv (order_Foo__to__order_Equiv A))*)
Check @equivP.
(* : forall s,
@Equivalence
(Equiv.sort
(Equiv.Pack (Setoid.sort s)
(Equiv.Class (Setoid.sort s)
(Setoid.order_hasEquiv_mixin (Setoid.sort s)
(Setoid.class s)))))
(@equiv
(Equiv.Pack (Setoid.sort s)
(Equiv.Class (Setoid.sort s)
(Setoid.order_hasEquiv_mixin (Setoid.sort s)
(Setoid.class s)))))
*)
pose proof (H := @equivP).
simpl in H.
(*
H: forall s : Setoid.type,
@Equivalence (Setoid.sort s)
(@equiv (Equiv.Pack (Setoid.sort s) (Equiv.Class (Setoid.sort s) (Setoid.order_hasEquiv_mixin (Setoid.sort s) (Setoid.class s)))))
*)
apply H.
(* Fail apply @equivP. *)
Abort.
This is a bug in the old unification.
I suspect it overreduces
(Equiv.sort
(Equiv.Pack (Setoid.sort ?s) ...))
to
match ?s with ...
while evarconv has a piece of code I wrote a long ago to not unfold "stuck" canonical projections (but rather reduce the other side of the unification problem). Indeed if I simplify the lemma statement by hand in the correct way, then legacy unification performs the canonical inference we expect.
Example
cc @robbertkrebbers @gares @FissoreD
Remark: Foo is the simplification of
Ofe
in Iris.The text was updated successfully, but these errors were encountered: