Stream: Coq users

Topic: Automatically apply with coercion

Patrick Nicodemus (Oct 30 2022 at 15:24):

Record SetoidMorphism `{Setoid x} `{Setoid y} := {
  morphism :> x → y;
  proper_morphism :> Proper@{h p} (respectful@{h p h p h p} equiv equiv) morphism
}.

Since SetoidMorphism coerces to a function, if I have a goal B and a setoid morphism f: (A, eqA)\to (B, eqB) then I can use f with apply but not with simple apply. So if a SetoidMorphism is in the list of hypotheses I want to
I would like to add some kind of Hint Extern to auto so that I can automatically apply any setoid morphism in the hypothesis to one in the goal.
The first thing that I came up with is

match goal with
| [ f  : context[SetoidMorphism _ _ ] |- _] => apply f
end

and this works. However it seems inelegant.
I was thinking it would be cleaner to go through each hypothesis in the context and see if the head term of the conclusion of the hypothesis is SetoidMorphism. But I don't know how to access the "conclusion" of the hypothesis manually in the same way that apply does.

Last updated: Sep 23 2023 at 14:01 UTC