internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.and a✝).depth
Tactic:
rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.or a✝).depth
Tactic:
rintro (⟨rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩) <;> simp[depth, Nat.lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.all.depth
Tactic:
rintro rfl rfl rfl
Proof state after:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.all.depth
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.all.depth
Tactic:
simp[depth]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x₁ : σ
m₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.ex.depth
Tactic:
rintro rfl rfl rfl
Proof state after:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.ex.depth
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
m₁ : ℕ
x₂ : σ
p₂ : UFormula L μ₁
⊢ p₂.depth < p₂.ex.depth
Tactic:
simp[depth]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
⊢ ∀ (b_1 : σ × ℕ × UFormula L μ₁),
    LO.FirstOrder.UFormula.bindqG b e b_1
        (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (LO.FirstOrder.UFormula.bindqL b_1)) =
      some ((fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) b_1)
Tactic:
rintro ⟨x, m, p⟩
Proof state after:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (LO.FirstOrder.UFormula.bindqL (x, m, p))) =
    some ((fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (x, m, p))
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (LO.FirstOrder.UFormula.bindqL (x, m, p))) =
    some ((fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2) (x, m, p))
Tactic:
simp[bindqL]
Proof state after:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2)
        (Sum.rec (fun val => [])
          (fun val =>
            Sum.rec (fun val => [])
              (fun val =>
                Sum.rec (fun val => List.map (fun x_1 => (x, m, x_1)) p.inversion.2)
                  (fun val => List.map (fun x_1 => (x, m + 1, x_1)) p.inversion.2) val)
              val)
          p.inversion.1.2)) =
    some (bindq (b x) (e x) m p)
Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
case mk.mk
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2)
        (Sum.rec (fun val => [])
          (fun val =>
            Sum.rec (fun val => [])
              (fun val =>
                Sum.rec (fun val => List.map (fun x_1 => (x, m, x_1)) p.inversion.2)
                  (fun val => List.map (fun x_1 => (x, m + 1, x_1)) p.inversion.2) val)
              val)
          p.inversion.1.2)) =
    some (bindq (b x) (e x) m p)
Tactic:
cases p <;> simp[inversion, bindq, bindqG]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rel_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 fun p => rel 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))
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 fun p => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.Semiformula.rel_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 ⋯
⊢ Primrec fun p => rel 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 _)
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)))⟩
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.Semiformula.rel_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 => rel p.snd.1 p.snd.2
Tactic:
have : Primrec (fun f => UFormula.rel f.2.1 (fun i => UTerm.subtEquiv (f.2.2 i))
    : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n) → UFormula L μ) :=
  UFormula.rel_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.rel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
⊢ Primrec fun p => rel p.snd.1 p.snd.2
Theorem: LO.FirstOrder.Semiformula.rel_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.rel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
⊢ Primrec fun p => rel 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.rel_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.rel_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.rel_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.rel_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.rel_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.rel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
⊢ ∀ (n_1 : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n)),
    encode (UFormula.rel n_1.snd.1 fun i => ↑(subtEquiv (n_1.snd.2 i))) = encode (rel 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.rel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ encode (UFormula.rel ⟨k, (r, v)⟩.snd.1 fun i => ↑(subtEquiv (⟨k, (r, v)⟩.snd.2 i))) =
    encode (rel ⟨k, (r, v)⟩.snd.1 ⟨k, (r, v)⟩.snd.2)
Theorem: LO.FirstOrder.Semiformula.rel_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.rel f.snd.1 fun i => ↑(subtEquiv (f.snd.2 i))
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ encode (UFormula.rel ⟨k, (r, v)⟩.snd.1 fun i => ↑(subtEquiv (⟨k, (r, v)⟩.snd.2 i))) =
    encode (rel ⟨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.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 : ℕ
⊢ 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))
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 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 ⋯
⊢ 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 _)
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)))⟩
⊢ Primrec fun p => nrel p.snd.1 p.snd.2