Что означает Метис: неиспользованные теоремы в этом контексте? - PullRequest
Новая
       78

Что означает Метис: неиспользованные теоремы в этом контексте?

0 голосов
/ 10 декабря 2018

Я очень плохо знаком с Изабель, поэтому извиняюсь, если этот вопрос плохо сформулирован.

Я пытаюсь доказать следующее: 

record 
  Point =
    x :: nat
    y :: nat

definition
  cond :: "Point ⇒ Point ⇒ ?"
where
  "cond point1 point2 ≡ 
     abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"

Мое доказательство: 

lemma cond_proof : "∃ point1 point2 . cond point1 point2 = True"
  sledgehammer
  by (metis Point_ext_def abs_division_segment add_diff_cancel_left' cond_def select_convs(1))

Это вызывает предупреждение: 

Metis: Unused theorems:

Пожалуйста, кто-нибудь может объяснить, что это значит?И, если возможно, помогите мне найти доказательство, которое удовлетворяет этому условию.

Я все еще очень плохо знаком с Изабель, поэтому все комментарии приветствуются.

1 Ответ

0 голосов
/ 11 декабря 2018

Я могу прокомментировать некоторые практические аспекты, связанные с вашей проблемой.Я считаю, что предупреждение не требует пояснений.Обычно вы можете удалить неиспользуемые теоремы, и metis все еще может доказать интересующую вас теорему (см. cond_proof_metis в приведенном ниже листинге кода).

Лемма cond_proof может быть доказана, если показать две точки, которые удовлетворяют условию леммы.Я считаю, что такой подход может считаться лучше, чем использование доказательства по умолчанию, найденного sledgehammer.Я показал, как сделать это в лемме cond_proof_Isar в приведенном ниже листинге кода.Есть более компактные способы показа примера.Однако, учитывая, что вы очень плохо знакомы с Изабель, я придерживался того, что мне показалось наиболее естественным.

Я не уверен, что вы оставили намеренно команду sledgehammer в своем доказательстве.Однако в большинстве случаев это не то, что вы хотите сделать.После того, как sledgehammer найдет доказательство, вы можете удалить команду sledgehammer из вашего доказательства.

В качестве дополнительного примечания я бы предложил вам ознакомиться с некоторыми примерами и упражнениями в книгах.«Помощник по проверке логики высшего порядка» Тобиаса Нипкова и др. И «Конкретная семантика с Изабель / HOL» Тобиаса Нипкова и Джервина Кляйна.Вышеупомянутые ссылки содержат много примеров, которые очень похожи на проблему, с которой вы имеете дело.

К сожалению, я недостаточно знаю о sledgehammer и metis, чтобы понять, почему предупреждениепроизводится с использованием вывода sledgehammer для доказательства теоремы.Для получения дополнительной информации о sledgehammer и metis см. «Руководство пользователя кувалды для Изабель / HOL», которое было написано Жасмин Кристиан Бланшетт и содержится в стандартной документации Изабель.Конечно, дополнительную информацию о metis можно также найти в Интернете (например, http://www.gilith.com/metis/).. Надеемся, что кто-то более знающий, чем я, сможет предоставить более подробную информацию относительно вашего запроса. 

record 
  Point =
    x :: nat
    y :: nat

definition
  cond :: "Point ⇒ Point ⇒ bool"
where
  "cond point1 point2 ≡ 
     abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"

(*Point_ext_def was part of the output produced by sledgehammer and is
listed as unused by metis. It can be removed with no effect on the
ability of metis to prove the result of interest.*)
lemma cond_proof_metis : "∃ point1 point2 . cond point1 point2 = True"
  by (metis (*Point_ext_def*) 
      abs_1 add_diff_cancel_left' cond_def of_nat_1_eq_iff select_convs(1))

lemma cond_proof_Isar : "∃ point1 point2 . cond point1 point2 = True"
proof - 
  define point1::Point where point1: "point1 ≡ ⦇x = 2, y = 0⦈"
  define point2::Point where point2: "point2 ≡ ⦇x = 1, y = 0⦈"
  from point1 point2 have "abs (x point1 - x point2) = 1" by simp
  then show ?thesis unfolding cond_def by auto
qed
...