Как использовать get, чтобы упростить чтение доказательств исключения? - PullRequest
Новая
       73

Как использовать get, чтобы упростить чтение доказательств исключения?

0 голосов
/ 12 ноября 2018

Я пытаюсь сделать основные естественные доказательства вычетов в Изабель, следуя этому документу (особенно слайд 23).

Я знаю, что могу делать такие вещи, как 

theorem ‹(A ⟶ B) ⟶ A ⟶ B›
proof -
  {
    assume ‹A ⟶ B›
    {
      assume ‹A›
      with ‹A ⟶ B› have ‹B› ..
    }
    hence ‹A ⟶ B› ..
  }
  thus ‹(A ⟶ B) ⟶ A ⟶ B› ..
qed

Но также 

theorem ‹(A ⟶ B) ⟶ A ⟶ B›
proof
  assume ‹A ⟶ B› and ‹A›
  then obtain ‹B› ..
qed

достигает той же цели.

Итак, когда я пытаюсь написать доказательство 

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof -
  {
    assume ‹A ⟶ A ⟶ B›
    {
      assume ‹A›
      with ‹A ⟶ A ⟶ B› have ‹A ⟶ B› ..
      hence ‹B› using ‹A› ..
    }
    hence ‹A ⟶ B› ..
  }
  thus ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B› ..
qed

как 

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
qed

почему Изабель жалуется, что 

Failed to finish proof:
goal (1 subgoal):
 1. A ⟶ A ⟶ B ⟹ A ⟶ B

Я знаю, что это очень простые вещи, которые Изабель может доказать за один шаг: цель здесь состоит в том, чтобы создать краткое доказательство, понятное человеку (в той степени, в которой это Естественная дедукция), без необходимости консультироваться с Изабель.

1 Ответ

0 голосов
/ 23 ноября 2018

Эта модификация ваших пробных работ: 

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then show ‹B› using ‹A› ..
qed

Проблема двоякая:

  1. При открытии блока доказательства автоматически применялось «стандартное» правило введения, основанное на форме цели, которую вы пытались доказать. В вашем случае это было импликация, то есть теорема impI. Проблема в том, что вы применяете это только один раз, что оставляет вас с предположением A -> A -> B и оставшейся целью A -> B. В результате у вас еще нет предположения A, которое, как вы предполагаете, у вас есть, поскольку для этого требуется второе использование impI. Вместо этого, используя proof(intros impI), я говорю Изабель воздержаться от использования ее стандартного набора правил введения и исключения в качестве первого шага в доказательстве и вместо этого применяю правило введения impI так часто, как это возможно (то есть дважды). Кроме того, proof(rule impI, rule impI) также будет работать здесь с тем же эффектом.
  2. Во-вторых, ваша последняя строка then obtain и далее не заканчивает доказательство: вы ничего не show! Используя явное show, вы даете Изабель понять, что хотели бы «уточнить» открытую цель и фактически завершить то, что вы намеревались доказать в начале блока.

Обратите внимание, что использование здесь obtain для работы с фактами A -> B и A не было неверным, если ваша единственная цель - получить B. Проблема в том, что вы пытаетесь работать с фактами, чтобы извлекать новые и одновременно улучшать открытую цель. Например, это также работает: 

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
  then show ‹B› .
qed

, где факт B получен в первой строке, а вторая строка тривиально использует этот факт для уточнения открытой цели B.

...