Circumvent non-positive occurence

Stream: lean4

[Marcus Rossel]

I'm trying to define LTL. I've defined the syntax:

-- The syntax of LTL.
inductive Proposition (V : Type)
  | true
  | var   (v : V)
  | not   (p : Proposition V)
  | and   (lhs rhs : Proposition V)
  | next  (p : Proposition V)
  | until (lhs rhs : Proposition V)

instance : Coe V (Proposition V) where
  coe := .var

notation "⊤"          => Proposition.true
notation:max "¬" p:40 => Proposition.not p
notation:max "◯" p:40 => Proposition.next p
infixr:35 " ∧ "       => Proposition.and
infixr:30 " U "       => Proposition.until

Now I'd like to define the satisfaction relation as:

def Assignment (V : Type) := V → Bool
def Trace (V : Type) := Nat → Assignment V

-- ERROR: (kernel) arg #5 of 'LTL.Proposition.Sat.not' has a non positive occurrence of the datatypes being declared
inductive Proposition.Sat (σ : Trace V) : Nat → Proposition V → Prop
  | true  :                                                                    Sat σ i ⊤
  | var   : (σ i v = Bool.true)                                              → Sat σ i v
  | not   : (¬ Sat σ i p)                                                    → Sat σ i (not p)
  | and   : (Sat σ i lhs) → (Sat σ i rhs)                                    → Sat σ i (lhs ∧ rhs)
  | next  : (Sat σ (i + 1) p)                                                → Sat σ i ◯p
  | until : (i ≤ j) → (Sat σ j rhs) → (∀ k, (i ≤ k) → (k < j) → Sat σ k lhs) → Sat σ i (lhs U rhs)

As you can see, this produces an error because the not constructor has a non-positive occurrence of Proposition.Sat by virtue of the negation. Is there any way to circumvent this issue by restructuring Proposition.Sat?

Of course, going for a plain definition is always an option:

def Proposition.Sat (σ : Trace V) (i : Nat) : (Proposition V) → Prop
  | true            => True
  | var v           => σ i v = Bool.true
  | not p           => ¬(Sat σ i p)
  | and lhs rhs     => (Sat σ i lhs) ∧ (Sat σ i rhs)
  | next p          => Sat σ (i + 1) p
  | «until» lhs rhs => ∃ j, (i ≤ j) ∧ (Sat σ j rhs) ∧ (∀ k, (i ≤ k) → (k < j) → Sat σ k lhs)

... but I find it tends to be nicer to work with the relations defined as an inductive type.

[Arthur Adjedj]

I would advise you to use the definition version of your predicate here. There isn't really a way to circumvent this kind of strict positivity issue, and fixpoints generally behave better than inductive definitions in Prop (for example, you can get large-elimination out of your def here, but not out of the inductive equivalent, even if it was strictly positive)

[Marcus Rossel]

That's reassuring, thanks!