The Coq mailing list

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

Dear James,

I must admit that I have only very rudimentary knowledge of Haskell and Agda 
(I know this is a mistake for both, but I can't help it right now), so I fear 
I can understand at most half of your answer. But I want to point out that my 
proposal was to *remove* possible dependencies of nested proofs, not to add 
them.

I use nested proofs mostly in cases where automated proofs fail for a 
specific subcase and need some additional human insight, which I then 
formulate as nested proof. To me the communication with proof automation is 
very similar to the communication between humans discussing a proof. I give a 
proof sketch and let the automation fill in the details. Sometimes the 
automations "says" "yes I see it", like a human would. Sometimes it says 
"hmm, I agree on everything except this case", and then I explain some 
additional aspect like in the discussion with a human. I usually can't do 
this with assert, because I need to add the lemma to some hint database or 
other proof automation system so that automation can find it. Usually the 
lemma does not solve the goal immediately, it just helps the automation is 
some way to solve it.

Best regards,

Michael
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
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928