Buenas,
En el ejercicio 2.10.7 se puede usar lógica clásica? Estoy teniendo problemas demostrarlo sin lógica clásica.
Hola.
Supongo que te referís al lema: forall m n: Nat, sum m n = O -> m = O /\ n = O.
Se puede usar lógica clásica pero no creo que en este problema te sirva de mucho.
Sugiero usar cosas previas de este ejercicios. En particular:
allNat, sum0, sumS y disc.
La prueba podría comenzar así:
Proof.
intros; elim (allNat n); intros.
...
Saludos, Carlos
Buenas... yo estoy trabajando en ese, quizás lo esté enfocando mal.
Una de las partes del And (forall m n: nat, sum m n = O -> n = O), me resulta sencillo ya que es el contra ejemplo del lema anterior.
Pero a la hora de encarar forall m n: nat, sum m n = O -> m = O se me viene a la mente usar la propiedad conmutativa de la suma, la cual no tenemos demostrada, y no creo que la idea sea demostrarla, o si?
Hola Germán.
Para la prueba no es estrictamente necesario probar la propiedad conmutativa de la suma.
Podés usar cosas previas, por ejemplo:
allNat n, rewrite ... in ..., sum0, sumS , disc, symmetry (táctica de Coq para la igualdad).
La prueba podría comenzar con:
Proof.
intros. elim (allNat n); intros.
...
Saludos, Carlos
Muchas Gracias, ya había arrancado por ahí, pero me tranque anoche.
Ahora salieron casi todos me falta una parte de otro ejercicio.
Buenísimo!
Si precisás, volvé a escribir.
Saludos, Carlos
Hola,
Estoy teniendo problemas con la segunda rama que se genera al aplicar elim(allNat) (la que corresponde al exist). Con la primera rama no hubo problema, pero con la segunda no llego a nada que me permita concluir la prueba o sacar más hipótesis.
Hay alguna cosa que se les ocurra que pueda estar omitiendo?
Gracias,
Noelia
Hola.
Supongo que allNat sobre n lo usás al inicio.
En la rama del existe que mencionás, tenés que eliminar el existe, reescribir en la hipótesis "sum m n = O" el valor para n luego de la eliminación del existe (que es un sucesor). Para esto usá la táctica rewrite ... in .... Luego ahí mismo podés reescribir usando SumS. Dado que ahora hay una contradicción en esta hiótesis, ya que queda un sucesor igual a cero, usás disc y seguramente symmetry para probar el goal.
Saludos, Carlos