Buenas.
Tengo una hipotesis que es la siguiente:
H : Execute mem1 (IFTHEN (BEnot (BEbool true)) p1 p2) mem2
Al hacerle "inversion", lo hace para TODOS los constructores de Execute. por ejemplo para SKIP que es de la forma Execute mem SKIP mem, no entiendo por que genera este tipo de casos ya que evidentemente SKIP <> IFTHEN.
Saludos
Edu.
Hola.
probaste inversion_clear?
Me parece raro lo que comentás. Si querés mandame el archivo a cluna@fing.edu.uy (indicando bien cuál es el lugar donde aplicás esto) y lo veo.
Saludos, Carlos
Buenas carlos, hice un ejemplo bien reducido donde se ve lo que pasa:
Section asd.
Inductive I: Set:=
| SKIP : I
| ASIGN : I
| BEGEND: LI->I
with LI :=
LI_NIL : LI.
Inductive Execute: I->Prop:=
| EA : True->Execute ASIGN
| EB : False->Execute SKIP.
Lemma lem: Execute SKIP -> False.
Proof.
intros.
inversion_clear H.
Qed.
End asd.
Si saco la referencia a LI dentro de I, hace el "inversion" bien, también si defino LI como un tipo aparte, pero así como está el "inversion_clear" me genera 2 subgoals, uno para EA y otro para EB.
Hola.
En este ejemplo hay un problema, ya que I se define inductivamente con LI.
Considerar la siguiente variante de dico ejemplo:
Inductive I: Set:=
| SKIP : I
| ASIGN : I.
Inductive Execute: I->Set:=
| EA : True->Execute ASIGN
| EB : False->Execute SKIP.
Lemma lem: Execute SKIP -> False.
Proof.
intros.
inversion H.
assumption.
Qed.
Hola Carlos, muchas gracias por tu respuesta, buscando diferencias con el código que publicaste, pude encontrar el problema:
Inductive I: Set:=
| SKIP : I
| ASIGN : I
| BEGEND: LI->I
with LI:=
LI_NIL : LI.
Declaro el tipo de I como "Set" pero no el de LI, en el código que pasaste no declaras en niguno, parece que si declaras uno si y uno no arma lío =P, muchas gracias, tema solucionado.
Saludos.
Hola.
Anexo un código (que está modificado -simplificado-) respecto al ejercicio en cuestión, pero que ilustra el ejercicio pedido y el uso de inversion (inversion_clear).
Saludos
-----------
Definition Var := nat.
Inductive BoolExpr : Set :=
| varExpr : Var -> BoolExpr
| boolExpr : bool -> BoolExpr
| notExpr : BoolExpr -> BoolExpr.
Definition Valor := bool.
Definition Memoria:=Var ->Valor.
Inductive BEval(m:Memoria):BoolExpr->Valor->Prop :=
| eboolt: BEval m (boolExpr true) true
| eboolf: BEval m (boolExpr false) false
| enott: forall e: BoolExpr, BEval m e true -> BEval m (notExpr e) false
| enotf: forall e: BoolExpr, BEval m e false -> BEval m (notExpr e) true.
Inductive I :=
| skip: I
| if_then_else: BoolExpr -> I -> I -> I
| while_do: BoolExpr -> I -> I
| begin_end : LI -> I
with LI :=
| nilLI: LI
| consLI: I -> LI ->LI.
Infix "::" := consLI (at level 60, right associativity).
Inductive Execute : Memoria -> I -> Memoria -> Prop :=
| xSkip m : Execute m skip m
| xIFthen m : forall c:BoolExpr, forall p1 p2:I, forall m1:Memoria, BEval m c true -> (Execute m p1 m1) -> (Execute m (if_then_else c p1 p2) m1)
| xIFelse m : forall c:BoolExpr, forall p1 p2:I, forall m2:Memoria, BEval m c false -> (Execute m p2 m2) -> (Execute m (if_then_else c p1 p2) m2)
| xWhileTrue m : forall c:BoolExpr, forall p:I, forall m1 m2:Memoria, BEval m c true -> Execute m p m1 -> Execute m1 (while_do c p) m2 -> Execute m (while_do c p) m2
| xWhileFalse m : forall c:BoolExpr, forall p:I, BEval m c false -> Execute m (while_do c p) m
| xBeginEnd m : forall p:LI, forall m1:Memoria, ExecuteLI m p m1 -> Execute m (begin_end p) m1
with ExecuteLI : Memoria -> LI -> Memoria -> Prop :=
xEmptyBlock m : ExecuteLI m nilLI m.
Lemma LIF : forall e1 e2:I, forall m m1:Memoria,
Execute m (if_then_else (notExpr (boolExpr true)) e1 e2) m1 -> Execute m (if_then_else (boolExpr true) e2 e1) m1.
Proof.
intros.
inversion_clear H.
inversion_clear H0.
inversion_clear H.
apply xIFthen.
apply eboolt.
assumption.
Qed.
