Práctico 6 - Ejercicio 6.5.2

Práctico 6 - Ejercicio 6.5.2

de Noelia Magali Lencina Alfonso -
Número de respuestas: 2

Hola,

Este ejercicio pide usar functional induction pero no estaría viendo cómo aplicarlo ni qué se ganaría haciendo eso en lugar de hacer induction por ejemplo.

Capaz estoy encarando el ejercicio de la manera incorrecta. Lo que tengo además de los dos tipos inductivos para definir Le y Gt es una función definida como fixpoint leBool que mira la forma de los parámetros (nats) para decidir si son menores o iguales. Tengo un caso en el que la función se llama a sí misma recursivamente con parámetros más chicos.

Si intento usar functional induction me pasa que lo tengo que usar después de decidir left o right, y eso hace que me aparezcan goals que no sé cómo probar (por ej.: Le (S k) 0 ). Si lo quiere usar antes de elegir left o right me sale el error "Ltac call to "functional induction (ne_constr_list) (fun_ind_using) (with_names)" failed. Error: cannot find leBool_rec" " que no he sabido cómo resolverlo.

Alguna sugerencia?

Gracias y saludos,

Noelia


En respuesta a Noelia Magali Lencina Alfonso

Re: Práctico 6 - Ejercicio 6.5.2

de Carlos Luna -

Hola Noelia.

Luego de definir la leBool con fixpoint tenés que generar el esquema:

Functional Scheme leBool_rec := Induction for leBool Sort Set.

para usar luego functional induction.

La prueba:

Lemma Le_Gt_dec: forall n m:nat, {(Le n m)}+{(Gt n m)}.

comenzaría con: intros; functional induction (leBool n m).

Los objetivos de prueba que aparece se demuestran con constructor y en algunos casos tenés que usar right (tener en cuenta que + es una disyunción). En el caso en que tenés la hipótesis inductiva (con un +) y tenés que probar el gol (con un +), tenés que eiminar primero la hipótesis (al igual que en un or, primero hay que analizar la hipótesis antes de probar el goal, eligiendo un lado).

Espero que con estas ayudas pueda avanzar.

Por las dudas te aclaro que para poder usar Functional Scheme tenés que importar:

Require Import FunInd.

Saludos, Carlos 



,