internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiterm.Operator.foldr_primrec
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this✝ : Primrec₂ fun x p => f.comp ![p.2, p.1]
this : Primrec fun a => List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id a)
l : List (Operator L k)
⊢ List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id l) = f.foldr z l
Tactic:
induction l <;> simp[foldr, *] at*
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_primrec
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
⊢ Primrec (numeral L)
Tactic:
have : Primrec₂ (fun _ n => Add.add.foldr One.one (List.replicate n One.one) : ℕ → ℕ → Const L) :=
  (foldr_primrec _ _).comp₂ (list_replicate.comp₂ .right (.const _))
Proof state after:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_primrec
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)
Tactic:
have := Primrec.nat_casesOn Primrec.id (.const Zero.zero) this
Proof state after:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_primrec
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)
Tactic:
exact this.of_eq <| by
  intro n; induction n <;> simp[numeral, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_primrec
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ ∀ (n : ℕ), (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n
Tactic:
intro n
Proof state after:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
n : ℕ
⊢ (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_primrec
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝⁹ : Primcodable α
inst✝⁸ : Primcodable μ
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝⁵ : Primcodable μ₁
inst✝⁴ : Primcodable μ₂
inst✝³ : Primcodable σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
n : ℕ
⊢ (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n
Tactic:
induction n <;> simp[numeral, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Positive.bvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
x : Fin (n + 1)
⊢ (#x).Positive ↔ 0 < x
Tactic:
simp[Positive]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Positive.fvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
x : ξ
⊢ (&x).Positive
Tactic:
simp[Positive]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Positive.func
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (func f v).Positive ↔ ∀ (i : Fin k), (v i).Positive
Tactic:
simp[Positive, bv]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (∀ (x : Fin (n + 1)) (x_1 : Fin k), x ∈ (v x_1).bv → 0 < x) ↔ ∀ (i : Fin k), ∀ x ∈ (v i).bv, 0 < x
Theorem: LO.FirstOrder.Semiterm.Positive.func
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (∀ (x : Fin (n + 1)) (x_1 : Fin k), x ∈ (v x_1).bv → 0 < x) ↔ ∀ (i : Fin k), ∀ x ∈ (v i).bv, 0 < x
Tactic:
rw [forall_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.bv_eq_empty_of_positive
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
t : Semiterm L ξ 1
ht : t.Positive
⊢ ∀ (x : Fin 1), x ∉ t.bv
Tactic:
simp [Positive, Fin.eq_zero] at ht ⊢
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
t : Semiterm L ξ 1
ht : 0 ∉ t.bv
⊢ 0 ∉ t.bv
Theorem: LO.FirstOrder.Semiterm.bv_eq_empty_of_positive
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
t : Semiterm L ξ 1
ht : 0 ∉ t.bv
⊢ 0 ∉ t.bv
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_func_lt
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
i : Fin k
⊢ (v i).complexity < (func f v).complexity
Tactic:
simp [complexity_func, Nat.lt_add_one_iff]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
i : Fin k
⊢ (v i).complexity ≤ Finset.univ.sup fun i => (v i).complexity
Theorem: LO.FirstOrder.Semiterm.complexity_func_lt
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
i : Fin k
⊢ (v i).complexity ≤ Finset.univ.sup fun i => (v i).complexity
Tactic:
exact Finset.le_sup (f := fun i ↦ complexity (v i)) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_func_lt
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
i : Fin k
⊢ i ∈ Finset.univ
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.mem_fvarList_func
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
x : ξ
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
⊢ x ∈ (func f v).fvarList ↔ ∃ i, x ∈ (v i).fvarList
Tactic:
simp[fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_empty
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
o : Type u_6
e : IsEmpty o
t : Semiterm L o n
⊢ t.fvarList = []
Tactic:
induction t <;> simp[List.eq_nil_iff_forall_not_mem]
Proof state after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
o : Type u_6
e : IsEmpty o
a✝ : o
⊢ False
Theorem: LO.FirstOrder.Semiterm.fvarList_empty
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
o : Type u_6
e : IsEmpty o
x : o
⊢ False
Tactic:
case fvar x => exact IsEmpty.elim e x
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_empty
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
o : Type u_6
e : IsEmpty o
x : o
⊢ False
Tactic:
exact IsEmpty.elim e x
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_to_finset
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
t : Semiterm L ξ n
⊢ t.fvarList.toFinset = t.fv
Tactic:
induction t <;> try simp [fvarList, fv_func]
Proof state after:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
a_ih✝ : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
⊢ (Matrix.toList fun i => (a✝ i).fvarList).join.toFinset = Finset.univ.biUnion fun i => (a✝ i).fv
Theorem: LO.FirstOrder.Semiterm.fvarList_to_finset
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
ih : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
⊢ (Matrix.toList fun i => (a✝ i).fvarList).join.toFinset = Finset.univ.biUnion fun i => (a✝ i).fv
Tactic:
case func ih => ext x; simp [←ih]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_to_finset
Proof state before:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
a_ih✝ : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
⊢ (func a✝¹ a✝).fvarList.toFinset = (func a✝¹ a✝).fv
Tactic:
simp [fvarList, fv_func]
Proof state after:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
a_ih✝ : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
⊢ (Matrix.toList fun i => (a✝ i).fvarList).join.toFinset = Finset.univ.biUnion fun i => (a✝ i).fv
Theorem: LO.FirstOrder.Semiterm.fvarList_to_finset
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
ih : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
⊢ (Matrix.toList fun i => (a✝ i).fvarList).join.toFinset = Finset.univ.biUnion fun i => (a✝ i).fv
Tactic:
ext x
Proof state after:
case a
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
ih : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
x : ξ
⊢ x ∈ (Matrix.toList fun i => (a✝ i).fvarList).join.toFinset ↔ x ∈ Finset.univ.biUnion fun i => (a✝ i).fv
Theorem: LO.FirstOrder.Semiterm.fvarList_to_finset
Proof state before:
case a
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝¹ inst✝ : DecidableEq ξ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
ih : ∀ (a : Fin arity✝), (a✝ a).fvarList.toFinset = (a✝ a).fv
x : ξ
⊢ x ∈ (Matrix.toList fun i => (a✝ i).fvarList).join.toFinset ↔ x ∈ Finset.univ.biUnion fun i => (a✝ i).fv
Tactic:
simp [←ih]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_positive
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
Φ : L₁ →ᵥ L₂
t : Semiterm L₁ ξ (n + 1)
⊢ (lMap Φ t).Positive ↔ t.Positive
Tactic:
induction t <;> simp [lMap_func, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_lMap
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝ : DecidableEq ξ
Φ✝ Φ : L₁ →ᵥ L₂
t : Semiterm L₁ ξ n
⊢ (lMap Φ t).fvarList = t.fvarList
Tactic:
induction t <;> simp [fvarList, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvEnumInv_fvEnum
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝² inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
t : Semiterm L ξ n
x : ξ
hx : x ∈ t.fvarList
⊢ t.fvEnumInv (t.fvEnum x) = x
Tactic:
simp [fvEnumInv, fvEnum]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝² inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
t : Semiterm L ξ n
x : ξ
hx : x ∈ t.fvarList
⊢ t.fvarList.length ≤ List.indexOf x t.fvarList → default = x
Theorem: LO.FirstOrder.Semiterm.fvEnumInv_fvEnum
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝² inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
t : Semiterm L ξ n
x : ξ
hx : x ∈ t.fvarList
⊢ t.fvarList.length ≤ List.indexOf x t.fvarList → default = x
Tactic:
intro h
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝² inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
t : Semiterm L ξ n
x : ξ
hx : x ∈ t.fvarList
h : t.fvarList.length ≤ List.indexOf x t.fvarList
⊢ default = x
Theorem: LO.FirstOrder.Semiterm.fvEnumInv_fvEnum
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
inst✝² inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
t : Semiterm L ξ n
x : ξ
hx : x ∈ t.fvarList
h : t.fvarList.length ≤ List.indexOf x t.fvarList
⊢ default = x
Tactic:
exact False.elim <| not_le.mpr (List.indexOf_lt_length.mpr $ hx) h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
⊢ (L)-Consistent Ax(L)
Tactic:
intro Γ hΓ
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
obtain ⟨q, hq⟩ := h.exists_unprovable
Proof state after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
q : Formula α
hq : L ⊬! q
⊢ L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.self_ParametricConsistent
Proof state before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
q : Formula α
hq : L ⊬! q
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
Proof state after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
q : Formula α
hq : L ⊬! q
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Theorem: LO.Modal.Standard.Theory.self_ParametricConsistent
Proof state before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
q : Formula α
hq : L ⊬! q
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! q := imp_trans! hC efq! ⨀ (iff_provable_list_conj.mpr $ λ _ h => ⟨Deduction.maxm $ hΓ _ h⟩)
Proof state after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
q : Formula α
hq : L ⊬! q
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! q
⊢ False
Theorem: LO.Modal.Standard.Theory.self_ParametricConsistent
Proof state before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
h : Consistent L
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ Ax(L)
q : Formula α
hq : L ⊬! q
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! q
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.def_not_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
⊢ ¬(L)-Consistent T ↔ ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
simp [ParametricConsistent]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (L)-Consistent (T₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂
Tactic:
simp only [ParametricConsistent]
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥) →
    (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
      ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥) →
    (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
      ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
    ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
    ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent
Proof state before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
. intro Γ hΓ; exact h (by intro p hp; simp; left; exact hΓ p hp);
Proof state after:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