Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is non-strict positivity ever okay?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is non-strict positivity ever okay?


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Is non-strict positivity ever okay?
  • Date: Wed, 15 Apr 2020 00:55:32 +0200 (CEST)

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




Archive powered by MHonArc 2.6.18.

Top of Page