Доказательства существования с полиморфными типами c - PullRequest
Новая
       82

Доказательства существования с полиморфными типами c

2 голосов
/ 30 апреля 2020

Я пытаюсь формализовать доказательство того, что DFA закрыты при объединении, и я дошел до доказательства "∀ ? ℬ. language ? ∪ language ℬ = language (DFA_union ? ℬ)", но на самом деле я хотел бы доказать это ∀ ? ℬ. ∃ ?. language ? ∪ language ℬ = language ?. Я верю, что проблема связана с полиморфными типами c, но я не уверен.

Вот что у меня есть: 

declare [[show_types]]
declare [[show_sorts]]
declare [[show_consts]]

record ('q, 'a)DFA =
  Q0 :: 'q
  F :: "'q set"
  δ :: "'q ⇒ 'a ⇒ 'q"

primrec δ_iter :: "('q, 'a)DFA ⇒ 'a list ⇒ 'q ⇒ 'q" where
  "δ_iter ? [] q = q" |
  "δ_iter ? (a # as) q = δ_iter ? as (δ ? q a)"

definition δ0_iter :: "('q, 'a)DFA ⇒ 'a list ⇒ 'q" where
  "δ0_iter ? as = δ_iter ? as (Q0 ?)"

definition language :: "('q, 'a)DFA ⇒ ('a list) set" where
  "language ? = {w . δ0_iter ? w ∈ (F ?)}"

fun DFA_union :: "('p, 'a)DFA ⇒ ('q, 'a)DFA ⇒ ('p × 'q, 'a)DFA" where
  "DFA_union ? ℬ = 
    ⦇ Q0 = (Q0 ?, Q0 ℬ)
    , F = {(q, r) . q ∈ F ? ∨ r ∈ F ℬ}
    , δ = λ (q, r). λ a. (δ ? q a, δ ℬ r a) 
    ⦈"

lemma extract_fst: "∀ ? ℬ p q. fst (δ_iter (DFA_union ? ℬ) ws (p, q)) = δ_iter ? ws p" 
  by (induct ws; simp)

lemma extract_snd: "∀ ? ℬ p q. snd (δ_iter (DFA_union ? ℬ) ws (p, q)) = δ_iter ℬ ws q" 
  by (induct ws; simp)

lemma "∀ ? ℬ. language ? ∪ language ℬ = language (DFA_union ? ℬ)"
proof((rule allI)+)
  fix ? ℬ
  let ?? = "DFA_union ? ℬ"
  have "language ?? = {w . δ0_iter ?? w ∈ F ??}" 
    by (simp add: language_def)
  also have "... = {w . fst (δ0_iter ?? w) ∈ (F ?) ∨ snd (δ0_iter ?? w) ∈ (F ℬ)}" 
    by auto 
  also have "... = {w . δ0_iter ? w ∈ F ? ∨ δ0_iter ℬ w ∈ F ℬ}"
    using DFA.select_convs(1) DFA_union.simps δ0_iter_def extract_fst extract_snd
    by (metis (no_types, lifting)) 
  also have "... = {w . δ0_iter ? w ∈ F ?} ∪ {w. δ0_iter ℬ w ∈ F ℬ}"
    by blast
  also have "... = language ? ∪ language ℬ"
    by (simp add: language_def)
  finally show "language ? ∪ language ℬ = language ??"
    by simp
qed

lemma DFA_union_closed: "∀ ? ℬ. ∃ ?. language ? ∪ language ℬ = language ?"
  sorry

Если я добавлю типы в to или ℬ в основной лемме я получаю «Не удалось уточнить любую ожидающую цель».

1 Ответ

2 голосов
/ 30 апреля 2020

проблема действительно в неявных типах. В вашем последнем утверждении Изабель неявно выводит типы состояний 'p, 'q, 'r для трех автоматов A, B, C, тогда как ваша лемма DFA_union фиксирует тип состояния от C до 'p * 'q. Поэтому, если вам нужно явно предоставить аннотации типов. Более того, обычно не требуется указывать ваши леммы с явными ∀ -квантователями.

Итак, вы можете продолжать так: 

lemma DFA_union: "language ? ∪ language ℬ = language (DFA_union ? ℬ)" 
  (is "_ = language ??")
proof -
   have "language ?? = {w . δ0_iter ?? w ∈ F ??}" 
   ...
qed

lemma DFA_union_closed: fixes ? :: "('q,'a)DFA" and ℬ :: "('p,'a)DFA"
  shows "∃ ? :: ('q × 'p, 'a)DFA. language ? ∪ language ℬ = language ?"
  by (intro exI, rule DFA_union)

Обратите внимание, что эти аннотации типов также важно в следующем смысле. Лемма, подобная следующей (где все типы состояний одинаковы) просто не соответствует действительности. 

lemma fixes ? :: "('q,'a)DFA" and ℬ :: "('q,'a)DFA"
  shows "∃ ? :: ('q, 'a)DFA. language ? ∪ language ℬ = language ?"

Проблема в том, что подключите bool -тип для 'q, тогда у вас есть автоматы которые имеют не более двух государств. И тогда вы не всегда можете найти автомат для объединения, которое также имеет не более двух состояний.

...