internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bind_eq_bind
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func f v))) =
    UTerm.func f fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (v i))
Tactic:
case func k f v ih =>
  simp[Rew.func]
  funext i; simp[ih]; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bind_eq_bind
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func f v))) =
    UTerm.func f fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (v i))
Tactic:
simp[Rew.func]
Proof state after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ (fun i => ↑(subtEquiv ((Rew.bind b e) (v i)))) = fun i =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bind_eq_bind
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ (fun i => ↑(subtEquiv ((Rew.bind b e) (v i)))) = fun i =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Tactic:
funext i
Proof state after:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ ↑(subtEquiv ((Rew.bind b e) (v i))) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bind_eq_bind
Proof state before:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ ↑(subtEquiv ((Rew.bind b e) (v i))) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Tactic:
simp[ih]
Proof state after:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subtEquiv (v i)) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bind_eq_bind
Proof state before:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subtEquiv (v i)) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.bv_subtEquiv
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
t : Semiterm L μ n
⊢ (↑(subtEquiv t)).bv ≤ n
Tactic:
induction t <;> simp [UTerm.bv]
Proof state after:
case bvar
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
a✝ : Fin n
⊢ ↑a✝ + 1 ≤ n
Theorem: LO.FirstOrder.Semiterm.bv_subtEquiv
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
x : Fin n
⊢ ↑x + 1 ≤ n
Tactic:
case bvar x => exact x.prop
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.bv_subtEquiv
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
x : Fin n
⊢ ↑x + 1 ≤ n
Tactic:
exact x.prop
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ↑(subtEquiv (Rew.bShift t)) = bShifts 1 ↑(subtEquiv t)
Tactic:
rw[Rew.eq_bind Rew.bShift, subtEquiv_bind_eq_bind]
Proof state after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if hx : x < k then ↑(subtEquiv ((⇑Rew.bShift ∘ bvar) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv ((⇑Rew.bShift ∘ fvar) x))) ↑(subtEquiv t) =
    bShifts 1 ↑(subtEquiv t)
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if hx : x < k then ↑(subtEquiv ((⇑Rew.bShift ∘ bvar) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv ((⇑Rew.bShift ∘ fvar) x))) ↑(subtEquiv t) =
    bShifts 1 ↑(subtEquiv t)
Tactic:
simp[bShifts]
Proof state after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if x < k then UTerm.bvar (x + 1) else default) (fun x => UTerm.fvar x) ↑(subtEquiv t) =
    UTerm.bind (fun x => UTerm.bvar (x + 1)) UTerm.fvar ↑(subtEquiv t)
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift
Proof state before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if x < k then UTerm.bvar (x + 1) else default) (fun x => UTerm.fvar x) ↑(subtEquiv t) =
    UTerm.bind (fun x => UTerm.bvar (x + 1)) UTerm.fvar ↑(subtEquiv t)
Tactic:
apply bind_eq_bind_of_eq
Proof state after:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ x < (↑(subtEquiv t)).bv, (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)

case he
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ (x : μ), UTerm.fvar x = UTerm.fvar x
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift
Proof state before:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ x < (↑(subtEquiv t)).bv, (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)
Tactic:
intro x hx
Proof state after:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
x : ℕ
hx : x < (↑(subtEquiv t)).bv
⊢ (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift
Proof state before:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
x : ℕ
hx : x < (↑(subtEquiv t)).bv
⊢ (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)
Tactic:
simp[lt_of_lt_of_le hx (bv_subtEquiv t)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift
Proof state before:
case he
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ (x : μ), UTerm.fvar x = UTerm.fvar x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.brew_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ₂ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const 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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Theorem: LO.FirstOrder.Semiterm.brew_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Tactic:
have : Primrec₂ (fun z x => (Nat.toFin n₁ x).casesOn default (fun i => (subtEquiv (b z i)).val) : α → ℕ → UTerm L μ₂) :=
  to₂' <| option_casesOn (α := α × ℕ) (nat_toFin.comp snd) (Primrec.const default) <| subtype_val.comp₂ <| of_equiv.comp₂ <|
  to₂' <| finArrow_app (v := fun (p : (α × ℕ) × Fin n₁) => b p.1.1) (hb.comp (fst.comp fst)) snd
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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Theorem: LO.FirstOrder.Semiterm.brew_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
⊢ Primrec₂ fun z x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default
Tactic:
exact this.of_eq <| by
  intro a x; simp[Nat.toFin]
  by_cases hx : x < n₁ <;> simp[hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.brew_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
⊢ ∀ (a : α) (b_1 : ℕ),
    (Option.casesOn (n₁.toFin b_1) default fun i => ↑(subtEquiv (b a i))) =
      if hx : b_1 < n₁ then ↑(subtEquiv (b a ⟨b_1, hx⟩)) else default
Tactic:
intro a x
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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ (Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b a i))) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default
Theorem: LO.FirstOrder.Semiterm.brew_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ (Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b a i))) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default
Tactic:
simp[Nat.toFin]
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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ Option.rec default (fun val => ↑(subtEquiv (b a val))) (if hx : x < n₁ then some ⟨x, hx⟩ else none) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default
Theorem: LO.FirstOrder.Semiterm.brew_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
hb : Primrec b
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun z x => Option.casesOn (n₁.toFin x) default fun i => ↑(subtEquiv (b z i))
a : α
x : ℕ
⊢ Option.rec default (fun val => ↑(subtEquiv (b a val))) (if hx : x < n₁ then some ⟨x, hx⟩ else none) =
    if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default
Tactic:
by_cases hx : x < n₁ <;> simp[hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.bind_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
⊢ Primrec fun x => (Rew.bind (b x) (e x)) (t x)
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ₁ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const 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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)) (t x)
Theorem: LO.FirstOrder.Semiterm.bind_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)) (t x)
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ₂ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const 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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)) (t x)
Theorem: LO.FirstOrder.Semiterm.bind_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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)) (t x)
Tactic:
have : Primrec (fun z =>
    UTerm.bind (fun x => if hx : x < n₁ then subtEquiv (b z ⟨x, hx⟩) else default) (fun x => subtEquiv $ e z x) (subtEquiv $ t z)
    : α → UTerm L μ₂) :=
  UTerm.bind_primrec_param (brew_primrec hb)
    (subtype_val.comp₂ $ of_equiv.comp₂ $ he.comp₂ Primrec₂.left Primrec₂.right)
    (subtype_val.comp $ of_equiv.comp ht)
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 σ
n₁ n₂ : ℕ
b : α → Fin n₁ → Semiterm L μ₂ n₂
e : α → μ₁ → Semiterm L μ₂ n₂
t : α → Semiterm L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
ht : Primrec t
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subtEquiv (t z))
⊢ Primrec fun x => (Rew.bind (b x) (e x)) (t x)