feat: Linear Temporal Logic

[mell-o-tron]

Hi! Here is my first attempt at formalizing LTL, by providing a semantics on omega-sequences and a few simple rules. I think this could be quite easily adapted to obtain a semantics on paths of transition systems.

I hope you'll forgive my naive proof style, I'm fairly new to Lean, and I hope we can work on this together to make it up to standards :)

[eric-wieser]

Suggested change

	def Satisfies (ls : ωSequence (Set T)) (φ : Proposition T) := match φ with
	def Satisfies (ls : ωSequence (Set T)) : Proposition T → Prop

[eric-wieser]

Suggested change

	| .next φ => Satisfies (ωSequence.drop 1 ls) φ
	| .next φ => Satisfies (ls.drop 1) φ

etc

[eric-wieser]

Suggested change

	def Proposition.equiv (φ₁ : Proposition T) (φ₂ : Proposition T) :=
	def Proposition.equiv (φ₁ : Proposition T) (φ₂ : Proposition T) : Prop :=

[eric-wieser]

style should be

Suggested change

	theorem next_self_dual {T} : ∀ (φ : Proposition T), φ.next.not ≈ φ.not.next :=
	by simp
	theorem next_self_dual {T} : ∀ (φ : Proposition T), φ.next.not ≈ φ.not.next := by
	simp

(throughout)

[eric-wieser]

Suggested change

	theorem expansion_until {T} : ∀ (φ : Proposition T) (ψ : Proposition T) ,
	Proposition.until_op φ ψ ≈ Proposition.or ψ (Proposition.and φ ((Proposition.until_op φ ψ).next)) :=
	by
	intros
	theorem expansion_until {T} (φ : Proposition T) (ψ : Proposition T) :
	φ.until_op ψ ≈ ψ.or (φ.and ((φ.until_op ψ).next)) := by

[eric-wieser]

Suggested change

	inductive Proposition (T : Type) : Type u where
	inductive Proposition (T : Type u) : Type u where

[ctchou]

These are my specific comments. I will give my general comments on Zulip:
#CSLib > LTL?

[ctchou]

You can put your name here.

[ctchou]

non-branching -> linear.

[ctchou]

Any reason implies and leads_to are not among the operators? Alternatively, can we take seriously the idea that (for example) always and eventuallycan be defined as derived operators and reduce this inductive definition to a minimal set of operators?

[ctchou]

Would it be possible to give \models a higher precedence than \iff, so that we can get rid of the parentheses on the LHS of \iff?

[ctchou]

Instead of Proposition.equiv φ₁ φ₂, I think you should define Proposition.valid φ to mean that φ is true over all models ls. This is more general, because Proposition.equiv φ₁ φ₂ is simply Proposition.valid (φ₁.iff φ₂). (You didn't define Proposition.iff, but there is no reason why you shouldn't.). Also, Proposition.equiv φ₁ φ₂ biases you toward equational reasoning. But sometimes it is more natural to reason about implications.

[eric-wieser]

Please fix the indents here and throughout

[eric-wieser]

Suggested change

	@[scoped grind .]
	theorem next_self_dual {T} : ∀ (φ : Proposition T), φ.next.not ≈ φ.not.next := by
	simp
	@[scoped grind .]
	theorem next_self_dual {T} : ∀ (φ : Proposition T), φ.next.not ≈ φ.not.next := by
	simp

[eric-wieser]

Suggested change

	def Proposition.valid (φ₁ : Proposition T) : Prop :=
	def Proposition.Valid (φ₁ : Proposition T) : Prop :=

or perhaps

Suggested change

	def Proposition.valid (φ₁ : Proposition T) : Prop :=
	def Proposition.IsValid (φ₁ : Proposition T) : Prop :=

[ctchou]

Instead of trying to anticipate and enumerate all propositional operators you will ever need, I wonder if it is better to limit yourself to a minimal set of operators in terms of which other operators can be defined. For example, even with the expanded set of operators given above, you still miss one important operator:

def Proposition.leadsTo (φ₁ φ₂ : Proposition T) : Proposition T :=
  (φ₁.implies φ₂.eventually).always

variable (φ₁ φ₂ : Proposition T)
#check (φ₁.leadsTo φ₂)

As you can see, the dot-notation enables the new operator to be written and used pretty much like those in the original inductive definition. By limiting yourself to a minimal set of core operators which will likely stay stable, you will have fewer operators to deal with if you ever want to develop any proof theory for LTL.

[mell-o-tron]

Makes a lot of sense. On it 👍

[ctchou]

Are you sure until doesn't work here? I played with it a little bit and it seems to work. These operators are never used "nakedly" and always appears as part of dot-notations.

[ctchou]

One more comment: I wonder if it is possible to change the type of a model from ωSequence (Set T) to ωSequence State, where State : Type* is a "state space". This of course requires a corresponding change in the notion of an "atomic proposition", which will need to take an object p of type State -> Prop or Set State and assert either p (ls 0) or ls 0 \in p. This way a user of the LTL does not need to define a different type T for each specific application, which can be rather tedious. (Of course, he still need to define a specific State, but that's unavoidable.)