Assignment 08_04

[alkaza]

I did not find any issues describing my problem. I gave up on solving this assignment, because i got stuck on a seemingly simple case which I couldn't prove.

3 subgoal
c1 : com
c2 : com
NOWHL : no_whiles (c1;; c2) = true
IHc1 : no_whiles c1 = true ->
       forall st : state, exists st' : state, c1 / st || st'
IHc2 : no_whiles c2 = true ->
       forall st : state, exists st' : state, c2 / st || st'
st : state
H0 : no_whiles c1 && no_whiles c2 = true
H : exists st' : state, c1 / st || st'
H1 : exists st'' : state, c2 / st || st''
x : state
H2 : c1 / st || x
x0 : state
H3 : c2 / st || x0
(1/3)
c2 / x || x0
______________________________________(2/3)
forall st : state, exists st' : state, (IFB b THEN c1 ELSE c2 FI) / st || st'
______________________________________(3/3)
forall st : state, exists st' : state, (WHILE b DO c END) / st || st'

I tried proving the theorem in the other way but it always comes to this case. What should I do or what am I doing wrong?

[alkaza]

I start by:

  intros. generalize dependent st.
  induction c.

and then get stuck on the third case:

3 subgoal
c1 : com
c2 : com
NOWHL : no_whiles (c1;; c2) = true
IHc1 : no_whiles c1 = true ->
       forall st : state, exists st' : state, c1 / st || st'
IHc2 : no_whiles c2 = true ->
       forall st : state, exists st' : state, c2 / st || st'
st : state
H0 : no_whiles c1 && no_whiles c2 = true
______________________________________(1/3)
exists st' : state, (c1;; c2) / st || st'
______________________________________(2/3)
forall st : state, exists st' : state, (IFB b THEN c1 ELSE c2 FI) / st || st'
______________________________________(3/3)
forall st : state, exists st' : state, (WHILE b DO c END) / st || st'

and doing:

  intros. inversion NOWHL. apply andb_true_iff in H0. inversion H0.
    assert (exists st', c1 / st || st'). apply IHc1. apply H.
    assert (exists st'', c2 / st || st''). apply IHc2. apply H1.
    inversion H2. inversion H3. exists x0. apply E_Seq with x. apply H4.

leads to nowhere.

[jeehoonkang]

You have to exploit IHc1 and IHc2. For this, you have to know no_whiles c1 and no_whiles c2. I believe the context has enough information to proceed in this way.

[alkaza]

But how? Since subgoal is like this:

______________________________________(1/3)
exists st' : state, (c1;; c2) / st || st'

And it should match

c1 / st ⇓ st' 
c2 / st' ⇓ st''   (E_Seq)  
c1;;c2 / st ⇓ st''

But it doesn't...

[alkaza]

When I do this

  intros. inversion NOWHL. apply andb_true_iff in H0. inversion H0.
    assert (exists st', c1 / st || st'). apply IHc1. apply H.
    assert (exists st'', c2 / st || st''). apply IHc2. apply H1.
    inversion H2. inversion H3. exists x0. apply E_Seq with x. apply H4.

I get unsolvable subgoal:

3 subgoal
c1 : com
c2 : com
NOWHL : no_whiles (c1;; c2) = true
IHc1 : no_whiles c1 = true ->
       forall st : state, exists st' : state, c1 / st || st'
IHc2 : no_whiles c2 = true ->
       forall st : state, exists st' : state, c2 / st || st'
st : state
H0 : no_whiles c1 = true /\ no_whiles c2 = true
H : no_whiles c1 = true
H1 : no_whiles c2 = true
H2 : exists st' : state, c1 / st || st'
H3 : exists st'' : state, c2 / st || st''
x : state
H4 : c1 / st || x
x0 : state
H5 : c2 / st || x0
______________________________________(1/3)
c2 / x || x0
______________________________________(2/3)
forall st : state, exists st' : state, (IFB b THEN c1 ELSE c2 FI) / st || st'
______________________________________(3/3)
forall st : state, exists st' : state, (WHILE b DO c END) / st || st'

[AdamBJ]

@alkaza You don't want to unfold the definition of hoare_triple for the questions in this assignment (with the exception of one questions where they tell you to). Instead of leading with inversion like we've done before, you want to use the hoare rules introduced in the two Hoare chapters in the text.

For this question, you should start with something like eapply hoare_seq.. Break down the program until you can apply rules like hoare_asgn to solve the subgoals.

[alkaza]

@AdamBJ but this is HW8, not 9

[AdamBJ]

Oh, woops:p

[alkaza]

@AdamBJ any tips on this one? :)

[AdamBJ]

@alkaza Assignment 8 seems like years ago now! If I manage to finish assignment 9 before the deadline I'll see if I even got that one when I did A8.

[alkaza]

Thnx

[jeehoonkang]

Sorry I am late. Try assert (exists st'', c2 / st' || st''). apply IHc2. apply H1.. instead.

[alkaza]

@jeehoonkang yeah i tried that before, it says:

Error: The reference st' was not found in the current environment.

[alkaza]

Seemed to me

    assert (exists st', c1 / st || st'). apply IHc1. apply H.
    assert (exists st'', c2 / st || st''). apply IHc2. apply H1.

was the only way, but then I get stuck

[AdamBJ]

@alkaza I didn't get 08_04 either

[jeehoonkang]

assert (ST': exists st', c1 / st || st'). apply IHc1. apply H.
destruct ST' as [st' ST'].
assert (ST'': exists st'', c2 / st || st''). apply IHc2. apply H1.
destruct ST'' as [st'' ST''].

[alkaza]

Stuck on the last case in a same way:

3 subgoal
c1 : com
c2 : com
NOWHL : no_whiles (c1;; c2) = true
IHc1 : no_whiles c1 = true ->
       forall st : state, exists st' : state, c1 / st || st'
IHc2 : no_whiles c2 = true ->
       forall st : state, exists st' : state, c2 / st || st'
st : state
H0 : no_whiles c1 = true /\ no_whiles c2 = true
H : no_whiles c1 = true
H1 : no_whiles c2 = true
st' : state
ST' : c1 / st || st'
st'' : state
ST'' : c2 / st || st''
______________________________________(1/3)
c2 / st' || st''

[jeehoonkang]

Ah sorry; replace assert (ST'': exists st'', c2 / st || st''). apply IHc2. apply H1. by assert (ST'': exists st'', c2 / st' || st''). apply IHc2. apply H1.

[alkaza]

Yaaay, thank you so much! Solved it!