The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

Hi Jonathan --

On Wed, Jul 1, 2020 at 3:30 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Tue, 30 Jun 2020 11:37:43 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

> It is a bit unfortunate that Coq's reduction mechanism works in this
> way, I too have often found that there are times that I would like to
> do lightweight computation using efficient reduction mechanisms. My
> understanding is that IPM suffers some of the same issues, you want to
> partition the hypotheses efficiently, but you don't want to compute
> inside them and it doesn't always make sense to go the full Atom
> route that Guillaume suggested above.

I am considering Guillaume's suggestion, and it does sound like a
difficult translation to pull off.  I'm still game to try it to see
what happens.  Since I already have the functions needed for
solve_sorted, I should be able to translate them from proof-carying to
bool-returning form.  But I still anticipate difficulties in the
proof of reflection_works needed here:

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

I don't think that this would be a very difficult translation to pull off. In most cases there is a mechanical translation.

>
> One thing that I've wanted for a while is the ability to control
> reduction with quoting and anti-quoting mechanisms a.la. meta
> programming. For example, something that would look roughly like this.
>
> Compute List.rev ((QUOTE (List.rev []) :: QUOTE (a ++ b) :: nil) ++
> []). = [QUOTE (List.rev []); QUOTE (a ++ b)]
>
> Note that QUOTE semantically acts as id, but for the purposes of
> reduction it blocks reduction of its "argument" (it really only allows
> substitutions). This would make it possible to write what you want
> without needing to introduce names. It also allows you to eliminate
> the required phase separation in standard reflective automation as
> mentioned by Guillaume (chapter 4, specifically 4.3, of my
> dissertation discusses some of these issues as well:
> https://gmalecha.github.io/publications/files/malecha-dissertation.pdf).

I have been having a discussion elsewhere with an Idris developer
involved in implementing erasability in Idris (now Idris2).  The new
Idris2 erasability binder annotations sound like they could be used in
the same way as you describe QUOTE, allowing one to selectively
determine which functions can and cannot compute on which arguments.
Furthermore, as they are built into Idris2, the language itself can
easily take advantage - skipping them completely during computation, not
just during extraction.  I wish Coq has something similar, as it
would also allow me to drop the erasure axiom (relevant Prop) hack I use
elsewhere.

I think that QUOTE is a little bit different than erasability in general, though it might operate the same way for your purpose. Consider, for example, you have a reflective procedure that doesn't solve the goal:

Definition simplify_things (ls : list Prop) : list Prop.

Theorem simplify_things_ok : forall ls,

   goalD (simplify_things ls) -> goalD ls.

You can clearly still phrase this in the standard fully-reflective style (as Guillaume suggested):

Definition rsimplify_things (ls : list term) : list term.

Theorem simplify_things_ok' : forall (ls ls' : list term),

  rsimplify_things ls = ls' ->

  forall mp : instantiation, goalD mp ls' -> goalD mp ls.

but things are a bit more verbose. Especially, note the (seemingly useless) equality proof, which hangs around because we want to use [vm_compute] to reduce [rsimplify_things], but we can not use [vm_compute] to simplify [goalD] because doing that would destroy the structure of our propositions.

Using QUOTE, you can write the original soundness theorem, and simply introduce a QUOTE around every symbol that you want to leave uninterpreted.

In your context, you could write 

Theorem reflection_works' : forall (f : Sorted_formula),

    if solve_sorted f then sfDenote f else True.

Which allows you to avoid the [eq_refl _ true : solve_sorted f = true] term in the resulting proof. This can be nice if [f] is large, we usually address it by introducing a [let f := ..]. It becomes more of a problem if, as in the problem above, the decision procedure returns a new goal (which has a large representation).

(BTW, why did the Coq Quote tactic get eliminated?)

I believe it was difficult to use effectively.

I will look more closely at your dissertation as well.

Jonathan

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING