The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Luke Palmer wrote:
> On Sun, Feb 22, 2009 at 11:21 AM, Adam Chlipala <adamc AT hcoop.net 
> <mailto:adamc AT hcoop.net>> wrote:
>
>     Robin Green wrote:
>
>              [With Program] The program you write will in general not
>             be the
>
>             Gallina term that you end up with, and it's that Gallina
>             term that
>             you'd need to prove things about.
>                
>
>
>         True, but so what? You can still see the term, but there's no
>         need to
>         put it in the source file.
>          
>
>
>     Terms with coercions are _much_ harder to reason about than terms
>     without.
>
>
> I don't know why you think that you don't need the coercions if you 
> write it by hand.

Well, I think it because it's true. ;-)  Compare the final Gallina terms 
in my original example program to what you get with Program.  I'm having 
trouble running Adam Koprowski's version, probably since I'm still using 
8.1pl3, but I'm guessing there are coercions in the final generated 
terms.  My version definitely ends up with no coercions.