feat: logical equivalence for modal logic

[fmontesi]

Adds logical equivalence for modal logic, proving that it is a Congruence (for any modal logic, regardless of the class of models considered) and a LogicalEquivalence (for logic K, i.e., when considering the class of all models).

The PR also renames Proposition.neg to Proposition.not and adds a useful lemma on Proposition.iff.

Depends on #528.

[thomaskwaring]

some minor comments but lgtm on the whole!

[fmontesi]

Thanks, @thomaskwaring. All done!

[chenson2018]

Out of scope for this PR, but derivation_def is written backwards.

[chenson2018]

Suggested change

	instance (S : Set (Model World Atom)) :
	IsEquiv (Proposition Atom) (Proposition.Equiv (Atom := Atom) S) where
	refl := by grind
	symm := by
	intro φ₁ φ₂ h m hₘ w
	specialize h m hₘ w
	grind
	trans := by
	intro φ₁ φ₂ φ₃ h₁ h₂ m hₘ w
	specialize h₁ m hₘ w
	specialize h₂ m hₘ w
	grind
	instance {World Atom} (S : Set (Model World Atom)) : IsEquiv (Proposition Atom) (Proposition.Equiv S) := by
	rw [← equivalence_iff_isEquiv]
	grind [Equivalence]

[chenson2018]

Suggested change

	apply Iff.intro <;> intro h'
	· simp_all only [valid]
	intro m hin w
	specialize h m hin w
	grind
	· simp_all only [valid]
	intro m hin w
	specialize h m hin w
	grind
	grind

[chenson2018]

Suggested change

	instance (S : Set (Model World Atom)) :
	Congruence (Proposition Atom) (Proposition.Equiv (Atom := Atom) S) where
	instance {World Atom} (S : Set (Model World Atom)) : Congruence (Proposition Atom) (Proposition.Equiv S) where

[chenson2018]

The fill notation is fighting against grind here. See how this works:

Suggested change

	elim :
	Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill)
	(Proposition.Equiv S) := by
	intro ctx φ₁ φ₂ heqv m hₘ w
	specialize heqv m hₘ
	induction ctx generalizing w
	case hole => grind
	case not c ih | andL c ih | andR c ih =>
	specialize ih w
	grind
	case diamond c ih =>
	simp only [Satisfies.iff_iff_iff]
	apply Iff.intro
	all_goals
	intro h
	rcases h with ⟨w', h⟩
	specialize ih w'
	grind
	elim ctx φ₁ φ₂ heqv m hₘ w := by
	have (Γ : HasContext.Context (Proposition Atom)) (φ) : Γ.fill φ = Γ<[φ] := rfl
	induction ctx generalizing w
	case hole => grind
	case not c ih | andL c ih | andR c ih =>
	specialize ih w
	grind
	case diamond c ih =>
	rw [Satisfies.iff_iff_iff]
	apply Iff.intro
	all_goals
	rintro ⟨w', h⟩
	specialize ih w'
	grind

(The first have should be a grind lemma somewhere.)

[chenson2018]

We don't usually provide types like this in an instance, right? There's also another notation lemma that needs to be extracted. See how:

Suggested change

	eqvFillValid {φ₁ φ₂ : Proposition Atom} (heqv : φ₁ ≡[Set.univ] φ₂)
	(c : HasHContext.Context (Judgement World Atom) (Proposition Atom))
	(h : ⇓c<[φ₁]) : ⇓c<[φ₂] := by
	simp only [HasHContext.fill, Satisfies.Context.fill] at ⊢ h
	specialize heqv c.m
	grind
	eqvFillValid heqv c h := by
	have (φ : Proposition Atom) : Modal[c.m,c.w ⊨ φ] = c<[φ] := rfl
	specialize heqv c.m
	grind

works