Practico 5 Ej 7.6

Practico 5 Ej 7.6

de Rodrigo Javier Vazquez Machado -
Número de respuestas: 4

Buenas.

Avanzando en la demostración haciendo inducción en n1, para el paso base (n1 = 0) llegue a tener que probar que:

S2 = S1

Donde mis hipotesis son las siguientes:

i : Instr

S1, S2 : Memoria

H : Execute (irepeat 0 i) S1 S2

Crei que haciendo inversion en H la prueba saldria muy facilmente dado la regla xRepeatO de Execute:
rxRepeatO    : forall (i: Instr)(S: Memoria), Execute (irepeat 0 i) S S

El problema es que al hacer inversion se me generan 2 pruebas, S2 = S2 (facil con reflexivity) y nuevamente S2 = S1, no me queda claro porque se genera esa segunda prueba.

En respuesta a Rodrigo Javier Vazquez Machado

Re: Practico 5 Ej 7.6

de Rodrigo Javier Vazquez Machado -
Creo entender porque se genera la segunda prueba, vendría a ser por la regla xRepeatS:

xRepeatS : forall (n: nat)(i: Instr)(S S1 S2: Memoria),
Execute i S S1 -> Execute (irepeat n i) S1 S2 -> Execute (irepeat (n+1) i) S S2

El problema es que las hipotesis que se me generan para probar S2 = S1 no me parecen tener mucho sentido:
H3 : Execute i S1 S0
H6 : Execute (irepeat n i) S0 S2
H1 : n + 1 = 0

Almenos en el caso de H1, dado que n es natural, creí que podría usar 'discriminate H1' pero no lo acepta.
En respuesta a Rodrigo Javier Vazquez Machado

Re: Practico 5 Ej 7.6

de Carlos Luna -

Hola Rodrigo.

Como definiste el constructor xRepeatS? La idea es que al hacer inversion o inversion_clear en este caso (con 0) solo haya un caso posible (el otro debería ser para (S n), que lo debería descartar). 

Saludos, Carlos 

 

En respuesta a Carlos Luna

Re: Practico 5 Ej 7.6

de Rodrigo Javier Vazquez Machado -
Fue ese mismo el problema Carlos, mi culpa por usar n +1 en vez de S n, cambiando la definicion a S n salio de una.

Gracias y saludos.