internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
have : ℕ ⊧ₘ* trueArithWithStarUnbounded c := by
  simp[trueArithWithStarUnbounded, models_iff]; exact this
Proof state after:
c : ℕ
this✝⁶ : Structure Language.unit ℕ := modelStar c
this✝⁵ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝⁴ : Structure.One ℒₒᵣ⋆ ℕ
this✝³ : Structure.Add ℒₒᵣ⋆ ℕ
this✝² : Structure.Eq ℒₒᵣ⋆ ℕ
this✝¹ : Structure.LT ℒₒᵣ⋆ ℕ
this✝ : ℕ ⊧ₘ* starUnbounded c
this : ℕ ⊧ₘ* trueArithWithStarUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁶ : Structure Language.unit ℕ := modelStar c
this✝⁵ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝⁴ : Structure.One ℒₒᵣ⋆ ℕ
this✝³ : Structure.Add ℒₒᵣ⋆ ℕ
this✝² : Structure.Eq ℒₒᵣ⋆ ℕ
this✝¹ : Structure.LT ℒₒᵣ⋆ ℕ
this✝ : ℕ ⊧ₘ* starUnbounded c
this : ℕ ⊧ₘ* trueArithWithStarUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)
Tactic:
exact satisfiable_intro ℕ this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ℕ ⊧ₘ* starUnbounded c
Tactic:
simp [starUnbounded, models_iff]
Proof state after:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ∀ (i : Fin c), ↑i < Semiterm.Operator.val Semiterm.Operator.Star.star ![]
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ∀ (i : Fin c), ↑i < Semiterm.Operator.val Semiterm.Operator.Star.star ![]
Tactic:
exact Fin.prop
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ ℕ ⊧ₘ* trueArithWithStarUnbounded c
Tactic:
simp[trueArithWithStarUnbounded, models_iff]
Proof state after:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ (Structure.add ℒₒᵣ Language.unit ℕ).toStruc ⊧* starUnbounded c
Theorem: LO.FirstOrder.Arith.satisfiable_trueArithWithStarUnbounded
Proof state before:
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ (Structure.add ℒₒᵣ Language.unit ℕ).toStruc ⊧* starUnbounded c
Tactic:
exact this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Nonstandard.star_unbounded
Proof state before:
n : ℕ
⊢ ↑n < ⋆
Tactic:
have : ℕ⋆ ⊧ₘ (“!!(Semiterm.Operator.numeral ℒₒᵣ⋆ n) < ⋆” : Sentence ℒₒᵣ⋆) :=
  models_union_trueArithWithStarUnbounded.realize
    (Set.mem_iUnion_of_mem (n + 1) (Set.mem_union_right _ $ Set.mem_range_self $ Fin.last n))
Proof state after:
n : ℕ
this :
  ℕ⋆ ⊧ₘ
    (“!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ n)) <
        !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”)
⊢ ↑n < ⋆
Theorem: LO.FirstOrder.Arith.Nonstandard.star_unbounded
Proof state before:
n : ℕ
this :
  ℕ⋆ ⊧ₘ
    (“!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ n)) <
        !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”)
