internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UTerm.bv_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
t : UTerm L μ
⊢ elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) t = t.bv
Tactic:
induction t <;> simp[elim, bv, *]
Proof state after:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv
Theorem: LO.FirstOrder.UTerm.bv_primrec
Proof state before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv
Tactic:
{ simp[List.sup_ofFn] }
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_primrec
Proof state before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv
Tactic:
simp[List.sup_ofFn]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
⊢ Primrec fun x => bind (b x) (e x) (g x)
Tactic:
have : Primrec₂ (fun _ p => funcL p.1 p.2 : σ → ((k : ℕ) × L.Func k) × List (UTerm L μ₂) → Option (UTerm L μ₂)) :=
  funcL_primrec.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right)
Proof state after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
⊢ Primrec fun x => bind (b x) (e x) (g x)
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
⊢ Primrec fun x => bind (b x) (e x) (g x)
Tactic:
have := elim_primrec_param_opt hb he (fun _ _ f v => func f v) this hg
  (by intro _ k f v; simp[funcL])
Proof state after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ Primrec fun x => bind (b x) (e x) (g x)
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ Primrec fun x => bind (b x) (e x) (g x)
Tactic:
exact this.of_eq <| by intro x; generalize g x = t; induction t <;> simp[elim, bind, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
⊢ ∀ (x : σ) {k : ℕ} (f : L.Func k) (v : Fin k → UTerm L μ₂),
    funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x k f v)
