Stream: math-comp users

Topic: ✔ have with inductive spec


view this post on Zulip Alex Loiko (Mar 23 2023 at 17:12):

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.

view this post on Zulip Pierre Roux (Mar 23 2023 at 17:17):

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)

view this post on Zulip Notification Bot (Mar 23 2023 at 17:30):

Alex Loiko has marked this topic as resolved.


Last updated: Jul 15 2024 at 20:02 UTC