Como definir uma função indutivamente em dois argumentos no Coq?

14

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.

yhirai
fonte
1
Você já tentou passar l e r juntos como um produto, em vez de usar curry? Isso deve ajudar.
Por Vognsen 30/09/10
1
Algumas pessoas pensam que esta pergunta é sobre programação e está fora do escopo deste site. Embora eu não tenha certeza se concordo, você pode querer saber sobre o possível problema. Se alguém tiver algo a dizer sobre a adequação, escreva na meta-discussão à qual vinculei.
Tsuyoshi Ito
3
Esta questão é realmente sobre a especificação de limites decrescentes monotonicamente nas estruturas de dados para garantir que a operação pairseja bem definida. Coq é apenas o veículo.
Dave Clarke

Respostas:

12

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.

Fixpoint pair l := fix pair1 (r : Tree) :=
  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 (pair1 rl) (pair lr r)
                   end
  end.

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 Programvernáculo .

Gilles 'SO- parar de ser mau'
fonte
Agora eu sei que é isso que eu pedi!
precisa saber é o seguinte
fará alguma diferença se eu for fix pair1 rpara o segundo ramo do nível superior match(e, é claro, adaptar o primeiro ramo para retornar um tipo de função de acordo)?
dia
@ plmday: Trabalho de mão dupla. Eles são extensionalmente equivalentes a alguma definição razoável de extensionalidade e, mais importante, são bem tipificados (a reescrita extensional não altera nenhuma das propriedades relevantes de covariância (positividade)).
Gilles 'SO- stop be evil'