Применение аксиом о секвестах - PullRequest
Новая
       8

Применение аксиом о секвестах

0 голосов
/ 12 июня 2018

Рассмотрим следующую минимальную разработку на основе библиотеки Isabelle Sequents: 

theory Test
  imports Pure Sequents.Sequents
begin

syntax "_Trueprop"    :: "two_seqe" ("((_)/ ⊢ (_))" [6,6] 5)
consts Trueprop :: two_seqi
parse_translation ‹[  (@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))  ]›
print_translation ‹[  (@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))  ]›

axiomatization where
  identity : "$A, P, $B ⊢ $C, P, $D" and
  xch : "$A, $B, $C, $D, $E ⊢ $F  ⟹  $A, $D, $C, $B, $E ⊢ $F"

lemma xch0 : "$A, $B, $D, $E ⊢ $F  ⟹  $A, $D, $B, $E ⊢ $F"
  apply (rule xch ; assumption)  done

lemma xch1 : "$A, $B, P, $D, $E ⊢ $F  ⟹  $A, $D, P, $B, $E ⊢ $F"
  apply (rule xch ; assumption)  done

lemma xch2 : "$A, $B, P1, P2, $D, $E ⊢ $F  ⟹  $A, $D, P1, P2, $B, $E ⊢ $F"
  apply (rule xch ; assumption)  done

Попытка доказательства лемм не удалась.Однако им это удастся, если я уберу аксиому identity!Итак, мой первый вопрос: почему присутствие аксиомы identity влияет на эти доказательства, которые ее не используют?

Мой главный вопрос - как заставить работать эти доказательства, когда у меня есть аксиома идентичности.Я предполагаю, что мне нужно явно специализировать переменные, например, применяя xch[of A B _ D E F].Это похоже на правильную специализацию (она работает при отсутствии identity), но дает очень странную ошибку 

Failed to meet type constraint:
Term   A :: 'a => seq'
Type   seq' => seq'

Нужно ли мне писать что-то явное вместо _?Если да, то?Я не могу понять, как явно написать «пустую последовательность» или «последовательность, содержащую только P» или «последовательность, содержащую только P1, P2» - волшебство нотации $A побеждает меня.

Редактировать: Ответ Андреаса на мой первый вопрос полностью решает мою актуальную проблему, поэтому я переименовываю этот вопрос и принимаю этот ответ.Но я все еще хотел бы знать ответ на свой второй вопрос, поэтому я переспрашиваю его отдельно здесь .

1 Ответ

0 голосов
/ 12 июня 2018

Сообщение об ошибке для явной реализации переменных уже указывает на то, что что-то с типами неверно.Проблема в том, что axiomatization вызывает вывод типа по всем аксиомам одновременно.Поскольку в аксиоме identity используется то же имя переменной A, что и в аксиоме xch, вывод типа присваивает им тот же тип.Если аксиомы identity нет, вывод типа вычисляет более общий тип, который заставляет доказательства работать.Следовательно, есть два способа избежать этой проблемы:

  1. Использовать разные имена переменных во всех аксиомах, упомянутых в блоке axiomatization.Это помогает, но обычно снижает читабельность и что-то упускает из виду.

  2. Избегайте свободных переменных в аксиомах, явно определяя их количественно с помощью мета-квантификатора Pure.

В вашем примере подход 2 будет выглядеть так: 

axiomatization where
  identity : "⋀A P B C D. $A, P, $B ⊢ $C, P, $D" and 
  xch : "⋀A B C D E F. $A, $B, $C, $D, $E ⊢ $F  ⟹  $A, $D, $C, $B, $E ⊢ $F"
...