internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.nrel_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
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
Proof 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
Theorem: LO.FirstOrder.Semiformula.nrel_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
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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.nrel_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
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⟩
Proof 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)))⟩
Theorem: LO.FirstOrder.Semiformula.nrel_primrec
Proof 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']
Proof 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))
Theorem: LO.FirstOrder.Semiformula.nrel_primrec
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Semiformula.nrel_primrec
Proof 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 _
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.nrel_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
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⟩
Proof 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)
Theorem: LO.FirstOrder.Semiformula.nrel_primrec
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.relL_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
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))
Proof 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
Theorem: LO.FirstOrder.Semiformula.relL_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
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 }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.relL_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
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⟩
Proof 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)
Theorem: LO.FirstOrder.Semiformula.relL_primrec
Proof 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]
Proof 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)
Theorem: LO.FirstOrder.Semiformula.relL_primrec
Proof 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]
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
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))
Theorem: LO.FirstOrder.Semiformula.relL_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
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 }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.relL_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
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]
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
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)))
Theorem: LO.FirstOrder.Semiformula.relL_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
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
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
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)))
Theorem: LO.FirstOrder.Semiformula.relL_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
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
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.nrelL_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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
⊢ Primrec₂ nrelL
Tactic:
letI : ∀ n, Primcodable { t : UTerm L μ // t.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp UTerm.bv_primrec (Primrec.const n))
Proof 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₂ nrelL
Theorem: LO.FirstOrder.Semiformula.nrelL_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
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.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)
⊢ Primrec₂ nrelL
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  rintro ⟨⟨k, f⟩, l⟩; simp[nrelL, UFormula.nrelL]
  by_cases hl : l.length = k <;> simp[hl]
  { simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
    funext i; congr }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.nrelL_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
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.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)
⊢ ∀ (n_1 : ((k : ℕ) × L.Rel k) × List (Semiterm L μ n)),
    encode ((fun f v => UFormula.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)) n_1.1 n_1.2) =
      encode (nrelL n_1.1 n_1.2)
Tactic:
rintro ⟨⟨k, f⟩, l⟩
Proof 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.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
⊢ encode ((fun f v => UFormula.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)) (⟨k, f⟩, l).1 (⟨k, f⟩, l).2) =
    encode (nrelL (⟨k, f⟩, l).1 (⟨k, f⟩, l).2)
Theorem: LO.FirstOrder.Semiformula.nrelL_primrec
Proof 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.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
⊢ encode ((fun f v => UFormula.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)) (⟨k, f⟩, l).1 (⟨k, f⟩, l).2) =
    encode (nrelL (⟨k, f⟩, l).1 (⟨k, f⟩, l).2)
Tactic:
simp[nrelL, UFormula.nrelL]
Proof 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.nrelL 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.nrel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) else none) =
    encode (if h : l.length = k then some (nrel f fun i => l.get (Fin.cast ⋯ i)) else none)
Theorem: LO.FirstOrder.Semiformula.nrelL_primrec
Proof 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.nrelL 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.nrel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) else none) =
    encode (if h : l.length = k then some (nrel 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
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.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
hl : l.length = k
⊢ encode (UFormula.nrel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (nrel f fun i => l.get (Fin.cast ⋯ i))
Theorem: LO.FirstOrder.Semiformula.nrelL_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
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.nrelL f (List.map (fun x => ↑(subtEquiv x)) v)
l : List (Semiterm L μ n)
k : ℕ
f : L.Rel k
hl : l.length = k
⊢ encode (UFormula.nrel f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (nrel f fun i => l.get (Fin.cast ⋯ i))
Tactic:
{ simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
  funext i; congr }
Proof state after:
no goals