internlm/Lean-Github huggingface dataset:
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 ⋯
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)
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  intro a
  simp[Encodable.encode_ofEquiv subtEquiv, Encodable.Subtype.encode_eq, subtEquiv_bind_eq_bind]
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
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))
⊢ ∀ (n : α),
    encode
        (UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b n ⟨x, hx⟩)) else default)
          (fun x => ↑(subtEquiv (e n x))) ↑(subtEquiv (t n))) =
      encode ((Rew.bind (b n) (e n)) (t n))
Tactic:
intro a
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))
a : α
⊢ encode
      (UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e a x)))
        ↑(subtEquiv (t a))) =
    encode ((Rew.bind (b a) (e a)) (t a))
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 ⋯
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))
a : α
⊢ encode
      (UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b a ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e a x)))
        ↑(subtEquiv (t a))) =
    encode ((Rew.bind (b a) (e a)) (t a))
Tactic:
simp[Encodable.encode_ofEquiv subtEquiv, Encodable.Subtype.encode_eq, subtEquiv_bind_eq_bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rewrite_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 n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
⊢ Primrec₂ fun v p => (Rew.rewrite v) p
Tactic:
exact this.of_eq <| by intro v p; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rewrite_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 n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
⊢ ∀ (a : Fin k → Semiterm L μ n) (b : Semiterm L (Fin k) n), (Rew.bind (fun x => #x) a) b = (Rew.rewrite a) b
Tactic:
intro v p
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 σ
k n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
v : Fin k → Semiterm L μ n
p : Semiterm L (Fin k) n
⊢ (Rew.bind (fun x => #x) v) p = (Rew.rewrite v) p
Theorem: LO.FirstOrder.Semiterm.rewrite_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 n : ℕ
this : Primrec₂ fun v t => (Rew.bind (fun x => #x) v) t
v : Fin k → Semiterm L μ n
p : Semiterm L (Fin k) n
⊢ (Rew.bind (fun x => #x) v) p = (Rew.rewrite v) p
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.castLE_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₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.castLE h)
Tactic:
rw[Rew.eq_bind (Rew.castLE h)]
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₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (⇑(Rew.castLE h) ∘ bvar) (⇑(Rew.castLE h) ∘ fvar))
Theorem: LO.FirstOrder.Semiterm.castLE_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₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (⇑(Rew.castLE h) ∘ bvar) (⇑(Rew.castLE h) ∘ fvar))
Tactic:
simp[Function.comp]
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₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (fun x => #(Fin.castLE h x)) fun x => &x)
Theorem: LO.FirstOrder.Semiterm.castLE_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₂ : ℕ
h : n₁ ≤ n₂
⊢ Primrec ⇑(Rew.bind (fun x => #(Fin.castLE h x)) fun x => &x)
Tactic:
exact bind_primrec (const _) (Semiterm.fvar_primrec.comp snd) Primrec.id
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.substs_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' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
⊢ Primrec₂ fun v p => (Rew.substs v) p
Tactic:
exact this.of_eq <| by { intro v p; rw[Rew.eq_bind (Rew.substs v)]; simp[Function.comp] }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.substs_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' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
⊢ ∀ (a : Fin n → Semiterm L μ n') (b : Semiterm L μ n), (Rew.bind a fun x => &x) b = (Rew.substs a) b
Tactic:
intro v p
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' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
v : Fin n → Semiterm L μ n'
p : Semiterm L μ n
⊢ (Rew.bind v fun x => &x) p = (Rew.substs v) p
Theorem: LO.FirstOrder.Semiterm.substs_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' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
v : Fin n → Semiterm L μ n'
p : Semiterm L μ n
⊢ (Rew.bind v fun x => &x) p = (Rew.substs v) p
Tactic:
rw[Rew.eq_bind (Rew.substs v)]
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' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
v : Fin n → Semiterm L μ n'
p : Semiterm L μ n
⊢ (Rew.bind v fun x => &x) p = (Rew.bind (⇑(Rew.substs v) ∘ bvar) (⇑(Rew.substs v) ∘ fvar)) p
Theorem: LO.FirstOrder.Semiterm.substs_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' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
v : Fin n → Semiterm L μ n'
p : Semiterm L μ n
⊢ (Rew.bind v fun x => &x) p = (Rew.bind (⇑(Rew.substs v) ∘ bvar) (⇑(Rew.substs v) ∘ fvar)) p
Tactic:
simp[Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.substs₁_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' : ℕ
⊢ ∀ (a : Semiterm L μ n'), Semiterm L μ 1 → encode [a] = encode ![a]
Tactic:
intro 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' : ℕ
x : Semiterm L μ n'
b✝ : Semiterm L μ 1
⊢ encode [x] = encode ![x]
Theorem: LO.FirstOrder.Semiterm.substs₁_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' : ℕ
x : Semiterm L μ n'
b✝ : Semiterm L μ 1
⊢ encode [x] = encode ![x]
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.substs₂_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' : ℕ
⊢ ∀ (a : Semiterm L μ n' × Semiterm L μ n'), Semiterm L μ 2 → encode [a.1, a.2] = encode ![a.1, a.2]
Tactic:
intro 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' : ℕ
x : Semiterm L μ n' × Semiterm L μ n'
b✝ : Semiterm L μ 2
⊢ encode [x.1, x.2] = encode ![x.1, x.2]
Theorem: LO.FirstOrder.Semiterm.substs₂_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' : ℕ
x : Semiterm L μ n' × Semiterm L μ n'
b✝ : Semiterm L μ 2
⊢ encode [x.1, x.2] = encode ![x.1, x.2]
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.emb_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 : ℕ
⊢ Primrec ⇑Rew.emb
Tactic:
rw[Rew.eq_bind Rew.emb]
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 : ℕ
⊢ Primrec ⇑(Rew.bind (⇑Rew.emb ∘ bvar) (⇑Rew.emb ∘ fvar))
Theorem: LO.FirstOrder.Semiterm.emb_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 : ℕ
⊢ Primrec ⇑(Rew.bind (⇑Rew.emb ∘ bvar) (⇑Rew.emb ∘ fvar))
Tactic:
simp[Function.comp]
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 : ℕ
⊢ Primrec ⇑(Rew.bind (fun x => #x) fun x => Rew.emb &x)
Theorem: LO.FirstOrder.Semiterm.emb_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 : ℕ
⊢ Primrec ⇑(Rew.bind (fun x => #x) fun x => Rew.emb &x)
Tactic:
exact bind_primrec (const _)
  (Primrec₂.option_some_iff.mp $ (Primrec₂.const none).of_eq <| by rintro _ ⟨⟩) Primrec.id
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.emb_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 : ℕ
⊢ Semiterm L Empty n → ∀ (b : Empty), none = some (Rew.emb &b)
Tactic:
rintro _ ⟨⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.comp_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 σ
l : ℕ
o : Operator L 2
⊢ Primrec fun a => encode fun x => (![a.1, a.2] x).term
Tactic:
simp[Matrix.comp_vecCons', Matrix.constant_eq_singleton]
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 σ
l : ℕ
o : Operator L 2
⊢ Primrec fun a => encode ![a.1.term, a.2.term]
Theorem: LO.FirstOrder.Semiterm.Operator.comp_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 σ
l : ℕ
o : Operator L 2
⊢ Primrec fun a => encode ![a.1.term, a.2.term]
Tactic:
have : Primrec (fun p : Operator L l × Operator L l => encode [p.1.term, p.2.term]) :=
  Primrec.encode.comp (list_cons.comp (term_primrec.comp fst) $
    list_cons.comp (term_primrec.comp snd) (.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 σ
l : ℕ
o : Operator L 2
this : Primrec fun p => encode [p.1.term, p.2.term]
⊢ Primrec fun a => encode ![a.1.term, a.2.term]
Theorem: LO.FirstOrder.Semiterm.Operator.comp_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 σ
l : ℕ
o : Operator L 2
this : Primrec fun p => encode [p.1.term, p.2.term]
⊢ Primrec fun a => encode ![a.1.term, a.2.term]
Tactic:
exact this.of_eq <| by simp[encode_finArrow]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.comp_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 σ
l : ℕ
o : Operator L 2
this : Primrec fun p => encode [p.1.term, p.2.term]
⊢ ∀ (n : Operator L l × Operator L l), encode [n.1.term, n.2.term] = encode ![n.1.term, n.2.term]
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
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
⊢ Primrec (f.foldr z)
Tactic:
have : Primrec₂ (fun _ p => f.comp ![p.2, p.1] : List (Operator L k) → Operator L k × Operator L k → Operator L k) :=
  by apply (comp_primrec₂ f).comp₂ (Primrec.snd.comp₂ .right) (Primrec.fst.comp₂ .right)
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 σ
k : ℕ
f : Operator L 2
z : Operator L k
this : Primrec₂ fun x p => f.comp ![p.2, p.1]
⊢ Primrec (f.foldr z)
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]
⊢ Primrec (f.foldr z)
Tactic:
have := Primrec.list_foldr Primrec.id (.const z) 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 σ
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)
⊢ Primrec (f.foldr z)
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)
⊢ Primrec (f.foldr z)
Tactic:
exact this.of_eq <| by
  intro l; induction l <;> simp[foldr, *] at*
Proof state after:
no goals
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
⊢ Primrec₂ fun x p => f.comp ![p.2, p.1]
Tactic:
apply (comp_primrec₂ f).comp₂ (Primrec.snd.comp₂ .right) (Primrec.fst.comp₂ .right)
Proof state after:
no goals
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)
⊢ ∀ (n : List (Operator L k)), List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id n) = f.foldr z n
Tactic:
intro l
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 σ
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