Theorem: FOL.NV.evalPrime_substPrime_eq_evalPrime_evalPrime (FOL/NV/Margaris/Prop.lean)

State before:
F : Formula
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ F) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) F
Tactic:
induction F
State after:
case pred_const_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (pred_const_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (pred_const_ a✝¹ a✝)

case pred_var_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (pred_var_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (pred_var_ a✝¹ a✝)

case eq_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : VarName
⊢ evalPrime V (substPrime σ (eq_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (eq_ a✝¹ a✝)

case true_
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ true_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) true_

case false_
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ false_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) false_

case not_
σ : Formula → Formula
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ a✝.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝.not_

case imp_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.imp_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.imp_ a✝)

case and_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.and_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.and_ a✝)

case or_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.or_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.or_ a✝)

case iff_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : evalPrime V (substPrime σ a✝¹) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝¹
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (a✝¹.iff_ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (a✝¹.iff_ a✝)

case forall_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (forall_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (forall_ a✝¹ a✝)

case exists_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : evalPrime V (substPrime σ a✝) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) a✝
⊢ evalPrime V (substPrime σ (exists_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (exists_ a✝¹ a✝)

case def_
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)

State before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Tactic:
case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  simp
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ false_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) false_
Tactic:
case true_ | false_ =>
  rfl
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  congr! 1
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V (substPrime σ (phi.iff_ psi)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp only [Formula.substPrime]
  simp only [Formula.evalPrime]
  congr! 1
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (substPrime σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Tactic:
simp only [Formula.substPrime]
State after:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)

State before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (def_ a✝¹ a✝)
Tactic:
simp only [Formula.evalPrime]
State after:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ decide (evalPrime V (σ (def_ a✝¹ a✝))) = true

State before:
σ : Formula → Formula
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
⊢ evalPrime V (σ (def_ a✝¹ a✝)) ↔ decide (evalPrime V (σ (def_ a✝¹ a✝))) = true
Tactic:
simp
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
⊢ evalPrime V (substPrime σ false_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) false_
Tactic:
rfl
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi.not_) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Tactic:
simp only [Formula.substPrime]
State after:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi).not_ ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ evalPrime V (substPrime σ phi).not_ ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi.not_
Tactic:
simp only [Formula.evalPrime]
State after:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ ¬evalPrime V (substPrime σ phi) ↔ ¬evalPrime (fun H => decide (evalPrime V (σ H))) phi

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
⊢ ¬evalPrime V (substPrime σ phi) ↔ ¬evalPrime (fun H => decide (evalPrime V (σ H))) phi
Tactic:
congr! 1
State after:
no goals

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V (substPrime σ (phi.iff_ psi)) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
Tactic:
simp only [Formula.substPrime]
State after:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V ((substPrime σ phi).iff_ (substPrime σ psi)) ↔
    evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ evalPrime V ((substPrime σ phi).iff_ (substPrime σ psi)) ↔
    evalPrime (fun H => decide (evalPrime V (σ H))) (phi.iff_ psi)
Tactic:
simp only [Formula.evalPrime]
State after:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ (evalPrime V (substPrime σ phi) ↔ evalPrime V (substPrime σ psi)) ↔
    (evalPrime (fun H => decide (evalPrime V (σ H))) phi ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi)

State before:
σ : Formula → Formula
V : VarBoolAssignment
phi psi : Formula
phi_ih : evalPrime V (substPrime σ phi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) phi
psi_ih : evalPrime V (substPrime σ psi) ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi
⊢ (evalPrime V (substPrime σ phi) ↔ evalPrime V (substPrime σ psi)) ↔
    (evalPrime (fun H => decide (evalPrime V (σ H))) phi ↔ evalPrime (fun H => decide (evalPrime V (σ H))) psi)
Tactic:
congr! 1
State after:
no goals