Cuando usoFunction Para definir una función recursiva no estructural en Coq, el objeto resultante se comporta de manera extraña cuando se solicita un cálculo específico. De hecho, en lugar de dar directamente el resultado, elEval compute in ... La directiva devuelve una expresión bastante larga (típicamente 170 000 líneas). Parece que Coq no puede evaluar todo y, por lo tanto, devuelve una expresión simplificada (pero larga) en lugar de solo un valor.

El problema parece provenir de la forma en que pruebo las obligaciones generadas porFunction. Primero, pensé que el problema provenía de los términos opacos que usé, y convertí todos los lemas a constantes transparentes. Por cierto, ¿hay alguna manera de enumerar los términos opacos que aparecen en un término? ¿O alguna otra forma de convertir lemas opacos en transparentes?

Luego comenté que el problema surgió más precisamente de la prueba de que el pedido utilizado está bien fundado. Pero obtuve resultados extraños.

Por ejemplo, definolog2 en los números naturales aplicando repetidamentediv2. Aquí está la definición:

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

Tengo dos obligaciones de prueba. El primero verifica quen respeta la relaciónlt en las llamadas recursivas y se puede probar fácilmente.

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.

El segundo verifica quelt Es un orden bien fundado. Esto ya está probado en la biblioteca estándar. El lema correspondiente esCoq.Arith.Wf_nat.lt_wf.

Si uso esta prueba, la función resultante se comporta normalmente.Eval compute in log24 10. devoluciones3.

Pero si quiero hacer la prueba yo mismo, no siempre obtengo este comportamiento. Primero, si termino la prueba conQed en lugar deDefined, el resultado del cálculo (incluso en números pequeños) es una expresión compleja y no un solo número. Entonces usoDefined e intente usar solo lemas transparentes.

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

Aquí, lemma1 es una prueba de la inducción bien fundada sobre los números naturales. Aquí nuevamente, puedo usar lemas existentes, comolt_wf_ind, lt_wf_rec, lt_wf_rec1 situado enCoq.Arith.Wf_nat, o inclusowell_founded_ind lt_wf. El primero no funciona, parece que esto se debe a que es opaco. Los otros tres trabajan.

Traté de demostrarlo directamente usando la inducción estándar en los números naturales,nat_ind. Esto da:

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.

Con esta prueba (y algunas variantes de la misma),log2 Tiene el mismo comportamiento extraño. Y esta prueba parece usar solo objetos transparentes, por lo que tal vez el problema no esté allí.

¿Cómo puedo definir unFunction que devuelve resultados comprensibles en valores específicos?