Zulip Chat Archive

Stream: new members

Topic: induction using user-defined recursors


view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 24 2020 at 23:56):

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

view this post on Zulip Reid Barton (Aug 24 2020 at 23:57):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 25 2020 at 00:07):

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

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 25 2020 at 00:11):

This may involve an interaction with the rich goal view

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 25 2020 at 00:17):

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

view this post on Zulip Mario Carneiro (Aug 25 2020 at 00:17):

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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Aug 25 2020 at 00:19):

cc: @Edward Ayers regarding the widget bug above.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 25 2020 at 00:36):

You can still get most of that functionality with plain refine

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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