CODEWITHSUNDEEP
prooflean
502E532E
502E532E

Reputation: 459

Cases tactic in Lean does not create hypothesis

When using the cases-tactic on an inductive data type, lean produces multiple cases, but does not create a hypothesis stating the assumption of the current case. For example:

inductive color | blue | red

theorem exmpl (c : color) : true :=
begin
    cases c,
end

results in the following tactic state

case color.blue
⊢ true
case color.red
⊢ true

but does not create a separate hypothesis (like c = color.red) to work with. How would you get such a hypothesis?

Upvotes: 5

Views: 432

Answers (1)

502E532E
502E532E

Reputation: 459

Use cases h : c to get a new hypothesis h for each case. For more detail, see the documentation.

In the example, this would be

theorem exmpl (c : color) : true :=
begin
  cases h : c,
end

resulting in

case color.blue
c: color
h: c = color.blue
⊢ true
case color.red
c: color
h: c = color.red
⊢ true

Upvotes: 5

Related Questions