The Coq mailing list

[Pablo Argon <pargon AT cadence.com>]

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