Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem (FOL/NV/Sub/Var/All/Rec/Fresh/Sub.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
c : Char
F : Formula
⊢ Holds D I V E (sub σ c F) ↔ Holds D I (V ∘ σ) E F
Tactic:
induction F generalizing σ V
State after:
case pred_const_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (pred_const_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (pred_const_ a✝¹ a✝)

case pred_var_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (pred_var_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (pred_var_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (eq_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c true_) ↔ Holds D I (V ∘ σ) E true_

case false_
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c false_) ↔ Holds D I (V ∘ σ) E false_

case not_
D : Type
I : Interpretation D
E : Env
c : Char
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c a✝.not_) ↔ Holds D I (V ∘ σ) E a✝.not_

case imp_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.imp_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.imp_ a✝)

case and_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.and_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.and_ a✝)

case or_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.or_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.or_ a✝)

case iff_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.iff_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.iff_ a✝)

case forall_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (forall_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (forall_ a✝¹ a✝)

case exists_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (exists_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (exists_ a✝¹ a✝)

case def_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (def_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (def_ a✝¹ a✝)

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (eq_ x y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Tactic:
case pred_const_ X xs | pred_var_ X xs | eq_ x y =>
  simp only [sub]
  simp only [Holds]
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c false_) ↔ Holds D I (V ∘ σ) E false_
Tactic:
case true_ | false_ =>
  simp only [sub]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi.not_) ↔ Holds D I (V ∘ σ) E phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [sub]
  simp only [Holds]
  congr! 1
  exact phi_ih V σ
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (eq_ x y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (eq_ (σ x) (σ y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (eq_ (σ x) (σ y)) ↔ Holds D I (V ∘ σ) E (eq_ x y)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ V (σ x) = V (σ y) ↔ (V ∘ σ) x = (V ∘ σ) y

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x y : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ V (σ x) = V (σ y) ↔ (V ∘ σ) x = (V ∘ σ) y
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c false_) ↔ Holds D I (V ∘ σ) E false_
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E false_ ↔ Holds D I (V ∘ σ) E false_

State before:
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E false_ ↔ Holds D I (V ∘ σ) E false_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi.not_) ↔ Holds D I (V ∘ σ) E phi.not_
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi).not_ ↔ Holds D I (V ∘ σ) E phi.not_

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi).not_ ↔ Holds D I (V ∘ σ) E phi.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ¬Holds D I V E (sub σ c phi) ↔ ¬Holds D I (V ∘ σ) E phi

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ¬Holds D I V E (sub σ c phi) ↔ ¬Holds D I (V ∘ σ) E phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
Tactic:
exact phi_ih V σ
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (phi.iff_ psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E ((sub σ c phi).iff_ (sub σ c psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E ((sub σ c phi).iff_ (sub σ c psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ (Holds D I V E (sub σ c phi) ↔ Holds D I V E (sub σ c psi)) ↔ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi)

State before:
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ (Holds D I V E (sub σ c phi) ↔ Holds D I V E (sub σ c psi)) ↔ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
Tactic:
exact phi_ih V σ
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
Tactic:
exact psi_ih V σ
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (exists_ x phi)) ↔ Holds D I (V ∘ σ) E (exists_ x phi)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E
      (exists_
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    Holds D I (V ∘ σ) E (exists_ x phi)

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E
      (exists_
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    Holds D I (V ∘ σ) E (exists_ x phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ (∃ d,
      Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    ∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ (∃ d,
      Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    ∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ∀ (a : D),
    Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          a)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi) ↔
      Holds D I (Function.updateITE (V ∘ σ) x a) E phi

State before:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ∀ (a : D),
    Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          a)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi) ↔
      Holds D I (Function.updateITE (V ∘ σ) x a) E phi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ Holds D I
      (Function.updateITE V
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        d)
      E
      (sub
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
        c phi) ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi

State before:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ Holds D I
      (Function.updateITE V
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        d)
      E
      (sub
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
        c phi) ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
simp only [phi_ih]
State after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ Holds D I
      (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      E phi ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi

State before:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ Holds D I
      (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      E phi ↔
    Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
apply Holds_coincide_Var
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ ∀ (v : VarName),
    isFreeIn v phi →
      (Function.updateITE V
              (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
              else x)
              d ∘
            Function.updateITE σ x
              (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
              else x))
          v =
        Function.updateITE (V ∘ σ) x d v

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
⊢ ∀ (v : VarName),
    isFreeIn v phi →
      (Function.updateITE V
              (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
              else x)
              d ∘
            Function.updateITE σ x
              (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
              else x))
          v =
        Function.updateITE (V ∘ σ) x d v
Tactic:
intro v a1
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
⊢ (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      v =
    Function.updateITE (V ∘ σ) x d v

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
⊢ (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d ∘
        Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x))
      v =
    Function.updateITE (V ∘ σ) x d v
Tactic:
simp
State after:
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V
      (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x) d
      (Function.updateITE σ x
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        v) =
    Function.updateITE (V ∘ σ) x d v

State before:
case h.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V
      (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x) d
      (Function.updateITE σ x
        (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x)
        v) =
    Function.updateITE (V ∘ σ) x d v
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
h✝ : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v

case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
h✝ : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ (∀ (d : D),
      Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    ∀ (d : D), Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ∀ (a : D),
    Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          a)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi) ↔
      Holds D I (Function.updateITE (V ∘ σ) x a) E phi

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ (∃ d,
      Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          d)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi)) ↔
    ∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ ∀ (a : D),
    Holds D I
        (Function.updateITE V
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
          else x)
          a)
        E
        (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi) ↔
      Holds D I (Function.updateITE (V ∘ σ) x a) E phi

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v
Tactic:
obtain s0 := fresh_not_mem x c (freeVarSet (sub (Function.updateITE σ x x) c phi))
State after:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
s0 : fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
s0 : fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) d
      (Function.updateITE σ x (fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet) v) =
    Function.updateITE (V ∘ σ) x d v
Tactic:
generalize (fresh x c (freeVarSet (sub (Function.updateITE σ x x) c phi))) = x' at *
State after:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
by_cases c2 : v = x
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v

case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [c2]
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' x) = Function.updateITE (V ∘ σ) x d x

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' x) = Function.updateITE (V ∘ σ) x d x
Tactic:
simp only [Function.updateITE]
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ (if (if True then x' else σ x) = x' then d else V (if True then x' else σ x)) = if True then d else (V ∘ σ) x

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : v = x
⊢ (if (if True then x' else σ x) = x' then d else V (if True then x' else σ x)) = if True then d else (V ∘ σ) x
Tactic:
simp
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
by_cases c3 : σ v = x'
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : σ v = x'
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v

case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : σ v = x'
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
subst c3
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [freeVarSet_sub_eq_freeVarSet_image] at s0
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
have s1 : σ v ∈ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
State after:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet

case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v

State before:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet

case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
apply Finset.mem_image_update
State after:
case s1.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ ¬v = x

case s1.h2
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ v ∈ phi.freeVarSet

case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s1 : σ v ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ Function.updateITE V (σ v) d (Function.updateITE σ x (σ v) v) = Function.updateITE (V ∘ σ) x d v
Tactic:
contradiction
State after:
no goals

State before:
case s1.h1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ ¬v = x
Tactic:
exact c2
State after:
no goals

State before:
case s1.h2
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ v ∈ phi.freeVarSet
Tactic:
simp only [← isFreeIn_iff_mem_freeVarSet]
State after:
case s1.h2
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ isFreeIn v phi

State before:
case s1.h2
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s0 : σ v ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ isFreeIn v phi
Tactic:
exact a1
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ Function.updateITE V x' d (Function.updateITE σ x x' v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [Function.updateITE]
State after:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if (if v = x then x' else σ v) = x' then d else V (if v = x then x' else σ v)) = if v = x then d else (V ∘ σ) v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if (if v = x then x' else σ v) = x' then d else V (if v = x then x' else σ v)) = if v = x then d else (V ∘ σ) v
Tactic:
simp only [if_neg c2]
State after:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if σ v = x' then d else V (σ v)) = (V ∘ σ) v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ (if σ v = x' then d else V (σ v)) = (V ∘ σ) v
Tactic:
simp only [if_neg c3]
State after:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ V (σ v) = (V ∘ σ) v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
x' : VarName
s0 : x' ∉ (sub (Function.updateITE σ x x) c phi).freeVarSet
c2 : ¬v = x
c3 : ¬σ v = x'
⊢ V (σ v) = (V ∘ σ) v
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
by_cases c2 : v = x
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v

case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
subst c2
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ Function.updateITE V v d (Function.updateITE σ v v v) = Function.updateITE (V ∘ σ) v d v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ Function.updateITE V v d (Function.updateITE σ v v v) = Function.updateITE (V ∘ σ) v d v
Tactic:
simp only [Function.updateITE]
State after:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ (if (if True then v else σ v) = v then d else V (if True then v else σ v)) = if True then d else (V ∘ σ) v

State before:
case pos
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {v}, σ y = v
⊢ (if (if True then v else σ v) = v then d else V (if True then v else σ v)) = if True then d else (V ∘ σ) v
Tactic:
simp
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
have s1 : ¬ σ v = x
State after:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ ¬σ v = x

case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ Function.updateITE V x d (Function.updateITE σ x x v) = Function.updateITE (V ∘ σ) x d v
Tactic:
simp only [Function.updateITE]
State after:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if (if v = x then x else σ v) = x then d else V (if v = x then x else σ v)) = if v = x then d else (V ∘ σ) v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if (if v = x then x else σ v) = x then d else V (if v = x then x else σ v)) = if v = x then d else (V ∘ σ) v
Tactic:
simp only [if_neg c2]
State after:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if σ v = x then d else V (σ v)) = (V ∘ σ) v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ (if σ v = x then d else V (σ v)) = (V ∘ σ) v
Tactic:
simp only [if_neg s1]
State after:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ V (σ v) = (V ∘ σ) v

State before:
case neg
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
s1 : ¬σ v = x
⊢ V (σ v) = (V ∘ σ) v
Tactic:
simp
State after:
no goals

State before:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
⊢ ¬σ v = x
Tactic:
intro contra
State after:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ False

State before:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ False
Tactic:
apply c1
State after:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ ∃ y ∈ phi.freeVarSet \ {x}, σ y = x

State before:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ ∃ y ∈ phi.freeVarSet \ {x}, σ y = x
Tactic:
apply Exists.intro v
State after:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x} ∧ σ v = x

State before:
case s1
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x} ∧ σ v = x
Tactic:
constructor
State after:
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x}

