internlm/Lean-Github huggingface dataset:
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]
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
⊢ (fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = fun i => ↑(subtEquiv (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
⊢ (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.nrelL 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.nrelL_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.nrelL 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.and_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 x x_1 => x ⋏ x_1
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp 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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Theorem: LO.FirstOrder.Semiformula.and_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Tactic:
have : Primrec₂ (fun p q => UFormula.and (subfEquiv p) (subfEquiv q)
    : Semiformula L μ n → Semiformula L μ n → UFormula L μ) :=
  UFormula.and_primrec.comp₂
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.left)
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.right)
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Theorem: LO.FirstOrder.Semiformula.and_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋏ x_1
Tactic:
exact Primrec₂.encode_iff.mp <| (Primrec.encode.comp₂ this).of_eq <| by
  intro p q
  simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.and_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
⊢ ∀ (a b : Semiformula L μ n), encode ((↑(subfEquiv a)).and ↑(subfEquiv b)) = encode (a ⋏ b)
Tactic:
intro p q
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).and ↑(subfEquiv q)) = encode (p ⋏ q)
Theorem: LO.FirstOrder.Semiformula.and_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).and ↑(subfEquiv q)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).and ↑(subfEquiv q)) = encode (p ⋏ q)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.or_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 x x_1 => x ⋎ x_1
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp 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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun x x_1 => x ⋎ x_1
Theorem: LO.FirstOrder.Semiformula.or_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec₂ fun x x_1 => x ⋎ x_1
Tactic:
have : Primrec₂ (fun p q => UFormula.or (subfEquiv p) (subfEquiv q)
    : Semiformula L μ n → Semiformula L μ n → UFormula L μ) :=
  UFormula.or_primrec.comp₂
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.left)
    (subtype_val.comp₂ $ of_equiv.comp₂ Primrec₂.right)
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).or ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋎ x_1
Theorem: LO.FirstOrder.Semiformula.or_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).or ↑(subfEquiv q)
⊢ Primrec₂ fun x x_1 => x ⋎ x_1
Tactic:
exact Primrec₂.encode_iff.mp <| (Primrec.encode.comp₂ this).of_eq <| by
  intro p q
  simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.or_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).or ↑(subfEquiv q)
⊢ ∀ (a b : Semiformula L μ n), encode ((↑(subfEquiv a)).or ↑(subfEquiv b)) = encode (a ⋎ b)
Tactic:
intro p q
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).or ↑(subfEquiv q)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).or ↑(subfEquiv q)) = encode (p ⋎ q)
Theorem: LO.FirstOrder.Semiformula.or_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec₂ fun p q => (↑(subfEquiv p)).or ↑(subfEquiv q)
p q : Semiformula L μ n
⊢ encode ((↑(subfEquiv p)).or ↑(subfEquiv q)) = encode (p ⋎ q)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.all_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 x => ∀' x
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp 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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ∀' x
Theorem: LO.FirstOrder.Semiformula.all_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ∀' x
Tactic:
have : Primrec (fun p => UFormula.all (subfEquiv p) : Semiformula L μ (n + 1) → UFormula L μ) :=
  UFormula.all_primrec.comp (subtype_val.comp $ of_equiv)
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).all
⊢ Primrec fun x => ∀' x
Theorem: LO.FirstOrder.Semiformula.all_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).all
⊢ Primrec fun x => ∀' x
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  intro p; simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.all_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).all
⊢ ∀ (n_1 : Semiformula L μ (n + 1)), encode (↑(subfEquiv n_1)).all = encode (∀' n_1)
Tactic:
intro p
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).all
p : Semiformula L μ (n + 1)
⊢ encode (↑(subfEquiv p)).all = encode (∀' p)
Theorem: LO.FirstOrder.Semiformula.all_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).all
p : Semiformula L μ (n + 1)
⊢ encode (↑(subfEquiv p)).all = encode (∀' p)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ex_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 x => ∃' x
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp 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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ∃' x
Theorem: LO.FirstOrder.Semiformula.ex_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ∃' x
Tactic:
have : Primrec (fun p => UFormula.ex (subfEquiv p) : Semiformula L μ (n + 1) → UFormula L μ) :=
  UFormula.ex_primrec.comp (subtype_val.comp $ of_equiv)
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).ex
⊢ Primrec fun x => ∃' x
Theorem: LO.FirstOrder.Semiformula.ex_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).ex
⊢ Primrec fun x => ∃' x
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  intro p; simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ex_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).ex
⊢ ∀ (n_1 : Semiformula L μ (n + 1)), encode (↑(subfEquiv n_1)).ex = encode (∃' n_1)
Tactic:
intro p
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).ex
p : Semiformula L μ (n + 1)
⊢ encode (↑(subfEquiv p)).ex = encode (∃' p)
Theorem: LO.FirstOrder.Semiformula.ex_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).ex
p : Semiformula L μ (n + 1)
⊢ encode (↑(subfEquiv p)).ex = encode (∃' p)
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.subfEquiv_neg_eq_neg_subfEquiv
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 : ℕ
p : Semiformula L μ n
⊢ ↑(subfEquiv (~p)) = (↑(subfEquiv p)).neg
Tactic:
induction p using rec' <;> simp[UFormula.neg, UTerm.ofSubterm_eq_subtEquiv, UFormula.ofSubformula_eq_subfEquiv, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.neg_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 x => ~x
Tactic:
letI : ∀ n , Primcodable { p : UFormula L μ // p.bv ≤ n } := fun n => Primcodable.subtype (nat_le.comp 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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ~x
Theorem: LO.FirstOrder.Semiformula.neg_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => ~x
Tactic:
have : Primrec (fun p => UFormula.neg (subfEquiv p) : Semiformula L μ n → UFormula L μ) :=
  UFormula.neg_primrec.comp (subtype_val.comp $ of_equiv)
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).neg
⊢ Primrec fun x => ~x
Theorem: LO.FirstOrder.Semiformula.neg_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).neg
⊢ Primrec fun x => ~x
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  intro p; simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq, subfEquiv_neg_eq_neg_subfEquiv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.neg_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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).neg
⊢ ∀ (n_1 : Semiformula L μ n), encode (↑(subfEquiv n_1)).neg = encode (~n_1)
Tactic:
intro p
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 { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : Primrec fun p => (↑(subfEquiv p)).neg
p : Semiformula L μ n
⊢ encode (↑(subfEquiv p)).neg = encode (~p)