The Coq mailing list

[Fl�vio Leonardo Cavalcanti de Moura <flaviomoura AT unb.br>]

Hi, 

Yes, Defined solved the problem.

Thanks a lot!

Flavio.

Em Seg, 2009-10-19 Ã s 19:58 +0200, AUGER escreveu:
> Le Mon, 19 Oct 2009 19:41:46 +0200, Flávio Leonardo Cavalcanti de Moura  
>Â <flaviomoura AT unb.br>
>  a écrit:
> 
> > Hi,
> >
> >  I am building an exercise in proposicional logic for undergraduate
> > students. I defined a recursive function to propagate negations over
> > conjunctions and disjunction (de Morgan laws) and to eliminate double
> > negations. Here is the function:
> >
> >  Function nnf (t:fprop) {measure flength t}: fprop :=
> >   match t with
> >     | neg(neg F) => nnf F
> >     | con F G => con (nnf F) (nnf G)
> >     | dis F G => dis (nnf F) (nnf G)
> >     | neg(con F G) => dis (nnf (neg F)) (nnf (neg G))
> >     | neg(dis F G) => con (nnf (neg F)) (nnf (neg G))
> >     | _ => t
> >   end.
> >
> > The type fprop is inductive. The proof of termination of nnf is simple;
> > when I try to use "Eval compute" to run some examples the reduction is
> > not performed...
> >
> > When I try
> >
> > Eval compute in (nnf(neg(con (var "p") (var "q")))).
> >
> > I get
> >
> >   = let (v, _) := nnf_terminate (neg (con (var "p") (var "q"))) in v
> >      : fprop
> >
> > What should I do in order to get (dis (neg (var "p")) (neg (var "q")))?
> 
> I never use Function, but in your case as compute doesn't unfold  
> nnf_terminate,
> I assume you defined it opaque (with a Qed somewhere); try to define it
> transparently (with Saved or Defined), and it should be ok I think
> 
> >
> > Thanks in advance,
> >
> > Flavio.
> >
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.saclay.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
>