unfold definition in tactic mode

Stream: general

[Bernd Losert]

Which tactic do I use to unfold a defintion. For example, say I have:

def foo : Prop := 1 = 0

theorem bar : ∀ x : nat, foo → foo := begin
  intros x h,
end

The context has h : foo. I would like it to read h : 1 = 0 after some tactic magic.

[Adam Topaz]

tactic#unfold

[Bernd Losert]

I tried unfold at h. It doesn't do anything.

[Adam Topaz]

unfold foo at h

[Adam Topaz]

If that doesn't work, try dsimp [foo] at h

[Bernd Losert]

Ah. Yes, that works.

[Bernd Losert]

If foo takes parameters, I still write unfold foo right?

[Adam Topaz]

Yeah, that's right

[Bernd Losert]

Nice. Thanks.

[Yakov Pechersky]

Often, one is able to say "rw foo at ..." depending on how complex your definition is.

[Bernd Losert]

Apparently you can't unfold complex definitions. For example:

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

def foo (p : nat × nat) : Prop :=
let
  (m, n) := p
in
  m = n

theorem bar : ∀ p : nat × nat, foo p → 1 = 0 := begin
  intros p h,
  unfold foo at h,
end

The context shows me h : foo._match_1 p.

[Yakov Pechersky]

Right, because that is how foo is defined, you're doing the equivalent of a match statement when you deconstruct in your let statement. You might make some progress with "cases p". A helper rfl lemma like "foo (m, n) <-> m = n := iff.rfl" is very helpful fight after you make a definition.

[Yakov Pechersky]

Then you make another lemma, "foo p <-> p.1 = p.2 := by cases p; refl"

[Yakov Pechersky]

The reason is that let statements aren't reduced instantly, I forget which Greek letter they correspond to, beta reduction/expansion? And there's also the eta reduction here, which in lean3 isn't definitionally true. Is "p = (p.1, p.2)" true by refl? My recollection is that, no, it's not.

[Bernd Losert]

OK. It's not show-stopper. I can always look at the definition in the code.

[Bernd Losert]

I'm trying the following, but it doesn't work:

def foo (p : nat × nat) : Prop :=
let
  (m, n) := p
in
  some m = some n

lemma lem1 {m n : nat} : foo (m, n) ↔ some m = some n := iff.rfl
lemma lem2 {p : nat × nat} : foo p ↔ some p.1 = some p.2 := by cases; rfl <-- COMPLAINS HERE

theorem bar : ∀ p : nat × nat, foo p → 1 = 0 := begin
  intros p h,
end

[Yakov Pechersky]

lemma lem2 {p : nat × nat} : foo p ↔ some p.1 = some p.2 := by cases p; refl

[Yakov Pechersky]

You have to indicate what you're deconstructing in the cases tactic. Also,rfl is a term, refl is a tactic.

[Bernd Losert]

Ah, OK.

[Bernd Losert]

So I have this now:

theorem bar : ∀ p : nat × nat, foo p → 1 = 0 := begin
  intros p h,
  rw lem2 at h,
  rw [some_injective] at h,
end

I'm trying to get rid of the some but it's not working.

[Yakov Pechersky]

docs#some_injective

[Yakov Pechersky]

What are your imports? This works for me:

import data.option.defs

def foo (p : nat × nat) : Prop :=
let
  (m, n) := p
in
  some m = some n

lemma lem1 {m n : nat} : foo (m, n) ↔ some m = some n := iff.rfl
lemma lem2 {p : nat × nat} : foo p ↔ some p.1 = some p.2 := by cases p; refl

theorem bar : ∀ p : nat × nat, foo p → 1 = 0 := begin
  intros p h,
  rw lem2 at h,
  rw [option.some_inj] at h,
  sorry
end

[Bernd Losert]

This is why I have now:

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical option
open_locale classical filter

def foo (p : nat × nat) : Prop :=
let
  (m, n) := p
in
  some m = some n

lemma lem1 {m n : nat} : foo (m, n) ↔ some m = some n := iff.rfl
lemma lem2 {p : nat × nat} : foo p ↔ some p.1 = some p.2 := by cases p; refl

