intro vs assume

Stream: general

[Siyuan Yan]

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]

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]

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]

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]

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

[Adam Topaz]

I bet the number of assumes is infinitesimal compared to those

[Adam Topaz]

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]

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

[Eric Wieser]

assume is also a synonym for fun and λ

[Reid Barton]

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

[Kalle Kytölä]

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]

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]

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]

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

[Mario Carneiro]

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