splitting up an && hypothesis

[AdamBJ]

I've got the following in my context:

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'
H0 : no_whiles c1 && no_whiles c2 = true

Since no_whiles c1 && no_whiles c2 = true I think no_whiles c2 = true and no_whiles c1 = true. How can I split H0 up so that I can apply it in parts to IHc1 and IHc2?

[jaewooklee93]

I remember there was a Check statement before the problem in the given script to provide a hint to us.

[jeehoonkang]

• SearchAbout andb.
• andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true

[AdamBJ]

Ok, got it. Now I've got:

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'
H0 : no_whiles c1 = true /\ no_whiles c2 = true
st : state
H : no_whiles c1 = true
H1 : no_whiles c2 = true

When I try apply IHc1 in H. I get Error: Unable to find an instance for the variable st. but when I try apply IHc1 in H with st. I get Syntax error: '.' or '...' expected after [tactic:tactic] (in [proof_mode:subgoal_command])..

[jeehoonkang]

You can try in many ways. To name two:

• eapply
• generalize (IHc1 H st).