Questions on dependent elimination failures

Stream: lean4

[Adrien Champion]

I have a relatively big/complex code base where I have a problem because of some dependent elimination failures.

I tried to produce a MWE which fails in a similar, but different, way. Hopefully that'll be enough to get help for my actual problem from you guys. This code is also here.

So my question is (for now), what should I change in the code below so that I don't have this dependent elimination failure?

/-- Equivalence between two functions with possibly different (co)domains.

The only constructor (`proof`) only allows constructing values where both functions *i)* have the
same (co)domain and *ii)* are equal.
-/
inductive MyEq
  {α β : Type u}
  (f : α → β)
: {γ δ : Type u}
  → (g : γ → δ)
  → Prop
where
| proof : (g : α → β) → (eq : f = g) → @MyEq α β f α β g

/-- Erases the domain and codomain of a function. -/
structure EFun where
  dom : Type u
  cod : Type u
  app : dom → cod

/-- Equivalence over `EFun` using `MyEq`. -/
abbrev EFun.equiv
  (f₁ f₂ : EFun)
: Prop :=
  @MyEq f₁.dom f₁.cod f₁.app f₂.dom f₂.cod f₂.app

/-- Give access to `≈` (`\~~`) notation for `EFun.equiv`. -/
instance : HasEquiv EFun where
  Equiv :=
    EFun.equiv



/-- Extracts `EFun` domain equality from the equivalence of two functions. -/
abbrev EFun.equiv.eqDom
  {f₁ f₂ : EFun}
  (h : f₁ ≈ f₂)
: f₁.dom = f₂.dom :=
  by
    cases h
    -- dependent elimination failed, failed to solve equation
    --   f₂.1 = f₁.1
    sorry

[Adrien Champion]

As I mentioned, my actual problem is similar but different. Interestingly, the problem above does not happen exactly like this in my original code.

Here is the relevant bit which does not fail, destructing the Fam.Cat.Hom.Equiv value works. Intuitively I assume it's because in this version Lean must unify parameters, whereas in my MWE it must unify "fields" of a structure.

The part that does fail however is here, where I extract a Fam.Cat.Hom.Equiv and try to destruct it, similar to the first link above, except I get pretty much the same error as in the MWE,

dependent elimination failed, failed to solve equation
  F₁₂'.1 α = F₁₂.1 α

which also has structure projection like the MWE.

The part that frustrates me the most is that just a few lines above I have let h_dom := h.domEq which has type F₁₂'.1 α = F₁₂.1 α, i.e. F₁₂'.fObj α = F₁₂.fObj α using the field's actual name.
So I can prove that both types have to be the same, now how do I actually have Lean enforce that?!

[Gabriel Ebner]

The message is indeed a bit misleading. Lean is not trying to prove the equation. It is trying to unify it, that is, make the two sides definitionally equal.

[Gabriel Ebner]

This is necessary for cases to work: if the two sides are not defeq, then the fields in Fam.Cat.Hom.Equiv won't typecheck.

[Gabriel Ebner]

Having the (propositional) equality in the local context doesn't help with that.

[Gabriel Ebner]

It is trying to unify it, that is, make the two sides definitionally equal.

For this, cases actually has one more trick than the plain unifier. For example if x is a free variable, then it can make x = t defeq by calling subst.

[Gabriel Ebner]

You can make your reduced example work by first calling cases f₁. This allows cases to "solve" the equation because it now reads f₂.1 = dom†.

[Gabriel Ebner]

However for the Cat case this doesn't work because after destructing the functor, you're left with the equation F₁₂'.1 α = fObj✝ α. And the right side is not a free variable so subst doesn't work.

[Gabriel Ebner]

Does this explanation help? I don't see any (reasonable) way to extend cases to succeed on the original example. But we could change the error message (for example to say "unify" instead of "solve", although "unify" could be confused with the unifier).

[James Gallicchio]

