Блог

При использовании cases тактики-для индуктивного типа данных lean создает несколько случаев, но не создает гипотезу, подтверждающую предположение о текущем случае. Например:

 inductive color | blue | red

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

приводит к следующему тактическому состоянию

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

но не создает отдельную гипотезу (например c = color.red ) для работы. Как бы вы получили такую гипотезу?

Используйте cases h : c , чтобы получить новую гипотезу h для каждого случая. Для получения более подробной информации см. документацию.

В приведенном примере это было бы

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

в результате чего

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