awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
g : β → α → α
hg : Primrec₂ g
l : List α
b : β
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (l, b).1 [] fun (b_1 : α) (l_1 : List α) ↦
      g ((l, b), b_1, l_1).1.2 ((l, b), b_1, l_1).2.1 :: ((l, b), b_1, l_1).2.2) =
    List.modifyHead (g b) l
have nil : (List.casesOn (motive := fun (x : List α) ↦ List α) ([], b).1 [] fun (b_1 : α) (l : List α) ↦
    g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
  List.modifyHead (g b) []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
g : β → α → α
hg : Primrec₂ g
l : List α
b : β
nil :
  (List.casesOn (motive := fun (x : List α) ↦ List α) ([], b).1 [] fun (b_1 : α) (l : List α) ↦
      g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
    List.modifyHead (g b) []
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (l, b).1 [] fun (b_1 : α) (l_1 : List α) ↦
      g ((l, b), b_1, l_1).1.2 ((l, b), b_1, l_1).2.1 :: ((l, b), b_1, l_1).2.2) =
    List.modifyHead (g b) l
have cons : ∀ (head : α) (tail : List α),
  (List.casesOn (motive := fun (x : List α) ↦ List α) (head :: tail, b).1 [] fun (b_1 : α) (l : List α) ↦
      g ((head :: tail, b), b_1, l).1.2 ((head :: tail, b), b_1, l).2.1 :: ((head :: tail, b), b_1, l).2.2) =
    List.modifyHead (g b) (head :: tail)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec (β := List ℕ) fun (n : ℕ) ↦ filter (fun (y : ℕ) ↦ decide (R y n)) (range s)
have simp : Primrec (β := List ℕ) fun (n : ℕ) ↦ filterMap (Option.guard fun (y : ℕ) ↦ decide (R y n)) (range s)
Tactic: simp only [← filterMap_eq_filter]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec (β := List ℕ) fun (n : ℕ) ↦ filterMap (Option.guard fun (y : ℕ) ↦ decide (R y n)) (range s)
have refine : Primrec₂ (β := ℕ) (σ := Option ℕ) fun (n : ℕ) ↦ Option.guard fun (y : ℕ) ↦ decide (R y n)
Tactic: refine listFilterMap (.const (range s)) ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec₂ (β := ℕ) (σ := Option ℕ) fun (n : ℕ) ↦ Option.guard fun (y : ℕ) ↦ decide (R y n)
have refine : Primrec (β := Bool) fun (p : ℕ × ℕ) ↦ (fun (y : ℕ) ↦ decide (R y p.1)) p.2
Tactic: refine ite (Primrec.eq.comp ?_ (const true)) (option_some_iff.mpr snd) (.const Option.none)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filter (fun (a : α) ↦ decide (R a b)) L
have simp : Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filterMap (Option.guard fun (a : α) ↦ decide (R a b)) L
Tactic: simp only [← List.filterMap_eq_filter]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filterMap (Option.guard fun (a : α) ↦ decide (R a b)) L
have refine_1 : PrimrecPred fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ (fun (a : α) ↦ decide (R a p.1.2)) p.2 = true
Tactic: refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
refine_1 : PrimrecPred fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ (fun (a : α) ↦ decide (R a p.1.2)) p.2 = true
⊢ Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filterMap (Option.guard fun (a : α) ↦ decide (R a b)) L
have refine_2 : Primrec (β := Option α) fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ some p.2
Tactic: refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
Tactic: have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have refine : PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = 0
Tactic: refine .of_eq (.not ?_) h
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
Tactic: classical
  have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
  refine .of_eq (.not ?_) h
  exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have have₁ : ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
  PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
Tactic: classical
  have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
  refine .of_eq (.not ?_) h
  exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
have₁ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have₂ : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
have₃ have₄ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have have₅ : ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
  PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = 0
Tactic: classical
  have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
  refine .of_eq (.not ?_) h
  exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
Tactic: have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have apply : PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = a.length
Tactic: apply PrimrecRel.of_eq ?_ h
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
Tactic: classical
  have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
  apply PrimrecRel.of_eq ?_ h
  exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have have₁ : ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
  PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
Tactic: classical
  have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
  apply PrimrecRel.of_eq ?_ h
  exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
have₁ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have₂ : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
have₃ have₄ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have have₅ : ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
  PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = a.length
Tactic: classical
  have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
  apply PrimrecRel.of_eq ?_ h
  exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
x : List.Vector α n
l : List α
h : l.length = n
⊢ (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h)).tail =
    List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h))
