Zulip Chat Archive

Stream: general

Topic: intro vs assume

Siyuan Yan (Nov 03 2022 at 21:12):

what's the difference? Here's what's from the tutorial of mathlib, demonstrating two ways of proving the same thing. In the first example there's intro h and it can be changed to assume h. But the second assume h can't be changed to intro h.

lemma le_of_le_add_eps {x y : } : ( ε > 0, y  x + ε)   y  x :=
  -- Let's prove the contrapositive, asking Lean to push negations right away.
  -- Assume `h : x < y`.
  intro h,
  -- We need to find `ε` such that `ε` is positive and `x + ε < y`.
  -- Let's use `(y-x)/2`
  use ((y-x)/2),
  -- we now have two properties to prove. Let's do both in turn, using `linarith`

Next we will study a compressed version of that proof:

example {x y : } : ( ε > 0, y  x + ε)   y  x :=
  exact assume h, ⟨(y-x)/2, by linarith, by linarith⟩,

Adam Topaz (Nov 03 2022 at 21:27):

When you write exact ... the ... needs to be the exact term that solves the goal in question. intro is a tactic and cannot be used in term-mode. You can replace assume with a lambda if you want.

Adam Topaz (Nov 03 2022 at 21:29):

I guess assume is also a tactic. I don't think anyone actually uses assume in real life (i.e. outside of the tutorials). We usually use lambdas or intro(s).

Eric Rodriguez (Nov 03 2022 at 21:43):

Adam Topaz said:

I guess assume is also a tactic. I don't think anyone actually uses assume in real life (i.e. outside of the tutorials). We usually use lambdas or intro(s).

assume is used like ~700+ times in mathlib, and in fact I think a few people are in favour of keeping those and not removing them

Adam Topaz (Nov 03 2022 at 21:45):

How many times does mathlib use intro/intros/rintro/rintros?

Adam Topaz (Nov 03 2022 at 21:45):

I bet the number of assumes is infinitesimal compared to those

Adam Topaz (Nov 03 2022 at 21:46):

I don't think assume should be removed, I'm just saying that people usually forget about assume pretty quickly once they actually start using Lean

Junyan Xu (Nov 03 2022 at 21:59):

I think they're mostly used in term mode; did people back then have trouble typing λ? :joy:

Eric Wieser (Nov 03 2022 at 22:10):

assume is also a synonym for fun and λ

Reid Barton (Nov 04 2022 at 05:57):

It used to be a stylistic thing to use assume in proofs and λ in functions, I think

Kalle Kytölä (Nov 04 2022 at 07:15):

Hopefully the answers above settled the original question (tactic vs term mode and lots of synonyms), but I would still add two comments.

In tactic mode intros and assume seem to behave completely identically; in particular they can do multiple introductions/assumptions at a time, whereas intro only does one at a time.

As a stylistic matter, reiterating Reid's point above, I find it very strange when people "assume data". In teaching math with Lean (rather than teaching Lean) I would (try to) be very careful to only ever use assume when the assumption is a Prop, and I would use intro/intros where mathematicians would write "let x be something" (data). In the converse direction, I do realize that in logic intro/intros makes sense also for Props as an introduction rule for connectives/quantifies, but this does not in my opinion correspond to pen-and-paper math use, so in teaching I'd have a preference for assume for propositions. In mathlib, on the other hand, I think using intro/intros throughout is commonplace and makes a lot of sense (we buy into Curry-Howard or understand the logic etymology and don't attempt to produce code for direct math pedagogical consumption).

Eric Wieser (Nov 04 2022 at 08:43):

In tactic mode assume is closer to rintro than to intro; it let's you specify the type of the thing being introd as assume a : A, with semantics intro a, change A at a

Mario Carneiro (Nov 04 2022 at 13:22):

Also, assume (in both term and tactic mode) has an additional feature not shared with intro / \lam: you can omit the identifier and it is named this. So assume A, e or assume A, as a tactic mean the same as λ this : A, e or rintro (this : A), respectively

Eric Wieser (Nov 04 2022 at 13:25):

I assume you meant assume : A, assume A means "call the variable A"

Mario Carneiro (Nov 04 2022 at 13:28):

ah, yes I forget the syntax since I never use it :see_no_evil:

Last updated: Aug 03 2023 at 10:10 UTC