Stream: Coq users

Topic: Help with exist destruct in hypothesis


view this post on Zulip Mycroft92 (May 09 2024 at 15:55):

Hi,
I have a hypothesis as follows:

ctxt: Env.t ident
ck: clock
i: ident
b: bool
IHck: forall st : ST, assign_clk_type ck = Some st -> wst_clock ck st
st: ST
H: assign_clk_type (Con ck i b) = Some st
H': exists (st' : ST) (ty : ident),
       st = st'  [ty] /\ assign_clk_type ck = Some st' /\ Env.find i ctxt = Some ty
1/1
wst_clock (Con ck i b) st

I want to open up H' to 3 different hypotheses. Is there a cleaner way to do it other than repeated destruct on it?

Originally I applied (using apply) a result on the hypothesis to get H'. However I could not find a proper intro pattern to achieve the 3 destruct case I specified.

view this post on Zulip Quentin VERMANDE (May 09 2024 at 16:02):

You can do destruct H' as [x [y [z [t u]]]].

view this post on Zulip Mycroft92 (May 09 2024 at 16:06):

Quentin VERMANDE said:

You can do destruct H' as [x [y [z [t u]]]].

Thank you that was exactly what I was looking for! I guess I can use this directly in the apply as well. I couldn't figure out the intro pattern correctly so far.

view this post on Zulip Kenji Maillard (May 10 2024 at 08:02):

For nested "pairs" like this you can also use destruct H' as (x & y & z & t & u).

view this post on Zulip Mycroft92 (May 10 2024 at 09:34):

Kenji Maillard said:

For nested "pairs" like this you can also use destruct H' as (x & y & z & t & u).

Cool. This is even cleaner. Thanks for all the help.


Last updated: Jun 23 2024 at 03:02 UTC