The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Sorry for the click-baity title.

I have a situation where I want to define the semantics of some formulae like textbooks usually do:

Inductive Formula {A: Type} : Type :=
  | FAtomic: (A -> bool) -> Formula
  | FNeg: Formula -> Formula
.

Inductive satisfies {A : Type} : list A -> Formula -> Prop :=
| sat_atomic : forall (f : A -> bool) x xs, f x = true
                                            -> satisfies (xs ++ [x]) (FAtomic f)
| sat_neg : forall xs f, ((satisfies xs f) -> False)
                           -> satisfies xs (FNeg f)
.

The last clause in the inductive predicate does not go through since it puts `satisfies` in a negative position.

I'd however think that this is not so bad because: (1) This is a standard way to define the semantics of negation and also (2) the second argument of satisfies is structurally bigger in the result.

Is there any chance I can convince Coq of (2) or some other reason that would make it work?

I have tried interchanging the order of the arguments of satisfies but that did not help.

--Agnishom