induction using user-defined recursors

Stream: new members

[Kyle Miller]

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]

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

[Reid Barton]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

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]

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]

This may involve an interaction with the rich goal view

[Kyle Miller]

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]

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

[Kyle Miller]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

cc: @Edward Ayers regarding the widget bug above.

[Mario Carneiro]

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]

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]

You can still get most of that functionality with plain refine

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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