Как доказать правила исключения с помощью Изара? - PullRequest
Новая
       11

Как доказать правила исключения с помощью Изара?

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

Вот простая теория: 

datatype t1 = A | B | C
datatype t2 = D | E t1 | F | G

inductive R where
  "R A B"
| "R B C"

inductive_cases [elim]: "R x B" "R x A" "R x C"

inductive S where
  "S D (E _)"
| "R x y ⟹ S (E x) (E y)"

inductive_cases [elim]: "S x D" "S x (E y)"

Я могу доказать лемму elim с помощью двух вспомогательных лемм: 

lemma tranclp_S_x_E:
  "S⇧+⇧+ x (E y) ⟹ x = D ∨ (∃z. x = E z)"
  by (induct rule: converse_tranclp_induct; auto)

(* Let's assume that it's proven *)
lemma reflect_tranclp_E:
  "S⇧+⇧+ (E x) (E y) ⟹ R⇧+⇧+ x y"
  sorry

lemma elim:
  "S⇧+⇧+ x (E y) ⟹
   (x = D ⟹ P) ⟹ (⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P) ⟹ P"
  using reflect_tranclp_E tranclp_S_x_E by blast

Мне нужно доказать elim с помощью Изара: 

lemma elim:
  assumes "S⇧+⇧+ x (E y)"
    shows "(x = D ⟹ P) ⟹ (⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P) ⟹ P"
proof -
  assume "S⇧+⇧+ x (E y)"
  then obtain z where "x = D ∨ x = E z"
    by (induct rule: converse_tranclp_induct; auto)
  also have "S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y"
    sorry
  finally show ?thesis

Но я получаю следующие ошибки: 

No matching trans rules for calculation:
    x = D ∨ x = E z
    S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (S⇧+⇧+ x (E y)) ⟹ P

Как их исправить?

Полагаю, эта лемма могла бы иметь более простое доказательство.Но мне нужно доказать это в два этапа:

  1. Показать возможные значения x
  2. Показать, что E отражает переходное замыкание

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

1 Ответ

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

Этот вариант работает: 

lemma elim:
  assumes "S⇧+⇧+ x (E y)"
      and "x = D ⟹ P"
      and "⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P"
    shows "P"
proof -
  have "S⇧+⇧+ x (E y)" by (simp add: assms(1))
  then obtain z where "x = D ∨ x = E z"
    by (induct rule: converse_tranclp_induct; auto)
  moreover
  have "S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y"
    sorry
  ultimately show ?thesis
    using assms by auto
qed
  • Предположения должны быть отделены от цели.
  • В качестве первого утверждения я должен использовать have вместо assume,Это не новое предположение, просто существующее.
  • Вместо finally я должен использовать ultimately.Кажется, что у более поздней логики приложения более простая.
...