Help on the final case of E_WhileLoop, question 18

[AdamBJ]

For question 18, I've managed to solve all the cases of induction on the command c except for the final clause of E_WhileLoop (ie the (WHILE b DO c END) / st' || st'' -> clause). My goal is (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) / st'0 || st'. My context is:

Case := "WHILE" : String.string
b : bexp
c : com
IHc : forall st' st : state,
      c / st || st' -> optimize_0plus_com c / st || st'
st' : state
st : state
H : (WHILE b DO c END) / st || st'
st'0 : state
H2 : beval st b = true
H3 : c / st || st'0
H6 : (WHILE b DO c END) / st'0 || st'

Both inversion on H6 and applying E_WHileLoop on the goal seem to circle back to the where they started from after awhile. I can't rewrite optimize_0plus_bexp b as b because there is no beval, and applying IHc in H3 doesn't seem to do anything useful. Can someone give me a hint about what I'm missing? I'm not looking for a complete answer obviously, just something that can help me get unstuck!

[jeehoonkang]

I believe the problem is not solvable by induction on the command c. That's becuase while case does not decrease the command c.

You may have to induct on the number of steps in the execution instead of the command itself.

[AdamBJ]

@jeehoonkang can you explain in more detail what you mean by "the number of steps in the execution"?

[jaewooklee93]

Maybe induction on H6 leads you to the goal. In order to do it, you need remember tactic as well.

But it is just my guess

[AdamBJ]

@jaewooklee93 But?

[jaewooklee93]

Ah I accidently clicked comment button before I finished my sentence

[AdamBJ]

@jaewooklee93 I'll think about your suggestion more, thanks. My first impression is that it creates more goals that I have to prove with less info in the context though! I think I must be using remember incorrectly.

In general, I've never done induction of something like H6 before (Only on aexp, bexp, com, etc) and I'm having some trouble understanding the subgoals it generates. Could you briefly explain what induction on H6 is doing here? I mean, I know when I do induction on a command I need to prove the goal for each of the inductive rules in the definition of com. What is happening when I do induction on H6?

[jaewooklee93]

