Why does the following work and is it documented somewhere?

```
Lemma test_lemma (x y: nat) : if x==y then x=y else x<>y.
have [if_true | if_false] := ifP.
```

produces the goals

```
x, y : nat
if_true : x == y
============================
x = y
subgoal 2 (ID 140) is:
x <> y
```

What I expect to happen after reading the manual is that the type of ifP

```
ifP
: forall (A : Type) (b : bool) (vT vF : A),
if_spec b vT vF (b = false) b (if b then vT else vF)
```

is matched with `[if_true | if_false]`

independently of the goal. I thought that `have`

is for forward reasoning steps only and that `case: ifP`

is the tactic to use with inductive specs.

`have [intro | intro'] := sthP`

is the same as `case: sthP => [intro | intro']`

(but is often nicer as it makes the introduced variable names more visible closer to the beginning of the line)

Alex Loiko has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC