eval compute rule

[Flavio L. C. de Moura]

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.


--------------------------------------------------------
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

[AUGER Cédric]

Le Mon, 19 Oct 2009 19:41:46 +0200, Flávio Leonardo Cavalcanti de Moura  
<flaviomoura@...> 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

--------------------------------------------------------
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

[Flavio L. C. de Moura]

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@...> 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
>
>

--------------------------------------------------------
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