Почему не работает правило 'linordered_field_class.frac_le'? (Изабель)

Question

Я пытаюсь использовать правило linordered_field_class.frac_le в доказательстве Изара. Вот фрагмент кода (он может зависеть от предыдущих частей доказательства, но это маловероятно). n имеет тип нац.

  ...
  then have 4:"2 ≤ (2^(n+1)::real)" by simp
  have 1:"(0::real)≤(1::real)" by simp
  have 2: "1≤(1::real)" by simp
  have 3:"(0::real)≤(2::real)" by simp
  from 1 2 3 4 have "1/(2^(n+1))≤1/(2::real)" by (rule linordered_field_class.frac_le)

Я думаю, что применил правило правильно, но он жалуется на "Не удалось закончить доказательство". Я думал, что это может быть ошибка типа, следовательно, излишнее :: real, но я не мог это исправить. Кто-нибудь знает в чем может быть проблема и как ее исправить? Или просто альтернативный способ доказать такое утверждение.

Answer 1

Если вы посмотрите на правило frac_leтретья предпосылка имеет вид 0 < ?wНо то, что вы цепляетесь в третьей позиции, 0 ≤ 2, Если вы замените это на 0 < 2работает нормально.

Обратите внимание, что вы можете сохранить многие из этих утомительных шагов вручную, просто написав auto intro: frac_le или даже simp add: divide_simps или же simp add: field_simps, Алгебраические рассуждения в Изабель имеют тенденцию быть очень утомительными, если вы не используете в полной мере существующую автоматизацию.