My impression (correct me if I'm wrong) is that the solution is always to introduce more variables, either by casing on objects (to make separate variables for each of the fields) or by doing generalizations a la generalize or suffices

[James Gallicchio]

(Because more variables = more likely that unification can substitute where needed)

[James Gallicchio]

So maybe that very generic hint would also be helpful in an error message

[Adrien Champion]

@Gabriel Ebner I was aware of the first half of your answer, but the second half did clarify a lot, thanks!

[Adrien Champion]

@James Gallicchio This sounds like a good direction to experiment in, hopefully it will lead me to a solution to my problem, thank you!

[Adrien Champion]

Gabriel Ebner said:

Does this explanation help? I don't see any (reasonable) way to extend cases to succeed on the original example. But we could change the error message (for example to say "unify" instead of "solve", although "unify" could be confused with the unifier).

By the way, is there a change you would suggest in the encoding of something (probably Hom.Equiv) leading to this problem that would solve it or make it more manageable?

[Adrien Champion]

My best shot so far is

• https://github.com/AdrienChampion/experimentalean4/blob/332c37ab5d7b5347623052353ae24e74f5bccf65/cat/Cat/Fam/HomEq.lean#L66-L85

but I end up with substitutions baked in the terms I manipulate, preventing me from building the results I want when using this theorem

[James Gallicchio]

do you have a snippet of code that relies on the unify theorem?

[James Gallicchio]

I'm not sure where you'd use this instead of just doing the cases on the equiv

[James Gallicchio]

if you case on an Equiv it will try unifying the (co)domains. if the (co)domains won't unify I think the answer is to generalize one of the arrows so that it unifies

[Adrien Champion]

James Gallicchio said:

do you have a snippet of code that relies on the unify theorem?

This part relies on unify to fail to prove the theorem I want

• https://github.com/AdrienChampion/experimentalean4/blob/64cbb844ded3c7a018ede75cfed7a5041cd8f4b9/cat/Cat/Fam/Functor.lean#L460-L471

[Adrien Champion]

I end up pretty close, I have this

p:
  Hom.Equiv
    (Morph.map (fMap F₂₃) (Morph.map (fMap F₁₂) f))
    (Morph.map (fMap F₂₃) (
      (_ : (fObj F₁₂' α ↠ fObj F₁₂ β) = (fObj F₁₂ α ↠ fObj F₁₂ β)) ▸
      (_ : (fObj F₁₂' α ↠ fObj F₁₂' β) = (fObj F₁₂' α ↠ fObj F₁₂ β)) ▸
      Morph.map (fMap F₁₂') f
    ))

which is the same as my goal except for the substitutions on the rhs:

Morph.map (fMap F₂₃) (Morph.map (fMap F₁₂) f)
≋
Morph.map (fMap F₂₃) (Morph.map (fMap F₁₂') f)

[Adrien Champion]

James Gallicchio said:

if you case on an Equiv it will try unifying the (co)domains. if the (co)domains won't unify I think the answer is to generalize one of the arrows so that it unifies

I wanted to do something like this originally, but for some reason it clicked when I read these sentences.

Everything goes smoothly if I generalize one of the arrows, which is basically what @Gabriel Ebner and @James Gallicchio were saying:

• https://github.com/AdrienChampion/experimentalean4/blob/5e808f65338beb66da7808b4fe12e2f19c57bde8/cat/Cat/Fam/Functor.lean#L456-L480

[Adrien Champion]

Thanks to all of you for helping me out :smile_cat:

[Jannis Limperg]

Your equivalence is essentially a specialisation of heterogeneous equality (HEq) to function types, but then generalised to an arbitrary equivalence relation. This looks fishy to me: heterogeneous equality is evil and should be avoided if at all possible. Instead, try to set up your library such that you only need to equate morphisms of the same type. This probably requires workarounds in other places, but afaik all the setoid-based category theory libraries do this.

[Adrien Champion]

@Jannis Limperg right but here I'm just porting a paper from Coq to Lean. I'm not an expert in category theory, this port is actually an exercise to further my understanding of it.

[Adrien Champion]

I doubt my code will ever become an actual library. If it does, I'll make sure to improve this aspect if I can assuming I have access to category theory experts, or I became one myself by then

[Adrien Champion]

Jannis Limperg said:

This probably requires workarounds in other places, but afaik all the setoid-based category theory libraries do this.

If it's not too much trouble, could you give a few examples of such libraries, ideally the one(s) you deem the most interesting/robust/clever in their design?

[Jannis Limperg]

That's fair of course, I would just say the paper is wrong on this aspect. (It's old and probably the first time anyone tried to do category theory in type theory.) Their motivation is that they want to state functor equality F = G as forall f, F f ~~ G f, which doesn't work unless forall A, F A = G A definitionally. But this can be solved by using a different definition of functor equality: F = G iff (a) forall A, F A ~= G A, where the ~= is isomorphism in the target category; and (b) forall (f : A -> B), F f ~~ i^-1 . G f . i, where i is the isomorphism from (a), . is composition and ~~ is (setoid) equality of arrows. So you use the isomorphism on objects to 'fix up' the typing for the equality on arrows. Then you can rewrite condition (b) to forall (f : A -> B), i . F f = G f . i to discover that i is a natural iso, so equality on functors is just natural isomorphism. I wrote this up in Agda at some point, with the definition of natural iso here and the category of small categories here. (I only dabble as well, btw, so grain of salt and all.)

For more professional libraries, look at this in Coq, this in Agda, or of course our own docs#category_theory.Cat.category in Lean 3.

[Adrien Champion]

Awesome answer, can't wait to take a look at these resources

[Adrien Champion]

Thanks!