internlm/Lean-Github huggingface dataset:
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this : Primrec₂ g'
⊢ Primrec₂ f
Tactic:
have : Primrec₂ (fun a n => f a n.unpair : α → ℕ → σ) := nat_strong_rec' (fun a n => f a n.unpair : α → ℕ → σ) this (fun a n => by simpa using H a n.unpair.1 n.unpair.2)
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this✝ : Primrec₂ g'
this : Primrec₂ fun a n => f a n.unpair
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this✝ : Primrec₂ g'
this : Primrec₂ fun a n => f a n.unpair
⊢ Primrec₂ f
Tactic:
have : Primrec₂ (fun a p => (fun a n => f a n.unpair : α → ℕ → σ) a (p.1.pair p.2) : α → ℕ × ℕ → σ) :=
  this.comp₂ Primrec₂.left (Primrec₂.natPair.comp (fst.comp snd) (snd.comp snd))
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this✝¹ : Primrec₂ g'
this✝ : Primrec₂ fun a n => f a n.unpair
this : Primrec₂ fun a p => (fun a n => f a n.unpair) a (p.1.pair p.2)
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this✝¹ : Primrec₂ g'
this✝ : Primrec₂ fun a n => f a n.unpair
this : Primrec₂ fun a p => (fun a n => f a n.unpair) a (p.1.pair p.2)
⊢ Primrec₂ f
Tactic:
exact this.of_eq (by simp)
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this : Primrec₂ g'
a : α
n : ℕ
⊢ g' (a, n) (List.map ((fun a n => f a n.unpair) a) (List.range n)) = some ((fun a n => f a n.unpair) a n)
Tactic:
simpa using H a n.unpair.1 n.unpair.2
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'2
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ × ℕ → σ
g : α × ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun i => f a i.unpair) (List.range (n.pair m))) = some (f a (n, m))
g' : α × ℕ → List σ → Option σ :=
  fun x =>
    match (motive := α × ℕ → List σ → Option σ) x with
    | (a, n) => g (a, n.unpair)
this✝¹ : Primrec₂ g'
this✝ : Primrec₂ fun a n => f a n.unpair
this : Primrec₂ fun a p => (fun a n => f a n.unpair) a (p.1.pair p.2)
⊢ ∀ (a : α) (b : ℕ × ℕ), (fun a n => f a n.unpair) a (b.1.pair b.2) = f a b
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'2'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
⊢ Primrec₂ f
Tactic:
have : Primrec₂ (fun p => g p.2 : Unit × (ℕ × ℕ) → List σ → Option σ) := hg.comp (snd.comp fst) snd
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this : Primrec₂ fun p => g p.2
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'2'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this : Primrec₂ fun p => g p.2
⊢ Primrec₂ f
Tactic:
have := nat_strong_rec'2 (fun _ i => f i.1 i.2 : Unit → ℕ × ℕ → σ) this (by simpa using H)
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝ : Primrec₂ fun p => g p.2
this : Primrec₂ fun x i => f i.1 i.2
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'2'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝ : Primrec₂ fun p => g p.2
this : Primrec₂ fun x i => f i.1 i.2
⊢ Primrec₂ f
Tactic:
have : Primrec₂ (fun n m => (fun _ i => f i.1 i.2 : Unit → ℕ × ℕ → σ) () (n, m)) := this.comp (const ()) Primrec.id
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ Primrec₂ f
Theorem: Primrec.nat_strong_rec'2'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ Primrec₂ f
Tactic:
exact this.of_eq (by simp)
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'2'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this : Primrec₂ fun p => g p.2
⊢ ∀ (a : Unit) (n m : ℕ),
    g (a, n, m).2 (List.map (fun i => (fun x i => f i.1 i.2) a i.unpair) (List.range (n.pair m))) =
      some ((fun x i => f i.1 i.2) a (n, m))
