internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.bind_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
have : Primrec (fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then subtEquiv (b z ⟨x, hx⟩) else default)
      (fun x => subtEquiv $ e z x) (subfEquiv (p z))
    : σ → UFormula L μ₂) :=
  UFormula.bind_primrec_param (Semiterm.brew_primrec hb)
    (subtype_val.comp₂ $ of_equiv.comp₂ $ he.comp₂ Primrec₂.left Primrec₂.right)
    (subtype_val.comp $ of_equiv.comp hp)
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Theorem: LO.FirstOrder.Semiformula.bind_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
⊢ Primrec fun x => (Rew.bind (b x) (e x)).hom (p x)
Tactic:
exact encode_iff.mp <| (Primrec.encode.comp this).of_eq <| by
  intro x
  simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq, subfEquiv_bind_eq_bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.bind_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
⊢ ∀ (n : σ),
    encode
        (UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b n ⟨x, hx⟩)) else default)
          (fun x => ↑(subtEquiv (e n x))) ↑(subfEquiv (p n))) =
      encode ((Rew.bind (b n) (e n)).hom (p n))
Tactic:
intro x
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
x : σ
⊢ encode
      (UFormula.bind (fun x_1 => if hx : x_1 < n₁ then ↑(subtEquiv (b x ⟨x_1, hx⟩)) else default)
        (fun x_1 => ↑(subtEquiv (e x x_1))) ↑(subfEquiv (p x))) =
    encode ((Rew.bind (b x) (e x)).hom (p x))
Theorem: LO.FirstOrder.Semiformula.bind_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n₁ n₂ : ℕ
b : σ → Fin n₁ → Semiterm L μ₂ n₂
e : σ → μ₁ → Semiterm L μ₂ n₂
p : σ → Semiformula L μ₁ n₁
hb : Primrec b
he : Primrec₂ e
hp : Primrec p
this✝² : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝¹ : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
this✝ : (n : ℕ) → Primcodable { p // p.bv ≤ n } := fun n => Primcodable.subtype ⋯
this :
  Primrec fun z =>
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b z ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e z x)))
      ↑(subfEquiv (p z))
x : σ
⊢ encode
      (UFormula.bind (fun x_1 => if hx : x_1 < n₁ then ↑(subtEquiv (b x ⟨x_1, hx⟩)) else default)
        (fun x_1 => ↑(subtEquiv (e x x_1))) ↑(subfEquiv (p x))) =
    encode ((Rew.bind (b x) (e x)).hom (p x))
