The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

what about defining unsat and sat mutually?

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, notsatisfies xs f
                           -> satisfies xs (FNeg f)
with

notsatisfies {A : Type} : list A -> Formula -> Prop :=
| unsat_atomic : forall (f : A -> bool) x xs, f x = false
                                            -> notsatisfies (xs ++ [x]) (FAtomic f)
| unsat_neg : forall xs f, satisfies xs f
                           -> notsatisfies xs (FNeg f)

I am not sure what's the right notion of unsat in your case but it looks to me now everything occurs positively.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Sent: April 14, 2020 9:27 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Is non-strict positivity ever okay?

 

I think most of this makes sense. Thanks for explaining.

The only issue is that now with the Fixpoint, we don't have a constructor any more. So this means with this definition, I cannot induct on the proof tree of a satisfaction or apply inversion.

On Tue 14 Apr, 2020, 19:44 Adam Chlipala, <adamc AT csail.mit.edu> wrote:

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