The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

[Previously: Re: [Coq-Club] record field is "lost" if import is used]

I have another problem with Imp.v, which is also related to
"Notation". The following inductive predicate should
be entirely defined using programming language notation,
but Coq is unable to parse "IF b1 THEN c1 ELSE c2" here.
Printing is OK. The conflict is with IF... then... else
from Init/Logic.v which seems to prevent a different use of IF.

Any clue? Is there a convenient solution with scopes?

BTW I'm unsure that "IF" in Init/Logic.v is as important as 
usual connectives ("/\", etc.).

NB. I use http://www.cis.upenn.edu/~bcpierce/sf

Inductive ceval : state -> com -> state -> Prop :=
  | CESkip : forall st,
      SKIP / st ~~> st
  | CEAss  : forall st a1 n l,
      aeval st a1 = n ->
      (l ::= a1) / st ~~> override st l n
  | CESeq : forall c1 c2 st st' st'',
      c1 / st  ~~> st' ->
      c2 / st' ~~> st'' ->
      (c1; c2) / st ~~> st''
  | CEIfTrue : forall st st' b1 c1 c2,
      beval st b1 = true ->
      c1 / st ~~> st' ->
(* should be     (IF b1 THEN c1 ELSE c2) / st ~~> st' *)
      (CIf b1 c1 c2) / st ~~> st'
  | CEIfFalse : forall st st' b1 c1 c2,
      beval st b1 = false ->
      c2 / st ~~> st' ->
(* should be     (IF b1 THEN c1 ELSE c2) / st ~~> st' *)
      (CIf b1 c1 c2) / st ~~> st'
  | CEWhileEnd : forall b1 st c1,
      beval st b1 = false ->
      (WHILE b1 DO c1 LOOP) / st ~~> st
  | CEWhileLoop : forall st st' st'' b1 c1,
      beval st b1 = true ->
      c1 / st ~~> st' ->
      (WHILE b1 DO c1 LOOP) / st' ~~> st'' ->
      (WHILE b1 DO c1 LOOP) / st ~~> st''

  where "c1 '/' st '~~>' st'" := (ceval st c1 st').


Thanks,
JF


On Wed, May 12, 2010 at 09:05:11PM +0200, Hugo Herbelin wrote:
> > to the start of the file where Imp is the theory from B.Pierce et al.'s
> > Software Foundations
> > (http://www.cs.princeton.edu/courses/archive/fall09/cos441/sf/) then I 
> > get the
> > following error message:
>  [...]
> This is a serious drawback of the grammar extensibility. Nothing in
> Coq prevents users to introduce conflicting grammar rules and
> extensions have to be used with care. I agree that this one (about
> ";") is a particularly annoying one but I don't see a solution to work
> around it.
> 
> Hugo Herbelin
> 
> 
> 

-- 
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458