The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Put another way, we can certainly imagine an alternative "Inductive" that allows arbitrary recursive uses of the same predicate, so long as a designated argument has decreased in size.  However, what we've just described is "Fixpoint"!  "Inductive" has no such criteria attached to it.  It is not clear how to maintain the great expressive power of "Inductive" while combining its validity checking with a rule based on an argument decreasing in size -- without just saying "Inductive" should fold in the behavior of "Fixpoint" as a special case, which doesn't sound useful, if we are going to have both commands anyway.

For concreteness in your example, I think Dominique is suggesting

Fixpoint satisfies {A : Type} (xs : list A) (f : Formula) : Prop :=
  match f with
  | FAtomic f => exists xs' x, xs = xs' ++ [x] /\ f x = true
  | FNeg f => ~satisfies xs f
  end.

On 4/14/20 7:09 PM, Dominique Larchey-Wendling wrote:

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