rename LogicalConnective, _ →ˡᶜ _

Logic/AutoProver/Litform.lean

@@ -16,7 +16,7 @@ inductive Litform (α : Type*) : Type _
 
 namespace Litform
 
-instance : LogicSymbol (Litform α) where
+instance : LogicalConnective (Litform α) where
   top   := Litform.verum
   bot   := Litform.falsum
   wedge := Litform.and
@@ -45,7 +45,7 @@ end ToString
 
 namespace Meta
 
-variable (F : Q(Type*)) (ls : Q(LogicSymbol $F))
+variable (F : Q(Type*)) (ls : Q(LogicalConnective $F))
 
 abbrev Lit (F : Q(Type*)) := Litform Q($F)
 

Logic/AutoProver/Prover.lean

@@ -5,7 +5,7 @@ namespace LO
 
 namespace Gentzen
 
-variable {F : Type*} [LogicSymbol F] [Gentzen F]
+variable {F : Type*} [LogicalConnective F] [Gentzen F]
 
 variable {Γ Δ : List F} {p q r : F}
 
@@ -49,13 +49,13 @@ open Qq Lean Elab Meta Tactic Litform Litform.Meta
 #check TwoSided.Derivation
 
 set_option linter.unusedVariables false in
-abbrev DerivationQ {F : Q(Type u)} (instLS : Q(LogicSymbol $F)) (instGz : Q(Gentzen $F)) (L R : List (Lit F)) :=
+abbrev DerivationQ {F : Q(Type u)} (instLS : Q(LogicalConnective $F)) (instGz : Q(Gentzen $F)) (L R : List (Lit F)) :=
   Q(TwoSided.Derivation $(Denotation.toExprₗ (denotation F instLS) L) $(Denotation.toExprₗ (denotation F instLS) R))
 
 namespace DerivationQ
 open Denotation
 
-variable {F : Q(Type u)} {instLS : Q(LogicSymbol $F)} {instGz : Q(Gentzen $F)} (L R : List (Lit F))
+variable {F : Q(Type u)} {instLS : Q(LogicalConnective $F)} {instGz : Q(Gentzen $F)} (L R : List (Lit F))
 
 def DEq {F : Q(Type*)} : Lit F → Lit F → MetaM Bool
   | Litform.atom e,  Litform.atom e'  => Lean.Meta.isDefEq e e'
