The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Helge,

I wonder how you do this "inside out" even without automation. As far as I 
know rewrite doesn't work under binders (let), so it should not be possible 
to do the rewrites inside out even non automated. Or are you using 
setoid_rewrite?

If you tell me how you do it manually (just send me a short working example), 
I can likely help you to automate it.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Helge Bahmann
Sent: Monday, August 10, 2015 10:19 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Let lifting/unwinding?

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

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928