internlm/Lean-Github huggingface dataset:
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:
simp only [Holds]
Proof 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'
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
⊢ (∀ (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'
Proof 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'
Theorem: MM0.holds_conv
Proof 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
Proof 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'
Theorem: MM0.holds_conv
Proof 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)
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:
obtain ⟨σ', a1⟩ := σ.2
Proof 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)
Theorem: MM0.holds_conv
Proof 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
Proof 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)
Theorem: MM0.holds_conv
Proof 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]
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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]
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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]
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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
Theorem: MM0.holds_conv
Proof 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
Proof 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)
Theorem: MM0.holds_conv
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : h1_phi ∈ h1_Δ
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E h1_phi
Tactic:
case hyp h1_Γ h1_Δ h1_phi h1_1 h1_2 =>
  intro V
  exact hyp h1_phi V h1_2
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_2 : IsProof E h1_Γ h1_Δ (h1_phi.imp_ h1_psi)
h1_ih_1 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) →
        ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ h1_psi)
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E h1_psi
Tactic:
case mp h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  simp only [Holds] at h1_ih_2
  intro V
  exact h1_ih_2 M nf hyp V (h1_ih_1 M nf hyp V)
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_1 h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 =>
  simp only [Holds]
  intro V a1 a2
  exact a1
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi h1_chi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
h1_3 : IsMetaVarOrAllDefInEnv E h1_chi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D),
    Holds D I V M E ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
case prop_2 h1_Γ h1_Δ h1_phi h1_psi h1_chi h1_1 h1_2 h1_3 =>
  simp only [Holds]
  intro V a1 a2 a3
  apply a1 a3
  exact a2 a3
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_3 h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 =>
  simp only [Holds]
  intro V a1 a2
  by_contra contra
  exact a1 contra a2
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F) → ∀ (V : Valuation D), Holds D I V M E h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (forall_ h1_x h1_phi)
Tactic:
case gen h1_Γ h1_Δ h1_phi h1_x h1_1 h1_ih =>
  simp only [Holds]
  intro V d
  exact h1_ih M nf hyp (Function.updateITE V h1_x d)
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D),
    Holds D I V M E ((forall_ h1_x (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_x h1_phi).imp_ (forall_ h1_x h1_psi)))
Tactic:
case pred_1 h1_Γ h1_Δ h1_phi h1_psi h1_x h1_1 h1_2 =>
  simp only [Holds]
  intro V a1 a2 d
  apply a1 d
  exact a2 d
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
Tactic:
case pred_2 h1_Γ h1_Δ h1_phi h1_x h1_1 h1_2 =>
  have s1 : IsNotFree D I M E h1_phi h1_x
  apply not_free_imp_is_not_free D I M E h1_phi h1_Γ h1_x h1_2
  exact nf h1_x
  simp only [Holds]
  intro V a1 a
  unfold IsNotFree at s1
  simp only [← s1 V a]
  exact a1
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y : VarName
h1_1 : ¬h1_y = h1_x
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (exists_ h1_x (eq_ h1_x h1_y))
Tactic:
case eq_1 h1_Γ h1_Δ h1_x h1_y h1_1 =>
  unfold exists_
  simp only [Holds]
  simp
  intro V
  apply Exists.intro (V h1_y)
  unfold Function.updateITE
  simp
Proof state after:
no goals
Theorem: MM0.holds_is_proof
Proof state before:
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_n : ℕ
h1_name : PredName
h1_xs h1_ys : Fin h1_n → VarName
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (eqSubPred h1_name h1_n h1_xs h1_ys)
Tactic:
case eq_3 h1_Γ h1_Δ h1_n h1_name h1_xs h1_ys =>
  sorry
Proof state after:
no goals