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