Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff (Logic/FirstOrder/Interpretation.lean)

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
t : Semiterm L' Empty n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals t) ↔ y = Semiterm.valbm (ι.Sub M) x t
Tactic:
induction t generalizing x y
State after:
case bvar
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Fin n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals #a✝) ↔ y = Semiterm.valbm (ι.Sub M) x #a✝

case fvar
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Empty
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals &a✝) ↔ y = Semiterm.valbm (ι.Sub M) x &a✝

case func
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n arity✝ : ℕ
a✝¹ : L'.Func arity✝
a✝ : Fin arity✝ → Semiterm L' Empty n
a_ih✝ :
  ∀ (a : Fin arity✝) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (a✝ a)) ↔ y = Semiterm.valbm (ι.Sub M) x (a✝ a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (Semiterm.func a✝¹ a✝)) ↔
    y = Semiterm.valbm (ι.Sub M) x (Semiterm.func a✝¹ a✝)

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Fin n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals #a✝) ↔ y = Semiterm.valbm (ι.Sub M) x #a✝
Tactic:
case bvar => simp [varEquals, Subtype.coe_inj]
State after:
no goals

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Empty
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals &a✝) ↔ y = Semiterm.valbm (ι.Sub M) x &a✝
Tactic:
case fvar => contradiction
State after:
no goals

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Fin n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals #a✝) ↔ y = Semiterm.valbm (ι.Sub M) x #a✝
Tactic:
simp [varEquals, Subtype.coe_inj]
State after:
no goals

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Empty
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals &a✝) ↔ y = Semiterm.valbm (ι.Sub M) x &a✝
Tactic:
contradiction
State after:
no goals

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (Semiterm.func f w)) ↔
    y = Semiterm.valbm (ι.Sub M) x (Semiterm.func f w)
Tactic:
simp [varEquals, eval_embSubsts, Matrix.comp_vecCons', Matrix.constant_eq_singleton, Semiterm.val_func, sub_func_iff]
State after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) ↔
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) ↔
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Tactic:
constructor
State after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) →
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)

case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f) →
    ∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)

State before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) →
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Tactic:
intro h
State after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h :
  ∀ (e : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
      (Evalb s (↑y :> fun i => e i)) (ι.func f)
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)

State before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h :
  ∀ (e : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
      (Evalb s (↑y :> fun i => e i)) (ι.func f)
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Tactic:
exact h _ (fun i ↦ ⟨ι.pval_sub_domain M _, (@ih i (Semiterm.valbm (Sub ι M) x (w i)) x).mpr rfl⟩)
State after:
no goals

State before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f) →
    ∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)
Tactic:
rintro h v hv
State after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)

State before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)
Tactic:
have : v = fun i ↦ (Semiterm.valbm (Sub ι M) x (w i)).val :=
  funext fun i ↦ by simpa using congr_arg Subtype.val ((@ih i ⟨v i, (hv i).1⟩ x).mp (hv i).2)
State after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
this : v = fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)

State before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
this : v = fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)
Tactic:
rcases this
State after:
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
hv :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => (fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i)) (ι.func f)

State before:
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
hv :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => (fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i)) (ι.func f)
Tactic:
exact h
State after:
no goals

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
i : Fin k
⊢ v i = ↑(Semiterm.valbm (ι.Sub M) x (w i))
Tactic:
simpa using congr_arg Subtype.val ((@ih i ⟨v i, (hv i).1⟩ x).mp (hv i).2)
State after:
no goals