internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.or_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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] (fintypeEquivFin false)) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] (fintypeEquivFin true)) = q
Tactic:
rw [fintypeEquivFin_false, fintypeEquivFin_true]
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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 0) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 1) = q
Theorem: LO.FirstOrder.UFormula.or_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 μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
p q : UFormula L μ
⊢ (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 0) = p ∧
    (equivW L μ).symm (![(equivW L μ) p, (equivW L μ) q] 1) = q
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.all_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 μ
⊢ Primrec all
Tactic:
have := w_mk₁ (β := Edge L μ) (fun (_ : Unit) => (true, Sum.inr $ Sum.inr $ Sum.inr ())) (by rintro ⟨⟩; simp[Edge]) (const _)
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 μ
this : Primrec₂ fun x w => WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
⊢ Primrec all
Theorem: LO.FirstOrder.UFormula.all_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 μ
this : Primrec₂ fun x w => WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
⊢ Primrec all
Tactic:
have := (Primrec.of_equiv_symm (e := equivW L μ)).comp
  ((this.comp (Primrec.const ()) Primrec.id).comp (Primrec.of_equiv (e := equivW L μ)))
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 μ
this✝ : Primrec₂ fun x w => WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
this :
  Primrec fun a =>
    (equivW L μ).symm (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) a))
⊢ Primrec all
Theorem: LO.FirstOrder.UFormula.all_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 μ
this✝ : Primrec₂ fun x w => WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
this :
  Primrec fun a =>
    (equivW L μ).symm (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) a))
⊢ Primrec all
Tactic:
exact this.of_eq (fun p => by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.all_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 μ
⊢ ∀ (x : Unit), Fintype.card (Edge L μ ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) x)) = 1
Tactic:
rintro ⟨⟩
Proof state after:
case unit
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 μ
⊢ Fintype.card (Edge L μ ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) PUnit.unit)) = 1
Theorem: LO.FirstOrder.UFormula.all_primrec
Proof state before:
case unit
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 μ
⊢ Fintype.card (Edge L μ ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) PUnit.unit)) = 1
Tactic:
simp[Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.all_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 μ
this✝ : Primrec₂ fun x w => WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
this :
  Primrec fun a =>
    (equivW L μ).symm (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) a))
p : UFormula L μ
⊢ (equivW L μ).symm (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) p)) =
    p.all
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ex_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 μ
⊢ Primrec ex
Tactic:
have := w_mk₁ (β := Edge L μ) (fun (_ : Unit) => (false, Sum.inr $ Sum.inr $ Sum.inr ())) (by rintro ⟨⟩; simp[Edge]) (const _)
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 μ
this : Primrec₂ fun x w => WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
⊢ Primrec ex
Theorem: LO.FirstOrder.UFormula.ex_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 μ
this : Primrec₂ fun x w => WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
⊢ Primrec ex
Tactic:
have := (Primrec.of_equiv_symm (e := equivW L μ)).comp
  ((this.comp (Primrec.const ()) Primrec.id).comp (Primrec.of_equiv (e := equivW L μ)))
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 μ
this✝ : Primrec₂ fun x w => WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
this :
  Primrec fun a =>
    (equivW L μ).symm (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) a))
⊢ Primrec ex
Theorem: LO.FirstOrder.UFormula.ex_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 μ
this✝ : Primrec₂ fun x w => WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
this :
  Primrec fun a =>
    (equivW L μ).symm (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) a))
⊢ Primrec ex
Tactic:
exact this.of_eq (fun p => by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ex_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 μ
⊢ ∀ (x : Unit), Fintype.card (Edge L μ ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) x)) = 1
Tactic:
rintro ⟨⟩
Proof state after:
case unit
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 μ
⊢ Fintype.card (Edge L μ ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) PUnit.unit)) = 1
Theorem: LO.FirstOrder.UFormula.ex_primrec
Proof state before:
case unit
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 μ
⊢ Fintype.card (Edge L μ ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) PUnit.unit)) = 1
Tactic:
simp[Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ex_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 μ
this✝ : Primrec₂ fun x w => WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) x) fun x => w
this :
  Primrec fun a =>
    (equivW L μ).symm (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) a))
