refactor(Modal/Hilbert): macro definition

Foundation/Modal/Entailment/EM.lean

@@ -24,7 +24,8 @@ instance [Entailment.EM 𝓢] : Entailment.RM 𝓢 := ⟨by
 ⟩
 
 instance [Entailment.E 𝓢] [Entailment.RM 𝓢] : Entailment.EM 𝓢 where
-  M φ ψ := by
+  M := by
+    intro φ ψ;
     apply CK_of_C_of_C;
     . apply rm; exact and₁;
     . apply rm; exact and₂;

Foundation/Modal/Entailment/EMC.lean

@@ -12,7 +12,7 @@ variable {S F : Type*} [BasicModalLogicalConnective F] [DecidableEq F] [Entailme
 variable {𝓢 : S}
 
 instance [Entailment.EMC 𝓢] : Entailment.HasAxiomK 𝓢 where
-  K φ ψ := by
+  K {φ ψ} := by
     haveI h₁ : 𝓢 ⊢! (□(φ ➝ ψ) ⋏ □φ) ➝ □((φ ➝ ψ) ⋏ φ) := axiomC;
     haveI h₂ : 𝓢 ⊢! ((φ ➝ ψ) ⋏ φ) ➝ ψ := C_trans CKK innerMDP
     haveI h₃ : 𝓢 ⊢! □((φ ➝ ψ) ⋏ φ) ➝ □ψ := rm h₂;

Foundation/Modal/Entailment/ET.lean

@@ -20,7 +20,7 @@ lemma diabot : 𝓢 ⊢ ◇⊤ := ⟨diabot!⟩
 
 namespace ET
 
-instance : Entailment.HasAxiomD 𝓢 := ⟨fun _ ↦ C_trans axiomT diaTc⟩
+instance : Entailment.HasAxiomD 𝓢 := ⟨C_trans axiomT diaTc⟩
 
 instance : Entailment.ED 𝓢 where
 

Foundation/Modal/Entailment/ET5.lean

@@ -22,15 +22,15 @@ variable [DecidableEq F]
 
 namespace ET5
 
-instance : Entailment.HasAxiomB 𝓢 := ⟨fun _ ↦ C_trans diaTc axiomFive⟩
+instance : Entailment.HasAxiomB 𝓢 := ⟨C_trans diaTc axiomFive⟩
 
 instance : Entailment.ETB 𝓢 where
 
 instance : Entailment.EN 𝓢 where
 
-instance : Entailment.HasAxiomPoint2 𝓢 := ⟨fun _ ↦ C_trans (C_trans axiomFiveDual! axiomT) axiomB⟩
+instance : Entailment.HasAxiomPoint2 𝓢 := ⟨C_trans (C_trans axiomFiveDual! axiomT) axiomB⟩
 
-instance : Entailment.HasAxiomFour 𝓢 := ⟨fun _ ↦ C_trans (C_trans axiomTDual! axiomFive) (K_left $ re $ K_intro axiomFiveDual! axiomTDual!)⟩
+instance : Entailment.HasAxiomFour 𝓢 := ⟨C_trans (C_trans axiomTDual! axiomFive) (K_left $ re $ K_intro axiomFiveDual! axiomTDual!)⟩
 end ET5
 
 

Foundation/Modal/Entailment/GL.lean

@@ -31,7 +31,7 @@ namespace GL
 
 variable {φ ψ : F}
 
-instance : HasAxiomZ 𝓢 := ⟨fun _ ↦ C_trans axiomL implyK⟩
+instance : HasAxiomZ 𝓢 := ⟨C_trans axiomL implyK⟩
 
 protected def axiomFour : 𝓢 ⊢! Axioms.Four φ := by
   dsimp [Axioms.Four];
@@ -41,14 +41,14 @@ protected def axiomFour : 𝓢 ⊢! Axioms.Four φ := by
     exact K_intro (FiniteContext.byAxm) (K_left (ψ := □□φ) $ FiniteContext.byAxm);
   have : 𝓢 ⊢! φ ➝ (□⊡φ ➝ ⊡φ) := C_trans this (CCC_of_C_left BoxBoxdot_BoxDotbox);
   exact C_trans (C_trans (implyBoxDistribute' this) axiomL) (implyBoxDistribute' $ and₂);
-instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ GL.axiomFour⟩
+instance : HasAxiomFour 𝓢 := ⟨GL.axiomFour⟩
 instance : Entailment.K4 𝓢 where
 
 protected def axiomHen : 𝓢 ⊢! Axioms.Hen φ := C_trans (implyBoxDistribute' and₁) axiomL
-instance : HasAxiomHen 𝓢 := ⟨fun _ ↦ GL.axiomHen⟩
+instance : HasAxiomHen 𝓢 := ⟨GL.axiomHen⟩
 
 protected def axiomZ : 𝓢 ⊢! Axioms.Z φ := C_trans axiomL implyK
-instance : HasAxiomZ 𝓢 := ⟨fun _ ↦ GL.axiomZ⟩
+instance : HasAxiomZ 𝓢 := ⟨GL.axiomZ⟩
 
 end GL
 

Foundation/Modal/Entailment/Grz.lean

@@ -16,14 +16,14 @@ namespace Grz
 noncomputable def lemma_axiomFour_axiomT : 𝓢 ⊢! □φ ➝ (φ ⋏ (□φ ➝ □□φ)) := C_trans (lemma_Grz₁ (φ := φ)) axiomGrz
 
 protected noncomputable def axiomFour : 𝓢 ⊢! □φ ➝ □□φ := C_of_CC $ C_trans lemma_axiomFour_axiomT and₂
-noncomputable instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ Grz.axiomFour⟩
+noncomputable instance : HasAxiomFour 𝓢 := ⟨Grz.axiomFour⟩
 
 protected noncomputable def axiomT : 𝓢 ⊢! □φ ➝ φ := C_trans lemma_axiomFour_axiomT and₁
-noncomputable instance : HasAxiomT 𝓢 := ⟨fun _ ↦ Grz.axiomT⟩
+noncomputable instance : HasAxiomT 𝓢 := ⟨Grz.axiomT⟩
 
 noncomputable instance : Entailment.S4 𝓢 where
 
-instance : HasAxiomDum 𝓢 := ⟨fun _ ↦ C_trans axiomGrz implyK⟩
+instance : HasAxiomDum 𝓢 := ⟨C_trans axiomGrz implyK⟩
 
 end Grz
 

Foundation/Modal/Entailment/K.lean

@@ -107,7 +107,7 @@ def collect_boxItr_and : 𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ ➝ □^[n](φ ⋏ ψ
 def collect_box_and : 𝓢 ⊢! □φ ⋏ □ψ ➝ □(φ ⋏ ψ) := collect_boxItr_and (n := 1)
 @[simp] lemma collect_box_and! : 𝓢 ⊢ □φ ⋏ □ψ ➝ □(φ ⋏ ψ) := ⟨collect_box_and⟩
 
-instance : Entailment.HasAxiomC 𝓢 := ⟨λ _ _ => collect_box_and⟩
+instance : Entailment.HasAxiomC 𝓢 := ⟨collect_box_and⟩
 
 def collect_boxItr_and' (h : 𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ) : 𝓢 ⊢! □^[n](φ ⋏ ψ) := collect_boxItr_and ⨀ h
 lemma collect_boxItr_and'! (h : 𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ) : 𝓢 ⊢ □^[n](φ ⋏ ψ) := ⟨collect_boxItr_and' h.some⟩
@@ -213,7 +213,7 @@ lemma distribute_boxItr_and'! (d : 𝓢 ⊢ □^[n](φ ⋏ ψ)) : 𝓢 ⊢ □^[
 def distribute_box_and' (h : 𝓢 ⊢! □(φ ⋏ ψ)) : 𝓢 ⊢! □φ ⋏ □ψ := distribute_boxItr_and' (n := 1) h
 lemma distribute_box_and'! (d : 𝓢 ⊢ □(φ ⋏ ψ)) : 𝓢 ⊢ □φ ⋏ □ψ := ⟨distribute_box_and' d.some⟩
 
-instance : Entailment.HasAxiomM 𝓢 := ⟨λ _ _ => distribute_box_and⟩
+instance : Entailment.HasAxiomM 𝓢 := ⟨distribute_box_and⟩
 
 
 def boxdotAxiomK : 𝓢 ⊢! ⊡(φ ➝ ψ) ➝ (⊡φ ➝ ⊡ψ) := by

Foundation/Modal/Entailment/K4Loeb.lean

@@ -29,7 +29,7 @@ protected def axiomL : 𝓢 ⊢! Axioms.L φ := by
     nth_rw 2 [←e]; apply deduct'; apply deduct;
     exact d₂ ⨀ (d₁ ⨀ ((of d₃) ⨀ (FiniteContext.byAxm)));
   exact loeb this;
-instance : HasAxiomL 𝓢 := ⟨fun _ ↦ K4Loeb.axiomL⟩
+instance : HasAxiomL 𝓢 := ⟨K4Loeb.axiomL⟩
 
 end K4Loeb
 

Foundation/Modal/Entailment/KP.lean

@@ -20,7 +20,7 @@ protected def axiomD [HasDiaDuality 𝓢] : 𝓢 ⊢! Axioms.D φ := by
   have : 𝓢 ⊢! □φ ➝ (∼□⊥ ➝ ∼□(∼φ)) := C_trans this CCCNN;
   have : 𝓢 ⊢! □φ ➝ ∼□(∼φ) := C_swap this ⨀ axiomP;
   exact C_trans this (K_right diaDuality);
-instance : HasAxiomD 𝓢 := ⟨fun _ ↦ KP.axiomD⟩
+instance : HasAxiomD 𝓢 := ⟨KP.axiomD⟩
 
 end KP
 

Foundation/Modal/Entailment/KT.lean

@@ -18,7 +18,7 @@ namespace KT'
 
 variable [Entailment.KT' 𝓢]
 
-instance : HasAxiomT 𝓢 := ⟨fun _ ↦ C_trans box_dni (C_of_CNN (C_trans diaTc diaDuality_mp))⟩
+instance : HasAxiomT 𝓢 := ⟨C_trans box_dni (C_of_CNN (C_trans diaTc diaDuality_mp))⟩
 instance : Entailment.KT 𝓢 where
 instance : Entailment.KP 𝓢 where
 instance : Entailment.KD 𝓢 where

Foundation/Modal/Entailment/KTc.lean

@@ -16,16 +16,16 @@ namespace KTc
 variable [Entailment.KTc 𝓢]
 
 protected def axiomFour : 𝓢 ⊢! Axioms.Four φ := axiomTc
-instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ KTc.axiomFour⟩
+instance : HasAxiomFour 𝓢 := ⟨KTc.axiomFour⟩
 
 protected def axiomFive : 𝓢 ⊢! ◇φ ➝ □◇φ := axiomTc
-instance : HasAxiomFive 𝓢 := ⟨fun _ ↦ KTc.axiomFive⟩
+instance : HasAxiomFive 𝓢 := ⟨KTc.axiomFive⟩
 
 protected def axiomDiaT : 𝓢 ⊢! ◇φ ➝ φ := by
   apply C_trans (K_left diaDuality) ?_;
   apply CN_of_CN_left;
   exact axiomTc;
-instance : HasAxiomDiaT 𝓢 := ⟨fun _ ↦ KTc.axiomDiaT⟩
+instance : HasAxiomDiaT 𝓢 := ⟨KTc.axiomDiaT⟩
 
 end KTc
 
@@ -35,7 +35,7 @@ namespace KTc'
 variable [Entailment.KTc' 𝓢]
 
 protected def axiomTc : 𝓢 ⊢! φ ➝ □φ := C_trans (C_of_CNN (C_trans (K_right diaDuality) diaT)) box_dne
-instance : HasAxiomTc 𝓢 := ⟨fun _ ↦ KTc'.axiomTc⟩
+instance : HasAxiomTc 𝓢 := ⟨KTc'.axiomTc⟩
 
 end KTc'
 

Foundation/Modal/Entailment/S5Grz.lean

@@ -25,7 +25,7 @@ protected noncomputable def S5Grz.diaT : 𝓢 ⊢! ◇φ ➝ φ := by
   have : 𝓢 ⊢! □◇φ ➝ φ := C_trans this axiomGrz;
   exact C_trans axiomFive this;
 
-noncomputable instance : HasAxiomDiaT 𝓢 := ⟨fun _ ↦ S5Grz.diaT⟩
+noncomputable instance : HasAxiomDiaT 𝓢 := ⟨S5Grz.diaT⟩
 noncomputable instance : Entailment.KTc' 𝓢 where
 
 end LO.Modal.Entailment

Foundation/Modal/Entailment/Ver.lean

@@ -26,10 +26,10 @@ lemma bot_of_dia'! (h : 𝓢 ⊢ ◇φ) : 𝓢 ⊢ ⊥ := ⟨bot_of_dia' h.some
 namespace Ver
 
 protected def axiomTc : 𝓢 ⊢! Axioms.Tc φ := C_of_conseq axiomVer
-instance : HasAxiomTc 𝓢 := ⟨fun _ ↦ Ver.axiomTc⟩
+instance : HasAxiomTc 𝓢 := ⟨Ver.axiomTc⟩
 
 protected def axiomL : 𝓢 ⊢! Axioms.L φ := C_of_conseq axiomVer
-instance : HasAxiomL 𝓢 := ⟨fun _ ↦ Ver.axiomL⟩
+instance : HasAxiomL 𝓢 := ⟨Ver.axiomL⟩
 
 end Ver