The Coq mailing list

[Helge Bahmann <hcb AT chaoticmind.net>]

Hello all,

I have expressions of the kind:

  f (
    let (x', _) := foo x in
    let (x'', _, _) := bar x' in
    let (x''', _) := baz x'' in
    x''')

which needs to be reduced for a proof, and there are
rules available for performing reduction per each individual
inner operator. There are different ways that I can present these, but
essentially they are all of the kind:
  
  let (x', _) := baz x in f x' = g_baz (f x)

What I am looking is for ways to automate applications of
these reductions. These need to be performed
"inside out" (first reduce f/baz, then f/bar, then f/foo), but
I always hit a wall trying to formulate the lifting required
in a generalizable fashion.

Does anyone have a trick handy that could apply in a situation
like this? Possibly even automating the case analysis, I already
have trouble with that (given that "foo x"/"bar x"/"baz x" all
have different types and I cannot seem to generalize over that).

Thanks,
Helge