intro

Stream: lean4

[Hallon]

When do I need to use it 'intro'? I'm a little confused. Some proofing need 'intro' after 'by', and some dont need.

[Mario Carneiro]

intro is used when the goal is a forall or implication statement and introduces names for the variables

[Mario Carneiro]

But when intro is the very first thing in the proof it is usually preferred to instead put the variables you want to introduce in binders before the : of the theorem statement, which has the same effect

[Mario Carneiro]

for example:

example : ∀ x y : Nat, x + y = y + x := by
  -- ⊢ ∀ (x y : Nat), x + y = y + x
  intro x y
  -- x y : Nat
  -- ⊢ x + y = y + x
  apply Nat.add_comm

example (x y : Nat) : x + y = y + x := by
  -- x y : Nat
  -- ⊢ x + y = y + x
  apply Nat.add_comm

[Hallon]

OK I think I know, Thanks very much

[Hallon]

could you give a examply which conclude implication statement and need 'intro'?

[Mario Carneiro]

example (x : Nat) : x = 1 → x + x = 2 := by
  -- x: Nat
  -- ⊢ x = 1 → x + x = 2
  intro h
  -- x: Nat
  -- h: x = 1
  -- ⊢ x + x = 2
  rw [h]

example (x : Nat) (h : x = 1) : x + x = 2 := by
  -- x: Nat
  -- h: x = 1
  -- ⊢ x + x = 2
  rw [h]

[Hallon]

Thanks very much