The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-04-22 9:18 GMT+02:00 Gabriel Scherer <gabriel.scherer AT gmail.com>:

The usual style for "code that extracts to what you expect" is to implement the algorithm on the plain, "weakly typed" data structure that you would use in ML, and prove after-the-fact that the invariants hold in a separate lemma. This approach produces code that is "trivially erasable", because after you forget about the lemmas you just have (strongly terminating) ML code written in Gallina syntax.

If I understand correctly, you made two different, orthogonal decisions:

1) you encode logical invariants directly in the data-structure declaration: one of the indices of the "rbtree" inductive is a list of its elements (that is, its semantics), and the constructors expect proofs that this list is sorted -- and you are careful to have this proof in Prop for erasability

2) you wrote all the algorithmic content not as programs, but as proof scripts using tactics, so that the various functions pass as "theorems" whose extraction returns the initial algorithm

Could you comment on why you made those choices? My (relatively limited) personal experience would rather indicate that (1) is not the most practical way to write software as of today (although it's an interesting design option that should be made as practical as possible by improvement to Gallina, in particular allowing tactic scripts as subparts of programs), and that (2) is a bad idea, as it makes code harder to both write and read.

I never tried the recent trunk versions, but when I read the Changelog, it seems that "$(<tactics>)$" allows to write tactics inside of terms. For (2), well, it depends on the set of tactics you use, and on how you use them. I often use the following pattern:

Definition foo (args) : type.
refine (
  term_with_holes_for_proofs
).
  + proof_of_first_hole
  + proof_of_second_hole
  …
  + proof_of_last_hole
Defined.

I find it perfectly readable.
 

An argument in favor of (1) would be that, as most after-the-fact correctness proof in fact follow the structure of the code (or conversely that most implementations are performed in the order natural to also prove them correct), doing the implementation and the proof at the same time would avoid some repeated structure and thus might result in shorter developments. Was this a goal of your approach?

On Mon, Apr 21, 2014 at 9:02 PM, Jonathan <jonikelee AT gmail.com> wrote:

To all,

If you're interested in a way to get full erasability in Coq, or yet another encoding of Red/Black trees in Coq, have a look at:

https://github.com/jonleivent/mindless-coding

Erasability is accomplished by adding a single injectivity axiom to a single wrapper Prop type (Erasable).  The readme explains things, and the Coq file is fairly well commented.

Any comments and/or criticisms are welcome!

-- Jonathan

--
.../Sedrikov\...