import MyNat.Definition

Tactic intro

If your goal is ⊢ P → Q then intro p will introduce a new hypothesis p : P and change the goal to ⊢ Q.

You can introduces one or more hypotheses, optionally naming and/or pattern-matching them. For each hypothesis to be introduced, the remaining main goal's target type must be a let or function type.

• intro by itself introduces one anonymous hypothesis, which can be accessed by e.g. assumption.
• intro x y introduces two hypotheses and names them. Individual hypotheses can be anonymized via _, or matched against a pattern:

  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...

• Alternatively, intro can be combined with pattern matching much like fun:

  intro
  | n + 1, 0 => tac
  | ...