The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Dear Pablo,

This is certainly not a Coq definition (f should not be
accepted as a parameter because it is used with different instances)
With respect to positivity condition, in order to answer your
question, we need to know how NNot is defined.
Could you please send us your example with enough information to be
executed ?
Thanks in advance,
Christine Paulin.

In his message of Wed April 12, 2000, Pablo Argon writes: 
> Hello all,
>       I want to encode a semantic function as an
> inductive type.
> An excerpt of my code is the following (hope is enough):
> 
> Inductive Seem  [f: (flaxpr Signal)] : nat -> Prop :=
>   semTT     : (t:nat)(Sem (TTrue Signal) t)
> | semFFalse : (t:nat)False -> (Sem (FFalse Signal) t)
> | semnot : (t:nat) (NNot (Sem f) t)->(Sem (snot f) t)
> .
> 
> Rule semnot doesn't comply with the strict positivity condition
> required.
> I remember that somewhere I read that we can 
> transform negative occurrences into positive ones... but I can't
> figure out where.
> 
> Someone can remember me the trick ?
> 
> Thank you all in advance,
>       Pablo A.

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84