Como convencer a Coq de que a função recursiva fornecida abaixo termina? A função usa dois argumentos indutivos. Intuitivamente, a recursão termina porque um dos argumentos é decomposto.
Especificamente, a função aceita duas árvores como entrada.
Inductive Tree :=
| Tip: Tree
| Bin: Tree -> Tree -> Tree.
Em Trees, eu gosto de fazer o seguinte estilo de indução.
Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -> Tree -> TreePair
| BinTip : Tree -> Tree -> TreePair
| BinBin : TreePair -> TreePair -> TreePair.
Fixpoint pair (l r: Tree): TreePair :=
match l with
| Tip =>
match r with
| Tip => TipTip
| Bin rl rr => TipBin rl rr
end
| Bin ll lr =>
match r with
| Tip => BinTip ll lr
| Bin rl rr => BinBin (pair l rl) (pair lr r)
end
end.
A definição de TreePair é aceita, mas a definição do par de funções gera a mensagem de erro:
Error: Cannot guess decreasing argument of fix.
Então, eu estou interessado em como convencer Coq da rescisão.
pair
seja bem definida. Coq é apenas o veículo.Respostas:
As definições de ponto de fixação da Coq exigem que chamadas indutivas recebam um argumento estruturalmente menor. No fundo, uma construção de ponto de fixação requer um único argumento: não há um conceito interno de definição recursiva sobre dois argumentos. Felizmente, a definição de Coq estruturalmente menor da Coq inclui tipos de ordem superior, o que é extremamente poderoso.
Sua definição de ponto de fixação de dois argumentos segue um padrão simples: o primeiro argumento se torna menor ou o primeiro argumento permanece idêntico e o segundo argumento se torna menor. Esse padrão bastante comum pode ser tratado por um simples reparo em reparo.
Para casos mais complexos, ou se o seu gosto for desse jeito, você pode usar a recursão mais próxima do que é ensinado nos cursos de matemática, construindo o ponto de correção a partir de uma computação em etapas e um argumento separado de fundamentação , geralmente usando uma medida inteira . Você também pode fazer sua definição parecer mais um programa clássico em um idioma não total com uma terminação separada usando o
Program
vernáculo .fonte
fix pair1 r
para o segundo ramo do nível superiormatch
(e, é claro, adaptar o primeiro ramo para retornar um tipo de função de acordo)?