The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Thu, 12 Jan 2012 17:59:03 +0100,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 a écrit :

> 2012/1/12 Luminous Fennell 
> <mstrlu AT gmx.net>
> 
> > On Thu, Jan 12 2012 at 17:06 +0100, Adam Chlipala wrote:
> >
> > > Luminous Fennell wrote:
> > >> Over the holidays, I wrote some Haskell code to export Coq
> > >> definitions to LaTeX or ASCII documents.[...]
> > >>
> > >> My questions is, if it would be worth it to put a little bit
> > >> more effort in this (i.e. making a real project out of this). Is
> > >> there already such a tool? And if not would anybody else be
> > >> interested or find this useful?
> > >>
> > >
> > > Have you looked at coqdoc, which is included in the standard Coq
> > > distribution?  It has been used successfully to typeset several
> > > books. (It only covers LaTeX and HTML, not ASCII.)
> >
> > Well, coqdoc is more a tool for code documentation; it's great for
> > exporting the actual source code, but I would be more interested in
> > exporting the definitions in a more informal form, like you would
> > write them in an email or paper. So instead of
> >
> > has_type : env -> exp -> ty -> Prop =
> > ...
> > | ht_app : forall e f E t1 t2,    has_type E e (t1 --> t2)
> >                               -> has_type E f t1
> >                               -> has_type E (app e f) t2
> >
> > the tool should give me something like:
> >
> > has_type:
> >
> > ht_app: [ E |- e : t1 --> t2,
> >          E |- f : t1 ]
> >        ==>
> >          E |- e f : t2
> >
> 
> Maybe using Coq Notation capabilities + coqdoc will give you what you
> need..
> 
> 
> >
> > And for the LaTeX version, the output should be close to how I would
> > typeset it manually in a thesis or paper, so that I can keep a
> > automatically generated version as long as possible in the draft.
> >
> > Best regards
> >
> > Lu
> >
> 
> 
> 

I think that the coq distribution lack of some useful tools on that
matter.

IMO, there should also be one mode for Coq, such that the printed
output should always be reparsable (a quick fix  to have it is
deactivation of all sytactic sugar, but it becomes ugly) for example
by desugaring ambiguous notations (I know that it isn't an easy matter
though).

Another interesting tool would be "pre-compiled files", that is that
beside the ".v" and ".vo" generated file, there could be some place for
a ".vg" which could be the ".v" file 'compiled' to pure Gallina (plus
maybe some other informations), so when updating the coq from a version
to an other one, we could just run "coqc myfile.vg" which won't run the
proof scripts of the ".v" file, and thus get a faster compilation.
That could also benefit to Coq theories, since it takes some time to
compile.

I tried what nuno said for this thread. I got some notations which may
interest some people using inference rules, but I find it quite ugly.

Maybe that if some people find parts of it nice it could be added to
the coq contributions (with some improvements of course).

✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂

Require Import Utf8_core.

(**** INFERENCE RULES *****)

Definition make_prop (P:Prop) :=
 fix mp (l:list Prop) :=
 match l with
 | nil => P
 | cons A l => A→(mp l)
 end.

Definition rule1 (P:Prop):Prop := P.
Definition rule2 (P:Prop):Prop := P.
Definition rule3 (P:Prop):Prop := P.
Definition rule4 (P:Prop):Prop := P.
Definition rule5 (P:Prop):Prop := P.

Notation "» x '  ' .. '  ' y '   ' z" :=
 (make_prop z (cons x .. (cons y nil) ..))
 (at level 90, right associativity
 , format "» '[v' '[' x '  ' .. '  ' y '   ' ']' '/' z ']'").
Notation "» '   ' z" :=
 (make_prop z nil)
 (at level 90, right associativity
 , format "» '[v' '   ' '/' z ']'").

(* WARNING: '   ' are unbreakable spaces;
   it is an ugly trick to make unseenable separations
   in the notation; should not be used too much *)

Notation "'─────' x" :=
 (rule1 x)
 (at level 90
 ,format "'[v' '─────' '/' x ']'").
Notation "'────────' x" :=
 (rule2 x)
 (at level 90
 ,format "'[v' '────────' '/' x ']'").
Notation "'─────────────' x" :=
 (rule3 x)
 (at level 90
 ,format "'[v' '─────────────' '/' x ']'").
Notation "'────────────────────' x" :=
 (rule4 x)
 (at level 90
 ,format "'[v' '────────────────────' '/' x ']'").
Notation "'────────────────────────────' x" :=
 (rule5 x)
 (at level 90
 ,format "'[v' '────────────────────────────' '/' x ']'").

(***** CODE *****)

Notation "'ℕ'" := nat.

Inductive type := ι     : type
                | Arrow : type → type → type.
Notation "x ⟹ y" := (Arrow x y) (at level 60, right associativity).

Inductive expr := Var    : ℕ → expr
                | Lambda : ℕ → expr → expr
                | App    : expr → expr → expr.
Notation "[ n ]" := (Var n).
Notation "'Λ'  n · e" := (Lambda n e) (at level 80).
Notation "x ' ' y" := (App x y) (at level 70).
 (*hack: use of unbreakable space*)

Definition add_type (E:ℕ→type) τ n :=
 λ x,
 (fix add m n :=
  match m, n with
  | O, O => τ
  | O, S _ => E x
  | S _, O => E x
  | S m, S n => add m n
  end) n x.
Print Grammar constr.
Notation "E { n ↦ τ }" := (add_type E τ n) (n at level 99, t at level
200, at level 0).

Reserved Notation "E ⊢ e ∷ τ" (at level 70).
Inductive well_typed : (ℕ → type) → expr → type → Prop :=
| Rule1: ∀ E n, »    
                  ─────────────
                  E ⊢ [n]∷E n

| Rule2: ∀ E e₁ e₂ τ₁ τ₂, » E ⊢ e₁∷τ₁⟹τ₂     E ⊢ e₂∷τ₁    
                            ────────────────────────────
                            E ⊢ (e₁   e₂)∷τ₂

| Rule3: ∀ E n e τ₁ τ₂, » E{n↦τ₁} ⊢ e∷τ₂    
                          ────────────────────
                          E ⊢ (Λ n·e)∷τ₁⟹τ₂

where "E ⊢ e ∷ τ" := (well_typed E e τ).

Print well_typed.




> > ht_app: [ E |- e : t1 --> t2,
> >          E |- f : t1 ]
> >        ==>
> >          E |- e f : t2