internlm/Lean-Github huggingface dataset:
Theorem: MM0.lem_4
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
ih :
  Env.WellFormed tl →
    d ∈ tl →
      (Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args))
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
specialize ih h1_right_right c2
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Theorem: MM0.lem_4
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔ Holds D I V M tl (def_ name args)
Tactic:
simp only [← ih]
Proof state after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F
Theorem: MM0.lem_4
Proof state before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Holds D I (Function.updateListITE V d.args (List.map V args)) M (hd :: tl) d.F ↔
    Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F
Tactic:
apply holds_coincide_env D I (Function.updateListITE V d.args (List.map V args)) M tl (hd :: tl) d.F s2
Proof state after:
case h2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)
Theorem: MM0.lem_4
Proof state before:
case h2
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ IsMetaVarOrAllDefInEnv tl d.F

case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)
Tactic:
apply def_in_well_formed_env_is_meta_var_or_all_def_in_env tl d h1_right_right c2
Proof state after:
case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)
Theorem: MM0.lem_4
Proof state before:
case h3
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
d : Definition
name : DefName
args : List VarName
h3 : name = d.name ∧ args.length = d.args.length
hd : Definition
tl : List Definition
s1 : Env.Nodup (hd :: tl)
s2 : ∃ E1, hd :: tl = E1 ++ tl
h1_left : ∀ d' ∈ tl, hd.name = d'.name → hd.args.length = d'.args.length → False
h1_right_left : IsMetaVarOrAllDefInEnv tl hd.F
h1_right_right : Env.WellFormed tl
c1 : ¬(name = hd.name ∧ args.length = hd.args.length)
c2 : d ∈ tl
ih : Holds D I (Function.updateListITE V d.args (List.map V args)) M tl d.F ↔ Holds D I V M tl (def_ name args)
⊢ Env.Nodup (hd :: tl)
Tactic:
exact s1
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof 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)
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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)
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof 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'
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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'
Proof 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''
Theorem: MM0.holds_conv
Proof 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
Proof 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''
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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]
Proof 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'
Theorem: MM0.holds_conv
Proof 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
Proof 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'
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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]
Proof 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'
Theorem: MM0.holds_conv
Proof 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
Proof 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'
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals