The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Guillaume, I think I see your point.  I think you are advocating for a
style of reflection where one has to prove:

  Theorem reflection_works: 
     forall (f : Sorted_formula), 
       (solve_sorted f = true) -> sfDenote atomics f

where solve_sorted performs the reflection, and can only access the
reified formula, not its denotation in any way.  With the performance
advantage that it only needs to return a bool.  That's not the style of
reflection I picked up from CPDT.

But I certainly see how it would be an improvement.

Also, it seems that any opaque theorems about real lists would be
used solely within the proof of reflection_works and not
within solve_sorted, which would only compute on reified lists.

I'll think about how to re-implement this in that style.  Thanks.

Jonathan


On Tue, 30 Jun 2020 20:53:54 +0200
Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

> Le 30/06/2020 à 20:00, jonikelee AT gmail.com a écrit :
> > I've attached the now working reflection code as a stand-alone .v
> > file, so that you can judge if it does reflection properly.  
> 
> Your final theorem states:
> 
> reflect_sorted :
> forall (A : Set) (ordA : Ordered A)
>   (atomics : list (@Atom A)) (f : Sorted_formula),
> if solve_sorted atomics f then sfDenote atomics f else True
> 
> Your decision procedure "solve_sorted" suffers from two flaws, in my
> opinion. First, it takes "atomics" as argument, that is, it has access
> to all the atoms and performs computations on them, instead of
> considering them as opaque. A proper decision procedure would only
> take the reified formula "f" as argument.
> 
> Second, it does not return a value of type "bool" but a value of type
> "option P" with "P:Prop". In other words, it computes a large proof
> term of type "P" for naught. Sure, the return type becomes "bool" if
> you were to extract your procedure and run it outside of Coq, but you
> are running it inside Coq. (Hopefully, the laziness of Coq's
> conversion checker will avoid building the whole proof term, but that
> might require a lot of tweaking using the "Strategy" command.)
> 
> To summarize, I see little hope that a function "solve_sorted" with
> such a signature will ever work in an efficient manner.
> Unfortunately, this signature is a direct consequence of your proof
> style, so I have no simple suggestion to provide.
> 
> Best regards,
> 
> Guillaume