internlm/Lean-Github huggingface dataset:
Theorem: LO.System.multiboxconj'_of_conj'multibox!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
⊢ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
Tactic:
intro p hp
Proof state after:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
p : F
hp : p ∈ Γ
⊢ 𝓢 ⊢! □^[n]p
Theorem: LO.System.multiboxconj'_of_conj'multibox!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
p : F
hp : p ∈ Γ
⊢ 𝓢 ⊢! □^[n]p
Tactic:
exact iff_provable_list_conj.mp d (□^[n]p) (by aesop)
Proof state after:
no goals
Theorem: LO.System.multiboxconj'_of_conj'multibox!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
p : F
hp : p ∈ Γ
⊢ □^[n]p ∈ □'^[n]Γ
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.System.multibox_cons_conj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ (□'^[n]Γ).conj'
Tactic:
apply conj'conj'_subset
Proof state after:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ ∀ p_1 ∈ □'^[n]Γ, p_1 ∈ □'^[n](p :: Γ)
Theorem: LO.System.multibox_cons_conj'!
Proof state before:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ ∀ p_1 ∈ □'^[n]Γ, p_1 ∈ □'^[n](p :: Γ)
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simpa using dhyp! multiboxverum!;
| hsingle => simp;
| hcons p Γ h ih =>
  simp_all;
  exact imp_trans! (implyRightAnd! (generalConj'! (by simp)) (imp_trans! (by simp) ih)) collect_multibox_and!;
Proof state after:
no goals
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
case hnil
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! (□'^[n][]).conj' ⟶ □^[n][].conj'
Tactic:
simpa using dhyp! multiboxverum!
Proof state after:
no goals
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
case hsingle
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
a✝ : F
⊢ 𝓢 ⊢! (□'^[n][a✝]).conj' ⟶ □^[n][a✝].conj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
case hcons
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ □^[n](p :: Γ).conj'
Tactic:
simp_all
Proof state after:
case hcons
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ □^[n](p ⋏ Γ.conj')
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
case hcons
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ □^[n](p ⋏ Γ.conj')
Tactic:
exact imp_trans! (implyRightAnd! (generalConj'! (by simp)) (imp_trans! (by simp) ih)) collect_multibox_and!
Proof state after:
no goals
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ □^[n]p ∈ □'^[n](p :: Γ)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.collect_multibox_conj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ (□'^[n]Γ).conj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.distribute_multidia_and!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ◇^[n](p ⋏ q) ⟶ ◇^[n]p ⋏ ◇^[n]q
Tactic:
suffices h : 𝓢 ⊢! ~(□^[n](~(p ⋏ q))) ⟶ ~(□^[n](~p)) ⋏ ~(□^[n](~q)) by
  exact imp_trans! (imp_trans! (conj₁'! multidiaDuality!) h) $ andReplace! (conj₂'! multidiaDuality!) (conj₂'! multidiaDuality!);
Proof state after:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~(p ⋏ q))) ⟶ ~(□^[n](~p)) ⋏ ~(□^[n](~q))
Theorem: LO.System.distribute_multidia_and!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~(p ⋏ q))) ⟶ ~(□^[n](~p)) ⋏ ~(□^[n](~q))
Tactic:
apply FiniteContext.deduct'!
Proof state after:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ [~(□^[n](~(p ⋏ q)))] ⊢[𝓢]! ~(□^[n](~p)) ⋏ ~(□^[n](~q))
Theorem: LO.System.distribute_multidia_and!
Proof state before:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ [~(□^[n](~(p ⋏ q)))] ⊢[𝓢]! ~(□^[n](~p)) ⋏ ~(□^[n](~q))
Tactic:
apply demorgan₃'!
Proof state after:
case h.b
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ { ctx := [~(□^[n](~(p ⋏ q)))] } ⊢! ~(□^[n](~p) ⋎ □^[n](~q))
Theorem: LO.System.distribute_multidia_and!
Proof state before:
case h.b
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ { ctx := [~(□^[n](~(p ⋏ q)))] } ⊢! ~(□^[n](~p) ⋎ □^[n](~q))
Tactic:
apply FiniteContext.deductInv'!
Proof state after:
case h.b.h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~(p ⋏ q))) ⟶ ~(□^[n](~p) ⋎ □^[n](~q))
Theorem: LO.System.distribute_multidia_and!
Proof state before:
case h.b.h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~(p ⋏ q))) ⟶ ~(□^[n](~p) ⋎ □^[n](~q))
Tactic:
apply contra₀'!
Proof state after:
case h.b.h.b
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! □^[n](~p) ⋎ □^[n](~q) ⟶ □^[n](~(p ⋏ q))
Theorem: LO.System.distribute_multidia_and!
Proof state before:
case h.b.h.b
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! □^[n](~p) ⋎ □^[n](~q) ⟶ □^[n](~(p ⋏ q))
Tactic:
apply imp_trans! collect_multibox_or! (imply_multibox_distribute'! demorgan₁!)
Proof state after:
no goals
Theorem: LO.System.distribute_multidia_and!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
h : 𝓢 ⊢! ~(□^[n](~(p ⋏ q))) ⟶ ~(□^[n](~p)) ⋏ ~(□^[n](~q))
⊢ 𝓢 ⊢! ◇^[n](p ⋏ q) ⟶ ◇^[n]p ⋏ ◇^[n]q
Tactic:
exact imp_trans! (imp_trans! (conj₁'! multidiaDuality!) h) $ andReplace! (conj₂'! multidiaDuality!) (conj₂'! multidiaDuality!)
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simpa using dhyp! verum!;
| hsingle p => simp;
| hcons p Γ h ih =>
  simp_all;
  exact imp_trans! distribute_multidia_and! $ by
    apply deduct'!;
    apply iff_provable_list_conj.mpr;
    intro q hq;
    simp at hq;
    cases hq with
    | inl => subst_vars; exact conj₁'! id!;
    | inr hq =>
      obtain ⟨r, hr₁, hr₂⟩ := hq;
      exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop);
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case hnil
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
⊢ 𝓢 ⊢! ◇^[n][].conj' ⟶ (◇'^[n][]).conj'
Tactic:
simpa using dhyp! verum!
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case hsingle
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
⊢ 𝓢 ⊢! ◇^[n][p].conj' ⟶ (◇'^[n][p]).conj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case hcons
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ 𝓢 ⊢! ◇^[n](p :: Γ).conj' ⟶ (◇'^[n](p :: Γ)).conj'
Tactic:
simp_all
Proof state after:
case hcons
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ 𝓢 ⊢! ◇^[n](p ⋏ Γ.conj') ⟶ (◇'^[n](p :: Γ)).conj'
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case hcons
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ 𝓢 ⊢! ◇^[n](p ⋏ Γ.conj') ⟶ (◇'^[n](p :: Γ)).conj'
Tactic:
exact imp_trans! distribute_multidia_and! $ by
  apply deduct'!;
  apply iff_provable_list_conj.mpr;
  intro q hq;
  simp at hq;
  cases hq with
  | inl => subst_vars; exact conj₁'! id!;
  | inr hq =>
    obtain ⟨r, hr₁, hr₂⟩ := hq;
    exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop);
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ 𝓢 ⊢! ◇^[n]p ⋏ ◇^[n]Γ.conj' ⟶ (◇'^[n](p :: Γ)).conj'
Tactic:
apply deduct'!
Proof state after:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ [◇^[n]p ⋏ ◇^[n]Γ.conj'] ⊢[𝓢]! (◇'^[n](p :: Γ)).conj'
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ [◇^[n]p ⋏ ◇^[n]Γ.conj'] ⊢[𝓢]! (◇'^[n](p :: Γ)).conj'
Tactic:
apply iff_provable_list_conj.mpr
Proof state after:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ ∀ p_1 ∈ ◇'^[n](p :: Γ), { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! p_1
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ ∀ p_1 ∈ ◇'^[n](p :: Γ), { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! p_1
Tactic:
intro q hq
Proof state after:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
hq : q ∈ ◇'^[n](p :: Γ)
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
hq : q ∈ ◇'^[n](p :: Γ)
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
simp at hq
Proof state after:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
hq : q = (UnaryModalOperator.mop false)^[n] p ∨ ∃ a ∈ Γ, (UnaryModalOperator.mop false)^[n] a = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
hq : q = (UnaryModalOperator.mop false)^[n] p ∨ ∃ a ∈ Γ, (UnaryModalOperator.mop false)^[n] a = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
cases hq with
| inl => subst_vars; exact conj₁'! id!;
| inr hq =>
  obtain ⟨r, hr₁, hr₂⟩ := hq;
  exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop);
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h.inl
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
h✝ : q = (UnaryModalOperator.mop false)^[n] p
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
subst_vars
Proof state after:
case h.inl
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! (UnaryModalOperator.mop false)^[n] p
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h.inl
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! (UnaryModalOperator.mop false)^[n] p
Tactic:
exact conj₁'! id!
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h.inr
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q : F
hq : ∃ a ∈ Γ, (UnaryModalOperator.mop false)^[n] a = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
obtain ⟨r, hr₁, hr₂⟩ := hq
Proof state after:
case h.inr.intro.intro
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r✝ : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q r : F
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop false)^[n] r = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
case h.inr.intro.intro
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r✝ : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q r : F
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop false)^[n] r = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop)
Proof state after:
no goals
Theorem: LO.System.iff_conj'multidia_multidiaconj'!
Proof state before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q✝ r✝ : F
Γ✝ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q r : F
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop false)^[n] r = q
⊢ q ∈ ◇'^[n]Γ
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.System.LoebRule.loeb!
Proof state before:
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
⊢ 𝓢 ⊢! □p ⟶ p → 𝓢 ⊢! p
Tactic:
rintro ⟨hp⟩
Proof state after:
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
hp : 𝓢 ⊢ □p ⟶ p
⊢ 𝓢 ⊢! p
Theorem: LO.System.LoebRule.loeb!
Proof state before:
case intro
F : Type u_1
inst✝⁸ : StandardModalLogicalConnective F
inst✝⁷ : DecidableEq F
S : Type u_2
inst✝⁶ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁵ : Classical 𝓢
inst✝⁴ : System.NegationEquiv 𝓢
inst✝³ : Necessitation 𝓢
inst✝² inst✝¹ : HasAxiomK 𝓢
inst✝ : LoebRule 𝓢
hp : 𝓢 ⊢ □p ⟶ p
⊢ 𝓢 ⊢! p
Tactic:
exact ⟨loeb hp⟩
Proof state after:
no goals