The Coq mailing list

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

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")))?

Thanks in advance, 

Flavio.