theorem bar : ∀ p : nat × nat, foo p → 1 = 0 := begin
  intros p h,
  rw lem2 at h,
  rw [some_injective] at h,
end

[Bernd Losert]

It seems there is a difference between option.some_inj and some_injective.

[Yakov Pechersky]

some_injective is not something you can rewrite with. Do you mean something like

  rw [(some_injective _).eq_iff] at h,

[Bernd Losert]

OK, then I am confused about the purpose of some_injective.

[Bernd Losert]

I'll stick to some_inj for now. Thanks.

[Yakov Pechersky]

some_injective is function.injective some, for some type T sending to option T. function.injective is not an "iff", it is only the implication that "f x = f y -> x = y`.
Consider:

#check some_injective
/-
some_injective : ∀ (α : Type u_1), function.injective some
-/
#print function.injective
/-
def function.injective : Π {α : Sort u₁} {β : Sort u₂}, (α → β) → Prop :=
λ {α : Sort u₁} {β : Sort u₂} (f : α → β), ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
-/
#check @function.injective.eq_iff
/-
function.injective.eq_iff :
  ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, function.injective f → ∀ {a b : α}, f a = f b ↔ a = b
-/

[Reid Barton]

Usually we avoid pattern matching in definitions (as opposed to proofs) for this reason, even though it looks nicer--you had to write the non-pattern matching definition in the statement of lem2 anyways, so just use that.

[Bernd Losert]

Yeah, it's a trade-off it seems.

[Bernd Losert]

Another question about unfolding: How do you unfold something like b ≈ a all the way. I had to do unfold has_equiv.equiv and then unfold setoid.r. Is there a quicker way?

[Yakov Pechersky]

Can you explain what you hope to do by unfolding?

[Yakov Pechersky]

By the way, in the widget view, one can click on any term, including a = or \~- or anything like that and see how it's defined and what implicit arguments it uses. I know that you don't use an editor with widget view, just declaring for posterity.

[Eric Wieser]

What type are a and b? Either you made a wrong turn when you introduced b ≈ a into your goal, or there's a lemma missing

[Bernd Losert]

a and b are just examples. I'm interested in unfolding what ≈ means.

[Bernd Losert]

Here's my proof where I had to do multiple unfoldings:

theorem act_congr : ∀ (g : G) (h₁y₁ h₂y₂ : G × X) (h : h₁y₁ ≈ h₂y₂), envelope.act g h₁y₁ = envelope.act g h₂y₂ := begin
  rintros (g : G) (⟨h₁,y₁⟩ : G × X) (⟨h₂,y₂⟩ : G × X) h,
  unfold act,
  simp [quotient.eq],
  unfold has_equiv.equiv,
  unfold setoid.r,
  unfold envelope,
  simp [mul_assoc],
  assumption,
end

[Anne Baanen]

I assume you're working with something like docs#quotient.lift?

[Anne Baanen]

I agree with Eric, there should be a lemma along the lines of quotient.eq expressed in terms of envelope.act.

[Bernd Losert]

So you're saying I should abstract the three unfolds into a lemma?

[Anne Baanen]

Or even the whole thing between unfold act and unfold envelope. unfold in a finished proof is a bit of a code smell, suggesting you need to abstract a lemma.

[Anne Baanen]

(During development unfold can be useful to get a sense of what's going on. Or clicking on the relevant widgets.)

[Bernd Losert]

Oh really? I didn't know that.

[Anne Baanen]

At least, that is my vision on the idiomatic style in the parts of mathlib I run into. It may be very different if there are many small definitions.

[Bernd Losert]

Alright. Thanks for the input.

[Eric Wieser]

I think the API around quotients is a bit messy at the moment - has_equiv.equivvs setoid.r vs docs#setoid.rel vs the_actual_relation_name, quot.mk vs quotient.mk vs quotient.mk' vs submodule.quotient.mk vs ...

[Anne Baanen]

Don't forget submodule.quotient.mk versus submodule.mkq :sweat_smile: