internlm/Lean-Github huggingface dataset:
Theorem: Primrec.of_list_decode_eq_some_cons
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 τ
a : α
as : List α
e : ℕ
⊢ decode e = some (a :: as) → decode e.pred.unpair.1 = some a ∧ decode e.pred.unpair.2 = some as
Tactic:
rcases e with (_ | e) <;> simp
Proof state after:
case succ
α : 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 τ
a : α
as : List α
e : ℕ
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) = some (a :: as) →
    decode e.unpair.1 = some a ∧ decode e.unpair.2 = some as
Theorem: Primrec.of_list_decode_eq_some_cons
Proof state before:
case succ
α : 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 τ
a : α
as : List α
e : ℕ
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) = some (a :: as) →
    decode e.unpair.1 = some a ∧ decode e.unpair.2 = some as
Tactic:
rcases (decode e.unpair.1) with (_ | a) <;> simp[seq_eq_bind_map, Option.bind_eq_bind]
Proof state after:
case succ.some
α : 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 τ
a✝ : α
as : List α
e : ℕ
a : α
⊢ decode e.unpair.2 = some as → a = a✝ → a = a✝ ∧ decode e.unpair.2 = some as
Theorem: Primrec.of_list_decode_eq_some_cons
Proof state before:
case succ.some
α : 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 τ
a✝ : α
as : List α
e : ℕ
a : α
⊢ decode e.unpair.2 = some as → a = a✝ → a = a✝ ∧ decode e.unpair.2 = some as
Tactic:
rcases (decode e.unpair.2) with (_ | as) <;> simp[seq_eq_bind_map, Option.bind_eq_bind]
Proof state after:
case succ.some.some
α : 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 τ
a✝ : α
as✝ : List α
e : ℕ
a : α
as : List α
⊢ as = as✝ → a = a✝ → a = a✝ ∧ as = as✝
Theorem: Primrec.of_list_decode_eq_some_cons
Proof state before:
case succ.some.some
α : 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 τ
a✝ : α
as✝ : List α
e : ℕ
a : α
as : List α
⊢ as = as✝ → a = a✝ → a = a✝ ∧ as = as✝
Tactic:
rintro rfl rfl
Proof state after:
case succ.some.some
α : 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 τ
e : ℕ
a : α
as : List α
⊢ a = a ∧ as = as
Theorem: Primrec.of_list_decode_eq_some_cons
Proof state before:
case succ.some.some
α : 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 τ
e : ℕ
a : α
as : List α
⊢ a = a ∧ as = as
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec.casesOn_eq_uncurry
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 τ
l : σ → List α
f : σ → β
g : σ → α → List α → β
⊢ (fun x => List.casesOn (l x) (f x) (g x)) = fun x =>
    List.casesOn (l x) (f x) fun a as => Function.uncurry (g x) (a, as)
Tactic:
rfl
Proof state after:
no goals
Theorem: Primrec.decodeZipWithRec_primrec
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 : σ → α × β → γ
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)))))
Proof state after:
no goals
Theorem: Primrec.decodeZipWithRec_primrec
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 : σ → α × β → γ
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₂'
Proof 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)))
Theorem: Primrec.decodeZipWithRec_primrec
Proof 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]
Proof 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)
Theorem: Primrec.decodeZipWithRec_primrec
Proof 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))))
Proof state after:
no goals
Theorem: Primrec.decodeZipWithRec_primrec
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 : σ → α × β → γ
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₂'
Proof 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
Theorem: Primrec.decodeZipWithRec_primrec
Proof 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]
Proof 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
Theorem: Primrec.decodeZipWithRec_primrec
Proof 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]
Proof 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)
Theorem: Primrec.decodeZipWithRec_primrec
Proof 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)))
Proof state after:
no goals
Theorem: Primrec.decodeZipWithRec_primrec
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 : σ → α × β → γ
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
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 : σ → α × β → γ
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
Theorem: Primrec.decodeZipWithRec_primrec
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 : σ → α × β → γ
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))
Proof state after:
no goals
Theorem: Primrec.list_zipWith_param
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 : σ → α × β → γ
hf : Primrec₂ f
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Tactic:
have h : Primrec₂ (fun x p => some (decodeZipWithRec f x p)) := option_some.comp (decodeZipWithRec_primrec hf)
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 : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Theorem: Primrec.list_zipWith_param
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 : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Tactic:
let F : σ → ℕ → Option (List γ) :=
  fun x n => (decode n : Option (List α × List β)).bind
    $ fun p => List.zipWith (fun a b => f x (a, b)) p.1 p.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 : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Theorem: Primrec.list_zipWith_param
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 : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
this : Primrec₂ F
⊢ Primrec₂ fun x p => List.zipWith (fun a b => f x (a, b)) p.1 p.2
Tactic:
exact Primrec₂.decode_iff₂.mp (this.of_eq $ fun x e => by simp only [Option.map_eq_bind]; rfl)
Proof state after:
no goals
Theorem: Primrec.list_zipWith_param
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 : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
⊢ some (Primrec.decodeZipWithRec f (x, e) (List.map (F x) (List.range e))) = some (F x e)
Tactic:
simp only [decodeZipWithRec, decode_prod_val, encode_prod_val, encode_nat, List.get?_map,
  Option.map_map, Option.some.injEq]
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 : σ → α × β → γ
hf : Primrec₂ f
h : Primrec₂ fun x p => some (Primrec.decodeZipWithRec f x p)
F : σ → ℕ → Option (List γ) := fun x n => (decode n).bind fun p => some (List.zipWith (fun a b => f x (a, b)) p.1 p.2)
x : σ
e : ℕ
⊢ (((decode e.unpair.1).bind fun a => Option.map (Prod.mk a) (decode e.unpair.2)).bind fun a =>
      List.rec (some [])
        (fun head tail tail_ih =>
          List.rec (some [])
            (fun head_1 tail tail_ih =>
              Option.map ((fun cs => f x (head, head_1) :: cs.iget) ∘ F x)
                ((List.range e).get? (e.unpair.1.pred.unpair.2.pair e.unpair.2.pred.unpair.2)))
            a.2)
        a.1) =
    F x e