Theorem: Primrec.finArrow_map (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
⊢ Primrec fun v i => f (v i)
Tactic:
have : Primrec (fun e => encode $ ((encodeDecode (Fin k → α) e).bind
  $ fun c => (decode c : Option (List α)).map (fun l => l.map f)) : ℕ → ℕ) :=
  (Primrec.encode.comp $ option_bind Primrec.encodeDecode
    (option_map (Primrec.decode.comp snd) (by apply list_map snd (hf.comp₂ Primrec₂.right))))
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
⊢ Primrec fun v i => f (v i)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
⊢ Primrec fun v i => f (v i)
Tactic:
exact decode_iff.mp (encode_iff.mp $ this.of_eq $ fun e => by
  simp[encodeDecode_eq_encode_map_decode, decode_finArrow]
  rcases (decode e) with (_ | as) <;> simp [Function.comp]
  { rcases (as.toVector k) with (_ | v) <;> simp
    { simp[encode_finArrow, Function.comp] } })
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
⊢ Primrec₂ fun p l => List.map f l
Tactic:
apply list_map snd (hf.comp₂ Primrec₂.right)
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
⊢ encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c)) =
    encode (Option.map (fun v i => f (v i)) (decode e))
Tactic:
simp[encodeDecode_eq_encode_map_decode, decode_finArrow]
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
⊢ encode
      ((Option.map encode ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l))).bind
        fun a => Option.map (fun l => List.map f l) (decode a)) =
    encode
      (Option.map (fun v i => f (v i))
        ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l)))

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
⊢ encode
      ((Option.map encode ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l))).bind
        fun a => Option.map (fun l => List.map f l) (decode a)) =
    encode
      (Option.map (fun v i => f (v i))
        ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l)))
Tactic:
rcases (decode e) with (_ | as) <;> simp [Function.comp]
State after:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
⊢ encode
      ((Option.map (fun x => encode ((Equiv.vectorEquivFin α k) x)) (List.toVector k as)).bind fun a =>
        Option.map (fun l => List.map f l) (decode a)) =
    encode (Option.map (fun x i => f ((Equiv.vectorEquivFin α k) x i)) (List.toVector k as))

State before:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
⊢ encode
      ((Option.map (fun x => encode ((Equiv.vectorEquivFin α k) x)) (List.toVector k as)).bind fun a =>
        Option.map (fun l => List.map f l) (decode a)) =
    encode (Option.map (fun x i => f ((Equiv.vectorEquivFin α k) x i)) (List.toVector k as))
Tactic:
{ rcases (as.toVector k) with (_ | v) <;> simp
  { simp[encode_finArrow, Function.comp] } }
State after:
no goals

State before:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
⊢ encode
      ((Option.map (fun x => encode ((Equiv.vectorEquivFin α k) x)) (List.toVector k as)).bind fun a =>
        Option.map (fun l => List.map f l) (decode a)) =
    encode (Option.map (fun x i => f ((Equiv.vectorEquivFin α k) x i)) (List.toVector k as))
Tactic:
rcases (as.toVector k) with (_ | v) <;> simp
State after:
case some.some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1

State before:
case some.some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1
Tactic:
{ simp[encode_finArrow, Function.comp] }
State after:
no goals

State before:
case some.some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
as : List α
v : Vector α k
⊢ encode (Option.map (fun l => List.map f l) (decode (encode ((Equiv.vectorEquivFin α k) v)))) =
    (encode fun i => f ((Equiv.vectorEquivFin α k) v i)) + 1
Tactic:
simp[encode_finArrow, Function.comp]
State after:
no goals