Zulip Chat Archive

Stream: new members

Topic: Let tactic

Patrick Johnson (Nov 17 2021 at 21:25):

Documentation seems to be unclear regarding the let tactic. What does it actually do? The let tactic introduces a hypothesis of the form x : t := v. What does it exactly mean? What is the := operator here? Is it the meta-operator (like in def of something), or is it a term-level syntactic operator defined inductively (like =)? How to use such a hypothesis? Consider this example:

(P :     Prop)
(h :  (a b : ), P a b  a = b) :
( (f :   Prop), f 0)  ( (f :   Prop), ¬f 1) :=
  let f := λ (x : ), P x 0,
  use f,
  simp only [f],
  exact (h 0 0).mpr rfl,
  use f,
  simp only [f],
  intro h1,
  exact one_ne_zero ((h 1 0).mp h1),

Is the simp only [f] preferred way to use such hypothesis? Why do rw and unfold fail? Is there a way to split

x : t := v

into two hypothesis

x : t
hx : x = v

Kevin Buzzard (Nov 17 2021 at 21:26):

You can use set if you want hx.

Kevin Buzzard (Nov 17 2021 at 21:27):

set f := λ (x : ℕ), P x 0 with hf,

Kyle Miller (Nov 17 2021 at 21:46):

The let tactic constructs a let ... in ... expression. Modulo some details, its effect is as if you turned

  let f := foo,


let f := foo
in begin

Kyle Miller (Nov 17 2021 at 21:47):

I'm not sure why simp only [f] works but rw f doesn't. I think it has something to do with the fact that f is only let-bound so doesn't have the "equation lemmas" that definitions get.

Kyle Miller (Nov 17 2021 at 21:50):

In the goal window, x : t := v is just how it writes a hypothesis that actually knows its value (unlike a hypothesis from an argument, or a hypothesis from have that intentionally forgets its value). It's supposed to represent the := in a let or a def.

Eric Rodriguez (Nov 17 2021 at 22:06):

simp has special code for let iirc

Last updated: Dec 20 2023 at 11:08 UTC