## Stream: new members

### Topic: induction using user-defined recursors

#### Kyle Miller (Aug 24 2020 at 23:55):

I'm probably not supposed to be doing this in the first place, but I was trying to define a user-defined recursor because I thought it might help with some problem I was having (I might ask about this in another topic). I'm observing something rather strange when I try to use it with the induction tactic, where it comes up with an unexpected type. In the following, elems_iff_eq is proof that rec' is usable, and elems_iff_eq' is showing the strange behavior.

import data.sym2

universes u v

@[reducible, recursor 5]
def rec' {α : Type u} {β : sym2 α → Sort v}
(f : Π (a : α × α), β ⟦a⟧) (h : ∀ (a b : α × α) (p : a ≈ b),
(eq.rec (f a) (quotient.sound p) : β ⟦b⟧) = f b)
(q : sym2 α) : β q :=
quot.rec f h q

variables {α : Type u}

lemma elems_iff_eq {x y : α} {z : sym2 α} (hne : x ≠ y) :
x ∈ z ∧ y ∈ z → z = ⟦(x, y)⟧ :=
λ ⟨hx, hy⟩, rec' (λ ⟨z₁, z₂⟩ hx hy, sym2.eq_iff.mpr begin
cases sym2.mem_iff.mp hx with hx hx; cases sym2.mem_iff.mp hy with hy hy; cc,
end) (by { intros, refl }) z hx hy

lemma elems_iff_eq' {x y : α} {z : sym2 α} (hne : x ≠ y) :
x ∈ z ∧ y ∈ z → z = ⟦(x, y)⟧ :=
begin
rintros ⟨hx, hy⟩,
induction z using rec',
sorry
end


At the point of the sorry, the primary goal becomes

α : Type u,
x y : α,
hne : x ≠ y,
z : (α × α) × α × α,
hx : x ∈ ⟦z⟧,
hy : y ∈ ⟦z⟧
⊢ ⟦z⟧ = ⟦(x, y)⟧


That z should be of type α × α, and nothing after that line is well-typed.

#### Reid Barton (Aug 24 2020 at 23:56):

I've also seen an ill-typed proof state when using induction with quotient

#### Reid Barton (Aug 24 2020 at 23:57):

I never looked into the cause though, since it was back in the dark ages

#### Kyle Miller (Aug 25 2020 at 00:06):

What I had been running into was that induction z using quotient.rec gives un-rewritable terms, and the reason seemed to be that the same setoid was being described in different ways (but I'm not completely certain). So, I thought maybe a new recursor that ensured I got exactly the setoid instance I wanted would help, but then I got behavior that was even more peculiar!

Here's an example where a rewrite fails even though it seems like it should work:

import data.sym2

universes u

variables {α : Type u}

lemma elems_iff_eq {x y : α} {z : sym2 α} (hne : x ≠ y) :
x ∈ z ∧ y ∈ z → z = ⟦(x, y)⟧ :=
begin
rintros ⟨hx, hy⟩,
induction z using quotient.rec,
cases z with z₁ z₂,
rw sym2.eq_iff, -- rewrite tactic failed
end


#### Mario Carneiro (Aug 25 2020 at 00:07):

usually that means that a previous tactic left an instantiated metavariable in the state

#### Kyle Miller (Aug 25 2020 at 00:09):

It looks like the first goal's context has no metavariables, but the second goal does have one because the construction hasn't been completed yet.

#### Kyle Miller (Aug 25 2020 at 00:10):

I'm just basing this off looking at set_option pp.all true. The first goal:

α : Type u,
x y : α,
hne : @ne.{u+1} α x y,
z₁ z₂ : α,
hx :
@has_mem.mem.{u u} α (sym2.{u} α) (@sym2.has_mem.{u} α) x
(@quotient.mk.{u+1} (prod.{u u} α α) (@setoid.r.{u+1} (prod.{u u} α α) (sym2.rel.setoid.{u} α))
(@prod.mk.{u u} α α z₁ z₂)),
hy :
@has_mem.mem.{u u} α (sym2.{u} α) (@sym2.has_mem.{u} α) y
(@quotient.mk.{u+1} (prod.{u u} α α) (@setoid.r.{u+1} (prod.{u u} α α) (sym2.rel.setoid.{u} α))
(@prod.mk.{u u} α α z₁ z₂))
⊢ @eq.{u+1} (sym2.{u} α)
(@quotient.mk.{u+1} (prod.{u u} α α) (@setoid.r.{u+1} (prod.{u u} α α) (sym2.rel.setoid.{u} α))
(@prod.mk.{u u} α α z₁ z₂))
(@quotient.mk.{u+1} (prod.{u u} α α) (sym2.rel.setoid.{u} α) (@prod.mk.{u u} α α x y))


#### Mario Carneiro (Aug 25 2020 at 00:11):

whoa, that mwe has a really weird bug in it. Put your cursor at the end of the cases line. You should see this:

2 goals
α : Type u,
x y : α,
hne : x ≠ y,
z₁ z₂ : α,
hx : x ∈ ⟦(z₁, z₂)⟧,
hy : y ∈ ⟦(z₁, z₂)⟧
⊢ ⟦(z₁, z₂)⟧ = ⟦(x, y)⟧

case h
α : Type u,
x y : α,
hne : x ≠ y,
z b : α × α,
p : z ≈ b
⊢ _ = _


Now move the cursor to the start of the line and then back to the end, and now the second goal will say _ = )_ (yes, an unclosed parenthesis). Repeating the cursor motion results in _ = ) )_ and so on.

