Использование получения в тактическом режиме в средстве доказательства теорем бережливого производства

Как использовать гипотезу формы

H : exists x, P x

в тактическом режиме? В термическом режиме я бы использовал

obtain x Hx, from H,

lean
person user3078439    schedule 28.06.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Это точно такой же синтаксис:

example (A : Type) (p : A × A) : A :=
begin
  obtain x y, from p, x
end

Конечно, вы можете снова войти в тактический режим, используя begin...end после from.

person Sebastian Ullrich    schedule 29.06.2016
comment
Спасибо! Понятия не имею, почему вчера это не сработало. - person user3078439; 29.06.2016
comment
теперь я знаю: это не работает для оператора Prop Hex : exists x, P x. Вам нужно сделать cases Hex with x Px, - person user3078439; 29.06.2016