Tactic:
intro _ k f v
Proof state after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
x✝ : σ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₂
⊢ funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x✝ k f v)
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
x✝ : σ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₂
⊢ funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x✝ k f v)
Tactic:
simp[funcL]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ ∀ (n : σ), elim (b n) (e n) (fun {k} => (fun x x f v => func f v) n k) (g n) = bind (b n) (e n) (g n)
Tactic:
intro x
Proof state after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x) = bind (b x) (e x) (g x)
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x) = bind (b x) (e x) (g x)
Tactic:
generalize g x = t
Proof state after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
t : UTerm L μ₁
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) t = bind (b x) (e x) t
Theorem: LO.FirstOrder.UTerm.bind_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
t : UTerm L μ₁
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) t = bind (b x) (e x) t
Tactic:
induction t <;> simp[elim, bind, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvar_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
n : ℕ
this : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
⊢ Primrec fun x => ↑(subtEquiv &x)
Tactic:
simpa using UTerm.fvar_primrec
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.funcL_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
n : ℕ
this : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
⊢ Primrec fun p => ↑(subtEquiv p.2)
Tactic:
apply subtype_val.comp <| of_equiv.comp snd
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.funcL_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
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
⊢ ∀ (a : (k : ℕ) × L.Func k) (b : List (Semiterm L μ n)),
    encode (UTerm.funcL a (List.map (fun x => ↑(subtEquiv x)) b)) = encode (funcL a b)
Tactic:
intro ⟨k, f⟩ 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
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
⊢ encode (UTerm.funcL ⟨k, f⟩ (List.map (fun x => ↑(subtEquiv x)) l)) = encode (funcL ⟨k, f⟩ l)
Theorem: LO.FirstOrder.Semiterm.funcL_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
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
⊢ encode (UTerm.funcL ⟨k, f⟩ (List.map (fun x => ↑(subtEquiv x)) l)) = encode (funcL ⟨k, f⟩ l)
Tactic:
simp[funcL, UTerm.funcL]
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 : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
⊢ encode (if h : l.length = k then some (UTerm.func f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) else none) =
    encode (if h : l.length = k then some (func f fun i => l.get (Fin.cast ⋯ i)) else none)
Theorem: LO.FirstOrder.Semiterm.funcL_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
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
⊢ encode (if h : l.length = k then some (UTerm.func f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) else none) =
    encode (if h : l.length = k then some (func f fun i => l.get (Fin.cast ⋯ i)) else none)
Tactic:
by_cases hl : l.length = k <;> simp[hl]
Proof state after:
case pos
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ encode (UTerm.func f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (func f fun i => l.get (Fin.cast ⋯ i))
Theorem: LO.FirstOrder.Semiterm.funcL_primrec
Proof state before:
case pos
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ encode (UTerm.func f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (func f fun i => l.get (Fin.cast ⋯ i))
Tactic:
{ simp[Encodable.encode_ofEquiv subtEquiv, Encodable.Subtype.encode_eq]
  funext i; congr }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.funcL_primrec
Proof state before:
case pos
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ encode (UTerm.func f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (func f fun i => l.get (Fin.cast ⋯ i))
Tactic:
simp[Encodable.encode_ofEquiv subtEquiv, Encodable.Subtype.encode_eq]
Proof state after:
case pos
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ (fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = fun i => ↑(subtEquiv (l.get (Fin.cast ⋯ i)))
Theorem: LO.FirstOrder.Semiterm.funcL_primrec
Proof state before:
case pos
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ (fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = fun i => ↑(subtEquiv (l.get (Fin.cast ⋯ i)))
Tactic:
funext i
Proof state after:
case pos.h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
i : Fin k
⊢ ↑(subtEquiv (l.get ⟨↑i, ⋯⟩)) = ↑(subtEquiv (l.get (Fin.cast ⋯ i)))
Theorem: LO.FirstOrder.Semiterm.funcL_primrec
Proof state before:
case pos.h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
i : Fin k
⊢ ↑(subtEquiv (l.get ⟨↑i, ⋯⟩)) = ↑(subtEquiv (l.get (Fin.cast ⋯ i)))
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.funcL_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
n k : ℕ
⊢ ∀ (a : L.Func k) (b : List (Semiterm L μ n)), funcL ⟨k, a⟩ b = funcL ⟨k, a⟩ b
Tactic:
simp[funcL]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.func₁_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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨1, f⟩ [t]
⊢ ∀ (a : L.Func 1) (b : Semiterm L μ n), funcL ⟨1, a⟩ [b] = some (func a ![b])
Tactic:
intro f t
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 : ℕ
this : Primrec₂ fun f t => funcL ⟨1, f⟩ [t]
f : L.Func 1
t : Semiterm L μ n
⊢ funcL ⟨1, f⟩ [t] = some (func f ![t])
Theorem: LO.FirstOrder.Semiterm.func₁_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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨1, f⟩ [t]
f : L.Func 1
t : Semiterm L μ n
⊢ funcL ⟨1, f⟩ [t] = some (func f ![t])
Tactic:
simp[funcL, Matrix.constant_eq_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.func₂_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
n : ℕ
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])
Tactic:
have : Primrec₂ (fun f t => funcL ⟨2, f⟩ [t.1, t.2] : L.Func 2 → Semiterm L μ n × Semiterm L μ n → Option (Semiterm L μ n)) :=
  (funcL_primrec' 2).comp₂ Primrec₂.left
    <| list_cons.comp₂ (fst.comp₂ Primrec₂.right) <| list_cons.comp₂ (snd.comp₂ Primrec₂.right) (Primrec₂.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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])
Theorem: LO.FirstOrder.Semiterm.func₂_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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])
Tactic:
exact this.of_eq <| fun f ⟨t₁, t₂⟩ => by
  simp[funcL]
  funext i; cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.func₂_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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
⊢ funcL ⟨2, f⟩ [(t₁, t₂).1, (t₁, t₂).2] = some (func f ![(t₁, t₂).1, (t₁, t₂).2])
Tactic:
simp[funcL]
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 : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
⊢ (fun i => [t₁, t₂].get i) = ![t₁, t₂]
Theorem: LO.FirstOrder.Semiterm.func₂_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
n : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
⊢ (fun i => [t₁, t₂].get i) = ![t₁, t₂]
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 : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
i : Fin 2
⊢ [t₁, t₂].get i = ![t₁, t₂] i
Theorem: LO.FirstOrder.Semiterm.func₂_primrec
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 : ℕ
this : Primrec₂ fun f t => funcL ⟨2, f⟩ [t.1, t.2]
f : L.Func 2
x✝ : Semiterm L μ n × Semiterm L μ n
t₁ t₂ : Semiterm L μ n
i : Fin 2
⊢ [t₁, t₂].get i = ![t₁, t₂] i
Tactic:
cases i using Fin.cases <;> simp
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₂
t : Semiterm L μ₁ n₁
⊢ ↑(subtEquiv ((Rew.bind b e) t)) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subtEquiv t)
Tactic:
induction t <;> simp[UTerm.bind]
Proof state after:
case func
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₂
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L μ₁ n₁
a_ih✝ :
  ∀ (a : Fin arity✝),
    ↑(subtEquiv ((Rew.bind b e) (a✝ a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (a✝ a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func a✝¹ a✝))) =
    UTerm.func a✝¹ fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (a✝ i))