Выполнение этого доказательства автоматически на Isabelle

Question

Я сататовал работать с Изабеллой несколько недель назад, и мне трудно сделать некоторые доказательства автоматически. Я просто использовал правило «less_induct», чтобы показать свойство в списке.

theorem cuenta_ordena_1: 
"cuenta (ordena xs) y = cuenta xs y" 

proof(induct "length xs" arbitrary: xs rule: less_induct) 
case less 
show ?case 
proof(cases xs) 
assume "xs=[]" 
    then show ?thesis by simp 
next 
fix a list 
assume "xs=a#list" 
have "length(menores a list)<Suc(length list)" by simp 
also have "... = length (a#list)" by simp 
also have "... = length (xs)" using `xs=a#list` by simp 
finally have 1:"length (menores a list)< length xs" by simp 

have "length(mayores a list)<Suc(length list)" by simp 
also have "... = length (a#list)" by simp 
also have "... = length (xs)" using `xs=a#list` by simp 
finally have 2:"length (mayores a list)< length xs" by simp 

have " cuenta (ordena xs) y= cuenta (ordena (a#list)) y" using `xs=a#list` by simp 
also have "...= cuenta ((ordena (menores a list)) @ (a # (ordena (mayores a list)))) y " by simp 
also have "... = cuenta (ordena (menores a list)) y + cuenta (a # (ordena (mayores a list))) y " by (rule cuenta_append) 
also have "... = cuenta (menores a list) y + cuenta (a # (ordena (mayores a list))) y " using less 1 by simp 
finally have 3:"cuenta(ordena xs) y = cuenta (menores a list) y + cuenta (a # (ordena (mayores a list))) y" by simp 
also have 4:"... = cuenta xs y" 
    proof(cases "a=y") 
    case False 
    then have "cuenta (menores a list) y + cuenta (a # (ordena (mayores a list))) y 
       = cuenta (menores a list) y + cuenta (ordena (mayores a list)) y " by simp 
    also have "... = cuenta (menores a list) y + cuenta (mayores a list) y " using less 2 by simp 
    also have "... = cuenta xs y" 
     proof (cases "y<a") 
     case True 
     hence "cuenta (menores a list) y + cuenta (mayores a list) y 
       = cuenta list y + cuenta (mayores a list) y" by (simp add: cuenta_menores) 
     also have "... = cuenta list y" using "True" by (simp add: cuenta_mayores) 
     also have "... = cuenta (a#list) y" using "False" by simp 
     finally show ?thesis using `xs=a#list` by simp 
     next 
     case False 
     hence "cuenta (menores a list) y + cuenta (mayores a list) y 
       = cuenta (mayores a list) y" by (simp add: cuenta_menores) 
     also have "... = cuenta list y" using "False" by (simp add: cuenta_mayores) 
     also have "... = cuenta (a#list) y" using `¬(a=y)` by simp 
     finally show ?thesis using `xs=a#list` by simp    
     qed 
    finally show ?thesis by simp 
    next 
    case True 
    hence "¬(y<a)" by simp 
    have "cuenta (menores a list) y + cuenta (a # (ordena (mayores a list))) y 
       = cuenta (menores a list) y + Suc(cuenta (ordena (mayores a list)) y) " using "True" by simp 
    also have "... = cuenta (menores a list) y + Suc(cuenta (mayores a list) y) " using less 2 by simp 
    also have "... = Suc(cuenta(mayores a list) y)" using `¬(y<a)` by (simp add: cuenta_menores) 
    also have "... = Suc(cuenta list y)" using `¬(y<a)` by (simp add: cuenta_mayores) 
    also have "... = cuenta (a#list) y" using "True" by simp 
    finally show ?thesis using `xs=a#list` by simp 
    qed 
    finally show ?thesis using 3 4 by simp 
qed 
qed 

Для автоматического доказательства я думаю, что я должен написать что-то вроде этого:

