Theorem: Primrec.decodeZipWithRec_primrec (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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ (Primrec.decodeZipWithRec f)
Tactic:
exact option_bind (Primrec.decode.comp $ snd.comp fst)
  (by apply to₂'; rw[casesOn_eq_uncurry]
      apply list_casesOn (fst.comp snd) (Primrec.const _)
        (by apply to₂'; simp[Function.uncurry]; rw[casesOn_eq_uncurry]
            apply list_casesOn (snd.comp $ snd.comp fst) (const _)
              (by unfold Function.uncurry
                  apply option_map (list_get?.comp (snd.comp $ fst.comp $ fst.comp fst)
                    (Primrec₂.natPair.comp
                      (snd.comp $ unpair.comp $ pred.comp $ fst.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
                      (snd.comp $ unpair.comp $ pred.comp $ snd.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)))
                    (list_cons.comp₂
                      (hf.comp₂
                        (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ Primrec₂.left)
                        (Primrec₂.pair.comp₂
                          (fst.comp₂ $ snd.comp₂ $ fst.comp₂ Primrec₂.left)
                          (fst.comp₂ $ snd.comp₂ Primrec₂.left)))
                      (option_iget.comp₂ Primrec₂.right)))))
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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun p l =>
    List.casesOn l.1 (some []) fun a x =>
      List.casesOn l.2 (some []) fun b x =>
        Option.map (fun cs => f p.1.1 (a, b) :: cs.iget)
          (p.2.get? (encode (p.1.2.unpair.1.pred.unpair.2, p.1.2.unpair.2.pred.unpair.2)))
Tactic:
apply to₂'
State after:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun p =>
    List.casesOn p.2.1 (some []) fun a x =>
      List.casesOn p.2.2 (some []) fun b x =>
        Option.map (fun cs => f p.1.1.1 (a, b) :: cs.iget)
          (p.1.2.get? (encode (p.1.1.2.unpair.1.pred.unpair.2, p.1.1.2.unpair.2.pred.unpair.2)))

State before:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun p =>
    List.casesOn p.2.1 (some []) fun a x =>
      List.casesOn p.2.2 (some []) fun b x =>
        Option.map (fun cs => f p.1.1.1 (a, b) :: cs.iget)
          (p.1.2.get? (encode (p.1.1.2.unpair.1.pred.unpair.2, p.1.1.2.unpair.2.pred.unpair.2)))
Tactic:
rw[casesOn_eq_uncurry]
State after:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun x =>
    List.casesOn x.2.1 (some []) fun a as =>
      Function.uncurry
        (fun head tail =>
          (fun a x_1 =>
              List.casesOn x.2.2 (some []) fun b x_2 =>
                Option.map (fun cs => f x.1.1.1 (a, b) :: cs.iget)
                  (x.1.2.get? (encode (x.1.1.2.unpair.1.pred.unpair.2, x.1.1.2.unpair.2.pred.unpair.2))))
            head tail)
        (a, as)

State before:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun x =>
    List.casesOn x.2.1 (some []) fun a as =>
      Function.uncurry
        (fun head tail =>
          (fun a x_1 =>
              List.casesOn x.2.2 (some []) fun b x_2 =>
                Option.map (fun cs => f x.1.1.1 (a, b) :: cs.iget)
                  (x.1.2.get? (encode (x.1.1.2.unpair.1.pred.unpair.2, x.1.1.2.unpair.2.pred.unpair.2))))
            head tail)
        (a, as)
Tactic:
apply list_casesOn (fst.comp snd) (Primrec.const _)
  (by apply to₂'; simp[Function.uncurry]; rw[casesOn_eq_uncurry]
      apply list_casesOn (snd.comp $ snd.comp fst) (const _)
        (by unfold Function.uncurry
            apply option_map (list_get?.comp (snd.comp $ fst.comp $ fst.comp fst)
              (Primrec₂.natPair.comp
                (snd.comp $ unpair.comp $ pred.comp $ fst.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
                (snd.comp $ unpair.comp $ pred.comp $ snd.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)))
              (list_cons.comp₂
                (hf.comp₂
                  (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ Primrec₂.left)
                  (Primrec₂.pair.comp₂
                    (fst.comp₂ $ snd.comp₂ $ fst.comp₂ Primrec₂.left)
                    (fst.comp₂ $ snd.comp₂ Primrec₂.left)))
                (option_iget.comp₂ Primrec₂.right))))
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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun a =>
    Function.uncurry fun head tail =>
      (fun a_1 x =>
          List.casesOn a.2.2 (some []) fun b x =>
            Option.map (fun cs => f a.1.1.1 (a_1, b) :: cs.iget)
              (a.1.2.get? (encode (a.1.1.2.unpair.1.pred.unpair.2, a.1.1.2.unpair.2.pred.unpair.2))))
        head tail
Tactic:
apply to₂'
State after:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun p =>
    Function.uncurry
      (fun head tail =>
        (fun a x =>
            List.casesOn p.1.2.2 (some []) fun b x =>
              Option.map (fun cs => f p.1.1.1.1 (a, b) :: cs.iget)
                (p.1.1.2.get? (encode (p.1.1.1.2.unpair.1.pred.unpair.2, p.1.1.1.2.unpair.2.pred.unpair.2))))
          head tail)
      p.2

State before:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun p =>
    Function.uncurry
      (fun head tail =>
        (fun a x =>
            List.casesOn p.1.2.2 (some []) fun b x =>
              Option.map (fun cs => f p.1.1.1.1 (a, b) :: cs.iget)
                (p.1.1.2.get? (encode (p.1.1.1.2.unpair.1.pred.unpair.2, p.1.1.1.2.unpair.2.pred.unpair.2))))
          head tail)
      p.2
Tactic:
simp[Function.uncurry]
State after:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun p =>
    List.rec (some [])
      (fun head tail tail_ih =>
        Option.map (fun cs => f p.1.1.1.1 (p.2.1, head) :: cs.iget)
          (p.1.1.2.get? ((p.1.1.1.2.unpair.1 - 1).unpair.2.pair (p.1.1.1.2.unpair.2 - 1).unpair.2)))
      p.1.2.2

State before:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun p =>
    List.rec (some [])
      (fun head tail tail_ih =>
        Option.map (fun cs => f p.1.1.1.1 (p.2.1, head) :: cs.iget)
          (p.1.1.2.get? ((p.1.1.1.2.unpair.1 - 1).unpair.2.pair (p.1.1.1.2.unpair.2 - 1).unpair.2)))
      p.1.2.2
Tactic:
rw[casesOn_eq_uncurry]
State after:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun x =>
    List.casesOn x.1.2.2 (some []) fun a as =>
      Function.uncurry
        (fun head tail =>
          Option.map (fun cs => f x.1.1.1.1 (x.2.1, head) :: cs.iget)
            (x.1.1.2.get? ((x.1.1.1.2.unpair.1 - 1).unpair.2.pair (x.1.1.1.2.unpair.2 - 1).unpair.2)))
        (a, as)

State before:
case hf
α : 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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec fun x =>
    List.casesOn x.1.2.2 (some []) fun a as =>
      Function.uncurry
        (fun head tail =>
          Option.map (fun cs => f x.1.1.1.1 (x.2.1, head) :: cs.iget)
            (x.1.1.2.get? ((x.1.1.1.2.unpair.1 - 1).unpair.2.pair (x.1.1.1.2.unpair.2 - 1).unpair.2)))
        (a, as)
Tactic:
apply list_casesOn (snd.comp $ snd.comp fst) (const _)
  (by unfold Function.uncurry
      apply option_map (list_get?.comp (snd.comp $ fst.comp $ fst.comp fst)
        (Primrec₂.natPair.comp
          (snd.comp $ unpair.comp $ pred.comp $ fst.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
          (snd.comp $ unpair.comp $ pred.comp $ snd.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)))
        (list_cons.comp₂
          (hf.comp₂
            (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ Primrec₂.left)
            (Primrec₂.pair.comp₂
              (fst.comp₂ $ snd.comp₂ $ fst.comp₂ Primrec₂.left)
              (fst.comp₂ $ snd.comp₂ Primrec₂.left)))
          (option_iget.comp₂ Primrec₂.right)))
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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun a =>
    Function.uncurry fun head tail =>
      Option.map (fun cs => f a.1.1.1.1 (a.2.1, head) :: cs.iget)
        (a.1.1.2.get? ((a.1.1.1.2.unpair.1 - 1).unpair.2.pair (a.1.1.1.2.unpair.2 - 1).unpair.2))
Tactic:
unfold Function.uncurry
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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun a a_1 =>
    (fun head tail =>
        Option.map (fun cs => f a.1.1.1.1 (a.2.1, head) :: cs.iget)
          (a.1.1.2.get? ((a.1.1.1.2.unpair.1 - 1).unpair.2.pair (a.1.1.1.2.unpair.2 - 1).unpair.2)))
      a_1.1 a_1.2

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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun a a_1 =>
    (fun head tail =>
        Option.map (fun cs => f a.1.1.1.1 (a.2.1, head) :: cs.iget)
          (a.1.1.2.get? ((a.1.1.1.2.unpair.1 - 1).unpair.2.pair (a.1.1.1.2.unpair.2 - 1).unpair.2)))
      a_1.1 a_1.2
Tactic:
apply option_map (list_get?.comp (snd.comp $ fst.comp $ fst.comp fst)
  (Primrec₂.natPair.comp
    (snd.comp $ unpair.comp $ pred.comp $ fst.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
    (snd.comp $ unpair.comp $ pred.comp $ snd.comp $ unpair.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)))
  (list_cons.comp₂
    (hf.comp₂
      (fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ fst.comp₂ $ Primrec₂.left)
      (Primrec₂.pair.comp₂
        (fst.comp₂ $ snd.comp₂ $ fst.comp₂ Primrec₂.left)
        (fst.comp₂ $ snd.comp₂ Primrec₂.left)))
    (option_iget.comp₂ Primrec₂.right))
State after:
no goals