Tactic:
simpa using H
Proof state after:
no goals
Theorem: Primrec.nat_strong_rec'2'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ ∀ (a b : ℕ), (fun x i => f i.1 i.2) () (a, b) = f a b
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
⊢ Primrec fun a => mapM' (g a) (f a)
Tactic:
have : Primrec₂ (fun a p => (g a p.1).bind $ fun c => p.2.2.map $ fun l => c :: l : α → β × List β × Option (List γ) → Option (List γ)) :=
  Primrec.option_bind (hg.comp fst (fst.comp snd)) (Primrec.option_map (snd.comp $ snd.comp $ snd.comp fst) (Primrec.list_cons.comp₂ (snd.comp fst) Primrec₂.right))
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
⊢ Primrec fun a => mapM' (g a) (f a)
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
⊢ Primrec fun a => mapM' (g a) (f a)
Tactic:
let F : α → Option (List γ) := fun a => List.recOn (f a) (some []) (fun b _ ih => (g a b).bind $ fun c => ih.map $ fun l => c :: l)
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
⊢ Primrec fun a => mapM' (g a) (f a)
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
⊢ Primrec fun a => mapM' (g a) (f a)
Tactic:
have : Primrec F := Primrec.list_rec hf (const (some [] : Option (List γ))) this
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
⊢ Primrec fun a => mapM' (g a) (f a)
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
⊢ Primrec fun a => mapM' (g a) (f a)
Tactic:
have e : ∀ (k : β → Option γ) (bs : List β),
  List.recOn bs (some [] : Option (List γ)) (fun b _ ih => (k b).bind $ fun c => ih.map $ fun l => c :: l) = bs.mapM' k := by
  intro k bs
  induction bs <;> simp[Option.pure_eq_some, Option.bind_eq_bind, *]
  { simp[Option.map_eq_bind, Function.comp] }
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
e :
  ∀ (k : β → Option γ) (bs : List β),
    (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
⊢ Primrec fun a => mapM' (g a) (f a)
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
e :
  ∀ (k : β → Option γ) (bs : List β),
    (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
⊢ Primrec fun a => mapM' (g a) (f a)
Tactic:
exact this.of_eq (by simp [F, e])
Proof state after:
no goals
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
⊢ ∀ (k : β → Option γ) (bs : List β),
    (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
Tactic:
intro k bs
Proof state after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
k : β → Option γ
bs : List β
⊢ (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
k : β → Option γ
bs : List β
⊢ (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
Tactic:
induction bs <;> simp[Option.pure_eq_some, Option.bind_eq_bind, *]
Proof state after:
case cons
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
k : β → Option γ
head✝ : β
tail✝ : List β
tail_ih✝ :
  (List.recOn tail✝ (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k tail✝
⊢ ((k head✝).bind fun a => Option.map (fun l => a :: l) (mapM' k tail✝)) =
    (k head✝).bind fun __do_lift => (mapM' k tail✝).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
Theorem: Primrec.option_list_mapM'
Proof state before:
case cons
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
k : β → Option γ
head✝ : β
tail✝ : List β
tail_ih✝ :
  (List.recOn tail✝ (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k tail✝
⊢ ((k head✝).bind fun a => Option.map (fun l => a :: l) (mapM' k tail✝)) =
    (k head✝).bind fun __do_lift => (mapM' k tail✝).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
Tactic:
{ simp[Option.map_eq_bind, Function.comp] }
Proof state after:
no goals
Theorem: Primrec.option_list_mapM'
Proof state before:
case cons
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
k : β → Option γ
head✝ : β
tail✝ : List β
tail_ih✝ :
  (List.recOn tail✝ (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k tail✝
⊢ ((k head✝).bind fun a => Option.map (fun l => a :: l) (mapM' k tail✝)) =
    (k head✝).bind fun __do_lift => (mapM' k tail✝).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
Tactic:
simp[Option.map_eq_bind, Function.comp]
Proof state after:
no goals
Theorem: Primrec.option_list_mapM'
Proof state before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → List β
g : α → β → Option γ
hf : Primrec f
hg : Primrec₂ g
this✝ : Primrec₂ fun a p => (g a p.1).bind fun c => Option.map (fun l => c :: l) p.2.2
F : α → Option (List γ) :=
  fun a => List.recOn (f a) (some []) fun b x ih => (g a b).bind fun c => Option.map (fun l => c :: l) ih
this : Primrec F
e :
  ∀ (k : β → Option γ) (bs : List β),
    (List.recOn bs (some []) fun b x ih => (k b).bind fun c => Option.map (fun l => c :: l) ih) = mapM' k bs
⊢ ∀ (n : α), F n = mapM' (g n) (f n)
Tactic:
simp [F, e]
Proof state after:
no goals