## 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 :=
begin
-- Let's prove the contrapositive, asking Lean to push negations right away.
contrapose!,
-- 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
split,
linarith,
linarith,
end

/-
Next we will study a compressed version of that proof:
-/

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x :=
begin
contrapose!,
exact assume h, ⟨(y-x)/2, by linarith, by linarith⟩,
end


#### 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):

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