Theorem: LO.FirstOrder.Semiformula.nrel_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 fun p => nrel p.snd.1 p.snd.2
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 fun p => nrel p.snd.1 p.snd.2

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 ⋯
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
have h : Primrec (fun f => ⟨f.1, f.2.1, (fun i => UTerm.subtEquiv (f.2.2 i))⟩
  : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n) → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)) :=
  encode_iff.mp (Primrec.encode.of_eq <| by
    rintro ⟨k, r, v⟩; simp[Encodable.encode_prod_val r, encode_finArrow']
    funext i; exact encode_ofEquiv subtEquiv _)
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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
⊢ Primrec fun p => nrel p.snd.1 p.snd.2

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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
have : Primrec (fun f => UFormula.nrel f.2.1 (fun i => UTerm.subtEquiv (f.2.2 i))
    : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n) → UFormula L μ) :=
  UFormula.nrel_primrec.comp h
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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
this : Primrec fun f => UFormula.nrel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
⊢ Primrec fun p => nrel p.snd.1 p.snd.2

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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
this : Primrec fun f => UFormula.nrel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
⊢ Primrec fun p => nrel p.snd.1 p.snd.2
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  rintro ⟨k, r, v⟩; simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
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 ⋯
⊢ ∀ (n_1 : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n)),
    encode n_1 = encode ⟨n_1.fst, (n_1.snd.1, fun i => ↑(subtEquiv (n_1.snd.2 i)))⟩
Tactic:
rintro ⟨k, r, v⟩
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 ⋯
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ encode ⟨k, (r, v)⟩ = encode ⟨⟨k, (r, v)⟩.fst, (⟨k, (r, v)⟩.snd.1, fun i => ↑(subtEquiv (⟨k, (r, v)⟩.snd.2 i)))⟩

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 ⋯
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ encode ⟨k, (r, v)⟩ = encode ⟨⟨k, (r, v)⟩.fst, (⟨k, (r, v)⟩.snd.1, fun i => ↑(subtEquiv (⟨k, (r, v)⟩.snd.2 i)))⟩
Tactic:
simp[Encodable.encode_prod_val r, encode_finArrow']
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 ⋯
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ (fun i => encode (v i)) = fun i => encode ↑(subtEquiv (v i))

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 ⋯
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ (fun i => encode (v i)) = fun i => encode ↑(subtEquiv (v i))
Tactic:
funext i
State after:
case mk.mk.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 ⋯
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
⊢ encode (v i) = encode ↑(subtEquiv (v i))

State before:
case mk.mk.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 ⋯
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
⊢ encode (v i) = encode ↑(subtEquiv (v i))
Tactic:
exact encode_ofEquiv subtEquiv _
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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
this : Primrec fun f => UFormula.nrel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
⊢ ∀ (n_1 : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n)),
    encode (UFormula.nrel n_1.snd.1 fun i => ↑(subtEquiv (n_1.snd.2 i))) = encode (nrel n_1.snd.1 n_1.snd.2)
Tactic:
rintro ⟨k, r, v⟩
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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
this : Primrec fun f => UFormula.nrel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ encode (UFormula.nrel ⟨k, (r, v)⟩.snd.1 fun i => ↑(subtEquiv (⟨k, (r, v)⟩.snd.2 i))) =
    encode (nrel ⟨k, (r, v)⟩.snd.1 ⟨k, (r, v)⟩.snd.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 ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
this : Primrec fun f => UFormula.nrel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ encode (UFormula.nrel ⟨k, (r, v)⟩.snd.1 fun i => ↑(subtEquiv (⟨k, (r, v)⟩.snd.2 i))) =
    encode (nrel ⟨k, (r, v)⟩.snd.1 ⟨k, (r, v)⟩.snd.2)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
State after:
no goals