theorem cuenta_ordena: 
    "cuenta (ordena xs) y = cuenta xs y" 
apply (induction "length xs" arbitrary: xs rule: less_induct) 
apply (cases xs) 
apply (auto simp add: cuenta_append cuenta_menores cuenta_mayores) 

Можете ли вы мне помочь?

Спасибо!

Answer 1

На основании вашего доказательства и моего скудного знание испанского языка, я полагаю, ваша теория выглядит следующим образом:

fun mejores :: "('a :: linorder) ⇒ 'a list ⇒ 'a list" where 
    "mejores y [] = []" 
| "mejores y (x#xs) = (if x ≥ y then [x] else []) @ mejores y xs" 

fun menores :: "('a :: linorder) ⇒ 'a list ⇒ 'a list" where 
    "menores y [] = []" 
| "menores y (x#xs) = (if x < y then [x] else []) @ menores y xs" 

lemma length_mejores [simp]: "length (mejores y xs) ≤ length xs" 
    by (induction xs) simp_all 

lemma length_menores [simp]: "length (menores y xs) ≤ length xs" 
    by (induction xs) simp_all 

fun ordena where 
    "ordena [] = []" 
| "ordena (x#xs) = ordena (menores x xs) @ [x] @ ordena (mejores x xs)" 

fun cuenta :: "_ list ⇒ _ ⇒ nat" where 
    "cuenta [] y = 0" 
| "cuenta (x#xs) y = (if y = x then 1 else 0) + cuenta xs y" 

Автоматическое доказательство вы предложили не может работать здесь, потому что, когда вы пишете apply (cases xs), xs переменных который универсально оценивается в цели. Если вы хотите сделать различие в данных по такой переменной, вы должны сделать доказательство Isar (как вы это делали раньше).

Более легкий подход требует меньшего количества вспомогательных лемм будет следующее:

lemma cuenta_append [simp]: "cuenta (xs @ ys) y = cuenta xs y + cuenta ys y" 
    by (induction xs) simp_all 

lemma cuenta_mejores_menores: "cuenta (menores x xs) y + cuenta (mejores x xs) y = cuenta xs y" 
    by (induction xs) auto 

... и доказательство полностью автоматизирован:

lemma "cuenta (ordena xs) y = cuenta xs y" 
    by (induction xs rule: ordena.induct) (auto simp: cuenta_mejores_menores) 

Обратите внимание, что я использовал индукционную правило для ordena функция. Индукция по длине списка, которую вы сделали, более общая, но это затрудняет использование автоматизации. Правило ordena.induct выглядит следующим образом:

P [] ⟹ 
(⋀x xs. 
    P (menores x xs) ⟹ 
    P (mejores x xs) ⟹ 
    P (x # xs)) ⟹ 
P a0 

То есть именно то, что вам нужно здесь. Также обратите внимание, что если вы хотите сделать индукцию по длине списка, использование правила length_induct намного проще, чем индукция натурального числа по самой длине списка, что и было сделано вами.

Кроме того, более простое определение ordena, что не требует дополнительных функций menores и mejores бы:

fun ordena :: "('a :: linorder) list ⇒ 'a list" where 
    "ordena [] = []" 
| "ordena (x#xs) = ordena [y ← xs. y < x] @ [x] @ ordena [y ← xs. y ≥ x]" 

Обратите внимание, что [y ← xs. y < x] просто синтаксический сахар для filter (λy. y < x) xs. Тогда вам не нужно cuenta_mejores_menores больше и может использовать следующую весьма общую лемму о взаимодействии между cuenta и filter:

lemma cuenta_filter [simp]: "cuenta (filter P xs) y = (if P y then cuenta xs y else 0)" 
    by (induction xs) simp_all 

и доказательство проходит автоматически снова:

lemma "cuenta (ordena xs) y = cuenta xs y" 
    by (induction xs rule: ordena.induct) auto