p : UFormula L μ
⊢ (equivW L μ).symm (WType.mk ((fun x => (false, Sum.inr (Sum.inr (Sum.inr ())))) ()) fun x => id ((equivW L μ) p)) =
    p.ex
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
case and.e_a.e_snd.e_a
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
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝¹ a✝ : UFormula L μ
a_ih✝¹ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝¹ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝¹)
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ (equivW L μ) a✝ = Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 1)
Tactic:
rw [fintypeEquivFin_symm_one]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
case or.e_a.e_snd.e_a
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
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝¹ a✝ : UFormula L μ
a_ih✝¹ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝¹ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝¹)
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ (equivW L μ) a✝ = Bool.rec ((equivW L μ) a✝¹) ((equivW L μ) a✝) (fintypeEquivFin.symm 1)
Tactic:
rw [fintypeEquivFin_symm_one]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
case all
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
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝ : UFormula L μ
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ γAll x
      (WType.elimL
        (fun p l =>
          Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
            (fun val =>
              Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                (fun val =>
                  Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                    (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                val)
            p.2)
        ((equivW L μ) a✝)) =
    γAll x
      (fintypeArrowEquivFinArrow
        (fun b =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
                (fun val =>
                  Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                    (fun val =>
                      Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                        (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                    val)
                p.2)
            ((equivW L μ) a✝))
        0)
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.elim_eq
Proof state before:
case ex
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
σ : Sort u_2
x : σ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
a✝ : UFormula L μ
a_ih✝ :
  elim (γVerum x) (γFalsum x) (fun {k} f v => γRel x ⟨k, (f, v)⟩) (fun {k} f v => γNrel x ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x (y₁, y₂)) (fun y₁ y₂ => γOr x (y₁, y₂)) (γAll x) (γEx x) a✝ =
    WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x (p, l))
      ((equivW L μ) a✝)
⊢ γEx x
      (WType.elimL
        (fun p l =>
          Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
            (fun val =>
              Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                (fun val =>
                  Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                    (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                val)
            p.2)
        ((equivW L μ) a✝)) =
    γEx x
      (fintypeArrowEquivFinArrow
        (fun b =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => bif p.1 then γRel x val else γNrel x val)
                (fun val =>
                  Sum.rec (fun val => bif p.1 then γVerum x else γFalsum x)
                    (fun val =>
                      Sum.rec (fun val => bif p.1 then γAnd x (l.getI 0, l.getI 1) else γOr x (l.getI 0, l.getI 1))
                        (fun val => bif p.1 then γAll x (l.getI 0) else γEx x (l.getI 0)) val)
                    val)
                p.2)
            ((equivW L μ) a✝))
        0)
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.elim_primrec_param
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
inst✝² : Primcodable σ
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
f : σ → UFormula L μ
hVerum : Primrec γVerum
hFalsum : Primrec γFalsum
hRel : Primrec₂ γRel
hNrel : Primrec₂ γNrel
hAnd : Primrec₂ γAnd
hOr : Primrec₂ γOr
hAll : Primrec₂ γAll
hEx : Primrec₂ γEx
hf : Primrec f
x✝ : σ
⊢ WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x✝ (p, l))
      ((equivW L μ) (f x✝)) =
    elim (γVerum x✝) (γFalsum x✝) (fun {k} f v => γRel x✝ ⟨k, (f, v)⟩) (fun {k} f v => γNrel x✝ ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x✝ (y₁, y₂)) (fun y₁ y₂ => γOr x✝ (y₁, y₂)) (γAll x✝) (γEx x✝) (f x✝)
Tactic:
simp[elim_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bv_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 μ
⊢ Primrec bv
Tactic:
have hr : Primrec (fun p => ((List.ofFn p.2.2).map UTerm.bv).sup : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → ℕ) :=
  (list_sup nat_max).comp
    (list_map (by apply sigma_finArrow_list_ofFn.comp (sigma_prod_right (β := L.Rel))) (UTerm.bv_primrec.comp₂ Primrec₂.right))
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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
⊢ Primrec bv
Theorem: LO.FirstOrder.UFormula.bv_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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
⊢ Primrec bv
Tactic:
have hb : Primrec₂ (fun m n => max m n : ℕ → ℕ → ℕ) := Primrec.nat_max
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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
⊢ Primrec bv
Theorem: LO.FirstOrder.UFormula.bv_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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
⊢ Primrec bv
Tactic:
have hq : Primrec (fun n => n.pred : ℕ → ℕ) := Primrec.pred
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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
hq : Primrec fun n => n.pred
⊢ Primrec bv
Theorem: LO.FirstOrder.UFormula.bv_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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
hq : Primrec fun n => n.pred
⊢ Primrec bv
Tactic:
have := elim_primrec 0 0 hr hr hb hb hq hq
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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
hq : Primrec fun n => n.pred
this :
  Primrec
    (elim 0 0 (fun {k} f v => (List.map UTerm.bv (List.ofFn ⟨k, (f, v)⟩.snd.2)).sup)
      (fun {k} f v => (List.map UTerm.bv (List.ofFn ⟨k, (f, v)⟩.snd.2)).sup) (fun m n => max m n) (fun m n => max m n)
      (fun n => n.pred) fun n => n.pred)
⊢ Primrec bv
Theorem: LO.FirstOrder.UFormula.bv_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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
hq : Primrec fun n => n.pred
this :
  Primrec
    (elim 0 0 (fun {k} f v => (List.map UTerm.bv (List.ofFn ⟨k, (f, v)⟩.snd.2)).sup)
      (fun {k} f v => (List.map UTerm.bv (List.ofFn ⟨k, (f, v)⟩.snd.2)).sup) (fun m n => max m n) (fun m n => max m n)
      (fun n => n.pred) fun n => n.pred)
⊢ Primrec bv
Tactic:
exact this.of_eq (fun p => by
  simp[Function.comp]
  induction p <;> simp[elim, *]
  { simp[List.sup_ofFn] }
  { simp[List.sup_ofFn] })
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bv_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 μ
⊢ Primrec fun p => List.ofFn p.snd.2
Tactic:
apply sigma_finArrow_list_ofFn.comp (sigma_prod_right (β := L.Rel))
Proof state after:
no goals