The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

No problem in defining a Fixpoint to Prop. Fixpoint does not imply computable.

---

De: "Agnishom Chattopadhyay" <agnishom AT cmi.ac.in>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mercredi 15 Avril 2020 01:05:04
Objet: Re: [Coq-Club] Is non-strict positivity ever okay?

Not really. I am trying to define a relation between my models and my formulae. This is a semantic notion and in some cases may even be uncomputable. So, I do not really want a Formula -> Bool, but rather some kind of Prop

On Tue, Apr 14, 2020 at 5:56 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Usually one uses a Fixpoint instead of an inductive definition for formula satisfaction.

D.

---

De: "Agnishom Chattopadhyay" <agnishom AT cmi.ac.in>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mercredi 15 Avril 2020 00:30:39
Objet: [Coq-Club] Is non-strict positivity ever okay?

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