Theorem: LO.FirstOrder.Semiterm.funcL_primrec (Logic/FirstOrder/Computability/Term.lean)

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
State after:
no goals

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
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)

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]
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)

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]
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))

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 }
State after:
no goals

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]
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)))

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
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)))

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
State after:
no goals