The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

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


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay