internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Tactic:
simp only [isFreeIn] at h1_1
Proof state after:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : ¬h1_v = h1_x ∧ isFreeIn h1_v h1_phi
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Tactic:
cases h1_1
Proof state after:
case intro
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
left✝ : ¬h1_v = h1_x
right✝ : isFreeIn h1_v h1_phi
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Tactic:
case intro h1_1_left h1_1_right =>
  simp only [if_neg h1_1_left]
  subst h1_ih
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi'
Tactic:
simp only [if_neg h1_1_left]
Proof state after:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = h1_phi'
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x h1_phi'
Tactic:
subst h1_ih
Proof state after:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
a✝¹ : ¬h1_x = h1_t
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
a✝ : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)
Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
a✝¹ : ¬h1_x = h1_t
h1_1_left : ¬h1_v = h1_x
h1_1_right : isFreeIn h1_v h1_phi
a✝ : IsSub h1_phi h1_v h1_t (Rec.fastReplaceFree h1_v h1_t h1_phi)
⊢ exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi) = exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (pred_var_ h1_X h1_xs) ↔
    Holds D I V E (pred_var_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
case pred_const_ h1_X h1_xs h1_v h1_t | pred_var_ h1_X h1_xs h1_v h1_t =>
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro x _
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 =>
    simp
    simp only [if_pos c1]
  case _ c1 =>
    simp
    simp only [if_neg c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (eq_ h1_x h1_y) ↔
    Holds D I V E (eq_ (if h1_v = h1_x then h1_t else h1_x) (if h1_v = h1_y then h1_t else h1_y))
Tactic:
case eq_ h1_x h1_y h1_v h1_t =>
  simp only [Holds]
  simp only [Function.updateITE]
  simp only [eq_comm]
  congr! 1 <;> { split_ifs <;> rfl }
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E false_ ↔ Holds D I V E false_
Tactic:
case true_ _ _ | false_ _ _ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
case not_ h1_phi h1_v h1_t h1_phi' _ h1_ih =>
  simp only [Holds]
  congr! 1
  apply h1_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi)
Tactic:
case
  forall_not_free_in h1_x h1_phi h1_v h1_t h1_1
| exists_not_free_in h1_x h1_phi h1_v h1_t h1_1 =>
  simp only [isFreeIn] at h1_1
  simp at h1_1
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply Holds_coincide_Var
  intro x a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    rfl
  case _ c1 c2 =>
    subst c2
    tauto
  case _ c1 c2 =>
    rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
h1_2 : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_phi')
Tactic:
case
  forall_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 h1_2 _ h1_ih
| exists_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 h1_2 _ h1_ih =>
  simp only [isFreeIn] at h1_1
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  specialize h1_ih (Function.updateITE V h1_x d)
  simp only [← h1_ih]
  apply Holds_coincide_Var
  intro x _
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 c2 c3 =>
    subst c2
    cases h1_1
    case intro h1_1_left h1_1_right =>
      contradiction
  case _ | _ | _ =>
    rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (pred_var_ h1_X h1_xs) ↔
    Holds D I V E (pred_var_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ I.pred_var_ h1_X (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) ↔
    I.pred_var_ h1_X (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ I.pred_var_ h1_X (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) ↔
    I.pred_var_ h1_X (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs =
    List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs =
    List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs = List.map (V ∘ fun x => if h1_v = x then h1_t else x) h1_xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ ∀ x ∈ h1_xs, Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
intro x _
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ Function.updateITE V h1_v (V h1_t) x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp only [Function.updateITE]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if x = h1_v then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp only [eq_comm]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
⊢ (if h1_v = x then V h1_t else V x) = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
h✝ : h1_v = x
⊢ V h1_t = (V ∘ fun x => if h1_v = x then h1_t else x) x

case neg
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
h✝ : ¬h1_v = x
⊢ V x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
case _ c1 =>
  simp
  simp only [if_pos c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
case _ c1 =>
  simp
  simp only [if_neg c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = V (if h1_v = x then h1_t else x)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : h1_v = x
⊢ V h1_t = V (if h1_v = x then h1_t else x)
Tactic:
simp only [if_pos c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = (V ∘ fun x => if h1_v = x then h1_t else x) x
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = V (if h1_v = x then h1_t else x)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
x : VarName
a✝ : x ∈ h1_xs
c1 : ¬h1_v = x
⊢ V x = V (if h1_v = x then h1_t else x)
Tactic:
simp only [if_neg c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (eq_ h1_x h1_y) ↔
    Holds D I V E (eq_ (if h1_v = h1_x then h1_t else h1_x) (if h1_v = h1_y then h1_t else h1_y))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Function.updateITE V h1_v (V h1_t) h1_x = Function.updateITE V h1_v (V h1_t) h1_y ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Function.updateITE V h1_v (V h1_t) h1_x = Function.updateITE V h1_v (V h1_t) h1_y ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)
Tactic:
simp only [Function.updateITE]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)
Tactic:
simp only [eq_comm]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_x = h1_v then h1_t else h1_x) = V (if h1_y = h1_v then h1_t else h1_y)
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ ((if h1_x = h1_v then V h1_t else V h1_x) = if h1_y = h1_v then V h1_t else V h1_y) ↔
    V (if h1_x = h1_v then h1_t else h1_x) = V (if h1_y = h1_v then h1_t else h1_y)
Tactic:
congr! 1 <;> { split_ifs <;> rfl }
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_3
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ (if h1_y = h1_v then V h1_t else V h1_y) = V (if h1_y = h1_v then h1_t else h1_y)
Tactic:
split_ifs <;> rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E false_ ↔ Holds D I V E false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi.not_ ↔ Holds D I V E h1_phi'.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ ¬Holds D I V E h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ ¬Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ ¬Holds D I V E h1_phi'
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
Tactic:
apply h1_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (h1_phi.iff_ h1_psi) ↔ Holds D I V E (h1_phi'.iff_ h1_psi')
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' h1_phi h1_psi : Formula
h1_v h1_t : VarName
h1_phi' h1_psi' : Formula
a✝¹ : IsSub h1_phi h1_v h1_t h1_phi'
a✝ : IsSub h1_psi h1_v h1_t h1_psi'
h1_ih_1 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I V E h1_phi'
h1_ih_2 : ∀ (V : VarAssignment D), Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi ↔ Holds D I V E h1_psi'
V : VarAssignment D
⊢ (Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_phi ↔ Holds D I (Function.updateITE V h1_v (V h1_t)) E h1_psi) ↔
    (Holds D I V E h1_phi' ↔ Holds D I V E h1_psi')