If you successfully finished Assignment08_03.v, you might learn how to use remember tactic properly and how induction on (c / st || st') works. Almost every subgoal is cleared by a simple inversion on Heq~~.

Nontrivial subcases are only two, one is for immediate stop and another one is for looping again, but they are actually equivalent to the induction on "the number of repetition"

[jaewooklee93]

I guess that you already did inversion on H and it created H6, but you didn't need to. Just doing induction on H is okay.

[AdamBJ]

Ok, I finally solved it! But now I'm stuck in the exactly same spot in the "->" direction, haha. Can you explain why the induction...; inversion... combo doesn't get rid of the non-while cases in the reverse direction like it did going forward?

8 subgoal
Case := "WHILE" : String.string
b : bexp
c : com
IHc : forall st' st : state,
      optimize_0plus_com c / st || st' -> c / st || st'
st' : state
st : state
H4 : beval st (optimize_0plus_bexp b) = false
loopdef : com
Heqloopdef : loopdef = (WHILE b DO c END)
H : loopdef = (WHILE b DO c END)
______________________________________(1/8)
(WHILE b DO c END) / st || st
______________________________________(2/8)
(WHILE b DO c END) / update st x n || update st x n
______________________________________(3/8)
(WHILE b DO c END) / st'' || st''
______________________________________(4/8)
(WHILE b DO c END) / st'0 || st'0
______________________________________(5/8)
(WHILE b DO c END) / st'0 || st'0
______________________________________(6/8)
(WHILE b DO c END) / st || st
______________________________________(7/8)
(WHILE b DO c END) / st'' || st''
______________________________________(8/8)
(WHILE b DO c END) / st || st'

Instead of a nice Heqloopdef : SKIP = (WHILE b DO c END) like before, we're left with Heqloopdef : loopdef = (WHILE b DO c END) for the SKIP case.

[jaewooklee93]

That's because you used remember tactic on the wrong object.

What induction does is similar to destruct in one sense, that is, it can destroy some of our information. The cure for destruct was destruct eqn. Similarly, the cure for induction is remember.

Thus, you have to choose the object to remember cautiously so that you keep all of your precious information. The rule is simple. You should remember all compound terms in the proposition to perform induction.

[AdamBJ]

@jaewooklee93 But for the "<-" direction, I was able to do remember (WHILE b DO c END) instead of remember (optimize_0plus_com (WHILE b DO c END)) to finish the proof. In fact, when I tried doing remember (optimize_0plus_com (WHILE b DO c END)) for the "<-" direction the inversion didn't get rid of any of the subcases at all!

The "->" direction does seem to follow the rule you as you suggested, ie without the optimize_0plus_com the inversion doesn't do anything. With the optimize... prefix inversion knocks out all but 2 subgoals.

One other thing that I've been struggling with is how to make the inductive hypothesis as general as possible in cases like this. For the last subgoal of this proof for example, my context is involves two inductive hypotheses that nearly fit the goal, but don't quite.

...(WHILE b DO c END) / st || st'
...(WHILE b DO c END) / st' || st''
__________________________________(1/1)
(WHILE b DO c END) / st || st''

I tried to generalize the states in the context before doing induction on H, but since H involves the states I want to generalize I can't do it. Do you have any suggestions?

[jaewooklee93]

In "<-" direction, we perform induction on H : (WHILE b DO c END) / st || st', while we perform induction on H : (optimize_0plus_com (WHILE b DO c END)) / st || st' in "->" direction. Since the target proposition H to do induction are different, the target terms need to be remembered are also different. I meant we should remember all compound terms in the proposition H.

And for your second question, I think I've never seen such context and goal status during doing my homework, but I guess your goal is provable. It depends on what quantifiers are in ... parts. If there is no such ..., I think the goal can be solved by the induction on (WHILE b DO c END) / st || st', but with ..., I can't be sure.

[AdamBJ]

That makes more sense regarding the first point, thanks. For the second part I think I should have been a bit more explicit. I'm looking at one inductive hypothesis in the context in particular:

IHceval2 : (WHILE b0 DO c0 END) = optimize_0plus_com (WHILE b DO c END) ->
           beval st' (optimize_0plus_bexp b) = true ->
           optimize_0plus_com c / st' || st'0 ->
           (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) / st'0
           || st'' -> (WHILE b DO c END) / st' || st''

Where my goal is as stated before. Now, I've got all the implications for IHceval2 in the context (I've just omitted them for readability). If I could just apply IHceval2 to the goal I could solve the proof! But the states are just a little bit off. That's why I wanted to generalize st' and st'': if I could I might have something like IHceval2: forall st' st'' .... which I could use to solve the proof.

[jaewooklee93]

Um..... It is really wild guess, but I think that you had done unnecessary inversion on H before you used remember and induction on H, that produced needless st'0. I think induction is the most delicate tactic so it's better to use it as early as possible. In this case, you'd better perform induction just after you step into Case := "WHILE"

[AdamBJ]

Yeah, I know what you mean about it being very delicate. I've been fiddling with it for hours it seems! I'll keep working at it, thanks for all your help:)

[AdamBJ]

Arrrrrrggg this is so frustrating. I've come so far to be stuck on the final case. I've got rid of st'0 by changing where I do inversion, but I still have the probelm of the IHs not lining up with the goal!

1 subgoals
Case := "WHILE" : String.string
b : bexp
c : com
IHc : forall st' st : state,
      optimize_0plus_com c / st || st' -> c / st || st'
st : state
st' : state
st'' : state
H0 : optimize_0plus_com c / st || st'
IHceval1 : optimize_0plus_com c = optimize_0plus_com (WHILE b DO c END) ->
           (WHILE b DO c END) / st || st'
H : beval st (optimize_0plus_bexp b) = true
Heqloopdef : (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) =
             optimize_0plus_com (WHILE b DO c END)
H1 : (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) / st' || st''
IHceval2 : (WHILE optimize_0plus_bexp b DO optimize_0plus_com c END) =
           optimize_0plus_com (WHILE b DO c END) ->
           (WHILE b DO c END) / st' || st''
______________________________________(1/1)
(WHILE b DO c END) / st || st''

[jaewooklee93]

Well, your context and goal look very nice. I can find it provable by just seeing it.

[AdamBJ]

haha, really? I've been staring at my computer for too long then.

[AdamBJ]

I give up! Hopefully I'll be able to see it in the morning. Good night.

[AdamBJ]

@jaewooklee93 Got it! Thanks again for all your help:)