internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n
Tactic:
have : x ≤ t.bv.pred := Nat.le_pred_of_lt hx
Proof state after:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
this : x ≤ t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
case inr.inr
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x > t.bv.pred
this : x ≤ t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n
Tactic:
exact False.elim (Nat.not_le_of_lt lt this)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_substLast
Proof state before:
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
⊢ ∀ (x : μ), (fvar x).bv ≤ n
Tactic:
simp[bv]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.toSubterm_ofSubterm
Proof state before:
L : Language
μ : Type v
n : ℕ
t : Semiterm L μ n
⊢ (↑(ofSubterm t)).toSubterm ⋯ = t
Tactic:
induction t <;> simp [ofSubterm, toSubterm]
Proof state after:
case func
L : Language
μ : Type v
n arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L μ n
a_ih✝ : ∀ (a : Fin arity✝), (↑(ofSubterm (a✝ a))).toSubterm ⋯ = a✝ a
⊢ (fun i => (↑(ofSubterm (a✝ i))).toSubterm ⋯) = a✝
Theorem: LO.FirstOrder.UTerm.toSubterm_ofSubterm
Proof state before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
⊢ (fun i => (↑(ofSubterm (v i))).toSubterm ⋯) = v
Tactic:
case func f v ih => funext i; exact ih i
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.toSubterm_ofSubterm
Proof state before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
⊢ (fun i => (↑(ofSubterm (v i))).toSubterm ⋯) = v
Tactic:
funext i
Proof state after:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
i : Fin arity✝
⊢ (↑(ofSubterm (v i))).toSubterm ⋯ = v i
Theorem: LO.FirstOrder.UTerm.toSubterm_ofSubterm
Proof state before:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
i : Fin arity✝
⊢ (↑(ofSubterm (v i))).toSubterm ⋯ = v i
Tactic:
exact ih i
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.ofSubterm_toSubterm
Proof state before:
L : Language
μ : Type v
n : ℕ
t : UTerm L μ
h : t.bv ≤ n
⊢ ↑(ofSubterm (t.toSubterm h)) = t
Tactic:
induction t <;> simp[ofSubterm, toSubterm]
Proof state after:
case func
L : Language
μ : Type v
n arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝) (h : (a✝ a).bv ≤ n), ↑(ofSubterm ((a✝ a).toSubterm h)) = a✝ a
h : (func a✝¹ a✝).bv ≤ n
⊢ (fun i => ↑(ofSubterm ((a✝ i).toSubterm ⋯))) = a✝
Theorem: LO.FirstOrder.UTerm.ofSubterm_toSubterm
Proof state before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
⊢ (fun i => ↑(ofSubterm ((v i).toSubterm ⋯))) = v
Tactic:
case func f v ih =>
  funext i
  have h : ∀ i, (v i).bv ≤ n := by simpa[bv] using h
  exact ih i (h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.ofSubterm_toSubterm
Proof state before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
⊢ (fun i => ↑(ofSubterm ((v i).toSubterm ⋯))) = v
Tactic:
funext i
Proof state after:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
i : Fin arity✝
⊢ ↑(ofSubterm ((v i).toSubterm ⋯)) = v i
Theorem: LO.FirstOrder.UTerm.ofSubterm_toSubterm
Proof state before:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
i : Fin arity✝
⊢ ↑(ofSubterm ((v i).toSubterm ⋯)) = v i
Tactic:
have h : ∀ i, (v i).bv ≤ n := by simpa[bv] using h
Proof state after:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h✝ : (func f v).bv ≤ n
i : Fin arity✝
h : ∀ (i : Fin arity✝), (v i).bv ≤ n
⊢ ↑(ofSubterm ((v i).toSubterm ⋯)) = v i
Theorem: LO.FirstOrder.UTerm.ofSubterm_toSubterm
Proof state before:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h✝ : (func f v).bv ≤ n
i : Fin arity✝
h : ∀ (i : Fin arity✝), (v i).bv ≤ n
⊢ ↑(ofSubterm ((v i).toSubterm ⋯)) = v i
Tactic:
exact ih i (h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.ofSubterm_toSubterm
Proof state before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
i : Fin arity✝
⊢ ∀ (i : Fin arity✝), (v i).bv ≤ n
Tactic:
simpa[bv] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.subtEquiv_fvar
Proof state before:
L : Language
μ : Type v
n : ℕ
x : μ
⊢ (fvar x).bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.subtEquiv_func
Proof state before:
L : Language
μ : Type v
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
⊢ (func f fun i => ↑(subtEquiv (v i))).bv ≤ n
Tactic:
simp[bv]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.funcL_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
⊢ Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr ⟨k, f⟩)) (List.map (⇑(equivW L μ)) l)) = funcL ⟨k, f⟩ l
Tactic:
simp[WType.mkL, Edge]
Proof state after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
⊢ Option.map (⇑(equivW L μ).symm)
      (if h : l.length = k then
        some
          (WType.mk (Sum.inr (Sum.inr ⟨k, f⟩)) (fintypeArrowEquivFinArrow.symm fun i => (equivW L μ) (l.get ⟨↑i, ⋯⟩)))
      else none) =
    funcL ⟨k, f⟩ l
