internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ 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 ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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 (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp at h3
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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 (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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 (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
cases h2_1
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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)
left✝ : a ∈ E
right✝ : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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)
h2_1_left : a ∈ E
h2_1_right : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
cases h2_1_right
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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)
h2_1_left : a ∈ E
left✝ : X = a.name
right✝ : xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V 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)
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
cases h3
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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 (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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 (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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 (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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 (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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)) (E1_tl ++ E) E1_hd.q
    else Holds D I V (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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)) (E1_tl ++ E) E1_hd.q
    else Holds D I V (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V E (def_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)

case neg
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
case _ c1 =>
  exact E1_ih h3_right
Proof state after:
no goals
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)
Tactic:
cases c1
Proof state after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)
Tactic:
exfalso
Proof state after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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: FOL.NV.Holds_coincide_Env
Proof state before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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: FOL.NV.Holds_coincide_Env
Proof state before:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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: FOL.NV.Holds_coincide_Env
Proof state before:
case a.h
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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: FOL.NV.Holds_coincide_Env
Proof state before:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a 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 (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
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:
subst c1_left
Proof state after:
case a
D : Type
I : Interpretation D
E : Env
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
h2_1_left : a ∈ E
h2_1_right_right : xs.length = a.args.length
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_right : xs.length = E1_hd.args.length
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 (E1_tl ++ E) (def_ E1_hd.name xs) ↔ Holds D I V E (def_ E1_hd.name xs))
h2_1_right_left : E1_hd.name = a.name
⊢ E1_hd.name = a.name
Theorem: FOL.NV.Holds_coincide_Env
Proof state before:
case a
D : Type
I : Interpretation D
E : Env
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
h2_1_left : a ∈ E
h2_1_right_right : xs.length = a.args.length
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_right : xs.length = E1_hd.args.length
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 (E1_tl ++ E) (def_ E1_hd.name xs) ↔ Holds D I V E (def_ E1_hd.name xs))
h2_1_right_left : E1_hd.name = a.name
⊢ E1_hd.name = a.name
Tactic:
exact h2_1_right_left
Proof state after:
no goals