#### Mario Carneiro (Aug 25 2020 at 00:11):

This may involve an interaction with the rich goal view

#### Kyle Miller (Aug 25 2020 at 00:14):

emacs has only well-matched parentheses here. Maybe the react-like diff algorithm isn't updating the goal view correctly. (I'm under the impression that's how it's set up.)

#### Mario Carneiro (Aug 25 2020 at 00:16):

the bug also goes away if I switch to plain goal view, so I'm sure it's a factor

#### Kyle Miller (Aug 25 2020 at 00:16):

Oh, this seems like a good place to ask: what does ?m_1[b, hx, hy] mean? I've just assumed it meant a metavariable that somehow depends on its lexical context, but I haven't been able to look it up.

#### Mario Carneiro (Aug 25 2020 at 00:17):

it's called a delayed abstraction. It represents a metavariable applied to concrete arguments

#### Mario Carneiro (Aug 25 2020 at 00:17):

it's like ?f (2+2) where ?f is a metavariable

#### Mario Carneiro (Aug 25 2020 at 00:18):

Basically these are not available for unification, they are only constraints, i.e. if you find ?f (2+2) =?= 4 you aren't allowed to assume that ?f is the identity

#### Bryan Gin-ge Chen (Aug 25 2020 at 00:19):

cc: @Edward Ayers regarding the widget bug above.

#### Mario Carneiro (Aug 25 2020 at 00:25):

Anyway, here's how I suggest you proceed, assuming you aren't specifically trying to use induction using, which I don't think has ever worked well

lemma elems_iff_eq {x y : α} {z : sym2 α} (hne : x ≠ y) :
x ∈ z ∧ y ∈ z → z = ⟦(x, y)⟧ :=
begin
refine quotient.rec_on_subsingleton z _,
rintros ⟨z₁, z₂⟩ ⟨hx, hy⟩,
rw sym2.eq_iff,
end


#### Kyle Miller (Aug 25 2020 at 00:31):

I'll keep quotient.rec_on_subsingleton in mind. What I had been doing before is induction without using, then possibly fixing up the quot.mk's that would appear with change before doing rewrites. In this case, I had used apply rather than rw to avoid needing change: https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/data/sym2.lean#L145

induction is nice because it updates the types of everything that depends on the thing being inducted on, so it would be nice if it worked properly.

#### Mario Carneiro (Aug 25 2020 at 00:36):

You can still get most of that functionality with plain refine

#### Mario Carneiro (Aug 25 2020 at 00:36):

you have to include the things to be reverted manually in the term but the motive generalization is done automatically

#### Mario Carneiro (Aug 25 2020 at 00:37):

You can also use regular quotient.rec_on but in this case you are proving a proposition so there is no need

#### Mario Carneiro (Aug 25 2020 at 00:40):

like this:

lemma elems_iff_eq {x y : α} {z : sym2 α} (hne : x ≠ y) :
x ∈ z ∧ y ∈ z → z = ⟦(x, y)⟧ :=
begin
rintros ⟨hx, hy⟩,
refine quotient.ind (λ z hx hy, _) z hx hy,
cases z with z₁ z₂,
rw sym2.eq_iff,
end


Last updated: May 17 2021 at 22:15 UTC