# Zulip Chat Archive

## 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