Доказательство существования в Изабель / HOL в этом примере - PullRequest
Новая
       12

Доказательство существования в Изабель / HOL в этом примере

2 голосов
/ 29 сентября 2019

Я пытаюсь научиться использовать Изабель / Изара с HOL, и я решил, что хороший способ сделать это - разработать некоторую элементарную теорию чисел.Я определил свои собственные операции «плюс» и «время», чтобы методы доказательства не делали всю работу за меня, так как уже много доказано о +, * в Main.Мои версии определены как: 

fun p:: "nat ⇒ nat ⇒ nat" (infix "⊕" 80) where
  p_0: "0 ⊕ n =n" |
  p_rec: " (Suc m) ⊕ n = Suc (m ⊕ n)"

fun t:: "nat ⇒ nat ⇒ nat" (infix "⊗" 90) where
  t_0: "0 ⊗ n= 0" |
  t_rec: "Suc m ⊗ n = n + m ⊗ n"

, и я уже показал, что умножение и сложение являются коммутативными, что справедливо в законе распределения.Затем я попытался показать следующее: 

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof (induction n)
  case 0
  have "0= 0 ⊗ m" by auto
  hence "∃q. 0 =q ⊗ m" by auto

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

Редактировать:

xanonec помог мне пройти этот шаг, но я сразу же застрял на следующем шаге, казалось бы, похожая проблема.В конечном итоге я хочу показать: 

"∃ q r. 0 = q ⊗ m⊕r"

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

"0 = 0 ⊗ m ⊕ 0"

1 Ответ

1 голос
/ 29 сентября 2019

Подходящей стратегией для решения может быть прямое применение правил (в jEdit вы можете cntrl + ЛКМ или cmd + ЛКМ на exI, чтобы перейти к его утверждению): 

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof(induction n)
  case 0
  have "0 = 0 ⊗ m" by auto
  hence "∃q. 0 = q ⊗ m" by (rule exI)    
qed

Вообще, во многих подобных случаях sledgehammer может найти подходящее (но часто неоптимальное) доказательство.Учебник по использованию sledgehammer является частью официальной документации Изабель.Кроме того, я хотел бы предложить следующие ресурсы: "Конкретная семантика с Изабель / HOL" Тобиаса Нипкова и Джервина Кляйна и "Помощник по доказательству для логики высшего порядка" Тобиаса Нипкова и др.

Обновление после внесения изменений в формулировку вопроса

В следующем списке представлены доказательства, основанные только на самых основных методах и прямом применении правил:

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof (induction n)
  case 0 show ?case
  proof-
    have "0 = 0 ⊗ m ⊕ 0" by simp
    then have "∃r. 0 = 0 ⊗ m ⊕ r" by (rule exI)
    then show "∃q r. 0 = q ⊗ m ⊕ r" by (rule exI) 
  qed
  case (Suc n) show ?case sorry
qed

Однако, если вы можете позволить себе больше полагаться на автоматизацию доказательств, вы можете использовать metis для доказательства всей теоремы:

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r" by (metis p_0 t_0)

...