Использование «также есть ... наконец» в Isabelle

Question

я обычно думаю о also have, как работает так:

have "P r Q1" by simp 
also have "... r Q2" by simp 
also have "... r Q3" by simp 
... 
also have "... r Qn" by simp 
finally have "P r Qn+1" by simp 

где "... r Qm" означает "Qm-1 r Qm" и r некоторое транзитивное отношение.

С r смысла = это, кажется, действительно случай, однако, при использовании ≥ я нашел контрпример к этому описанию:

... 
have "1- 1/(2^(n+1))≥1/(2::real)" by simp 
also have "... ≥ 0" (* here when I check the 'output' it seems to be 
considering "0 ≤ 1 - 1/2^(n + 1)" which in the previous notation 
would be Qn r Qn+2 !*) 

Мой вопрос, как же also have работу, в частности, как я предсказываю, что будет ...?

Answer 1

AFAIR, a ≥ b является аббревиатурой от b ≤ a. Имея это в виду, вы видите, что это не соответствует шаблону, ожидаемому also.

Я предлагаю вам указать свою цепочку неравенств в обратном порядке, от самого низкого до высшего. Вы все равно можете указать конечный результат, используя ≥, если хотите - в конце концов, это всего лишь аббревиатура.