Buenas,
Estoy teniendo problemas para encarar las pruebas de los lemas propuestos en este ejercicio. No me doy cuenta como aplicar las tacticas y no he visto ejemplos de como hacerlo.
Algun pique me de una idea de como comenzar?
Saludos
En respuesta a Agustin Di Vincezo Fernandez
Re: [Practico 2] Ejercicio 10
Buenas, te comento lo que hice yo pero no sé si es lo más eficiente.
Hay una táctica que se llama transitivity. Con esta podés ir armando una cadena de igualdades tal que cada una la podés probar aplicando los axiomas (o lo que sea). La idea es que sólo apliques transitivity a términos que te den igualdades que sabrías probar "en un solo paso".
Hay una táctica que se llama transitivity. Con esta podés ir armando una cadena de igualdades tal que cada una la podés probar aplicando los axiomas (o lo que sea). La idea es que sólo apliques transitivity a términos que te den igualdades que sabrías probar "en un solo paso".
En respuesta a Julian Tricanico Gadea
Re: [Practico 2] Ejercicio 10
Gracias por la respuesta.
En el lema1 he llegado a: S (sum (S O) O) = S (S O) que en una prueba matematica por decirlo de alguna manera, eliminaria la aplicacion de S sobre los dos terminos de la igualdad. En otras palabras aplicar el axioma inj para que me quede la igualdad sum (S O) O = S O y ahi aplicar sum0. Pero no me doy cuenta como hacerlo, si hago apply o elim de inj con diferentes terminos no llego a lo que pretendo.
Saludos
En el lema1 he llegado a: S (sum (S O) O) = S (S O) que en una prueba matematica por decirlo de alguna manera, eliminaria la aplicacion de S sobre los dos terminos de la igualdad. En otras palabras aplicar el axioma inj para que me quede la igualdad sum (S O) O = S O y ahi aplicar sum0. Pero no me doy cuenta como hacerlo, si hago apply o elim de inj con diferentes terminos no llego a lo que pretendo.
Saludos
Hola.
Respondí previamente sobre este lema. Acá inj no te sirve; estás confundiendo hipótesis con tesis (lo que tenés y lo que precisás probar).
Lemma L10_1: (sum (S O) (S O)) = (S (S O)).
Proof.
rewrite sumS.
rewrite sum0.
reflexivity.
Qed.
Saludos, Carlos
Hola Agustin.
Los nuevo en esta parte es que se usa la igualdad. También aparecen más hipótesis (como axiomas), que en particular usan la igualdad.
Para la igualdad una táctica muy necesaria es: rewrite (con las variantes vistas en clase); también está replace, pero esta última no es estrictamente necesaria. La reescritura permite reemplazar un lado de la igualdad por el otro. La información puede estar en una hipótesis (o axioma) y la reescritura se hace en el goal y también en hipótesis si se usa la variante "in". Para probar igualdades (en el goal), las tácticas reflexivity, symmetry y transitivity son utilizadas.
Por ejemplo:
Lemma L10_1: (sum (S O) (S O)) = (S (S O)).
Proof.
rewrite sumS.
rewrite sum0.
reflexivity.
Qed.