feat(ModalLogic+Congruence): modal reasoning for Lean

[fmontesi]

This PR develops a concept of modal reasoning for Lean theorems, powered by the laws of modal logic. This development led to some polishing for Congruence and some definitions for Relation.

Specifically, the PR:

• Introduces the first development where CSLib's modal logic is instantiated with Lean's Prop as the type of atomic propositions. We use this to construct models out of Lean predicates and containers and show some general properties in terms of logical equivalence.
• Introduces a construction that, given any scalar multiplication operator, builds an accessibility relation. If the operator is an action of some kind (as defined in mathlib), this accessibility relation has interesting properties (like transitivity or diamond) that are relevant for modal reasoning.
• Develops an example of how this framework can be used to prove mathematical theorems. In particular, we apply the new construction to obtain an accessibility relation on Ideals. In this interpretation, membership of radicals of ideals is characterised by the diamond connective in modal logic. This allows for applying modal logic to proving properties about radicals.
• As examples, we show that Ideal.radical_inf and Ideal.radical_idem from mathlib can be proven by applying modal logical equivalence.

This put the ergonomics and expressive power of our infrastructure for modal logic, logical equivalence, relations, and congruence to the test. This PR also:

• Polishes a bit the ergonomics of LawfulCongruence (e.g., by making Congruence.r an abbrev so that typeclass resolution works in proofs).
• Adds a Preserves property for relations.
• Defines and proves soundness and completeness of modal axioms for relations with the diamond property.
• Refactors a bit LogicalEquivalence for modal logic so that it is more fundamental (based on a single model instead of a set of models, and then derives the latter on the first).

The last point not only helps with proofs, but also aligns logical equivalence with how it is handled in HML. This means that we can start working on a shared abstraction for this kind of logics, which would then derive the natural notion of logical equivalence for free.

Depends on #788

[thomaskwaring]

preliminary review here, but overall i like this

one question (which i was thinking about as relates to the earlier axiom L PR) is whether we can state IsAxiom as an inference system, where the judgement is r ⊨ φ for "this the proposition is valid at every world for every valuation" — logically it is the same but it avoids introducing a new definition and might down-the-track mesh better with our infrastructure. what do you think?

[fmontesi]

preliminary review here, but overall i like this

one question (which i was thinking about as relates to the earlier axiom L PR) is whether we can state IsAxiom as an inference system, where the judgement is r ⊨ φ for "this the proposition is valid at every world for every valuation" — logically it is the same but it avoids introducing a new definition and might down-the-track mesh better with our infrastructure. what do you think?

Like this?

/-- Every accessibility relation induces an inference system tag for proving valid axioms under
the relation. -/
inductive Axiom (r : World → World → Prop)

/-- A proposition `φ` is an axiom under the relation `r` (the 'frame') if it holds for all
valuations and worlds. -/
instance (r : World → World → Prop) : InferenceSystem (Axiom r) (Proposition Atom) where
  derivation φ := ∀ v w, ⇓Modal[⟨r,v⟩,w ⊨ φ]

I think it's a good idea, might even go in the class for modal-like logics later on. I've tried it and the proofs don't work out of the box though, there's some plumbing that becomes necessary compared to the current abbrev, so it'll take some (unclear amount of) work.

EDIT: I've figured it out. :) Now in the PR, let me know what you think.

[thomaskwaring]

i like the new Axiom design i think! this review is mostly some further golfing / simplifying of proofs, plus a few natural extensions to Modal.Lean.SMul

[thomaskwaring]

for completeness, the following two properties (which are referenced in Modal.Basic) also have natural analogues in this setting.

Suggested change

	/-- The relation induced by a group action is symmetric. -/
	instance [Group G] [MulAction G α] : Std.Symm (ofSMul G α) where
	symm := by
	rintro x _ ⟨g, rfl⟩
	use g⁻¹
	simp
	/-- The relation induced by an action of a nonempty type is serial. -/
	instance [SMul M α] [Nonempty M] : Serial (ofSMul M α) where
	serial x := ⟨Classical.arbitrary M • x, Classical.arbitrary M, rfl⟩

[thomaskwaring]

It seems reasonable to me to use the existing typeclass for "commuting actions" — weird that the relevant instance doesn't exist in mathlib.

Suggested change

	/-- The relation induced by a semigroup action of a commutative semigroup has the diamond property.
	-/
	@[scoped grind .]
	theorem ofSMul_diamond [CommSemigroup M] [SemigroupAction M α] : Diamond (ofSMul M α) := by
	intro x y z hxy hxz
	rcases hxy with ⟨m, rfl⟩
	rcases hxz with ⟨n, rfl⟩
	refine ⟨n • (m • x), ?_, ?_⟩
	· use n
	· use m
	grind only [=_ mul_smul]
	/-- TODO: upstream this generalisation of Mathlib's `smulCommClass_self`, which applies only to
	monoids `M`. -/
	instance {M α} [CommSemigroup M] [SemigroupAction M α] : SMulCommClass M M α where
	smul_comm m n a := by rw [←mul_smul, mul_comm, mul_smul]
	/-- The relation induced by an action commuting with itself has the diamond property. -/
	@[scoped grind .]
	theorem ofSMul_diamond [SMul M α] [SMulCommClass M M α] : Diamond (ofSMul M α) := by
	rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
	use! n • m • x, n, m, smul_comm ..

[thomaskwaring]

Suggested change

	apply Iff.intro
	constructor

[thomaskwaring]

Suggested change

	trans x y z hxy hyz := by
	rcases hxy with ⟨m, rfl⟩
	rcases hyz with ⟨n, rfl⟩
	trans := by
	rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩

[thomaskwaring]

This doesn't use the associativity of M, but (strangely? maybe for good reason?) SemigroupAction / MulAction require more than Mul M, so best to leave it as-is I suppose.

[thomaskwaring]

Suggested change

	rw [Submodule.coe_inf]
	simp only [Ideal.radical_eq_modal_denotation]
	rw [Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)]
	simp_rw [Submodule.coe_inf, Ideal.radical_eq_modal_denotation,
	Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)]

[thomaskwaring]

Suggested change

	(Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := by
	apply Iff.intro <;> intro h
	case mp =>
	intro v w
	exact h v w
	case mpr =>
	intro v w
	exact h v w
	(Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := Iff.rfl

[thomaskwaring]

Suggested change

	intro h
	rw [Satisfies.and_iff_and] at h
	rcases h with ⟨hφ₁, hφ₂⟩
	rw [Satisfies.diamond_iff_exists] at hφ₁ hφ₂ ⊢
	rcases hφ₁ with ⟨b, hab, hb⟩
	rcases hφ₂ with ⟨c, hac, hc⟩
	rw [Satisfies.and_iff_and, Satisfies.diamond_iff_exists]
	rintro ⟨⟨b, hab, hb⟩, ⟨c, hac, hc⟩⟩

[thomaskwaring]

perhaps this pattern (which occurs elsewhere) could be extracted into a lemma, which would be the converse of Proposition.equiv_iff

[thomaskwaring]

Suggested change

	intro h m hm w
	subst hm
	rintro h m rfl w