精益中的案例策略不会产生假设

Question

当对cases归纳数据类型使用 - 策略时，精益会生成多个案例，但不会创建说明当前案例假设的假设。例如：

\n

inductive color | blue | red\n\ntheorem exmpl (c : color) : true :=\nbegin\n    cases c,\nend\n

\n

导致以下战术状态

\n

case color.blue\n\xe2\x8a\xa2 true\ncase color.red\n\xe2\x8a\xa2 true\n

\n

但没有创建一个单独的假设（如c = color.red）来使用。你如何得到这样的假设？

\n

Answer 1

用于为每个案例cases h : c获取新的假设h。有关更多详细信息，请参阅文档。

\n

在示例中，这将是

\n

theorem exmpl (c : color) : true :=\nbegin\n  cases h : c,\nend\n

\n

导致

\n

case color.blue\nc: color\nh: c = color.blue\n\xe2\x8a\xa2 true\ncase color.red\nc: color\nh: c = color.red\n\xe2\x8a\xa2 true\n

\n