@@ -166,7 +166,7 @@ def rImplyRight {p q : Lit F} (d : DerivationQ instLS instGz (L ++ [p]) (R ++ [q
     ($(Denotation.toExprₗ (denotation F instLS) R) ++ [$(toExpr F q)])) := d
   q(Gentzen.rImplyRight $d)
 
-def deriveAux {F : Q(Type u)} (instLS : Q(LogicSymbol $F)) (instGz : Q(Gentzen $F)) :
+def deriveAux {F : Q(Type u)} (instLS : Q(LogicalConnective $F)) (instGz : Q(Gentzen $F)) :
     ℕ → Bool → (L R : List (Lit F)) → MetaM (DerivationQ instLS instGz L R)
   | 0,        _,     L,      R       => throwError m!"failed to prove {L} ⊢ {R}"
   | s + 1,    true,  [],     R       => deriveAux instLS instGz s false [] R
@@ -219,7 +219,7 @@ def deriveAux {F : Q(Type u)} (instLS : Q(LogicSymbol $F)) (instGz : Q(Gentzen $
       let d ← deriveAux instLS instGz s true (L ++ [p]) (R ++ [q])
       return rImplyRight L R d
 
-def derive {F : Q(Type u)} (instLS : Q(LogicSymbol $F)) (instGz : Q(Gentzen $F)) (s : ℕ) (L R : List (Lit F)) :
+def derive {F : Q(Type u)} (instLS : Q(LogicalConnective $F)) (instGz : Q(Gentzen $F)) (s : ℕ) (L R : List (Lit F)) :
     MetaM (DerivationQ instLS instGz L R) := deriveAux instLS instGz s true L R
 
 end DerivationQ
@@ -232,7 +232,7 @@ section
 
 open Litform.Meta Denotation
 
-variable {F : Q(Type u)} (instLS : Q(LogicSymbol $F)) (instSys : Q(System $F))
+variable {F : Q(Type u)} (instLS : Q(LogicalConnective $F)) (instSys : Q(System $F))
   (instGz : Q(Gentzen $F)) (instLTS : Q(LawfulTwoSided $F))
 
 
@@ -290,8 +290,8 @@ elab "tautology" n:(num)? : tactic => do
   let goalType ← Elab.Tactic.getMainTarget
   let ty ← inferPropQ goalType
   let ⟨u, F, T, p⟩ ← isExprProvable? ty
-  let .some instLS ← trySynthInstanceQ (q(LogicSymbol.{u} $F) : Q(Type u))
-    | throwError m! "error: failed to find instance LogicSymbol {F}"
+  let .some instLS ← trySynthInstanceQ (q(LogicalConnective.{u} $F) : Q(Type u))
+    | throwError m! "error: failed to find instance LogicalConnective {F}"
   let .some instSys ← trySynthInstanceQ q(System $F)
     | throwError m! "error: failed to find instance System {F}"
   let .some instGz ← trySynthInstanceQ q(Gentzen $F)
@@ -310,8 +310,8 @@ elab "prover" n:(num)? seq:(termSeq)? : tactic => do
   let goalType ← Elab.Tactic.getMainTarget
   let ty ← inferPropQ goalType
   let ⟨u, F, T, p⟩ ← isExprProvable? ty
-  let .some instLS ← trySynthInstanceQ (q(LogicSymbol.{u} $F) : Q(Type u))
-    | throwError m! "error: failed to find instance LogicSymbol {F}"
+  let .some instLS ← trySynthInstanceQ (q(LogicalConnective.{u} $F) : Q(Type u))
+    | throwError m! "error: failed to find instance LogicalConnective {F}"
   let .some instSys ← trySynthInstanceQ q(System $F)
     | throwError m! "error: failed to find instance System {F}"
   let .some instGz ← trySynthInstanceQ q(Gentzen $F)

Logic/FirstOrder/Arith/Hierarchy.lean

@@ -35,7 +35,7 @@ namespace Hierarchy
 @[simp] lemma and_iff {p q : Semiformula L μ n} : Hierarchy Γ s (p ⋏ q) ↔ Hierarchy Γ s p ∧ Hierarchy Γ s q :=
   ⟨by generalize hr : p ⋏ q = r
       intro H
-      induction H <;> try simp [LogicSymbol.ball, LogicSymbol.bex] at hr
+      induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
       case and =>
         rcases hr with ⟨rfl, rfl⟩
         constructor <;> assumption,
@@ -44,7 +44,7 @@ namespace Hierarchy
 @[simp] lemma or_iff {p q : Semiformula L μ n} : Hierarchy Γ s (p ⋎ q) ↔ Hierarchy Γ s p ∧ Hierarchy Γ s q :=
   ⟨by generalize hr : p ⋎ q = r
       intro H
-      induction H <;> try simp [LogicSymbol.ball, LogicSymbol.bex] at hr
+      induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
       case or =>
         rcases hr with ⟨rfl, rfl⟩
         constructor <;> assumption,
@@ -162,7 +162,7 @@ lemma neg {p : Semiformula L μ n} : Hierarchy Γ s p → Hierarchy Γ.alt s (~p
     Hierarchy Γ s (∀[“#0 < !!t”] p) ↔ Hierarchy Γ s p :=
   ⟨by generalize hq : (∀[“#0 < !!t”] p) = q
       intro H
-      induction H <;> try simp [LogicSymbol.ball, LogicSymbol.bex] at hq
+      induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hq
       case ball p t pt hp ih =>
         rcases hq with ⟨rfl, rfl⟩
         assumption
@@ -182,7 +182,7 @@ lemma neg {p : Semiformula L μ n} : Hierarchy Γ s p → Hierarchy Γ.alt s (~p
     Hierarchy Γ s (∃[“#0 < !!t”] p) ↔ Hierarchy Γ s p :=
   ⟨by generalize hq : (∃[“#0 < !!t”] p) = q
       intro H
-      induction H <;> try simp [LogicSymbol.ball, LogicSymbol.bex] at hq
+      induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hq
       case bex p t pt hp ih =>
         rcases hq with ⟨rfl, rfl⟩
         assumption
@@ -202,7 +202,7 @@ lemma pi_of_pi_all {p : Semiformula L μ (n + 1)} : Hierarchy Π s (∀' p) →
   generalize hr : ∀' p = r
   generalize hb : Π = Γ
   intro H
-  cases H <;> try simp [LogicSymbol.ball, LogicSymbol.bex] at hr
+  cases H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
   case ball => rcases hr with rfl; simpa
   case all => rcases hr with rfl; simpa
   case pi hp => rcases hr with rfl; exact hp.accum _
@@ -215,7 +215,7 @@ lemma sigma_of_sigma_ex {p : Semiformula L μ (n + 1)} : Hierarchy Σ s (∃' p)
   generalize hr : ∃' p = r
   generalize hb : Σ = Γ
   intro H
-  cases H <;> try simp [LogicSymbol.ball, LogicSymbol.bex] at hr
+  cases H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
   case bex => rcases hr with rfl; simpa
   case ex => rcases hr with rfl; simpa
   case sigma hp => rcases hr with rfl; exact hp.accum _
@@ -280,13 +280,13 @@ lemma exClosure : {n : ℕ} → {p : Semiformula L μ n} → Hierarchy Σ (s + 1
   | 0,     _, hp => hp
   | n + 1, p, hp => by simpa using exClosure (hp.ex)
 
-instance : LogicSymbol.AndOrClosed (Hierarchy Γ s : Semiformula L μ k → Prop) where
+instance : LogicalConnective.AndOrClosed (Hierarchy Γ s : Semiformula L μ k → Prop) where
   verum := verum _ _ _
   falsum := falsum _ _ _
   and := and
   or := or
 
-instance : LogicSymbol.Closed (Hierarchy Γ 0 : Semiformula L μ k → Prop) where
+instance : LogicalConnective.Closed (Hierarchy Γ 0 : Semiformula L μ k → Prop) where
   not := by simp[neg_iff]
   imply := by simp[Semiformula.imp_eq, neg_iff]; intro p q hp hq; simp[*]
 

Logic/FirstOrder/Basic/Calculus.lean

@@ -220,7 +220,7 @@ def em {p : SyntacticFormula L} {Δ : Sequent L} (hpos : p ∈ Δ) (hneg : ~p 
     have : ⊢¹ Rew.free.hom p :: Δ⁺ := (ex &0 this).wk
       (by simp; right;
           have := mem_shifts_iff.mpr hneg
-          rwa [Rew.ex, Rew.q_shift, LogicSymbol.HomClass.map_neg] at this)
+          rwa [Rew.ex, Rew.q_shift, LogicalConnective.HomClass.map_neg] at this)
     exact this.all.wk (by simp[hpos])
   case hex p ih         =>
     have : ⊢¹ Rew.free.hom p :: ~Rew.free.hom p :: Δ⁺ := ih (by simp) (by simp)

Logic/FirstOrder/Basic/Elab.lean

@@ -282,21 +282,21 @@ def unexpandArrow : Unexpander
   | `($_ $t:term         “$q:foformula”) => `(“ (!$t → $q) ”)
   | _                                     => throw ()
 
-@[app_unexpander LogicSymbol.iff]
+@[app_unexpander LogicalConnective.iff]
 def unexpandIff : Unexpander
   | `($_ “$p:foformula” “$q:foformula”) => `(“ ($p ↔ $q) ”)
   | `($_ “$p:foformula” $u:term)         => `(“ ($p ↔ !$u) ”)
   | `($_ $t:term         “$q:foformula”) => `(“ (!$t ↔ $q) ”)
   | _                                     => throw ()
 
-@[app_unexpander LogicSymbol.ball]
+@[app_unexpander LogicalConnective.ball]
 def unexpandBall : Unexpander
   | `($_ “$p:foformula” “$q:foformula”) => `(“ (∀[$p] $q) ”)
   | `($_ “$p:foformula” $u:term)         => `(“ (∀[$p] !$u) ”)
   | `($_ $t:term         “$q:foformula”) => `(“ (∀[!$t] $q) ”)
   | _                                     => throw ()
 
-@[app_unexpander LogicSymbol.bex]
+@[app_unexpander LogicalConnective.bex]
 def unexpandBEx : Unexpander
   | `($_ “$p:foformula” “$q:foformula”) => `(“ (∃[$p] $q) ”)
   | `($_ “$p:foformula” $u:term)         => `(“ (∃[$p] !$u) ”)

Logic/FirstOrder/Basic/Semantics/Semantics.lean

@@ -204,7 +204,7 @@ def Eval' (s : Structure L M) (ε : μ → M) : ∀ {n}, (Fin n → M) → Semif
     Eval' s ε e (~p) = ¬Eval' s ε e p :=
   by induction p using rec' <;> simp[*, Eval', ←neg_eq, or_iff_not_imp_left]
 
-def Eval (s : Structure L M) (e : Fin n → M) (ε : μ → M) : Semiformula L μ n →L Prop where
+def Eval (s : Structure L M) (e : Fin n → M) (ε : μ → M) : Semiformula L μ n →ˡᶜ Prop where
   toTr := Eval' s ε e
   map_top' := rfl
   map_bot' := rfl
@@ -214,19 +214,19 @@ def Eval (s : Structure L M) (e : Fin n → M) (ε : μ → M) : Semiformula L 
   map_imply' := by simp[imp_eq, Eval'_neg, ←neg_eq, Eval', imp_iff_not_or]
 
 abbrev Eval! (M : Type w) [s : Structure L M] {n} (e : Fin n → M) (ε : μ → M) :
-    Semiformula L μ n →L Prop := Eval s e ε
+    Semiformula L μ n →ˡᶜ Prop := Eval s e ε
 
-abbrev Val (s : Structure L M) (ε : μ → M) : Formula L μ →L Prop := Eval s ![] ε
+abbrev Val (s : Structure L M) (ε : μ → M) : Formula L μ →ˡᶜ Prop := Eval s ![] ε
 
-abbrev PVal (s : Structure L M) (e : Fin n → M) : Semisentence L n →L Prop := Eval s e Empty.elim
+abbrev PVal (s : Structure L M) (e : Fin n → M) : Semisentence L n →ˡᶜ Prop := Eval s e Empty.elim
 
 abbrev Val! (M : Type w) [s : Structure L M] (ε : μ → M) :
-    Formula L μ →L Prop := Val s ε
+    Formula L μ →ˡᶜ Prop := Val s ε
 
 abbrev PVal! (M : Type w) [s : Structure L M] (e : Fin n → M) :
-    Semiformula L Empty n →L Prop := PVal s e
+    Semiformula L Empty n →ˡᶜ Prop := PVal s e
 
-abbrev Realize (s : Structure L M) : Formula L M →L Prop := Eval s ![] id
+abbrev Realize (s : Structure L M) : Formula L M →ˡᶜ Prop := Eval s ![] id
 
 lemma eval_rel {k} {r : L.Rel k} {v} :
     Eval s e ε (rel r v) ↔ s.rel r (fun i => Semiterm.val s e ε (v i)) := of_eq rfl
@@ -272,7 +272,7 @@ lemma eval_nrel {k} {r : L.Rel k} {v} :
 
 @[simp] lemma eval_ball {p q : Semiformula L μ (n + 1)} :
     Eval s e ε (∀[p] q) ↔ ∀ x : M, Eval s (x :> e) ε p → Eval s (x :> e) ε q := by
-  simp[LogicSymbol.ball]
+  simp[LogicalConnective.ball]
 
 @[simp] lemma eval_ex {p : Semiformula L μ (n + 1)} :
     Eval s e ε (∃' p) ↔ ∃ x : M, Eval s (x :> e) ε p := of_eq rfl
@@ -286,7 +286,7 @@ lemma eval_nrel {k} {r : L.Rel k} {v} :
 
 @[simp] lemma eval_bex {p q : Semiformula L μ (n + 1)} :
     Eval s e ε (∃[p] q) ↔ ∃ x : M, Eval s (x :> e) ε p ⋏ Eval s (x :> e) ε q := by
-  simp[LogicSymbol.bex]
+  simp[LogicalConnective.bex]
 
 lemma eval_rew (ω : Rew L μ₁ n₁ μ₂ n₂) (p : Semiformula L μ₁ n₁) :
     Eval s e₂ ε₂ (ω.hom p) ↔ Eval s (Semiterm.val s e₂ ε₂ ∘ ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ω ∘ Semiterm.fvar) p := by
@@ -451,7 +451,7 @@ section
 
 variable (M : Type u) [Nonempty M] [s : Structure L M] {T U : Theory L}
 
-abbrev Models : Sentence L →L Prop := Semantics.realize s.toStruc
+abbrev Models : Sentence L →ˡᶜ Prop := Semantics.realize s.toStruc
 
 postfix:max " ⊧ₘ " => Models
 
@@ -464,7 +464,7 @@ abbrev Theory.Mod (T : Theory L) := Semantics.Mod s.toStruc T
 
 lemma Theory.Mod.iff {T : Theory L} : T.Mod M ↔ M ⊧ₘ* T := iff_of_eq <| by simp [Mod, Semantics.Mod.iff]
 
-abbrev Realize (M : Type u) [s : Structure L M] : Formula L M →L Prop := Semiformula.Val s id
+abbrev Realize (M : Type u) [s : Structure L M] : Formula L M →ˡᶜ Prop := Semiformula.Val s id
 
 postfix:max " ⊧ₘᵣ " => Realize
 

Logic/FirstOrder/Basic/Syntax/Formula.lean

@@ -54,7 +54,7 @@ def neg {n} : Semiformula L ξ n → Semiformula L ξ n
 lemma neg_neg (p : Semiformula L ξ n) : neg (neg p) = p :=
   by induction p <;> simp[*, neg]
 
-instance : LogicSymbol (Semiformula L ξ n) where
+instance : LogicalConnective (Semiformula L ξ n) where
   tilde := neg
   arrow := fun p q => or (neg p) q
   wedge := and
@@ -130,10 +130,10 @@ lemma ball_eq (p q : Semiformula L ξ (n + 1)) : (∀[p] q) = ∀' (p ⟶ q) :=
 lemma bex_eq (p q : Semiformula L ξ (n + 1)) : (∃[p] q) = ∃' (p ⋏ q) := rfl
 
 @[simp] lemma neg_ball (p q : Semiformula L ξ (n + 1)) : ~(∀[p] q) = ∃[p] ~q := by
-  simp[LogicSymbol.ball, LogicSymbol.bex, imp_eq]
+  simp[LogicalConnective.ball, LogicalConnective.bex, imp_eq]
 
 @[simp] lemma neg_bex (p q : Semiformula L ξ (n + 1)) : ~(∃[p] q) = ∀[p] ~q := by
-  simp[LogicSymbol.ball, LogicSymbol.bex, imp_eq]
+  simp[LogicalConnective.ball, LogicalConnective.bex, imp_eq]
 
 @[simp] lemma and_inj (p₁ q₁ p₂ q₂ : Semiformula L ξ n) : p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂ :=
 by simp[Wedge.wedge]
@@ -455,7 +455,7 @@ lemma lMapAux_neg {n} (p : Semiformula L₁ ξ n) :
     (~p).lMapAux Φ = ~p.lMapAux Φ :=
   by induction p using Semiformula.rec' <;> simp[*, lMapAux, ←Semiformula.neg_eq]
 
-def lMap (Φ : L₁ →ᵥ L₂) {n} : Semiformula L₁ ξ n →L Semiformula L₂ ξ n where
+def lMap (Φ : L₁ →ᵥ L₂) {n} : Semiformula L₁ ξ n →ˡᶜ Semiformula L₂ ξ n where
   toTr := lMapAux Φ
   map_top' := by simp[lMapAux]
   map_bot' := by simp[lMapAux]

Logic/FirstOrder/Basic/Syntax/Rew.lean

@@ -642,7 +642,7 @@ lemma neg' (p : Semiformula L ξ₁ n₁) : ω.loMap (~p) = ~ω.loMap p := loMap
 
 lemma or' (p q : Semiformula L ξ₁ n₁) : ω.loMap (p ⋎ q) = ω.loMap p ⋎ ω.loMap q := by rfl
 
-def hom (ω : Rew L ξ₁ n₁ ξ₂ n₂) : Semiformula L ξ₁ n₁ →L Semiformula L ξ₂ n₂ where
+def hom (ω : Rew L ξ₁ n₁ ξ₂ n₂) : Semiformula L ξ₁ n₁ →ˡᶜ Semiformula L ξ₂ n₂ where
   map_top' := by rfl
   map_bot' := by rfl
   map_neg' := ω.loMap_neg
@@ -665,7 +665,7 @@ lemma neg' (p : Semiformula L ξ₁ n₁) : ω (~p) = ~ω p := loMap_neg ω p
 
 lemma or' (p q : Semiformula L ξ₁ n₁) : ω (p ⋎ q) = ω p ⋎ ω q := by rfl
 
-instance : LogicSymbol.homClass (Rew L ξ₁ n₁ ξ₂ n₂) (Semiformula L ξ₁ n₁) (Semiformula L ξ₂ n₂) where
+instance : LogicalConnective.homClass (Rew L ξ₁ n₁ ξ₂ n₂) (Semiformula L ξ₁ n₁) (Semiformula L ξ₂ n₂) where
   map_top := fun ω => by rfl
   map_bot := fun ω => by rfl
   map_neg := loMap_neg
@@ -736,7 +736,7 @@ lemma hom_ext' {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) {
 
 end
 
-@[simp] lemma hom_id_eq : (Rew.id.hom : Semiformula L ξ n →L Semiformula L ξ n) = LogicSymbol.Hom.id := by
+@[simp] lemma hom_id_eq : (Rew.id.hom : Semiformula L ξ n →ˡᶜ Semiformula L ξ n) = LogicalConnective.Hom.id := by
   ext p; induction p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel, *]
 
 lemma hom_comp_eq (ω₂ : Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : Rew L ξ₁ n₁ ξ₂ n₂) : (ω₂.comp ω₁).hom = ω₂.hom.comp ω₁.hom := by
@@ -838,13 +838,13 @@ lemma eq_ex_iff {p : Semiformula L ξ₁ n₁} {q} :
 
 lemma eq_ball_iff {p : Semiformula L ξ₁ n₁} {q₁ q₂} :
     (ω.hom p = ∀[q₁] q₂) ↔ ∃ p₁ p₂, ω.q.hom p₁ = q₁ ∧ ω.q.hom p₂ = q₂ ∧ p = ∀[p₁] p₂ := by
-  simp[LogicSymbol.ball, eq_all_iff]; constructor
+  simp[LogicalConnective.ball, eq_all_iff]; constructor
   · rintro ⟨p', ⟨p₁, rfl, p₂, rfl, rfl⟩, rfl⟩; exact ⟨p₁, rfl, p₂, rfl, rfl⟩
   · rintro ⟨p₁, rfl, p₂, rfl, rfl⟩; simp
 
 lemma eq_bex_iff {p : Semiformula L ξ₁ n₁} {q₁ q₂} :
     (ω.hom p = ∃[q₁] q₂) ↔ ∃ p₁ p₂, ω.q.hom p₁ = q₁ ∧ ω.q.hom p₂ = q₂ ∧ p = ∃[p₁] p₂ := by
-  simp[LogicSymbol.bex, eq_ex_iff]; constructor
+  simp[LogicalConnective.bex, eq_ex_iff]; constructor
   · rintro ⟨p', ⟨p₁, rfl, p₂, rfl, rfl⟩, rfl⟩; exact ⟨p₁, rfl, p₂, rfl, rfl⟩
   · rintro ⟨p₁, rfl, p₂, rfl, rfl⟩; simp