The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

Yves Bertot wrote:

> Another method, easier to generalize, is to keep the relation between
> (f O) and the couple as an equality.  Here is the technique:
>
> Goal  let (n,_) = (f O) in (n=O).
> Cut (f O)=(f O);[Pattern -1 (f O);Case (f O);Intros n1 n2 H1|Auto].

Thanks. This looks like the kind of mysterious thing that should be a tactic.

Suppose, though, that instead of having the let in the goal it appears in a
hypothesis or definition.

Given

R := [x:T] let (l,r) = x in P /\ Q[l]
H: R a

we want to prove

Q b

or even just P.

It seems that what I want is a commuting conversion, but there doesn't seem
to be any support for these (?).

Ewen