dependent elimination failed

Stream: new members

[Vivek Rajesh Joshi]

I'm defining a new function to erase all occurences of an element in a list. Why does it not work with a DecidableEq instance?

def list_eraseAll [DecidableEq α] : List α → α → List α
  | [],    _ => []
  | a::as, b => match a = b with
    | true  => list_eraseAll as b
    | false => a :: list_eraseAll as b

error:

dependent elimination failed, type mismatch when solving alternative with type
  motive (true = true)
but expected
  motive x✝

[Damiano Testa]

Try using == instead of = (= is Prop-valued, while == is Bool-valued)

[Vivek Rajesh Joshi]

It works, but what goes wrong with the Prop-valued =?

[Chris Bailey]

It's not an inductive type with two constructors 'false' and 'true'.

[Vivek Rajesh Joshi]

Ahh okay, got it

[Chris Bailey]

You can use the DecidableEq instance in its prop form with an if-then-else:

def list_eraseAll [DecidableEq α] : List α → α → List α
  | [],    _ => []
  | a::as, b =>
    if a = b
    then list_eraseAll as b
    else a :: list_eraseAll as b

[Vivek Rajesh Joshi]

I see, thanks!

[Klaus Gy]

I'm puzzled about this example, why does the dummy above typecheck, but the actual example below not? Does it have something to do with function types being treated special?

import Mathlib.CategoryTheory.Limits.Shapes.Equalizers

variable {a : Type} (dep : a -> Type)

structure Foo where
  app : a
  naturality : dep app

def fooEqual {x y : Foo dep} {h0 : x.app = y.app} {h1 : x.naturality = h0 ▸ y.naturality} : x = y := by
    cases x; cases y
    cases h0; cases h1
    rfl

open CategoryTheory Limits

variable {C : Type u} [Category C] {X Y : C} {f g : X ⟶ Y} [HasEqualizer f g]

theorem barEqual (w : Fork f g) (h0 : w.π.app = (Fork.ofι w.ι w.condition).π.app) : w.π = (Fork.ofι w.ι w.condition).π :=
  let h1 : (Fork.ofι w.ι w.condition).π.naturality = h0 ▸ w.π.naturality := by rfl
  by
    cases (Fork.ofι w.ι w.condition).π; cases w.π
    cases h0; cases h1
    rfl

[Aaron Liu]

you have to take apart w.π in h0 too

[Kyle Miller]

If you see "dependent elimination failed" it means "the sides of the printed equation are not constructor applications, or a few other basic things I know how to reason about".

One side is a fun, and the other is a projection application.

[Klaus Gy]

I see, will think about this! Sorry, I wanted to create a new thread, but apparently one already exists with this name. I can't mark it as solved now.

[Kyle Miller]

(We never wanted anyone to ever mark threads as solved, and Zulip recently implemented an option to disable the feature. A "got it" or "thanks" is enough!)

[Kyle Miller]

Style question: why are you mixing term let and by?

Also, why do you have let h1 in the first place? Proofs are definitionally equal, so it's not saying anything. (Another style thing: for proofs, use have, since the proof is irrelevant.)

[Kyle Miller]

Here:

theorem barEqual (w : Fork f g) (h0 : w.π.app = (Fork.ofι w.ι w.condition).π.app) :
    w.π = (Fork.ofι w.ι w.condition).π := by
  revert h0
  cases (Fork.ofι w.ι w.condition).π
  cases w.π
  intro h0
  cases h0
  rfl

The revert is a way to get cases to generalize the term that's in h0 too.

[Kyle Miller]

A way around that is to add in a proof clause to cases and use rw:

theorem barEqual (w : Fork f g) (h0 : w.π.app = (Fork.ofι w.ι w.condition).π.app) :
    w.π = (Fork.ofι w.ι w.condition).π := by
  cases h : (Fork.ofι w.ι w.condition).π
  rw [h] at h0
  cases h' : w.π
  rw [h'] at h0
  cases h0
  rfl

[Kyle Miller]

Even better: use the extensionality principle for natural transformations:

theorem barEqual (w : Fork f g) (h0 : w.π.app = (Fork.ofι w.ι w.condition).π.app) :
    w.π = (Fork.ofι w.ι w.condition).π := by
  ext
  rw [h0]

[Kyle Miller]

In particular, you might not need this theorem because it's docs#CategoryTheory.NatTrans.ext

[Kyle Miller]

theorem barEqual (w : Fork f g) (h0 : w.π.app = (Fork.ofι w.ι w.condition).π.app) :
    w.π = (Fork.ofι w.ι w.condition).π :=
  NatTrans.ext h0

[Klaus Gy]

about the mixing, i usually put the tactic to the end, if i need it, but if thats bad style, ill do it differently, if that's what you meant by mixing by and let. thanks a lot for your answers!!

[Kyle Miller]

I'd say that if you are going to use tactics for a theorem, you may as well start with by immediately, since that saves you from ever need to think about moving the by around. Imagine wanting to put a tactic before the let during a refactor — you need to do some unnecessary edits.

Or, what if you have a tactic proof and after some refactoring you notice that it now starts with a let/have. Do you then need to move the by to after the let/have and indent the rest to try to match that style?

[Klaus Gy]

good points, ill keep that in mind. for me it was more like vice versa, i first put down some intermediate results and then in the end i see if i need a tactic to unite them, or not. but i'm happy to do whatever is considered best style.

[Klaus Gy]

this is a bit offtopic, but is there a better way to generate equality between structures from equalities between fields (if there is no corresponing ext lemma)? because im running into different errors now (result is not type correct), and im not sure if the revert/cases/intro/cases approach is the cleanest?

[Kyle Miller]

When you say "there's no ext lemma" do you mean that there can't be one, or that there's not currently one?

You can add @[ext] to a structure to generate an ext lemma automatically.

[Klaus Gy]

i meant the former, i can try to add @[ext] (in this case to Cone).

[Kyle Miller]

You can add it after the fact with attribute [ext] Cone too

[Klaus Gy]

yes, but that's also global then, right? i just worry to pollute the global namespace by adding ext to any structure i want to use it with. are there cases where the ext lemma was deliberately not added?

[Kyle Miller]

There's attribute [local ext] Cone to add it only locally.

[Kyle Miller]

Sometimes an @[ext] isn't deliberately added because there's a better one that's added in manually later. I can't think of any reason you wouldn't want an ext lemma if the type's constructor isn't private.

[Klaus Gy]

thanks for the elaboration!

[Kenny Lau]

@Klaus Gy talking about equalities of Cone is evil

[Kenny Lau]

you have CategoryTheory.Limits.Cones.ext instead, which is not evil (the result is an isomorphism)

[Klaus Gy]

But what if we get equality for free? like in Fork.ofι w.ι w.condition = w?

[Klaus Gy]

(i didnt add the ext lemma to Cone, i just used it privately for this proof.)