have nil : ∀ (h : List.length.{u_1} (α := α) [] = n),
  Eq.{u_1 + 1} (α := List α)
    (List.tail (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
    (List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
x : List.Vector α n
l : List α
h : l.length = n
nil :
  ∀ (h : List.length.{u_1} (α := α) [] = n),
    Eq.{u_1 + 1} (α := List α)
      (List.tail (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
      (List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
⊢ (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h)).tail =
    List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h))
have cons : ∀ (head : α) (tail : List α) (h : (head :: tail).length = n),
  (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)).tail =
    List.Vector.toList (n := n - 1)
      (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h))
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
⊢ List.Vector.get (List.Vector.ofFn fun (i : Fin n) ↦ f a i) = f a
have h₁ : ∀ (i : Fin n), List.Vector.get (List.Vector.ofFn fun (i : Fin n) ↦ f a i) i = f a i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
⊢ Primrec f
have zero : Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0
Tactic: induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
zero : Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0
⊢ Primrec f
have succ : Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ
Tactic: induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
zero : Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0
succ : Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ
⊢ Primrec f
have get : ∀ {n : ℕ} (i : Fin n), Primrec (β := ℕ) fun (v : List.Vector ℕ n) ↦ v.get i
Tactic: induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
zero : Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0
succ : Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ
get : ∀ {n : ℕ} (i : Fin n), Primrec (β := ℕ) fun (v : List.Vector ℕ n) ↦ v.get i
⊢ Primrec f
have comp : ∀ {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ),
  Primrec' f →
    (∀ (i : Fin n), Primrec' (g i)) →
      ∀ (hf : Primrec f) (hg : ∀ (i : Fin n), Primrec (g i)),
        Primrec (β := ℕ) fun (a : List.Vector ℕ m) ↦ f (ofFn fun (i : Fin n) ↦ g i a)
Tactic: induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
zero : Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0
succ : Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ
get : ∀ {n : ℕ} (i : Fin n), Primrec (β := ℕ) fun (v : List.Vector ℕ n) ↦ v.get i
comp :
  ∀ {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ),
    Primrec' f →
      (∀ (i : Fin n), Primrec' (g i)) →
        ∀ (hf : Primrec f) (hg : ∀ (i : Fin n), Primrec (g i)),
          Primrec (β := ℕ) fun (a : List.Vector ℕ m) ↦ f (ofFn fun (i : Fin n) ↦ g i a)
⊢ Primrec f
have prec : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ},
  Primrec' f →
    Primrec' g →
      ∀ (hf : Primrec f) (hg : Primrec g),
        Primrec (β := ℕ) fun (v : List.Vector ℕ (n + 1)) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic: induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun (i : Fin n) ↦ v.get i.succ) = f v.tail
have rw : f (ofFn fun (i : Fin n) ↦ v.get i.succ) = f (ofFn v.tail.get)
Tactic: rw [← ofFn_get v.tail]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun (i : Fin n) ↦ v.get i.succ) = f (ofFn v.tail.get)
have e_a : (fun (i : Fin n) ↦ v.get i.succ) = v.tail.get
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ (fun (i : Fin n) ↦ v.get i.succ) = v.tail.get
have e_a : ∀ (i : Fin n), v.get i.succ = v.tail.get i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v).head) v.head = v.head.pred
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) v.head = v.head - 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) v.head = v.head - 1
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) 0 = HSub.hSub (α := ℕ) 0 1
Tactic: cases v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0)
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) 0 = HSub.hSub (α := ℕ) 0 1
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) v.head = v.head - 1
have succ : ∀ (n : ℕ), Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) (n + 1) = n + 1 - 1
Tactic: cases v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.succ) v.head =
    v.head + v.tail.head
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) v.head = v.head + v.tail.head
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) v.head = v.head + v.tail.head
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) 0 = 0 + v.tail.head
Tactic: induction v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) 0 = 0 + v.tail.head
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) v.head = v.head + v.tail.head
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) n = n + v.tail.head →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) (n + 1) = n + 1 + v.tail.head
Tactic: induction v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ (fun (a b : ℕ) ↦ b - a) v.head v.tail.head
have refine : ∀ (v : List.Vector ℕ (Nat.succ 0 + 1)),
  Eq (α := ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.pred) v.head : ℕ)
    ((fun (a b : ℕ) ↦ b - a) v.head v.tail.head : ℕ)
Tactic: refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Eq (α := ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.pred) v.head : ℕ)
    ((fun (a b : ℕ) ↦ b - a) v.head v.tail.head : ℕ)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) v.head = v.tail.head - v.head
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) v.head = v.tail.head - v.head
have zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) 0 = v.tail.head - 0
Tactic: induction v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) 0 = v.tail.head - 0
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) v.head = v.tail.head - v.head
have succ : ∀ (n : ℕ),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) n = v.tail.head - n →
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH - 1) (n + 1) = v.tail.head - (n + 1)
Tactic: induction v.head
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
Goal:
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ v.head - v.tail.head
have this : Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ (fun (a b : ℕ) ↦ b - a) v.head v.tail.head
Tactic: have : @Primrec' 2 fun v ↦ (fun a b ↦ b - a) v.head v.tail.head := by
    refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_
    simp; induction v.head <;> simp [*, Nat.sub_add_eq]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.tail.head + (y ::ᵥ IH ::ᵥ v.tail).tail.head) v.head =
    v.head * v.tail.head
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ v.tail.head + IH) v.head = v.head * v.tail.head
Tactic: simp