⊢ ↑n < ⋆
Tactic:
simpa [models_iff, Model.numeral_eq_natCast] using this
Proof state after:
no goals
Theorem: Classical.choose!_eq_iff
Proof state before:
α : Sort u_1
p : α → Prop
h : ∃! x, p x
x : α
⊢ x = choose! h → p x
Tactic:
rintro rfl
Proof state after:
α : Sort u_1
p : α → Prop
h : ∃! x, p x
⊢ p (choose! h)
Theorem: Classical.choose!_eq_iff
Proof state before:
α : Sort u_1
p : α → Prop
h : ∃! x, p x
⊢ p (choose! h)
Tactic:
exact choose!_spec h
Proof state after:
no goals
Theorem: LO.FirstOrder.not_fvar?_newVar
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
p : SyntacticFormula L
Γ : Sequent L
h : p ∈ Γ
⊢ upper p ≤ newVar Γ
Tactic:
simpa[newVar] using List.le_max_of_le (List.mem_map_of_mem _ h) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.not_fvar?_newVar
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
p : SyntacticFormula L
Γ : Sequent L
h : p ∈ Γ
⊢ upper p ≤ upper p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bShifts_zero
Proof state before:
L : Language
μ : Type v
t : UTerm L μ
⊢ bShifts 0 t = t
Tactic:
simp[bShifts]
Proof state after:
L : Language
μ : Type v
t : UTerm L μ
⊢ bind (fun x => bvar x) fvar t = t
Theorem: LO.FirstOrder.UTerm.bShifts_zero
Proof state before:
L : Language
μ : Type v
t : UTerm L μ
⊢ bind (fun x => bvar x) fvar t = t
Tactic:
induction t <;> simp[bind, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
μ₃ : Type u_3
t : UTerm L μ₁
b₁ : ℕ → UTerm L μ₂
e₁ : μ₁ → UTerm L μ₂
b₂ : ℕ → UTerm L μ₃
e₂ : μ₂ → UTerm L μ₃
⊢ bind b₂ e₂ (bind b₁ e₁ t) = bind (fun x => bind b₂ e₂ (b₁ x)) (fun x => bind b₂ e₂ (e₁ x)) t
Tactic:
induction t <;> simp[bind, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bShifts_bShifts
Proof state before:
L : Language
μ : Type v
t : UTerm L μ
m₁ m₂ : ℕ
⊢ bShifts m₂ (bShifts m₁ t) = bShifts (m₁ + m₂) t
Tactic:
simp[bShifts, bind_bind, bind, add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.substAt_bvar
Proof state before:
L : Language
μ : Type v
z : ℕ
u : UTerm L μ
⊢ substAt z u (bvar z) = u
Tactic:
simp[substLast, substAt, bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.substAt_bvar_fin
Proof state before:
L : Language
μ : Type v
z : ℕ
u : UTerm L μ
x : Fin z
⊢ substAt z u (bvar ↑x) = bvar ↑x
Tactic:
simp[substLast, substAt, bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.substAt_fvar
Proof state before:
L : Language
μ : Type v
x : μ
z : ℕ
u : UTerm L μ
⊢ substAt z u (fvar x) = fvar x
Tactic:
simp[substLast, substAt, bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.substAt_func
Proof state before:
L : Language
μ : Type v
z : ℕ
u : UTerm L μ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ
⊢ substAt z u (func f v) = func f fun i => substAt z u (v i)
Tactic:
simp[substLast, substAt, bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
hb : ∀ x < t.bv, (b x).bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
⊢ (bind b e t).bv ≤ m
Tactic:
induction t
Proof state after:
case bvar
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (bvar a✝)).bv ≤ m

case fvar
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (fvar a✝)).bv ≤ m

case func
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ₁
a_ih✝ : ∀ (a : Fin arity✝), (∀ x < (a✝ a).bv, (b x).bv ≤ m) → (bind b e (a✝ a)).bv ≤ m
hb : ∀ x < (func a✝¹ a✝).bv, (b x).bv ≤ m
⊢ (bind b e (func a✝¹ a✝)).bv ≤ m
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (bvar a✝)).bv ≤ m
Tactic:
case bvar => simp[bind, bv] at hb ⊢; exact hb _ (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (fvar a✝)).bv ≤ m
Tactic:
case fvar => simp[bind, bv] at he ⊢; exact he _
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ (bind b e (func f v)).bv ≤ m
Tactic:
case func k f v ih =>
  simp[bind, bv]; intro i; exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (bvar a✝)).bv ≤ m
Tactic:
simp[bind, bv] at hb ⊢
Proof state after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < a✝ + 1, (b x).bv ≤ m
⊢ (b a✝).bv ≤ m
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < a✝ + 1, (b x).bv ≤ m
⊢ (b a✝).bv ≤ m
Tactic:
exact hb _ (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (fvar a✝)).bv ≤ m
Tactic:
simp[bind, bv] at he ⊢
Proof state after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (e a✝).bv ≤ m
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (e a✝).bv ≤ m
Tactic:
exact he _
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ (bind b e (func f v)).bv ≤ m
Tactic:
simp[bind, bv]
Proof state after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ ∀ (b_1 : Fin k), (bind b e (v b_1)).bv ≤ m
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ ∀ (b_1 : Fin k), (bind b e (v b_1)).bv ≤ m
Tactic:
intro i
Proof state after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
⊢ (bind b e (v i)).bv ≤ m
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
⊢ (bind b e (v i)).bv ≤ m
Tactic:
exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (func f v).bv
Tactic:
simp[bv]
Proof state after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Theorem: LO.FirstOrder.UTerm.bv_bind
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
t : UTerm L μ₁
hb : ∀ x < t.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind b₁ e₁ t = bind b₂ e₂ t
Tactic:
induction t <;> simp[bind, he]
Proof state after:
case bvar
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, b₁ x = b₂ x
⊢ b₁ a✝ = b₂ a✝

case func
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ₁
a_ih✝ : ∀ (a : Fin arity✝), (∀ x < (a✝ a).bv, b₁ x = b₂ x) → bind b₁ e₁ (a✝ a) = bind b₂ e₂ (a✝ a)
hb : ∀ x < (func a✝¹ a✝).bv, b₁ x = b₂ x
⊢ (fun i => bind b₁ e₁ (a✝ i)) = fun i => bind b₂ e₂ (a✝ i)
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hb : ∀ x_1 < (bvar x).bv, b₁ x_1 = b₂ x_1
⊢ b₁ x = b₂ x
Tactic:
case bvar x => exact hb x (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
⊢ (fun i => bind b₁ e₁ (v i)) = fun i => bind b₂ e₂ (v i)
Tactic:
case func k f v ih => funext i; exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hb : ∀ x_1 < (bvar x).bv, b₁ x_1 = b₂ x_1
⊢ b₁ x = b₂ x
Tactic:
exact hb x (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hb : ∀ x_1 < (bvar x).bv, b₁ x_1 = b₂ x_1
⊢ x < (bvar x).bv
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
⊢ (fun i => bind b₁ e₁ (v i)) = fun i => bind b₂ e₂ (v i)
Tactic:
funext i
Proof state after:
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
⊢ bind b₁ e₁ (v i) = bind b₂ e₂ (v i)
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
⊢ bind b₁ e₁ (v i) = bind b₂ e₂ (v i)
Tactic:
exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (func f v).bv
Tactic:
simp[bv]
Proof state after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Theorem: LO.FirstOrder.UTerm.bind_eq_bind_of_eq
Proof state before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_rewrite
Proof state before:
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ (bvar x).bv ≤ m
Tactic:
simp
Proof state after:
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ x + 1 ≤ m
Theorem: LO.FirstOrder.UTerm.bv_rewrite
Proof state before:
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ x + 1 ≤ m
Tactic:
exact lt_of_lt_of_le hx ht
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
have : x < (bv t).pred ∨ x = (bv t).pred ∨ x > (bv t).pred := Nat.lt_trichotomy _ _
Proof state after:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
this : x < t.bv.pred ∨ x = t.bv.pred ∨ x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
this : x < t.bv.pred ∨ x = t.bv.pred ∨ x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
rcases this with (lt | rfl | lt)
Proof state after:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n

case inr.inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
hx : t.bv.pred < t.bv
⊢ (if t.bv.pred < t.bv.pred then bvar t.bv.pred else if t.bv.pred = t.bv.pred then u else bvar t.bv.pred.pred).bv ≤ n

case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
have : x < n := by simpa using lt_of_lt_of_le lt (Nat.pred_le_pred ht)
Proof state after:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
simp only [lt, ↓reduceIte, bv_bvar, ge_iff_le]
Proof state after:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ x + 1 ≤ n
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ x + 1 ≤ n
Tactic:
exact this
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
⊢ x < n
Tactic:
simpa using lt_of_lt_of_le lt (Nat.pred_le_pred ht)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inr.inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
hx : t.bv.pred < t.bv
⊢ (if t.bv.pred < t.bv.pred then bvar t.bv.pred else if t.bv.pred = t.bv.pred then u else bvar t.bv.pred.pred).bv ≤ n
Tactic:
simp [hu]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
Tactic:
simp [Nat.lt_asymm lt, Nat.ne_of_gt lt]
Proof state after:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n