Exists tactic on hypotheses in the context

[AdamBJ]

If we have something like:

IHc1 : no_whiles c1 = true -> forall st : state, exists st' : state, c1 / st || st'

in the context, how can we assert that some case exists? For a goal we could do something like exists st, but I'm not sure how to do it when I'm working with something in the context.

[jeehoonkang]

• You have to provide H: no_whiles c1 = true and st to use IHc1.
• Do: destruct (IHc1 H st) as [st' ST'].

Jeehoon

[AdamBJ]

That works, the only problem is if st' already exists in the context I get a message that says st' is already used. The reason I want to do the destruct in the first place though is to assert that those two states are equal! It seems strange that this would be an error as IHc1 says "forall st". It seems like it should say "for all states not already introduced into the context" though. Is there a way around this?

[jeehoonkang]

I am not quite sure what you want, but I guess:

• is destruct (IHc1 H st') as [st'' ST''] good for your purpose?
• if not, would you please give me more information on context and goal?

Jeehoon

[AdamBJ]

I see why it doesn't work now, I'll try to find a workaround.

[AdamBJ]

Say my context includes IHc2 : no_whiles c2 = true -> forall st : state, exists st' : state, c2 / st || st' and I'm trying to prove c2 / st' || st'. I think it should be possible to do this, since IHc2 is "forall st, exists st'". If I assert that st' = st' I should be able to solve the goal right? Since IHc2 is forall st. What are the semantics for this kind of operation though? I'm not sure how to translate my thought into Coq.

[AdamBJ]

I should also say that I have H1 : no_whiles c2 = true in the context.

[jeehoonkang]

The hypothesis IHc2 merely asserts existence of st' such that c2 / st || st', but we cannot guarantee that such st' is the one already in the context.

If you want to proceed, you have to prove the uniqueness of the semantics: if c2 / st || st' and c2 / st || st'' then st' = st''. If you cannot prove this, it is a sign that you have to rethink your proof structure.

Jeehoon

[jaewooklee93]

First, st' in IHc2 (under the exists) and another st', you already fixed with exists st', in your context are not the same object.

Your goal may look like exists st' : state, (c1;; c2) / st || st' at the beginning. You should determine what is the solution st' of (c1;; c2) / st || st' from both of IHc1 and IHc2, first, and then prove your goal. However, it seems that you tried to provide the wrong solution using IHc1 only and then use IHc2 to solve the impossible goal. The order of Logic is reversed.