Изабель Прувинг с проблемой перевода - PullRequest
Новая
       55

Изабель Прувинг с проблемой перевода

1 голос
/ 03 августа 2020

Я определил несколько таких переводов: 

consts
  "time" :: "i"
  "sig" :: "i ⇒ i"
  "BaseChTy" :: "i"

syntax
  "time" :: "i"
  "sig" :: "i ⇒ i"
translations
  "time" ⇌ "CONST int"
  "sig(A)" ⇌ "CONST int → A"

Затем я хочу доказать следующую теорему: 

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"

Это должна быть очень простая теорема, и должно быть доказано с помощью теоремы Pi_mono за один шаг: 

thm Pi_mono
?B ⊆ ?C ⟹ ?A → ?B ⊆ ?A → ?C

Итак, я сделал это так: 

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"

apply(drule Pi_mono[of _ _ "time"])
(*Output:
goal (1 subgoal):
 1. sig(A) ⊆ sig(B) ⟹ sig(A) ⊆ sig(B)
*)

apply(simp)
(*Output:
Failed ...
*)

Поскольку посылка стала такой же, как цель, она должна быть доказана немедленно, но этого не произошло. Могу ли я узнать, сделал ли я что-нибудь не так в определении перевода? Я попытался изменить теорему на: 

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ (time → A) ⊆ (time → B)"
(*Output:
goal (1 subgoal):
 1. A ⊆ B ⟹ sig(A) ⊆ sig(B)
*)

apply(drule Pi_mono[of _ _ "time"])
(*Output:
goal (1 subgoal):
 1. sig(A) ⊆ sig(B) ⟹ sig(A) ⊆ sig(B)
*)

apply(simp)
(*Output:
Success ...
*)

Тогда она работает немедленно, но разве перевод не сделает их одинаковыми?

Обновление: Спасибо за ответ Матиаса Флери , Я попытался сделать упрощенную трассировку, и она показывает примерно следующее: 

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"
using [[show_sorts]] apply(drule Pi_mono[of _ _ "time"])
using [[simp_trace]] apply(simp)
oops

(*
Output:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sig(A::i) ⊆ sig(B::i) ⟹ sig(A) ⊆ sig(B) 
[1]Adding rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
*)

, в то время как время -> версия A показывает: 

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ time → A ⊆ time → B"
using [[show_sorts]] apply(drule Pi_mono[of _ _ "time"])
using [[simp_trace]] apply(simp)
oops

(*
Output:
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sig(A::i) ⊆ sig(B::i) ⟹ sig(A) ⊆ sig(B) 
[1]Adding rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
[1]Applying instance of rewrite rule "??.unknown":
sig(A::i) ⊆ sig(B::i) ≡ True 
[1]Rewriting:
sig(A::i) ⊆ sig(B::i) ≡ True
*)

Почему Может ли эта версия на этот раз применить экземпляр правила перезаписи, чтобы продолжить доказательство, а исходная - нет?

1 Ответ

2 голосов
/ 04 августа 2020

Благодаря импорту, который вы упомянули в своем комментарии (спасибо), я смог воспроизвести проблему. Проблема в переводе, вам нужно сделать что-то вроде 

syntax
  "sig" :: "i ⇒ i" (‹sig(_)›)
translations
  "sig(A)" == "CONST int → A"

theorem sig_mono: "⟦ A ⊆ B ⟧ ⟹ sig(A) ⊆ sig(B)"
  apply(rule Pi_mono)
  apply assumption
  done

Просто чтобы развернуть мой комментарий и объяснить, как я обнаружил, что проблема в переводе. Я посмотрел на ошибку объединения: 

theorem ⟦ A ⊆ B ⟧ ⟹ time → A ⊆ time → B
  supply[[unify_trace_failure]]
   apply (rule PI_mono)

Сообщение об ошибке сообщает, что sig и Pi не унифицируемы. Это уже странно. Чтобы быть уверенным, что проблема связана с переводом, я посмотрел на основной термин: 

ML ‹@{print}@{term ‹sig(A)›}›

Он показывает основной термин, и мы видим, что перевод не работает, и я просмотрел другие переводы в библиотека для устранения проблемы.

...