Zulip Chat Archive

Stream: general

Topic: unfold definition in tactic mode


Bernd Losert (Dec 23 2021 at 01:19):

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 (Dec 23 2021 at 01:41):

tactic#unfold

Bernd Losert (Dec 23 2021 at 01:44):

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

Adam Topaz (Dec 23 2021 at 01:44):

unfold foo at h

Adam Topaz (Dec 23 2021 at 01:45):

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

Bernd Losert (Dec 23 2021 at 01:45):

Ah. Yes, that works.

Bernd Losert (Dec 23 2021 at 01:47):

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

Adam Topaz (Dec 23 2021 at 01:47):

Yeah, that's right

Bernd Losert (Dec 23 2021 at 01:48):

Nice. Thanks.

Yakov Pechersky (Dec 23 2021 at 02:24):

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

Bernd Losert (Dec 23 2021 at 19:53):

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 (Dec 23 2021 at 19:56):

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 (Dec 23 2021 at 19:56):

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

Yakov Pechersky (Dec 23 2021 at 19:58):

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 (Dec 23 2021 at 20:00):

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

Bernd Losert (Dec 23 2021 at 20:35):

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 (Dec 23 2021 at 20:38):

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

Yakov Pechersky (Dec 23 2021 at 20:39):

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

Bernd Losert (Dec 23 2021 at 20:39):

Ah, OK.

Bernd Losert (Dec 23 2021 at 20:42):

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 (Dec 23 2021 at 20:45):

docs#some_injective

Yakov Pechersky (Dec 23 2021 at 20:45):

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 (Dec 23 2021 at 20:46):

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 (Dec 23 2021 at 20:48):

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

Yakov Pechersky (Dec 23 2021 at 20:48):

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

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

Bernd Losert (Dec 23 2021 at 20:56):

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

Bernd Losert (Dec 23 2021 at 20:57):

I'll stick to some_inj for now. Thanks.

Yakov Pechersky (Dec 23 2021 at 21:01):

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 (Dec 23 2021 at 21:03):

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 (Dec 23 2021 at 21:07):

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

Bernd Losert (Jan 19 2022 at 22:19):

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 (Jan 19 2022 at 22:23):

Can you explain what you hope to do by unfolding?

Yakov Pechersky (Jan 19 2022 at 22:23):

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 (Jan 19 2022 at 22:26):

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 (Jan 19 2022 at 22:31):

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

Bernd Losert (Jan 19 2022 at 22:32):

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 (Jan 19 2022 at 22:32):

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

Anne Baanen (Jan 19 2022 at 22:35):

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

Bernd Losert (Jan 19 2022 at 22:36):

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

Anne Baanen (Jan 19 2022 at 22:38):

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 (Jan 19 2022 at 22:38):

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

Bernd Losert (Jan 19 2022 at 22:39):

Oh really? I didn't know that.

Anne Baanen (Jan 19 2022 at 22:41):

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 (Jan 19 2022 at 22:46):

Alright. Thanks for the input.

Eric Wieser (Jan 19 2022 at 22:50):

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 (Jan 19 2022 at 22:51):

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


Last updated: Dec 20 2023 at 11:08 UTC