The ceval definitions

[AdamBJ]

How come I can apply E_Ass here:

7 subgoal
st : state
a1 : aexp
x : id
H : (x ::= a1) / st || update st x (aeval st a1)
______________________________________(1/7)
constfold_0plus (x ::= a1) / st || update st x (aeval st a1)

But I can't apply E_Seq here:

6 subgoal
st : state
st' : state
c1 : com
c2 : com
st'0 : state
H0 : c1 / st || st'0
H1 : c2 / st'0 || st'
H : (c1;; c2) / st || st'
______________________________________(1/6)
constfold_0plus (c1;; c2) / st || st'

Also, why can't I rewrite the goal below using optimize_0plus_com_sound (the definition unfolds to

1 subgoals
______________________________________(1/1)
forall c : com, cequiv c (optimize_0plus_com c

)

6 subgoal
st : state
st' : state
c1 : com
c2 : com
st'0 : state
H0 : c1 / st || st'0
H1 : c2 / st'0 || st'
H : (c1;; c2) / st || st'
______________________________________(1/6)
optimize_0plus_com (fold_constants_com (c1;; c2)) / st || st'

[jaewooklee93]

In order to apply E_Ass, the goal should have the following syntactic structure. (See the definition.) (x ::= a1) / st || (update st x n). Does constfold_0plus (x ::= a1) / st || update st x (aeval st a1) have such form? Not exactly, but if you try unfold constfold_0plus, fold_constants_com, optimize_0plus_com, it reduces to that form and Coq just perform such unfolding internally.

Similarly, in order to apply E_Seq, the goal constfold_0plus (c1;; c2) / st || st' should match the syntactic structure (c1 ;; c2) / st || st''. Does it match? Not in this case, even if you perform several number of unfold. unfold will make the goal very complex. You may wonder whether constfold_0plus (c1;; c2) should be same as (constfold_0plus c1;; constfold_0plus c2) so it should satisfy such syntactic structure. However, unfortuantely, that is not the case. Because, constfold_0plus removes unnecessary SKIP term. For example,

Eval compute in constfold_0plus (SKIP;;SKIP).
(* Result: SKIP *)

That's the reason why Coq just complains if you try to use apply E_Seq to that goal.

For the next question, to solve forall c : com, cequiv c (optimize_0plus_com c), it seems that we have to do apply optimize_0plus_com_sound here, but rewrite optimize_0plus_com_sound doesn't work. rewrite only works for = or <-> relations, but cequiv is our custom definition and Coq doesn't accept it to rewrite.

[AdamBJ]

Frustratingly, apply optimize_0plus_com_sound takes optimize_0plus_com (fold_constants_com (c1;; c2)) / st || st' to optimize_0plus_com (optimize_0plus_com (fold_constants_com (c1;; c2))) / st || st'

I guess this is just a case of Coq being dumb about what it applies the theorem too. Perhaps using assert I could get it to do what I want, but is there an easier way? There's no ->/<- for apply like there is for rewrite, right? Is there any way to get that kind of behavior without going through the trouble of using assert?

[jaewooklee93]

Do you mean apply brings (c1;; c2) to (IFB b THEN c1 ELSE c2 FI)? I cannot imagine such cases.

For cequiv, if you use sym_cequiv and trans_cequiv lemmas properly, you can conveniently deal with cexp only using apply, as if you use rewrite ->/<-.

[AdamBJ]

Sorry, I copied the wrong thing. I correct my post. Should have been ... takes it to optimize_0plus_com (optimize_0plus_com (fold_constants_com (c1;; c2))) / st || st'

[jaewooklee93]

Okay. I guess the following may work.

assert (SOUND:=optimize_0plus_com_sound).
unfold ctrans_sound,cequiv in SOUND.
rewrite <- SOUND.

After unfolding, it becomes <-> proposition, so rewrite works then.

But... Is it Assignment08_19.v? Then the best way to avoid such thing is just not to unfold cequiv from the beginning. #134