The Coq mailing list

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

There is no way to change a negative inductive definition into a
positive one but, in your case, the best thing to do would be to 
define sem as a recursive fuction (using Fixpoint and Cases) over 
flaeexp. In that case there will be no positivity problem.

C. Paulin.

In his message of Thu April 13, 2000, Pablo Argon writes: 
> Christine Paulin wrote:
> > This is certainly not a Coq definition (f should not be
> > accepted as a parameter because it is used with different instances)
> 
>  I'm sorry, it was a cut&paste error from a scratch file,
> below you could see an executable excerpt.
> 
> For example, I should be able to prove:
>       (t:nat)(Sem (snot (FFalse Signal)) t)
>       
> Pablo
> 
> 
> In his message of Wed April 12, 2000, Pablo Argon writes: 
> > Rule semnot doesn't comply with the strict positivity condition
> > required.
> 
> Error: Non strictly positive occurrence of #GENTERM (REL 3) in
>   (t:nat; f:(flaexpr Signal))(NNot (Sem f) t)->(Sem (snot f) t)
> 
> 
> > 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.
> 
> NB: I use V6.3.1 (December 1999)
> 
> Excerpt,
> -------------------------------------
> Require Export Classical_Prop.
> 
> (* The semantic definition of temporal operators *)
> 
> Definition NNot [s : nat->Prop] : nat->Prop :=
>   [t : nat] ~ (s t).
> 
> Definition AAnd [s1, s2 : nat->Prop] : nat->Prop :=
>   [t : nat] (s1 t) /\ (s2 t).
> 
> Inductive FF [s : nat -> Prop] : nat -> Prop
>     := FF_n   : (t:nat) (s t)    -> ((FF s) t)
>     | FF_pred : (t:nat)((FF s) (S t))-> ((FF s) t).
> 
> Implicit Arguments On.
> 
> Section SyntaxFlas.
> 
> Variable Signal : Set.
> 
> Inductive flaexpr : Set :=
>   Var   : Signal -> flaexpr
> | TTrue : flaexpr (* syntactic true  *)
> | FFalse: flaexpr (* syntactic false *)
> | snot  : flaexpr -> flaexpr
> | sFF   : flaexpr -> flaexpr
> .
> End SyntaxFlas.
> 
> 
> Inductive Sem  : (flaexpr Signal) -> nat -> Prop :=
>   semTTrue  : (t:nat)(Sem (TTrue Signal) t)
> | semFFalse : (t:nat)False -> (Sem (FFalse Signal) t)
> | semnot    : (t:nat)(f:(flaexpr Signal)) (NNot (Sem f) t)->(Sem (snot
> f) t)
> .
> 

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