The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

Indeed, there is an alternative that avoids tricks like Abort instead
of Qed or the use of a false axiom: use modules and functors. The FSet
contrib heavily use such functors
(http://www.lri.fr/~filliatr/fsets/index.en.html).  For example, I made
a development that was assuming some graph implementation, by using a
functor taking as argument a signature for graph. To give you an idea,
it looks like (summarized):

Require FSetInterface.

Module Type Graph.

  Declare Module Node : OrderedType.

  Definition node := Node.t.
  
  Parameter arc : node -> node -> Prop.

  Declare Module NodeSet : S with Module E := Node.

  Parameter successors : node -> NodeSet.t.

  Axiom arc_and_successors :
    (n,m:node)(arc n m)<->(NodeSet.In m (successors n)).

 [...]

End Graph.

then possibly in another file,

Module GraphProperties[G:Graph].

Import G.

Inductive exist_path: node -> node -> Prop := 
| path_refl : (n1,n2:node)(Node.eq n1 n2)->(exist_path n1 n2)
| path_trans : (n1,n2,n3:node)
   (exist_path n1 n2) -> (arc n2 n3) ->
   (exist_path n1 n3)
.

[...]

End GraphProperties.

and again in another file

Module MyApplicationUsingGraphs[G:Graph].

...


So doing, you are able to make your development, while somebody
else is developing one or more implementations of the Graph module.
Also you may have noticed I was using the FSetInterface without
bothering about its implementation, indeed two different ones have
been given by their authors.

- Claude





>>>>> "David" == David Aspinall 
>>>>>Â <David.Aspinall AT ed.ac.uk>
>>>>>  writes:

    David> Dear Coq'ers,
    David> Interesting this has been raised.  Although you may be able to 
simulate
    David> both cases with a proof control command (Abort) or using a false
    David> axiom(!), I think it would be an excellent idea to extend the 
vernacular
    David> to make these important cases explicit.   In particular, this 
would help
    David> not only readers of your scripts but also tools concerned with
    David> generating and analysing proof scripts (something we are looking 
at in
    David> the Proof General Kit project).

    David> For comparison, Isabelle's Isar language uses the words "oops" to 
stop
    David> the proof attempt and forget theorem, and "sorry" to stop the 
    David> proof attempt and retain the theorem --- morally there is a proof
    David> obligation in this second case, although there is no way to 
    David> discharge the obligation later apart from rewriting the script
    David> (as far as I know).
 
    David>  - David.
    
    David> -- 
    David> David Aspinall 
<David.Aspinall AT ed.ac.uk>

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |