Stream: Coq users

Topic: Writing automation to solve unification problems?


view this post on Zulip Patrick Nicodemus (Jan 15 2024 at 20:48):

Today I wrote some code like
let s : A := t in ...
and the unification algorithm failed, saying "Error: Expected a term of type A but type of t is B[?x,?y]" where there were a couple evars in the displayed type of t whose values could not be inferred.
So I had to add more detail to t and fill in ?x and ?y explicitly.
This got me wondering, is it possible for me to automate this?
Like if I have a goal Aand I write refine tthen this command may fail if there are evars in t that cannot be instantiated, and I get an error saying "Error: type of t is B[?x,?y]", is it possible for me to to write some kind of tactic which would return the list of metavariables ?x and ?y which need to be instantiated before this unification can be made and apply some kind of ad hoc methods for instantiating them based on inspection of the goal?

view this post on Zulip Patrick Nicodemus (Jan 15 2024 at 20:51):

I think that if I understand Enrico Tassi's "Unification Hints" in Elpi this would allow you to declare hints like this similar to canonical structures and type classes but more general. Like I could declare hints in the context that would allow let s : A :=t to go through.

view this post on Zulip Patrick Nicodemus (Jan 15 2024 at 20:57):

Here's a specific example

Open Scope bicategory_scope.
Goal forall (C :Bicategory) {w x y z: @bi0cell C}
    {h h' : bicat y z} {g g': bicat x y} {f f': bicat w x}
    (γ : bi2cell h h') (β : bi2cell g g')
    (α : bi2cell f f'), (@hom _ ((h ∘∘∘ g) ∘∘∘ f) ((h' ∘∘∘ g') ∘∘∘ f')).
  intros.
  refine (@fmap _ _ (@hcompose C _ _ _ ) _ _
        ((@fmap _ _ (@hcompose C x _ _ )_ _
            (γ, β)), α)).

The unification algo needs to know that the last two arguments to fmap are ordered pairs. Then it can be solved.

Open Scope bicategory_scope.
Goal forall (C :Bicategory) {w x y z: @bi0cell C}
    {h h' : bicat y z} {g g': bicat x y} {f f': bicat w x}
    (γ : bi2cell h h') (β : bi2cell g g')
    (α : bi2cell f f'), (@hom _ ((h ∘∘∘ g) ∘∘∘ f) ((h' ∘∘∘ g') ∘∘∘ f')).
  intros.
  refine (@fmap _ _ (@hcompose C _ _ _ ) (_ , _) (_ , _)
        ((@fmap _ _ (@hcompose C x _ _ ) (_ , _) (_ , _)
            (γ, β)), α)).

view this post on Zulip Patrick Nicodemus (Jan 15 2024 at 21:00):

So I would like to be able to write some kind of Ltac2 or Elpi code which tries to instantiate all variables and then tries to look at the variables which could not be instantiated and apply some case specific reasoning to deal with them, such that when considering maps between Cartesian products of sets, the elements of the domain and codomain type are ordered pairs.


Last updated: Jun 13 2024 at 21:01 UTC