Tactic:
simp[Encodable.encode_ofEquiv subfEquiv, Encodable.Subtype.encode_eq, subfEquiv_bind_eq_bind]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rewrite_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v p => (Rew.bind (fun x => #x) v).hom p
⊢ Primrec₂ fun v p => (Rew.rewrite v).hom p
Tactic:
exact this.of_eq <| by intro v p; rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rewrite_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v p => (Rew.bind (fun x => #x) v).hom p
⊢ ∀ (a : Fin k → Semiterm L μ n) (b : Semiformula L (Fin k) n), (Rew.bind (fun x => #x) a).hom b = (Rew.rewrite a).hom b
Tactic:
intro v 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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v p => (Rew.bind (fun x => #x) v).hom p
v : Fin k → Semiterm L μ n
p : Semiformula L (Fin k) n
⊢ (Rew.bind (fun x => #x) v).hom p = (Rew.rewrite v).hom p
Theorem: LO.FirstOrder.Semiformula.rewrite_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k n : ℕ
this : Primrec₂ fun v p => (Rew.bind (fun x => #x) v).hom p
v : Fin k → Semiterm L μ n
p : Semiformula L (Fin k) n
⊢ (Rew.bind (fun x => #x) v).hom p = (Rew.rewrite v).hom p
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.substs_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
⊢ Primrec₂ fun v p => (Rew.substs v).hom p
Tactic:
exact this.of_eq <| by { intro v p; rw[Rew.eq_bind (Rew.substs v)]; simp[Function.comp] }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.substs_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
⊢ ∀ (a : Fin n → Semiterm L μ n') (b : Semiformula L μ n), (Rew.bind a fun x => &x).hom b = (Rew.substs a).hom b
Tactic:
intro v 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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.substs v).hom p
Theorem: LO.FirstOrder.Semiformula.substs_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.substs v).hom p
Tactic:
rw[Rew.eq_bind (Rew.substs v)]
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.bind (⇑(Rew.substs v) ∘ Semiterm.bvar) (⇑(Rew.substs v) ∘ Semiterm.fvar)).hom p
Theorem: LO.FirstOrder.Semiformula.substs_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.bind (⇑(Rew.substs v) ∘ Semiterm.bvar) (⇑(Rew.substs v) ∘ Semiterm.fvar)).hom p
Tactic:
simp[Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.substs₁_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n' : ℕ
⊢ ∀ (a : Semiterm L μ n'), Semiformula L μ 1 → encode [a] = encode ![a]
Tactic:
intro x _
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n' : ℕ
x : Semiterm L μ n'
b✝ : Semiformula L μ 1
⊢ encode [x] = encode ![x]
Theorem: LO.FirstOrder.Semiformula.substs₁_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n' : ℕ
x : Semiterm L μ n'
b✝ : Semiformula L μ 1
⊢ encode [x] = encode ![x]
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.shift_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec ⇑(Rew.hom ⇑)
Tactic:
rw[Rew.eq_bind Rew.shift]
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec ⇑(Rew.bind (⇑⇑ ∘ Semiterm.bvar) (⇑⇑ ∘ Semiterm.fvar)).hom
Theorem: LO.FirstOrder.Semiformula.shift_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec ⇑(Rew.bind (⇑⇑ ∘ Semiterm.bvar) (⇑⇑ ∘ Semiterm.fvar)).hom
Tactic:
exact bind_primrec (const _) (Semiterm.fvar_primrec.comp $ succ.comp snd) Primrec.id
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.free_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec ⇑(Rew.hom Rew.free)
Tactic:
rw[Rew.eq_bind Rew.free]
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec ⇑(Rew.bind (⇑Rew.free ∘ Semiterm.bvar) (⇑Rew.free ∘ Semiterm.fvar)).hom
Theorem: LO.FirstOrder.Semiformula.free_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec ⇑(Rew.bind (⇑Rew.free ∘ Semiterm.bvar) (⇑Rew.free ∘ Semiterm.fvar)).hom
Tactic:
exact bind_primrec (const _) (Semiterm.fvar_primrec.comp $ succ.comp snd) Primrec.id
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.emb_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
⊢ Primrec ⇑Rew.emb.hom
Tactic:
rw[Rew.eq_bind Rew.emb]
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
⊢ Primrec ⇑(Rew.bind (⇑Rew.emb ∘ Semiterm.bvar) (⇑Rew.emb ∘ Semiterm.fvar)).hom
Theorem: LO.FirstOrder.Semiformula.emb_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
⊢ Primrec ⇑(Rew.bind (⇑Rew.emb ∘ Semiterm.bvar) (⇑Rew.emb ∘ Semiterm.fvar)).hom
Tactic:
simp[Function.comp]
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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
⊢ Primrec ⇑(Rew.bind (fun x => #x) fun x => Rew.emb &x).hom
Theorem: LO.FirstOrder.Semiformula.emb_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
⊢ Primrec ⇑(Rew.bind (fun x => #x) fun x => Rew.emb &x).hom
Tactic:
exact bind_primrec (const _)
  (Primrec₂.option_some_iff.mp $ (Primrec₂.const none).of_eq <| by rintro _ ⟨⟩) Primrec.id
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.emb_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
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
⊢ Semiformula L Empty 0 → ∀ (b : Empty), none = some (Rew.emb &b)
Tactic:
rintro _ ⟨⟩
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Derivation.length_cast
Proof state before:
α : Type u_1
Δ Δ₁ Δ₂ Γ : Sequent α
d :  ⊢¹ Δ
e : Δ = Γ
⊢ length (Derivation.cast d e) = length d
Tactic:
rcases e with rfl
Proof state after:
α : Type u_1
Δ Δ₁ Δ₂ : Sequent α
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d
Theorem: LO.Propositional.Classical.Derivation.length_cast
Proof state before:
α : Type u_1
Δ Δ₁ Δ₂ : Sequent α
d :  ⊢¹ Δ
⊢ length (Derivation.cast d ⋯) = length d
Tactic:
simp[Derivation.cast]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.neg_neg
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p : Formula α
⊢ p.neg.neg = p
Tactic:
induction p <;> simp[*, neg]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.neg_inj
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ ~p = ~q ↔ p = q
Tactic:
constructor
Proof state after:
case mp
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ ~p = ~q → p = q

case mpr
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ p = q → ~p = ~q
Theorem: LO.Propositional.Classical.Formula.neg_inj
Proof state before:
case mp
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ ~p = ~q → p = q
Tactic:
intro h
Proof state after:
case mp
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
h : ~p = ~q
⊢ p = q
Theorem: LO.Propositional.Classical.Formula.neg_inj
Proof state before:
case mpr
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
⊢ p = q → ~p = ~q
Tactic:
exact congr_arg _
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.and_inj
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Wedge.wedge]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.or_inj
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p₁ q₁ p₂ q₂ : Formula α
⊢ p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Vee.vee]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.complexity_neg
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p : Formula α
⊢ (~p).complexity = p.complexity
Tactic:
induction p using rec' <;> simp[*]
Proof state after:
no goals
Theorem: LO.Propositional.Classical.Formula.ne_of_ne_complexity
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p q : Formula α
h : p.complexity ≠ q.complexity
⊢ p ≠ q
Tactic:
rintro rfl
Proof state after:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p : Formula α
h : p.complexity ≠ p.complexity
⊢ False
Theorem: LO.Propositional.Classical.Formula.ne_of_ne_complexity
Proof state before:
α : Type u
α₁ : Type u₁
α₂ : Type u₂
α₃ : Type u₃
p : Formula α
h : p.complexity ≠ p.complexity
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.System.ModusPonens.mdp!
Proof state before:
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
⊢ 𝓢 ⊢! p ⟶ q → 𝓢 ⊢! p → 𝓢 ⊢! q
Tactic:
rintro ⟨hpq⟩ ⟨hp⟩
Proof state after:
case intro.intro
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
𝓢 : S
p q : F
inst✝ : ModusPonens 𝓢
hpq : 𝓢 ⊢ p ⟶ q
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! q