Theorem: LO.FirstOrder.UTerm.funcL_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
⊢ Option.map (⇑(equivW L μ).symm)
      (if h : l.length = k then
        some
          (WType.mk (Sum.inr (Sum.inr ⟨k, f⟩)) (fintypeArrowEquivFinArrow.symm fun i => (equivW L μ) (l.get ⟨↑i, ⋯⟩)))
      else none) =
    funcL ⟨k, f⟩ l
Tactic:
by_cases hl : l.length = k <;> simp[hl, funcL]
Proof state after:
case pos
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
⊢ (fun i => l.get ⟨↑i, ⋯⟩) = fun i => l.get (Fin.cast ⋯ i)
Theorem: LO.FirstOrder.UTerm.funcL_primrec
Proof state before:
case pos
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
⊢ (fun i => l.get ⟨↑i, ⋯⟩) = fun i => l.get (Fin.cast ⋯ i)
Tactic:
{ funext i; congr }
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.funcL_primrec
Proof state before:
case pos
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
⊢ (fun i => l.get ⟨↑i, ⋯⟩) = fun i => l.get (Fin.cast ⋯ i)
Tactic:
funext i
Proof state after:
case pos.h
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
i : Fin k
⊢ l.get ⟨↑i, ⋯⟩ = l.get (Fin.cast ⋯ i)
Theorem: LO.FirstOrder.UTerm.funcL_primrec
Proof state before:
case pos.h
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
i : Fin k
⊢ l.get ⟨↑i, ⋯⟩ = l.get (Fin.cast ⋯ i)
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.funcL_primrec'
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
⊢ ∀ (a : L.Func k) (b : List (UTerm L μ)), funcL ⟨k, a⟩ b = funcL ⟨k, a⟩ b
Tactic:
intro f l
Proof state after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
f : L.Func k
l : List (UTerm L μ)
⊢ funcL ⟨k, f⟩ l = funcL ⟨k, f⟩ l
Theorem: LO.FirstOrder.UTerm.funcL_primrec'
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
f : L.Func k
l : List (UTerm L μ)
⊢ funcL ⟨k, f⟩ l = funcL ⟨k, f⟩ l
Tactic:
simp[WType.mkL, Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.func_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Tactic:
have h₁ := w_mkFin (β := Edge L μ)
  (fun f => (Sum.inr $ Sum.inr ⟨k, f⟩) : L.Func k → Node L μ)
  (fun _ => Fintype.card_fin k)
  (sum_inr.comp $ sum_inr.comp $ sigma_pair k)
Proof state after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Theorem: LO.FirstOrder.UTerm.func_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Tactic:
have h₂ : Primrec (fun v => (fun i => equivW L μ (v i)) : (Fin k → UTerm L μ) → (Fin k → WType (Edge L μ))) :=
  finArrow_map Primrec.of_equiv k
Proof state after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Theorem: LO.FirstOrder.UTerm.func_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Tactic:
exact (Primrec₂.comp₂ h₁ Primrec₂.left (h₂.comp₂ Primrec₂.right)).of_eq
  (fun a v => by simp[equivW, toW, Edge])
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.func_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
a : L.Func k
v : Fin k → UTerm L μ
⊢ WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) a) ((fintypeArrowEquivFinArrow' ⋯).symm fun i => (equivW L μ) (v i)) =
    (equivW L μ) (func a v)
Tactic:
simp[equivW, toW, Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.elim_eq
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
t : UTerm L μ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
⊢ elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) t =
    WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) t)
