Theorem: Primrec.option_list_mapM' (Logic/Vorspiel/Computability.lean)

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))
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)

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)
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)

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
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)

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] }
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)

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])
State after:
no goals

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
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

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, *]
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)

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] }
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals