Luego de de esta prolongada búsqueda de información dimos con la respuesta esta traba que tienen algunos los lectores. Te dejamos la respuesta y nuestro deseo es resultarte de gran ayuda.
Solución:
En este caso, en realidad no necesita una recursividad bien fundada en toda su generalidad:
Require Import Coq.Lists.List.
Set Implicit Arguments.
Inductive tree := Node : nat -> list tree -> tree.
Fixpoint map_tree (f : nat -> nat) (t : tree) : tree :=
match t with
| Node x ts => Node (f x) (map (fun t => map_tree f t) ts)
end.
Coq es capaz de descubrir por sí mismo que las llamadas recursivas a map_tree se realizan bajo estrictos subterráneos. Sin embargo, probar algo sobre esta función es difícil, ya que el principio de inducción generado para tree no es útil:
tree_ind :
forall P : tree -> Prop,
(forall (n : nat) (l : list tree), P (Node n l)) ->
forall t : tree, P t
Este es esencialmente el mismo problema que describió anteriormente. Afortunadamente, podemos solucionar el problema probando nuestro propio principio de inducción con un término de prueba.
Require Import Coq.Lists.List.
Import ListNotations.
Unset Elimination Schemes.
Inductive tree := Node : nat -> list tree -> tree.
Set Elimination Schemes.
Fixpoint tree_ind
(P : tree -> Prop)
(IH : forall (n : nat) (ts : list tree),
fold_right (fun t => and (P t)) True ts ->
P (Node n ts))
(t : tree) : P t :=
match t with
| Node n ts =>
let fix loop ts :=
match ts return fold_right (fun t' => and (P t')) True ts with
| [] => I
| t' :: ts' => conj (tree_ind P IH t') (loop ts')
end in
IH n ts (loop ts)
end.
Fixpoint map_tree (f : nat -> nat) (t : tree) : tree :=
match t with
| Node x ts => Node (f x) (map (fun t => map_tree f t) ts)
end.
El Unset Elimination Schemes El comando evita que Coq genere su principio de inducción predeterminado (y no útil) para tree. La ocurrencia de fold_right en la hipótesis de inducción simplemente expresa que el predicado P agarra de cada árbol t' apareciendo en ts.
Aquí hay una declaración que puede probar usando este principio de inducción:
Lemma map_tree_comp f g t :
map_tree f (map_tree g t) = map_tree (fun n => f (g n)) t.
Proof.
induction t as [n ts IH]; simpl; f_equal.
induction ts as [|t' ts' IHts]; try easy.
simpl in *.
destruct IH as [IHt' IHts'].
specialize (IHts IHts').
now rewrite IHt', <- IHts.
Qed.
Ahora puede hacer esto con ecuaciones y obtener el principio de eliminación correcto automáticamente, utilizando recursividad anidada estructural o recursividad bien fundada
En general, puede ser aconsejable evitar este problema. Pero si uno realmente quiere obtener la obligación de prueba que le da Isabelle, aquí hay una manera:
En Isabelle, podemos dar un lema externo que las estadísticas map aplica sus argumentos solo a los miembros de la lista dada. En Coq, no podemos hacer esto en un lema externo, pero podemos hacerlo en el tipo. Entonces, en lugar del tipo normal de mapa
forall A B, (A -> B) -> list A -> list B
queremos que el tipo diga "f solo se aplica a los elementos de la lista:
forall A B (xs : list A), (forall x : A, In x xs -> B) -> list B
(Requiere reordenar el argumento para que el tipo de f puedo mencionar xs).
Escribir esta función no es trivial y me resultó más fácil usar un script de prueba:
Definition map A B (xs : list A) (f : forall (x:A), In x xs -> B) : list B.
Proof.
induction xs.
* exact [].
* refine (f a _ :: IHxs _).
- left. reflexivity.
- intros. eapply f. right. eassumption.
Defined.
Pero también puedes escribirlo "a mano":
Fixpoint map A B (xs : list A) : forall (f : forall (x:A), In x xs -> B), list B :=
match xs with
| [] => fun _ => []
| x :: xs => fun f => f x (or_introl eq_refl) :: map xs (fun y h => f y (or_intror h))
end.
En cualquier caso, el resultado es bueno: puedo usar esta función en mapTree, es decir
Program Fixpoint mapTree (f : nat -> nat) (t : Tree) measure (height t) : Tree :=
match t with
Node x ts => Node (f x) (map ts (fun t _ => mapTree f t))
end.
Next Obligation.
y no tengo que hacer nada con el nuevo argumento para f, pero aparece en la obligación de prueba de terminación, como In t ts → height t < height (Node x ts) como se desee. Entonces puedo probar eso y definir mapTree:
simpl.
apply Lt.le_lt_n_Sm.
induction ts; inversion_clear H.
- subst. apply PeanoNat.Nat.le_max_l.
- rewrite IHts by assumption.
apply PeanoNat.Nat.le_max_r.
Qed.
Solo funciona con Program Fixpoint, no con Function, Desafortunadamente.
Sección de Reseñas y Valoraciones
Tienes la opción de confirmar nuestra misión escribiendo un comentario o dejando una valoración te lo agradecemos.