Quando eu usoFunction para definir uma função não-estruturalmente recursiva no Coq, o objeto resultante se comporta estranhamente quando uma computação específica é solicitada. De fato, em vez de dar diretamente o resultado, oEval compute in ... A diretiva retorna uma expressão bastante longa (normalmente 170.000 linhas). Parece que Coq não pode avaliar tudo e, portanto, retorna uma expressão simplificada (mas longa) em vez de apenas um valor.

O problema parece vir da maneira como provo as obrigações geradas porFunction. Primeiro, achei que o problema vinha dos termos opacos que usei e converti todos os lemas em constantes transparentes. A propósito, existe uma maneira de listar os termos opacos que aparecem em um termo? Ou alguma outra maneira de transformar lemas opacos em transparentes?

Comentei então que o problema veio mais precisamente da prova de que a ordem usada é bem fundamentada. Mas obtive resultados estranhos.

Por exemplo, eu definolog2 sobre os números naturais, aplicando repetidamentediv2. Aqui está a definição:

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | n => S (log2 (Nat.div2 n))
  end.

Eu tenho duas obrigações de prova. O primeiro verifica sen respeita a relaçãolt nas chamadas recursivas e pode ser comprovada facilmente.

forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)

intros. apply Nat.lt_div2. apply le_n_S. apply le_0_n.

O segundo verifica selt é uma ordem bem fundamentada. Isso já está provado na biblioteca padrão. O lema correspondente éCoq.Arith.Wf_nat.lt_wf.

Se eu usar essa prova, a função resultante se comportará normalmente.Eval compute in log24 10. retorna3.

Mas se eu quero fazer a prova pessoalmente, nem sempre entendo esse comportamento. Primeiro, se eu terminar a prova comQed ao invés deDefined, o resultado da computação (mesmo em números pequenos) é uma expressão complexa e não um número único. Então eu usoDefined e tente usar apenas lemas transparentes.

Lemma lt_wf2 : well_founded lt.
Proof.
  unfold well_founded. intros n.
  apply (lemma1 n). clear n.
  intros. constructor. apply H.
Defined.

Aqui, o lema1 é uma prova da indução bem fundamentada nos números naturais. Aqui, novamente, eu posso usar lemas já existentes, comolt_wf_ind, lt_wf_rec, lt_wf_rec1 localizado emCoq.Arith.Wf_natou mesmowell_founded_ind lt_wf. O primeiro não funciona, parece que é porque é opaco. Os outros três trabalham.

Eu tentei provar isso diretamente usando a indução padrão nos números naturais,nat_ind. Isto dá:

Lemma lemma1 : forall n (P:nat -> Prop),
  (forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
  intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
  simpl in H0. apply H0 with (n:=S n).
  - intros. inversion H1.
  - intros. inversion H2.
    + apply H. exact H1.
    + apply H1. assumption.
  - apply le_n.
Defined.

Com essa prova (e algumas variantes),log2 tem o mesmo comportamento estranho. E essa prova parece usar apenas objetos transparentes, então talvez o problema não esteja lá.

Como posso definir umFunction que retorna resultados compreensíveis em valores específicos?