Set operation with equality casting

Stream: general

[SnO2WMaN]

I'm formalizing modal logic with neighborhood semantics and i have to deal Set operation with equality casting. Main point is that below code need to be proved. are they correct? Intuitively they might be right, but i dont how to prove.

import Mathlib.Data.Set.Image

variable {α β} (eq : α = β)
         {a b : Set α}
         {x y : Set β}

example : (∅ : Set α) = eq ▸ (∅ : Set β) := by sorry;

example : (eq ▸ a) ∪ (eq ▸ b) = eq ▸ (a ∪ b) := by sorry;

example : (eq ▸ a)ᶜ = (eq ▸ (aᶜ)) := by sorry;

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0ARFJHAZQFMYcBJEJAc1ICgGA3JKYJLdUuAb0EbgOICbgAL5wAFKQCOcAFxxBAXmEBKBnA2bNvJHCxy4ZePxHqtW3gA84ATwNHhphqUtJw3A+MCgRPfIKVcMrScIAdpBI+8g5CAbLKWHYAztBQNgDcTC5uYB7ykjJhSAGAVEQSwWFYAUH5ErolFXJxiclpGa7uPLllcIWAObiBpdXiSD0qMY1wSVApqUA

[Aaron Liu]

You shouldn't have eq : α = β because it's really easy to stumble into a goal that's both "obviously" true and not possible to prove (and not possible to disprove either)

[Aaron Liu]

but yes in this case they are true

[Aaron Liu]

you can solve them by cases eq; rfl

[Aaron Liu]

what led you to have these problems in the first place?

[SnO2WMaN]

To tell why i have, i have to explain some modal logic / neighborhood semantics following textbook, but it's longer.
So extract main point. I've define structure Frame, and Frame.IsCanonical as below. to prove truthlemma, we need to prove eq_empty, eq_union, eq_comp and iff_mem.

structure Frame where
  World : Type
  [world_nonempty : Nonempty World]
  N : World → Set (Set World)

