unfold at [TERM]

Stream: new members

[Klaus Gy]

Hi, I noticed that unfold id at h pattern only works if h is a single variable, but sometimes I want to use it at a term. What works here is let foo := TERM; unfold id at foo; exact foo which seems kinda clumsy, is there a simpler way?

for example here

def a := 3
def b := 3
def eq : a = b := by unfold a b; rfl
def double (x : Nat) := x + x
def eq' := congrArg double eq
-- this is not working!
-- def eq'' := by unfold a b at (congrArg double eq)
def eq'' := by let foo := congrArg double eq; unfold a b at foo; exact foo

eq' has type double a = double b and eq'' has type double 3 = double 3.

[Aaron Liu]

What do you expect this to do?

[Kenny Lau]

don't use def for theorems, and don't use tactic for def

[Kenny Lau]

and don't use let for theorems

[Kenny Lau]

and don't define anything without specifying the type

[Klaus Gy]

ah ok def eq'' := by simpa only [a,b] using (congrArg double eq) does work

[Klaus Gy]

@Kenny Lau my usecase was inside a proof where i didnt state any type, and the types are long winded, which is why i wanted lean to unfold them so that i dont have to write them out

[Klaus Gy]

there is no way to create an abbrev or notation inside a proof context, right? i feel it would be nice being able to write a transparent let which is really just shorthand and never needs to be unfolded or simplified.

[Kenny Lau]

maybe it's time to split your proof into lemmas

[Klaus Gy]

Hmm, @Jireh Loreaux said the same in another thread (which I didn't want to hijack), and I'm sure you have a point. But do you never just want to abbreviate a term inside a proof context for sake of abbreviation? For example, I started a proof like this

noncomputable instance singleton_is_mono : Mono (singleton hPB) :=
  ⟨ fun {X} (b b' : X ⟶ B) eq ↦ by
    let B_sub := Subobject.mk (cmdiag B)
    let P := (Subobject.pullback (B ◁ b)).obj B_sub
    let P' := (Subobject.pullback (B ◁ b')).obj B_sub
    let PeqP' : P = P' := by ...

It just fits my mental image to call those pullbacks P and P', but I don't want to manually unfold them later, ideally I'd like that PeqP' has actually type (Subobject.pullback (B ◁ b)).obj B_sub = (Subobject.pullback (B ◁ b')).obj B_sub and P = P' is just shorthand. This feels to me very close to writing an actual math proof.

[Aaron Liu]

you can just treat it as if it's a term of type (Subobject.pullback (B ◁ b)).obj B_sub = (Subobject.pullback (B ◁ b')).obj B_sub, because the lets can be definitionally unfolded

[Klaus Gy]

@Aaron Liu yes, I do unfold them later via unfold P P', but wouldn't it be nice if we had reducibles in proof context? Something like rdef P := ... for creating a transparent / reducible definitions / macros?

[Aaron Liu]

that's what let does

[Aaron Liu]

I think let has reducible zeta-delta

[Klaus Gy]

Awesome! I could swear that I tripped over this before, but now I can't reconstruct it, so it must have been some other mistake, thank you!

[Jireh Loreaux]

You can also use letI (the I means "inline") which is reasonable for defs because there are no actual lets inside the expression.

[Kyle Miller]

I guess you could write value_of% P = value_of% P' if you really wanted P and P' to not appear, though that doesn't look very nice.

[Kyle Miller]

By the way, simp by default doesn't unfold local variables unless either you specify which variables you want to be unfolded (e.g. simp [a,b]) or by using the option simp +zetaDelta.

[Klaus Gy]

Aaron Liu said:

I think let has reducible zeta-delta

Hm, I could now reproduce my case, but maybe I'm also misunderstanding what you meant.

structure Foo where
  n : Nat

def test : Nat :=
  let x := 3
  let y := 3
  --this is not working
  --have : (⟨ x ⟩ : Foo) = (⟨ y ⟩ : Foo) := by simp
  have : (⟨ x ⟩ : Foo) = (⟨ y ⟩ : Foo) := by unfold x y; simp
  1

This is still not a perfect example, since rfl here would work, but imagine something with an actual simp lemma where rfl won't suffice (which is the case in my current project).

Unfortunately, letI instead of let is also not working without unfolding.

This does work (thank you @Kyle Miller !):

  have : (⟨ value_of% x ⟩ : Foo) = (⟨ value_of% y ⟩ : Foo) := by simp

but I'd like to have it the other way around, make x and y transparent at the point where I introduce them, and then not having to think about that extra layer anymore.