case s1.right
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ σ v = x

State before:
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x}
Tactic:
simp
State after:
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet ∧ ¬v = x

State before:
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet ∧ ¬v = x
Tactic:
simp only [← isFreeIn_iff_mem_freeVarSet]
State after:
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ isFreeIn v phi ∧ ¬v = x

State before:
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ isFreeIn v phi ∧ ¬v = x
Tactic:
tauto
State after:
no goals

State before:
case s1.right
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ σ v = x
Tactic:
exact contra
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) E (def_ X xs)
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)

case cons
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I V tail✝ (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) tail✝ (def_ X xs)
⊢ Holds D I V (head✝ :: tail✝) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (head✝ :: tail✝) (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Tactic:
case nil =>
  simp only [sub]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V [] (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [sub] at E_ih
State after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (sub σ c (def_ X xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ Holds D I V (E_hd :: E_tl) (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q

case neg
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
case neg c1 =>
  exact E_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v E_hd.q →
      Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
        Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v

State before:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v E_hd.q →
      Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
        Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
intro v a1
State after:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v

State before:
case h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
apply Function.updateListITE_map_mem_ext
State after:
case h1.h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ ∀ y ∈ xs, (V ∘ σ) y = (V ∘ σ) y

case h1.h2
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ E_hd.args.length = xs.length

case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ v ∈ E_hd.args

State before:
case h1.h1
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ ∀ y ∈ xs, (V ∘ σ) y = (V ∘ σ) y
Tactic:
simp
State after:
no goals

State before:
case h1.h2
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ E_hd.args.length = xs.length
Tactic:
cases c1
State after:
case h1.h2.intro
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
case _ c1_left c1_right =>
  symm
  exact c1_right
State after:
no goals

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ E_hd.args.length = xs.length
Tactic:
symm
State after:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ xs.length = E_hd.args.length

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
v : VarName
a1 : isFreeIn v E_hd.q
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ xs.length = E_hd.args.length
Tactic:
exact c1_right
State after:
no goals

State before:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ v ∈ E_hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args

State before:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args
Tactic:
simp only [← List.mem_toFinset]
State after:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args.toFinset

State before:
case h1.h3
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args.toFinset
Tactic:
apply Finset.mem_of_subset E_hd.h1 a1
State after:
no goals

State before:
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
Tactic:
exact E_ih
State after:
no goals