Theorem: LO.FirstOrder.Semiformula.relL_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
⊢ Primrec₂ relL
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const n))
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ relL

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
⊢ Primrec₂ relL
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  rintro ⟨⟨k, f⟩, l⟩; simp[relL, UFormula.relL]
  by_cases hl : l.length = k <;> simp[hl]
  { simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
    funext i; congr }
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
⊢ ∀ (n_1 : ((k : ℕ) × L.Rel k) × List (Semiterm L μ n)),
    encode ((fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)) n_1.1 n_1.2) = encode (relL n_1.1 n_1.2)
Tactic:
rintro ⟨⟨k, f⟩, l⟩
State after:
case mk.mk
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
⊢ encode ((fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)) (⟨k, f⟩, l).1 (⟨k, f⟩, l).2) =
    encode (relL (⟨k, f⟩, l).1 (⟨k, f⟩, l).2)

State before:
case mk.mk
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
⊢ encode ((fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)) (⟨k, f⟩, l).1 (⟨k, f⟩, l).2) =
    encode (relL (⟨k, f⟩, l).1 (⟨k, f⟩, l).2)
Tactic:
simp[relL, UFormula.relL]
State after:
case mk.mk
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
⊢ encode (if h : l.length = k then some (UFormula.rel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) else none) =
    encode (if h : l.length = k then some (rel f fun i => l.get (Fin.cast ⋯ i)) else none)

State before:
case mk.mk
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
⊢ encode (if h : l.length = k then some (UFormula.rel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) else none) =
    encode (if h : l.length = k then some (rel 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
hl : l.length = k
⊢ encode (UFormula.rel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (rel 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
hl : l.length = k
⊢ encode (UFormula.rel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (rel f fun i => l.get (Fin.cast ⋯ i))
Tactic:
{ simp[Encodable.encode_ofEquiv subfEquiv, 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
hl : l.length = k
⊢ encode (UFormula.rel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (rel f fun i => l.get (Fin.cast ⋯ i))
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun f v => UFormula.relL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
hl : l.length = k
i : Fin k
⊢ ↑(subtEquiv (l.get ⟨↑i, ⋯⟩)) = ↑(subtEquiv (l.get (Fin.cast ⋯ i)))
Tactic:
congr
State after:
no goals