Симп не использует предоставленную лемму в Изабель - PullRequest
Новая
       107

Симп не использует предоставленную лемму в Изабель

2 голосов
/ 21 января 2020

Я делаю Упражнение 2.6 из книги Конкретная семантика :

Начиная с типа 'дерева, определенного в тексте, определите содержимое функции ::' дерева ⇒ 'список, который собирает все значения в дереве в списке в любом порядке, не удаляя дубликаты. Затем определите функцию sum_tree :: nat tree ⇒ nat, которая суммирует все значения в дереве натуральных чисел и доказывает sum_tree t = sum_list (содержимое t) (где sum_list предопределен).

Я начал доказывать теорему, не используя авто, а руководствуясь Изабель, чтобы использовать необходимые теоремы: 

theory Minimal

imports Main

begin

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

fun contents :: "'a tree ⇒ 'a list" where
  "contents Tip = []"
| "contents (Node l a r) = a # (contents l) @ (contents r)"

fun sum_tree :: "nat tree ⇒ nat" where
  "sum_tree Tip = 0"
| "sum_tree (Node l a r) = a + (sum_tree l) + (sum_tree r)"

lemma sum_list_contents: 
  "sum_list (contents t1) + sum_list (contents t2) = sum_list (contents t1 @ contents t2)"
  apply auto
  done

lemma sum_commutes: "sum_tree(t) = sum_list(contents(t))"
  apply (induction t)
   apply (simp only: sum_tree.simps contents.simps sum_list.Nil)
   apply (simp only: sum_list.Cons contents.simps sum_tree.simps  sum_list_contents)

Здесь она приходит в состояние доказательства 

proof (prove)
goal (1 subgoal):
 1. ⋀t1 x2 t2.
   sum_tree t1 = sum_list (contents t1) ⟹
   sum_tree t2 = sum_list (contents t2) ⟹
   x2 + sum_list (contents t1) + sum_list (contents t2) = x2 + sum_list (contents t1 @ contents t2)

Где мне интересно, почему simp не использовал предоставленную sum_list_contents лемму. Я знаю, что простое simp решит уравнение.

Что общего simp содержит, что simp only не будет использовать в этом случае?

1 Ответ

2 голосов
/ 21 января 2020

Как указано в комментариях, отсутствующим элементом является ассоциативность сложения для натуральных чисел. Добавление add.assoc к правилам simpplification решает уравнение.

В качестве альтернативы можно изменить порядок операндов при определении суммы дерева: 

fun sum_tree_1 :: "nat tree ⇒ nat" where
  "sum_tree_1 Tip = 0"
| "sum_tree_1 (Node l a r) = a + ((sum_tree_1 l) + (sum_tree_1 r))"

Тогда ассоциативность не требуется: 

lemma sum_commutes_1: "sum_tree_1(t) = sum_list(contents(t))"
  apply (induction t)
   apply (simp only: sum_tree_1.simps contents.simps sum_list.Nil)
  apply (simp only: sum_list.Cons contents.simps sum_tree_1.simps sum_list_contents)
  done
...