Tactic:
induction t <;> simp[elim, WType.elimL_mk, F, *]
Proof state after:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ :
  ∀ (a : Fin arity✝),
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (a✝ a) =
      WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (a✝ a))
⊢ u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn fun i =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
            ((equivW L μ) (a✝ i))) =
    u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b_1 =>
            WType.elimL
              (fun p l =>
                Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
              ((equivW L μ) (a✝ b_1))))
Theorem: LO.FirstOrder.UTerm.elim_eq
Proof state before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ :
  ∀ (a : Fin arity✝),
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (a✝ a) =
      WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (a✝ a))
⊢ u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn fun i =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
            ((equivW L μ) (a✝ i))) =
    u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b_1 =>
            WType.elimL
              (fun p l =>
                Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
              ((equivW L μ) (a✝ b_1))))
Tactic:
{ simp[Edge] }
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.elim_eq
Proof state before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ :
  ∀ (a : Fin arity✝),
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (a✝ a) =
      WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (a✝ a))
⊢ u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn fun i =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
            ((equivW L μ) (a✝ i))) =
    u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b_1 =>
            WType.elimL
              (fun p l =>
                Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
              ((equivW L μ) (a✝ b_1))))
Tactic:
simp[Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.elim_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Tactic:
have hF : Primrec₂ (F b e u) :=
  sum_casesOn (fst.comp snd) (hb.comp₂ (fst.comp₂ Primrec₂.left) Primrec₂.right)
    (sum_casesOn snd (he.comp₂ (fst.comp₂ $ fst.comp₂ $ Primrec₂.left) Primrec₂.right)
      (hu.comp₂ (fst.comp₂ $ fst.comp₂ $ Primrec₂.left) (Primrec₂.pair.comp₂ snd (snd.comp₂ $ snd.comp₂ $ fst.comp₂ $ Primrec₂.left))))
Proof state after:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Theorem: LO.FirstOrder.UTerm.elim_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Tactic:
exact (w_elimL_param hF (Primrec.of_equiv.comp ht)).of_eq (fun x => by simp[elim_eq])
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.elim_primrec_param
Proof state before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
x : σ
⊢ WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (t x)) =
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Tactic:
simp[elim_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.elim_primrec_param_opt
Proof state before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝² : Primcodable σ
inst✝¹ : Inhabited γ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
u : σ → {k : ℕ} → L.Func k → (Fin k → γ) → γ
uOpt : σ → ((k : ℕ) × L.Func k) × List γ → Option γ
hu : Primrec₂ uOpt
ht : Primrec t
H : ∀ (x : σ) {k : ℕ} (f : L.Func k) (v : Fin k → γ), uOpt x (⟨k, f⟩, List.ofFn v) = some (u x f v)
x✝ : σ
⊢ elim (b x✝) (e x✝) (fun {k} f v => (uOpt x✝ (⟨k, f⟩, List.ofFn v)).iget) (t x✝) =
    elim (b x✝) (e x✝) (fun {k} => u x✝) (t x✝)
Tactic:
simp[H]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.elim_primrec_opt
Proof state before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
γ : Type u_1
inst✝¹ : Inhabited γ
inst✝ : Primcodable γ
b : ℕ → γ
e : μ → γ
hb : Primrec b
he : Primrec e
u : {k : ℕ} → L.Func k → (Fin k → γ) → γ
uOpt : (k : ℕ) × L.Func k → List γ → Option γ
hu : Primrec₂ uOpt
H : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → γ), uOpt ⟨k, f⟩ (List.ofFn v) = some (u f v)
t : UTerm L μ
⊢ elim b e (fun {k} f v => (uOpt ⟨k, f⟩ (List.ofFn v)).iget) t = elim b e (fun {k} => u) t
Tactic:
simp[H]
Proof state after:
no goals
Theorem: LO.FirstOrder.UTerm.bv_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
⊢ Primrec bv
Tactic:
have : Primrec (elim (L := L) (μ := μ) Nat.succ (fun _ => 0) fun {k} _ v => (List.ofFn v).sup) :=
  elim_primrec Primrec.succ (Primrec.const 0) ((list_sup nat_max).comp₂ Primrec₂.right)
Proof state after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
⊢ Primrec bv
Theorem: LO.FirstOrder.UTerm.bv_primrec
Proof state before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
⊢ Primrec bv
Tactic:
exact this.of_eq (fun t => by
  induction t <;> simp[elim, bv, *]
  { simp[List.sup_ofFn] })
Proof state after:
no goals