The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Sorry but this is a weird discussion. Semantics is defined recursively not inductively. What you try to do doesn’t make any sense. Sure you can interpret into Prop or Bool. So why don’t you recursively define Formula -> Prop, I just did this recently in my course (even though in agda).

 

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 15 April 2020 at 00:06
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: 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

 

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.