internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1 ++ E)
⊢ Holds D I V M (E1 ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
induction E1
Proof state after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V M ([] ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

case cons
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (tail✝ ++ E) →
    (Holds D I V M (tail✝ ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (head✝ :: tail✝ ++ E)
⊢ Holds D I V M (head✝ :: tail✝ ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V M ([] ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V M ([] ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_hd :: E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp at h3
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
cases h3
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
left✝ : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
right✝ : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V M (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ (if X = E1_hd.name ∧ xs.length = E1_hd.args.length then
      Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) M (E1_tl ++ E) E1_hd.F
    else Holds D I V M (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ (if X = E1_hd.name ∧ xs.length = E1_hd.args.length then
      Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) M (E1_tl ++ E) E1_hd.F
    else Holds D I V M (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V M E (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h✝ : X = E1_hd.name ∧ xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)

case neg
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h✝ : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
case _ c1 =>
  exact E1_ih h3_right
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : X = E1_hd.name ∧ xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)
Tactic:
cases c1
Proof state after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
left✝ : X = E1_hd.name
right✝ : xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)
Tactic:
exfalso
Proof state after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ False
Theorem: MM0.holds_coincide_env
Proof state before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ False
Tactic:
apply h3_left a
Proof state after:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E1_tl ∨ a ∈ E

case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = a.name

case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = a.args.length
Theorem: MM0.holds_coincide_env
Proof state before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E1_tl ∨ a ∈ E
Tactic:
right
Proof state after:
case a.h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E
Theorem: MM0.holds_coincide_env
Proof state before:
case a.h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E
Tactic:
exact h2_1_left
Proof state after:
no goals
Theorem: MM0.holds_coincide_env
Proof state before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = a.name
Tactic:
simp only [← h2_1_right_left]
Proof state after:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = X
Theorem: MM0.holds_coincide_env
Proof state before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = X
Tactic:
simp only [c1_left]
Proof state after:
no goals