Theorem: MM0.holds_conv (FOL/MM0/MM0.lean)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2 : IsConv E F F'
⊢ Holds D I V M E F ↔ Holds D I V M E F'
Tactic:
induction h2 generalizing V
State after:
case conv_refl
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ : Formula
V : Valuation D
⊢ Holds D I V M E phi✝ ↔ Holds D I V M E phi✝

case conv_symm
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ : Formula
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
V : Valuation D
⊢ Holds D I V M E phi'✝ ↔ Holds D I V M E phi✝

case conv_trans
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ phi''✝ : Formula
a✝¹ : IsConv E phi✝ phi'✝
a✝ : IsConv E phi'✝ phi''✝
a_ih✝¹ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi'✝ ↔ Holds D I V M E phi''✝
V : Valuation D
⊢ Holds D I V M E phi✝ ↔ Holds D I V M E phi''✝

case conv_not
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ : Formula
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
V : Valuation D
⊢ Holds D I V M E phi✝.not_ ↔ Holds D I V M E phi'✝.not_

case conv_imp
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : IsConv E phi✝ phi'✝
a✝ : IsConv E psi✝ psi'✝
a_ih✝¹ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E psi✝ ↔ Holds D I V M E psi'✝
V : Valuation D
⊢ Holds D I V M E (phi✝.imp_ psi✝) ↔ Holds D I V M E (phi'✝.imp_ psi'✝)

