Как сгенерировать код для экзистенциального квантификатора - PullRequest
Новая
       7

Как сгенерировать код для экзистенциального квантификатора

0 голосов
/ 26 февраля 2019

Вот пример теории: 

datatype ty = A | B | C

inductive test where
  "test A B"
| "test B C"

inductive test2 where
  "¬(∃z. test x z) ⟹ test2 x"

code_pred [show_modes] test .
code_pred [show_modes] test2 .

values "{x. test2 A}"

Сгенерированный код пытается перечислить более ty.И поэтому ничего не получается.

Я пытаюсь определить исполняемую версию предиката test: 

definition "test_ex x ≡ ∃y. test x y"

definition "test_ex_fun x ≡
  Predicate.singleton (λ_. False)
    (Predicate.map (λ_. True) (test_i_o x))"

lemma test_ex_code [code_abbrev, simp]:
  "test_ex_fun = test_ex"
  apply (intro ext)
  unfolding test_ex_def test_ex_fun_def Predicate.singleton_def
  apply (simp split: if_split)

Но я не могу доказать лемму.Не могли бы вы предложить лучший подход?

Ответы [ 3 ]

0 голосов
/ 26 февраля 2019

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

lemma test_ex_code [code_abbrev, simp]:
  "Predicate.singleton (λ_. False)
    (Predicate.map (λ_. True) (test_i_o x)) = (∃y. test x y)"
  apply (intro ext iffI)
  unfolding Predicate.singleton_def
  apply (simp_all split: if_split)
  apply (metis SUP1_E mem_Collect_eq pred.sel test_i_o_def)
  apply (intro conjI impI)
  apply (smt SUP1_E the_equality)
  apply (metis (full_types) SUP1_E SUP1_I mem_Collect_eq pred.sel test_i_o_def)
  done

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

0 голосов
/ 26 февраля 2019

Экзистенциальные квантификаторы над аргументом индуктивного предиката можно сделать исполняемым, введя другой индуктивный предикат.Например: 

inductive test2_aux where "test x z ==> test2_aux x"
inductive test2 where "~ test2_aux x ==> test2 x"

с соответствующими code_pred инструкциями.Свободная переменная z в предположении test2_aux действует как экзистенциальная.Поскольку это преобразование каноническое, code_pred имеет для этого препроцессор: 

code_pred [inductify] test2 .

выполняет свою работу.

0 голосов
/ 26 февраля 2019

Ну, values жалуется на тот факт, что ty не относится к enum.Таким образом, в данном конкретном случае проще всего выполнить эту реализацию. 

instantiation ty :: enum
begin
definition enum_ty :: "ty list" where
  "enum_ty = [A,B,C]"  
definition "enum_all_ty f = list_all f [A,B,C]" 
definition "enum_ex_ty f = list_ex f [A,B,C]" 
instance
proof (intro_classes)
  let ?U = "UNIV :: ty set" 
  show id: "?U = set enum_class.enum" 
    unfolding enum_ty_def
    using ty.exhaust by auto
  fix P
  show "enum_class.enum_all P = Ball ?U P" 
    "enum_class.enum_ex P = Bex ?U P" 
    unfolding id enum_all_ty_def enum_ex_ty_def enum_ty_def by auto
  show "distinct (enum_class.enum :: ty list)" unfolding enum_ty_def by auto
qed

После этого ваша values -команда оценивает без проблем.

...