The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq Users,

I found that in many cases I use asserts, the assert expression is the result
of a hypothesis with precondition, with another hypothesis used as the
precondition.

E.g. in the following (shortened) state:

IHE1_1 : forall (s2 : status) (st2 : state),
         c1 / st || s2 / st2 -> st' = st2 /\ SContinue = s2
H1 : c1 / st || SContinue / st'0
______________________________________(1/10)
st'' = st2 /\ SContinue = SContinue

I can do this:

assert( st'=st'0 /\ SContinue = SContinue ) as EQ1. apply IHE1_1. exact H1.

This can be writte more elegantly, if the hypothesis is used as a function:

assert( EQ1 := IHE1_1 _ _ H1 ).

Coq is even smart enough to figure out the two forall variables, if an
argument for the precondition is given. The advantage of this is, that one
doesn't have to think about what the assert expression should be. This opens
the door for automating this kind of asserts. One would just have to try
hypothesis and see if other hypothesis fit as preconditions. If not all forall
variables can be resolved from the precondition, one could return a Hypotheis,
where this variable is still free.

Unfortunately I am still a Coq beginner and have no idea how one could write a
tactic, which would do this. Some hints would be very welcome.

Or is there a built in tactic, which does this?

Thanks & best regards,

Michael