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

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
name : DefName
args : List VarName
h1 : Holds D I V M E (def_ name args)
⊢ ∃ d ∈ E, name = d.name ∧ args.length = d.args.length
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length

case cons
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I V M tail✝ (def_ name args) → ∃ d ∈ tail✝, name = d.name ∧ args.length = d.args.length
h1 : Holds D I V M (head✝ :: tail✝) (def_ name args)
⊢ ∃ d ∈ head✝ :: tail✝, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length
Tactic:
case nil =>
  simp only [Holds] at h1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
h1 : Holds D I V M [] (def_ name args)
⊢ ∃ d ∈ [], name = d.name ∧ args.length = d.args.length
Tactic:
simp only [Holds] at h1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 : Holds D I V M (E_hd :: E_tl) (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
simp only [Holds] at h1
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 :
  if name = E_hd.name ∧ args.length = E_hd.args.length then
    Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
  else Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 :
  if name = E_hd.name ∧ args.length = E_hd.args.length then
    Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
  else Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
split_ifs at h1
State after:
case pos
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h✝ : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

case neg
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h✝ : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
case _ c1 =>
  apply Exists.intro E_hd
  simp
  exact c1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
apply Exists.intro E_hd
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ E_hd ∈ E_hd :: E_tl ∧ name = E_hd.name ∧ args.length = E_hd.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ E_hd ∈ E_hd :: E_tl ∧ name = E_hd.name ∧ args.length = E_hd.args.length
Tactic:
simp
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ name = E_hd.name ∧ args.length = E_hd.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : name = E_hd.name ∧ args.length = E_hd.args.length
h1 : Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
⊢ name = E_hd.name ∧ args.length = E_hd.args.length
Tactic:
exact c1
State after:
no goals

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
specialize E_ih h1
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
apply Exists.elim E_ih
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∀ (a : Definition),
    a ∈ E_tl ∧ name = a.name ∧ args.length = a.args.length →
      ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
⊢ ∀ (a : Definition),
    a ∈ E_tl ∧ name = a.name ∧ args.length = a.args.length →
      ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
intro d E_ih_1
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1 : d ∈ E_tl ∧ name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1 : d ∈ E_tl ∧ name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
cases E_ih_1
State after:
case intro
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
left✝ : d ∈ E_tl
right✝ : name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
Tactic:
apply Exists.intro d
State after:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl ∧ name = d.name ∧ args.length = d.args.length

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl ∧ name = d.name ∧ args.length = d.args.length
Tactic:
constructor
State after:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl

case right
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ name = d.name ∧ args.length = d.args.length

State before:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_hd :: E_tl
Tactic:
simp
State after:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d = E_hd ∨ d ∈ E_tl

State before:
case left
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d = E_hd ∨ d ∈ E_tl
Tactic:
right
State after:
case left.h
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_tl

State before:
case left.h
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ d ∈ E_tl
Tactic:
exact E_ih_1_left
State after:
no goals

State before:
case right
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
c1 : ¬(name = E_hd.name ∧ args.length = E_hd.args.length)
h1 : Holds D I V M E_tl (def_ name args)
E_ih : ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
d : Definition
E_ih_1_left : d ∈ E_tl
E_ih_1_right : name = d.name ∧ args.length = d.args.length
⊢ name = d.name ∧ args.length = d.args.length
Tactic:
exact E_ih_1_right
State after:
no goals