abbrev MaximalConsistentSet (𝓢 : S) : Type := { T : FormulaSet ℕ // (Consistent 𝓢 T) ∧ (∀ {U}, T ⊂ U → Inconsistent 𝓢 U)}

class Frame.IsCanonical (F : Frame) (𝓢 : S) : Prop where
  eq_world : F.World = MaximalConsistentSet 𝓢
  box_proofset : ∀ φ, F.box (eq_world ▸ (proofset 𝓢 φ)) = eq_world ▸ (proofset 𝓢 (□φ))

@[simp]
lemma eq_empty : (canonical.eq_world ▸ (∅ : Set (MaximalConsistentSet 𝓢))) = ∅ := by
  cases canonical.eq_world;
  --
  -- rfl;

@[simp]
lemma eq_union {X Y : Set (MaximalConsistentSet 𝓢)} : (canonical.eq_world ▸ (X ∪ Y)) = ((canonical.eq_world ▸ X) ∪ (canonical.eq_world ▸ Y)) := by
  sorry;

@[simp]
lemma eq_comp {X : Set (MaximalConsistentSet 𝓢)} : (canonical.eq_world ▸ Xᶜ) = (canonical.eq_world ▸ X)ᶜ := by
  sorry;

@[simp]
lemma iff_mem {Γ : MaximalConsistentSet 𝓢} {X : Set _} : Γ ∈ X ↔ (canonical.eq_world ▸ Γ) ∈ (canonical.eq_world ▸ X) := by
  sorry;

lemma truthlemma : canonical.eq_world ▸ (proofset 𝓢 φ) = ((canonicalModel F 𝓢).truthset φ) := by
  induction φ with
  | hatom => simp [canonicalModel]
  | hfalsum => simp [canonicalModel];
  | himp φ ψ ihφ ihψ => simp_all [MaximalConsistentSet.proofset.eq_imp, ←ihφ, ←ihψ];
  | hbox φ ihφ =>
    rw [Model.truthset.eq_box, ←ihφ, ←(canonical.box_proofset φ)];
    rfl;

[SnO2WMaN]

I can prove them by ↓．thanks to hint.

haveI := canonical.eq_world;
grind;

[Aaron Liu]

Why are you bundling World in your Frame?

[Aaron Liu]

can you make it like structure Frame (World : Type) where, like how groups are class Group (G : Type u) extends DivInvMonoid G where?

[SnO2WMaN]

we define class (set) of frame def FrameClass := Set (Frame) and operating with semantics. binding world is too much complex

[Aaron Liu]

put the world as a parameter to your frames

[Aaron Liu]

Mashu Noguchi said:

we define class (set) of frame def FrameClass := Set (Frame) and operating with semantics. binding world is too much complex

why do you want this?

[SnO2WMaN]

This definition suits our (FormalizedFormalLogic) meta-logical semantics tools. Refer our codes (it's the case of Kripke semantics, not neighborhood one, but almost same)

https://github.com/FormalizedFormalLogic/Foundation/blob/8c5fc737bed001eef5eab12c68cc6477db53db9c/Foundation/Modal/Kripke/Basic.lean#L532-L558

[SnO2WMaN]

Yes structure Frame (World : Type) where I considered once. but this def was harder to liftup for frameclass and don't have good idea, when i tried (half years ago).

[Aaron Liu]

this still feels like a bad idea

[Aaron Liu]

What is the usage of Frame.IsCanonical?

[Aaron Liu]

Why don't you just state your lemmas for canonicalFrame instead of having a typeclass?

[Aaron Liu]

I can't tell what you need here

[SnO2WMaN]

plz wait a moment, I'll push current codes to our repo as PR. I'll refer the codes to explain.

[Aaron Liu]

but bundling the type and using type equality just seems like a bad idea overall

[SnO2WMaN]

Logical background:

We use Frame.IsCanonical for prove completeness for usual proof. more precisely, if some frame that is canonical is exists in class of frame C, then logic is complete for C. (In normal modal logic with Kripke semantics, canonical frame is defined and exact one, but in neighborhood, defined "frame is canonical" and don't know if there's)

https://github.com/FormalizedFormalLogic/Foundation/blob/a5c8cb72b74855a7669e069b8f55748a73d14b4b/Foundation/Modal/Neighborhood/Completeness.lean#L147

So to prove completeness, we have to find canonical frame. the minimal canonical frame (minimalCanonicalFrame) is defined and it can proved in canonicality. and all FrameClass (i.e. Set.univ) trivially contains it, so weakest modal logic E is complete.

https://github.com/FormalizedFormalLogic/Foundation/blob/a5c8cb72b74855a7669e069b8f55748a73d14b4b/Foundation/Modal/Neighborhood/Completeness.lean#L170-L172

but this is weak for (i.e. is not canonical for) more extended logics (e.g. EM,EC, ET, etc.). we need to supplementation of frame (it defined for all frame). it conserve the property reflexivity, transitivity.

https://github.com/FormalizedFormalLogic/Foundation/blob/a5c8cb72b74855a7669e069b8f55748a73d14b4b/Foundation/Modal/Neighborhood/Supplementation.lean#L10

https://github.com/FormalizedFormalLogic/Foundation/blob/a5c8cb72b74855a7669e069b8f55748a73d14b4b/Foundation/Modal/Neighborhood/Supplementation.lean#L63-L89

And the "supplement of canonical frame" is canonical in these extended logics >= EM.

[Aaron Liu]

interesting

[Aaron Liu]

and what was the problem using structure Frame (World : Type) where?

[SnO2WMaN]

In this case we might have define frame class as Set (W : Type) × (Frame W), it cumbersome for our framework.

[Aaron Liu]

what do you want frame classes for again?

[Aaron Liu]

Set ((W : Type) × (Frame W)) will probably run into the same type equality issues

[SnO2WMaN]

in (purely) modal logic perspective, in following textbook or manner in set-based argument, frame class is for capturing "frame is reflexive", "frame has only finite points", "frame is tree-like form" etc.
However I can't say what means frame class in perspective implementing logic in type theory / theorem prover / lean4. I implement the fact of modal logics followed straightforward the textbook and nothing change with big treatement. is it satisfy your question?

[Aaron Liu]

then this might be reasonable

[SnO2WMaN]

anyway i close this,. thanks

[Edward van de Meent]

Won't this be solved if you only claim that F.World is equivalent to MaximalConsistentSet? Then most of these casting lemmas are just normal set theory lemmas, I think...

[Edward van de Meent]

That way you also stand a chance of disproving that a frame is canonical

[Edward van de Meent]

Or that a frame is canonical in a nontrivial way

[SnO2WMaN]

Edward van de Meent said:

Won't this be solved if you only claim that F.World is equivalent to MaximalConsistentSet? Then most of these casting lemmas are just normal set theory lemmas, I think...

You mean equivalent to F.World ≊ MaximalConsistentSet 𝓢? might be well, but it's cumbersome. I don't think F.World = MaximalConsistentSet 𝓢 is not so problematic. I don't need to prove the "frame is not canonical", it's not necessary. Sorry if i misunderstand your saying.

[Aaron Liu]

no I think that's problematic, since it makes things more difficult

[Edward van de Meent]

i was personally thinking F.World ≃ MaximalConsistentSet 𝓢

[Aaron Liu]

That would be data

[Edward van de Meent]

ah, right.. then i guess something like ∃ e : F.World ≃ MaximalConsistentSet 𝓢, ∀ φ, F.box (e '' (proofset 𝓢 φ)) = e '' (proofset 𝓢 (□φ)) is the right thing?

[SnO2WMaN]

i don't know how equality version = causes crucial problem so can't judge your concern. for proving eq_world in miniCanonicalFrame use simply rfl and box_proofset is usual way. would you show me your simple example how break?

[Edward van de Meent]

my concern is that at some point you might have to state something like "this frame is equivalent to a canonical one" rather than "this frame is a canonical one", because you can't prove stuff like {x:A // x = x} = A or {x:A // P x} ⊕ {x:A//¬P x} = A in lean, whereas you can show that they're equivalent by giving an explicit bijection.

[SnO2WMaN]

all right i understand your concern but currently equality is going well. canonicity is only needed to prove completeness and no longer needed when proved. if i have some problem, i'll change them. (for main point, it is good if truthlemma and 1 lemma is holded whatever defined canonicity)