case conv_forall
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
x✝ : VarName
phi✝ phi'✝ : Formula
a✝ : IsConv E phi✝ phi'✝
a_ih✝ : ∀ (V : Valuation D), Holds D I V M E phi✝ ↔ Holds D I V M E phi'✝
V : Valuation D
⊢ Holds D I V M E (forall_ x✝ phi✝) ↔ Holds D I V M E (forall_ x✝ phi'✝)

case conv_unfold
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d✝ : Definition
σ✝ : Instantiation
a✝ : d✝ ∈ E
V : Valuation D
⊢ Holds D I V M E (def_ d✝.name (List.map (↑σ✝) d✝.args)) ↔ Holds D I V M E (sub σ✝ meta_var_ d✝.F)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi : Formula
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi
Tactic:
case conv_refl h2_phi =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi
Tactic:
case conv_symm h2_phi h2_phi' _ h2_ih =>
  symm
  exact h2_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi''
Tactic:
case conv_trans h2_phi h2_phi' h2_phi'' _ _ h2_ih_1 h2_ih_2 =>
  trans Holds D I V M E h2_phi'
  exact h2_ih_1 V
  exact h2_ih_2 V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi.not_ ↔ Holds D I V M E h2_phi'.not_
Tactic:
case conv_not h2_phi h2_phi' _ h2_ih =>
  simp only [Holds]
  congr! 1
  exact h2_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E (forall_ h2_x h2_phi) ↔ Holds D I V M E (forall_ h2_x h2_phi')
Tactic:
case conv_forall h2_x h2_phi h2_phi' _ h2_ih =>
  simp only [Holds]
  apply forall_congr'
  intro a
  exact h2_ih (Function.updateITE V h2_x a)
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)
Tactic:
case conv_unfold d σ h2 =>
  obtain ⟨σ', a1⟩ := σ.2
  have s1 : IsMetaVarOrAllDefInEnv E d.F := def_in_well_formed_env_is_meta_var_or_all_def_in_env E d h1 h2
  simp only [← holds_sub D I V M E σ σ' meta_var_ d.F s1 a1]
  clear s1
  have s2 : d.name = d.name ∧ (List.map σ.val d.args).length = d.args.length
  simp
  simp only [← lem_4 D I V M E d d.name (List.map σ.val d.args) h1 h2 s2]
  clear s2
  have s3 : d.F.metaVarSet = ∅ := no_meta_var_imp_meta_var_set_is_empty d.F d.args d.nf
  simp only [holds_coincide_meta_var_no_meta_var D I (V ∘ σ.val) (fun (X' : MetaVarName) (V' : Valuation D) => Holds D I (V' ∘ σ') M E (meta_var_ X')) M E d.F s3]
  clear s3
  apply holds_coincide_var D I (Function.updateListITE V d.args (List.map V (List.map σ.val d.args))) (V ∘ σ.val) M E d.F d.args d.nf
  intro v a2
  simp
  exact Function.updateListITE_map_mem V (V ∘ σ.val) d.args v a2
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi : Formula
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi
Tactic:
symm
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
Tactic:
exact h2_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi''
Tactic:
trans Holds D I V M E h2_phi'
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'

D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'

D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
Tactic:
exact h2_ih_1 V
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_phi'' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_phi' h2_phi''
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
V : Valuation D
⊢ Holds D I V M E h2_phi' ↔ Holds D I V M E h2_phi''
Tactic:
exact h2_ih_2 V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi.not_ ↔ Holds D I V M E h2_phi'.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ ¬Holds D I V M E h2_phi ↔ ¬Holds D I V M E h2_phi'

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ ¬Holds D I V M E h2_phi ↔ ¬Holds D I V M E h2_phi'
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
Tactic:
exact h2_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
⊢ Holds D I V M E (h2_phi.imp_ h2_psi) ↔ Holds D I V M E (h2_phi'.imp_ h2_psi')
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
⊢ Holds D I V M E h2_phi → Holds D I V M E h2_psi ↔ Holds D I V M E h2_phi' → Holds D I V M E h2_psi'

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
⊢ Holds D I V M E h2_phi → Holds D I V M E h2_psi ↔ Holds D I V M E h2_phi' → Holds D I V M E h2_psi'
Tactic:
congr! 1
State after:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝² : IsConv E h2_phi h2_phi'
a✝¹ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
a✝ : Holds D I V M E h2_phi'
⊢ Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'

State before:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝¹ : IsConv E h2_phi h2_phi'
a✝ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
⊢ Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
Tactic:
exact h2_ih_1 V
State after:
no goals

State before:
case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_phi h2_phi' h2_psi h2_psi' : Formula
a✝² : IsConv E h2_phi h2_phi'
a✝¹ : IsConv E h2_psi h2_psi'
h2_ih_1 : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
h2_ih_2 : ∀ (V : Valuation D), Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
V : Valuation D
a✝ : Holds D I V M E h2_phi'
⊢ Holds D I V M E h2_psi ↔ Holds D I V M E h2_psi'
Tactic:
exact h2_ih_2 V
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ Holds D I V M E (forall_ h2_x h2_phi) ↔ Holds D I V M E (forall_ h2_x h2_phi')
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h2_x d) M E h2_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h2_x d) M E h2_phi'

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ (∀ (d : D), Holds D I (Function.updateITE V h2_x d) M E h2_phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V h2_x d) M E h2_phi'
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h2_x a) M E h2_phi ↔ Holds D I (Function.updateITE V h2_x a) M E h2_phi'

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
⊢ ∀ (a : D), Holds D I (Function.updateITE V h2_x a) M E h2_phi ↔ Holds D I (Function.updateITE V h2_x a) M E h2_phi'
Tactic:
intro a
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
a : D
⊢ Holds D I (Function.updateITE V h2_x a) M E h2_phi ↔ Holds D I (Function.updateITE V h2_x a) M E h2_phi'

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
h2_x : VarName
h2_phi h2_phi' : Formula
a✝ : IsConv E h2_phi h2_phi'
h2_ih : ∀ (V : Valuation D), Holds D I V M E h2_phi ↔ Holds D I V M E h2_phi'
V : Valuation D
a : D
⊢ Holds D I (Function.updateITE V h2_x a) M E h2_phi ↔ Holds D I (Function.updateITE V h2_x a) M E h2_phi'
Tactic:
exact h2_ih (Function.updateITE V h2_x a)
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)
Tactic:
obtain ⟨σ', a1⟩ := σ.2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)
Tactic:
have s1 : IsMetaVarOrAllDefInEnv E d.F := def_in_well_formed_env_is_meta_var_or_all_def_in_env E d h1 h2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s1 : IsMetaVarOrAllDefInEnv E d.F
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s1 : IsMetaVarOrAllDefInEnv E d.F
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔ Holds D I V M E (sub σ meta_var_ d.F)
Tactic:
simp only [← holds_sub D I V M E σ σ' meta_var_ d.F s1 a1]
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s1 : IsMetaVarOrAllDefInEnv E d.F
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s1 : IsMetaVarOrAllDefInEnv E d.F
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
clear s1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
have s2 : d.name = d.name ∧ (List.map σ.val d.args).length = d.args.length
State after:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length

case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s2 : d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length

case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s2 : d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
simp
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s2 : d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s2 : d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length
⊢ Holds D I V M E (def_ d.name (List.map (↑σ) d.args)) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
simp only [← lem_4 D I V M E d d.name (List.map σ.val d.args) h1 h2 s2]
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s2 : d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s2 : d.name = d.name ∧ (List.map (↑σ) d.args).length = d.args.length
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
clear s2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
have s3 : d.F.metaVarSet = ∅ := no_meta_var_imp_meta_var_set_is_empty d.F d.args d.nf
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s3 : d.F.metaVarSet = ∅
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s3 : d.F.metaVarSet = ∅
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (meta_var_ X')) E d.F
Tactic:
simp only [holds_coincide_meta_var_no_meta_var D I (V ∘ σ.val) (fun (X' : MetaVarName) (V' : Valuation D) => Holds D I (V' ∘ σ') M E (meta_var_ X')) M E d.F s3]
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s3 : d.F.metaVarSet = ∅
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔ Holds D I (V ∘ ↑σ) M E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
s3 : d.F.metaVarSet = ∅
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔ Holds D I (V ∘ ↑σ) M E d.F
Tactic:
clear s3
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔ Holds D I (V ∘ ↑σ) M E d.F

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I (Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args))) M E d.F ↔ Holds D I (V ∘ ↑σ) M E d.F
Tactic:
apply holds_coincide_var D I (Function.updateListITE V d.args (List.map V (List.map σ.val d.args))) (V ∘ σ.val) M E d.F d.args d.nf
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∀ v ∈ d.args, Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args)) v = (V ∘ ↑σ) v

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ ∀ v ∈ d.args, Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args)) v = (V ∘ ↑σ) v
Tactic:
intro v a2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
v : VarName
a2 : v ∈ d.args
⊢ Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args)) v = (V ∘ ↑σ) v

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
v : VarName
a2 : v ∈ d.args
⊢ Function.updateListITE V d.args (List.map V (List.map (↑σ) d.args)) v = (V ∘ ↑σ) v
Tactic:
simp
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
v : VarName
a2 : v ∈ d.args
⊢ Function.updateListITE V d.args (List.map (V ∘ ↑σ) d.args) v = V (↑σ v)

State before:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
F F' : Formula
h1 : E.WellFormed
d : Definition
σ : Instantiation
h2 : d ∈ E
V : Valuation D
σ' : VarName → VarName
a1 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
v : VarName
a2 : v ∈ d.args
⊢ Function.updateListITE V d.args (List.map (V ∘ ↑σ) d.args) v = V (↑σ v)
Tactic:
exact Function.updateListITE_map_mem V (V ∘ σ.val) d.args v a2
State after:
no goals