[GOAL]
n : ℕ
⊢ Nat.pair (unpair n).fst (unpair n).snd = id n
[PROOFSTEP]
simp
[GOAL]
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
n : ℕ
⊢ unpaired (fun z n => Nat.rec m (fun y IH => f (unpair (Nat.pair z (Nat.pair y IH))).snd) n) (Nat.pair 0 (id n)) =
    Nat.rec m (fun y IH => f (Nat.pair y IH)) n
[PROOFSTEP]
simp
[GOAL]
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
⊢ ∀ (n : ℕ), Nat.rec m (fun y IH => f (unpair (Nat.pair y IH)).fst) n = Nat.casesOn n m f
[PROOFSTEP]
simp
[GOAL]
f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
n : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec (f z)
          (fun y IH =>
            g
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).fst
                (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).fst))
          n)
      n =
    unpaired (fun z n => Nat.casesOn n (f z) fun y => g (Nat.pair z y)) n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ Nat.pair (unpair n).snd (unpair n).fst = unpaired (swap Nat.pair) n
[PROOFSTEP]
simp
[GOAL]
f : ℕ → ℕ → ℕ
hf : Nat.Primrec (unpaired f)
n : ℕ
⊢ unpaired f (unpaired (swap Nat.pair) n) = unpaired (swap f) n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ Nat.casesOn n 0 id = Nat.pred n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ Nat.casesOn Nat.zero 0 id = Nat.pred Nat.zero
[PROOFSTEP]
simp [*]
[GOAL]
case succ
n✝ : ℕ
⊢ Nat.casesOn (succ n✝) 0 id = Nat.pred (succ n✝)
[PROOFSTEP]
simp [*]
[GOAL]
p : ℕ
⊢ unpaired (fun z n => Nat.rec (id z) (fun y IH => succ (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).snd) n) p =
    unpaired (fun x x_1 => x + x_1) p
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ Nat.rec (unpair p).fst (fun y IH => succ IH) (unpair p).snd = (unpair p).fst + (unpair p).snd
[PROOFSTEP]
induction p.unpair.2
[GOAL]
case zero
p : ℕ
⊢ Nat.rec (unpair p).fst (fun y IH => succ IH) Nat.zero = (unpair p).fst + Nat.zero
[PROOFSTEP]
simp [*, add_succ]
[GOAL]
case succ
p n✝ : ℕ
n_ih✝ : Nat.rec (unpair p).fst (fun y IH => succ IH) n✝ = (unpair p).fst + n✝
⊢ Nat.rec (unpair p).fst (fun y IH => succ IH) (succ n✝) = (unpair p).fst + succ n✝
[PROOFSTEP]
simp [*, add_succ]
[GOAL]
p : ℕ
⊢ unpaired (fun z n => Nat.rec (id z) (fun y IH => Nat.pred (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).snd) n)
      p =
    unpaired (fun x x_1 => x - x_1) p
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ Nat.rec (unpair p).fst (fun y IH => Nat.pred IH) (unpair p).snd = (unpair p).fst - (unpair p).snd
[PROOFSTEP]
induction p.unpair.2
[GOAL]
case zero
p : ℕ
⊢ Nat.rec (unpair p).fst (fun y IH => Nat.pred IH) Nat.zero = (unpair p).fst - Nat.zero
[PROOFSTEP]
simp [*, sub_succ]
[GOAL]
case succ
p n✝ : ℕ
n_ih✝ : Nat.rec (unpair p).fst (fun y IH => Nat.pred IH) n✝ = (unpair p).fst - n✝
⊢ Nat.rec (unpair p).fst (fun y IH => Nat.pred IH) (succ n✝) = (unpair p).fst - succ n✝
[PROOFSTEP]
simp [*, sub_succ]
[GOAL]
p : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec 0
          (fun y IH =>
            unpaired (fun x x_1 => x + x_1)
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).fst
                (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).snd))
          n)
      p =
    unpaired (fun x x_1 => x * x_1) p
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ Nat.rec 0 (fun y IH => (unpair p).fst + IH) (unpair p).snd = (unpair p).fst * (unpair p).snd
[PROOFSTEP]
induction p.unpair.2
[GOAL]
case zero
p : ℕ
⊢ Nat.rec 0 (fun y IH => (unpair p).fst + IH) Nat.zero = (unpair p).fst * Nat.zero
[PROOFSTEP]
simp [*, mul_succ, add_comm _ (unpair p).fst]
[GOAL]
case succ
p n✝ : ℕ
n_ih✝ : Nat.rec 0 (fun y IH => (unpair p).fst + IH) n✝ = (unpair p).fst * n✝
⊢ Nat.rec 0 (fun y IH => (unpair p).fst + IH) (succ n✝) = (unpair p).fst * succ n✝
[PROOFSTEP]
simp [*, mul_succ, add_comm _ (unpair p).fst]
[GOAL]
p : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec 1
          (fun y IH =>
            unpaired (fun x x_1 => x * x_1)
              (Nat.pair (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).snd
                (unpair (Nat.pair z (Nat.pair y IH))).fst))
          n)
      p =
    unpaired (fun x x_1 => x ^ x_1) p
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ Nat.rec 1 (fun y IH => IH * (unpair p).fst) (unpair p).snd = (unpair p).fst ^ (unpair p).snd
[PROOFSTEP]
induction p.unpair.2
[GOAL]
case zero
p : ℕ
⊢ Nat.rec 1 (fun y IH => IH * (unpair p).fst) Nat.zero = (unpair p).fst ^ Nat.zero
[PROOFSTEP]
simp [*, pow_succ]
[GOAL]
case succ
p n✝ : ℕ
n_ih✝ : Nat.rec 1 (fun y IH => IH * (unpair p).fst) n✝ = (unpair p).fst ^ n✝
⊢ Nat.rec 1 (fun y IH => IH * (unpair p).fst) (succ n✝) = (unpair p).fst ^ succ n✝
[PROOFSTEP]
simp [*, pow_succ]
[GOAL]
α : Type ?u.12281
inst✝ : Denumerable α
⊢ ∀ (n : ℕ), Nat.succ n = encode (decode n)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.13346
β : Type ?u.13353
inst✝ : Primcodable α
e : β ≃ α
src✝ : Encodable β := Encodable.ofEquiv α e
n : ℕ
⊢ encode (decode n) = encode (decode n)
[PROOFSTEP]
rw [decode_ofEquiv]
[GOAL]
α : Type ?u.13346
β : Type ?u.13353
inst✝ : Primcodable α
e : β ≃ α
src✝ : Encodable β := Encodable.ofEquiv α e
n : ℕ
⊢ encode (decode n) = encode (Option.map (↑e.symm) (decode n))
[PROOFSTEP]
cases (@decode α _ n)
[GOAL]
case none
α : Type ?u.13346
β : Type ?u.13353
inst✝ : Primcodable α
e : β ≃ α
src✝ : Encodable β := Encodable.ofEquiv α e
n : ℕ
⊢ encode none = encode (Option.map (↑e.symm) none)
[PROOFSTEP]
simp [encode_ofEquiv]
[GOAL]
case some
α : Type ?u.13346
β : Type ?u.13353
inst✝ : Primcodable α
e : β ≃ α
src✝ : Encodable β := Encodable.ofEquiv α e
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map (↑e.symm) (some val✝))
[PROOFSTEP]
simp [encode_ofEquiv]
[GOAL]
n : ℕ
⊢ (Nat.casesOn n 1 fun x => 0) = encode (decode n)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ (Nat.casesOn Nat.zero 1 fun x => 0) = encode (decode Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ (Nat.casesOn (Nat.succ n✝) 1 fun x => 0) = encode (decode (Nat.succ n✝))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn n 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) = encode (decode n)
[PROOFSTEP]
cases n with
| zero => rfl
| succ n =>
  rw [decode_option_succ]
  cases H : @decode α _ n <;> simp [H]
[GOAL]
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn n 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) = encode (decode n)
[PROOFSTEP]
cases n with
| zero => rfl
| succ n =>
  rw [decode_option_succ]
  cases H : @decode α _ n <;> simp [H]
[GOAL]
case zero
α : Type u_1
h : Primcodable α
⊢ (Nat.casesOn Nat.zero 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (decode Nat.zero)
[PROOFSTEP]

| zero => rfl
[GOAL]
case zero
α : Type u_1
h : Primcodable α
⊢ (Nat.casesOn Nat.zero 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (decode Nat.zero)
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (Nat.succ n) 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (decode (Nat.succ n))
[PROOFSTEP]

| succ n =>
  rw [decode_option_succ]
  cases H : @decode α _ n <;> simp [H]
[GOAL]
case succ
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (Nat.succ n) 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (decode (Nat.succ n))
[PROOFSTEP]
rw [decode_option_succ]
[GOAL]
case succ
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (Nat.succ n) 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (Option.map some (decode n))
[PROOFSTEP]
cases H : @decode α _ n
[GOAL]
case succ.none
α : Type u_1
h : Primcodable α
n : ℕ
H : decode n = none
⊢ (Nat.casesOn (Nat.succ n) 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (Option.map some none)
[PROOFSTEP]
simp [H]
[GOAL]
case succ.some
α : Type u_1
h : Primcodable α
n : ℕ
val✝ : α
H : decode n = some val✝
⊢ (Nat.casesOn (Nat.succ n) 1 fun n => Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) =
    encode (Option.map some (some val✝))
[PROOFSTEP]
simp [H]
[GOAL]
n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x => Nat.casesOn x 2 fun x => 0) = encode (decode (n + 2))
[PROOFSTEP]
rw [decode_ge_two]
[GOAL]
n✝ n : ℕ
⊢ (Nat.casesOn (n + 2) 1 fun x => Nat.casesOn x 2 fun x => 0) = encode none
[PROOFSTEP]
simp
[GOAL]
case h
n✝ n : ℕ
⊢ 2 ≤ n + 2
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
⊢ encode (decode n) = encode (Option.map encode (decode n))
[PROOFSTEP]
cases @decode α _ n
[GOAL]
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
⊢ encode none = encode (Option.map encode none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
val✝ : α
⊢ encode (some val✝) = encode (Option.map encode (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Primrec f
n : ℕ
⊢ Nat.pred (encode (Option.map f (decode n))) = encode (f (ofNat α n))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Nat.Primrec fun n => encode (f (ofNat α n))
n : ℕ
⊢ Nat.succ (encode (f (ofNat α n))) = encode (Option.map f (decode n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n => Nat.succ (Nat.succ n)) = encode (Option.map some (decode n))
[PROOFSTEP]
cases @decode α _ n
[GOAL]
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n => Nat.succ (Nat.succ n)) = encode (Option.map some none)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n => Nat.succ (Nat.succ n)) = encode (Option.map some (some val✝))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun x_1 => Nat.succ (encode x)) = encode (Option.map (fun x_1 => x) (decode n))
[PROOFSTEP]
cases @decode α _ n
[GOAL]
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun x_1 => Nat.succ (encode x)) = encode (Option.map (fun x_1 => x) none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
x : σ
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun x_1 => Nat.succ (encode x)) = encode (Option.map (fun x_1 => x) (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
⊢ ∀ (n : ℕ), encode (decode n) = encode (Option.map id (decode n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n =>
      encode (Option.map f (decode (Nat.pred (encode (Option.map g (decode n))))))) =
    encode (Option.map (fun a => f (g a)) (decode n))
[PROOFSTEP]
cases @decode α _ n
[GOAL]
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n => encode (Option.map f (decode (Nat.pred (encode (Option.map g (decode n))))))) =
    encode (Option.map (fun a => f (g a)) none)
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n =>
      encode (Option.map f (decode (Nat.pred (encode (Option.map g (decode n))))))) =
    encode (Option.map (fun a => f (g a)) (some val✝))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a => encode (f a)
n : ℕ
⊢ encode (Option.map (fun a => encode (f a)) (decode n)) = encode (Option.map f (decode n))
[PROOFSTEP]
cases @decode α _ n
[GOAL]
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a => encode (f a)
n : ℕ
⊢ encode (Option.map (fun a => encode (f a)) none) = encode (Option.map f none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a => encode (f a)
n : ℕ
val✝ : α
⊢ encode (Option.map (fun a => encode (f a)) (some val✝)) = encode (Option.map f (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β✝
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
this : Primcodable β := Primcodable.ofEquiv α e
⊢ Primrec fun a => encode (↑e (↑e.symm a))
[PROOFSTEP]
simp [Primrec.encode]
[GOAL]
α : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β✝
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → β
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun a => ↑e (f a)
a : σ
⊢ ↑e.symm (↑e (f a)) = f a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β✝
inst✝ : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → α
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec fun a => ↑e.symm (f a)
a : σ
⊢ ↑e (↑e.symm (f a)) = f a
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.29317
β : Type ?u.29320
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => Nat.succ (Nat.pair z y))
            (Nat.pair (Nat.unpair (Nat.pair z y)).snd (encode (decode (Nat.unpair (Nat.pair z y)).fst))))
      (Nat.pair (Nat.unpair n).snd (encode (decode (Nat.unpair n).fst))) =
    encode (decode n)
[PROOFSTEP]
simp [Nat.unpaired]
[GOAL]
α : Type ?u.29317
β : Type ?u.29320
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ (Nat.pair n_1 n)) (encode (decode (Nat.unpair n).snd)))
      (encode (decode (Nat.unpair n).fst)) =
    encode (Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
[PROOFSTEP]
cases @decode α _ n.unpair.1
[GOAL]
case none
α : Type ?u.29317
β : Type ?u.29320
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ (Nat.pair n_1 n)) (encode (decode (Nat.unpair n).snd)))
      (encode none) =
    encode (Option.bind none fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
[PROOFSTEP]
simp
[GOAL]
case some
α : Type ?u.29317
β : Type ?u.29320
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ (Nat.pair n_1 n)) (encode (decode (Nat.unpair n).snd)))
      (encode (some val✝)) =
    encode (Option.bind (some val✝) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd))
[PROOFSTEP]
cases @decode β _ n.unpair.2
[GOAL]
case some.none
α : Type ?u.29317
β : Type ?u.29320
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => Nat.rec 0 (fun n_1 n_ih => Nat.succ (Nat.pair n n_1)) (encode none)) (encode (some val✝)) =
    encode (Option.bind (some val✝) fun a => Option.map (Prod.mk a) none)
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type ?u.29317
β : Type ?u.29320
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih => Nat.rec 0 (fun n_1 n_ih => Nat.succ (Nat.pair n n_1)) (encode (some val✝)))
      (encode (some val✝¹)) =
    encode (Option.bind (some val✝¹) fun a => Option.map (Prod.mk a) (some val✝))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => Nat.succ (Nat.unpair (Nat.pair z y)).fst)
            (Nat.pair (Nat.unpair (Nat.pair z y)).snd (encode (decode (Nat.unpair (Nat.pair z y)).fst))))
      (Nat.pair (Nat.unpair n).snd (encode (decode (Nat.unpair n).fst))) =
    encode (Option.map Prod.fst (decode n))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ n_1) (encode (decode (Nat.unpair n).snd)))
      (encode (decode (Nat.unpair n).fst)) =
    encode
      (Option.map Prod.fst
        (Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)))
[PROOFSTEP]
cases @decode α _ n.unpair.1
[GOAL]
case none
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ n_1) (encode (decode (Nat.unpair n).snd)))
      (encode none) =
    encode (Option.map Prod.fst (Option.bind none fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)))
[PROOFSTEP]
simp
[GOAL]
case some
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ n_1) (encode (decode (Nat.unpair n).snd)))
      (encode (some val✝)) =
    encode (Option.map Prod.fst (Option.bind (some val✝) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)))
[PROOFSTEP]
simp
[GOAL]
case some
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => Nat.succ (encode val✝)) (encode (decode (Nat.unpair n).snd)) =
    encode (Option.map (Function.const β val✝) (decode (Nat.unpair n).snd))
[PROOFSTEP]
cases @decode β _ n.unpair.2
[GOAL]
case some.none
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => Nat.succ (encode val✝)) (encode none) = encode (Option.map (Function.const β val✝) none)
[PROOFSTEP]
simp
[GOAL]
case some.some
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih => Nat.succ (encode val✝¹)) (encode (some val✝)) =
    encode (Option.map (Function.const β val✝¹) (some val✝))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => Nat.succ (Nat.unpair (Nat.pair z y)).snd)
            (Nat.pair (Nat.unpair (Nat.pair z y)).snd (encode (decode (Nat.unpair (Nat.pair z y)).fst))))
      (Nat.pair (Nat.unpair n).snd (encode (decode (Nat.unpair n).fst))) =
    encode (Option.map Prod.snd (decode n))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ n) (encode (decode (Nat.unpair n).snd)))
      (encode (decode (Nat.unpair n).fst)) =
    encode
      (Option.map Prod.snd
        (Option.bind (decode (Nat.unpair n).fst) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)))
[PROOFSTEP]
cases @decode α _ n.unpair.1
[GOAL]
case none
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ n) (encode (decode (Nat.unpair n).snd))) (encode none) =
    encode (Option.map Prod.snd (Option.bind none fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)))
[PROOFSTEP]
simp
[GOAL]
case some
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => Nat.succ n) (encode (decode (Nat.unpair n).snd)))
      (encode (some val✝)) =
    encode (Option.map Prod.snd (Option.bind (some val✝) fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).snd)))
[PROOFSTEP]
simp
[GOAL]
case some
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => Nat.succ n) (encode (decode (Nat.unpair n).snd)) = encode (decode (Nat.unpair n).snd)
[PROOFSTEP]
cases @decode β _ n.unpair.2
[GOAL]
case some.none
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => Nat.succ n) (encode none) = encode none
[PROOFSTEP]
simp
[GOAL]
case some.some
α✝ : Type u_1
σ : Type u_2
inst✝³ : Primcodable α✝
inst✝² : Primcodable σ
α : Type u_3
β : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih => Nat.succ n) (encode (some val✝)) = encode (some val✝)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
σ : Type u_2
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable σ
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n =>
      Nat.succ (Nat.pair (Nat.pred (encode (Option.map f (decode n)))) (Nat.pred (encode (Option.map g (decode n)))))) =
    encode (Option.map (fun a => (f a, g a)) (decode n))
[PROOFSTEP]
cases @decode α _ n
[GOAL]
case none
α✝ : Type u_1
σ : Type u_2
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable σ
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n =>
      Nat.succ (Nat.pair (Nat.pred (encode (Option.map f (decode n)))) (Nat.pred (encode (Option.map g (decode n)))))) =
    encode (Option.map (fun a => (f a, g a)) none)
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α✝ : Type u_1
σ : Type u_2
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable σ
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n =>
      Nat.succ (Nat.pair (Nat.pred (encode (Option.map f (decode n)))) (Nat.pred (encode (Option.map g (decode n)))))) =
    encode (Option.map (fun a => (f a, g a)) (some val✝))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ ((Nat.unpair n).fst, (Nat.unpair n).snd) = Nat.unpair n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
a : α
l : List α
n : ℕ
⊢ (Nat.casesOn n (Nat.succ (encode a)) fun n => encode (List.get? l (ofNat ℕ n))) =
    encode (List.get? (a :: l) (ofNat ℕ n))
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
a : α
l : List α
⊢ (Nat.casesOn Nat.zero (Nat.succ (encode a)) fun n => encode (List.get? l (ofNat ℕ n))) =
    encode (List.get? (a :: l) (ofNat ℕ Nat.zero))
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
a : α
l : List α
n✝ : ℕ
⊢ (Nat.casesOn (Nat.succ n✝) (Nat.succ (encode a)) fun n => encode (List.get? l (ofNat ℕ n))) =
    encode (List.get? (a :: l) (ofNat ℕ (Nat.succ n✝)))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
⊢ f = g
[PROOFSTEP]
funext a b
[GOAL]
case h.h
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
a : α
b : β
⊢ f a b = g a b
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
⊢ Primrec₂ Nat.pair
[PROOFSTEP]
simp [Primrec₂, Primrec]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
⊢ Nat.Primrec fun n => Nat.succ n
[PROOFSTEP]
constructor
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : ℕ → ℕ → α
h : Primrec (Nat.unpaired f)
⊢ Primrec₂ f
[PROOFSTEP]
simpa using h.comp natPair
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
σ✝ : Type u_3
inst✝⁵ : Primcodable α✝
inst✝⁴ : Primcodable β✝
inst✝³ : Primcodable σ✝
α : Type u_4
β : Type u_5
σ : Type u_6
inst✝² : Denumerable α
inst✝¹ : Denumerable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun n => f (ofNat (α × β) n).fst (ofNat (α × β) n).snd) ↔
    Primrec (Nat.unpaired fun m n => f (ofNat α m) (ofNat β n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f
[PROOFSTEP]
rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p => f p.fst p.snd) ↔ Primrec₂ f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α × β → σ
⊢ Primrec₂ (Function.curry f) ↔ Primrec f
[PROOFSTEP]
rw [← uncurry, Function.uncurry_curry]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec₂ f ↔
    Nat.Primrec (Nat.unpaired fun m n => encode (Option.bind (decode m) fun a => Option.map (f a) (decode n)))
[PROOFSTEP]
have :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p : α × β => f p.1 p.2) (Option.bind a fun a : α => Option.map (Prod.mk a) b) =
      Option.bind a fun a => Option.map (f a) b :=
  fun a b => by cases a <;> cases b <;> rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
a : Option α
b : Option β
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind a fun a => Option.map (Prod.mk a) b) =
    Option.bind a fun a => Option.map (f a) b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind none fun a => Option.map (Prod.mk a) b) =
    Option.bind none fun a => Option.map (f a) b
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
val✝ : α
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind (some val✝) fun a => Option.map (Prod.mk a) b) =
    Option.bind (some val✝) fun a => Option.map (f a) b
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind none fun a => Option.map (Prod.mk a) none) =
    Option.bind none fun a => Option.map (f a) none
[PROOFSTEP]
rfl
[GOAL]
case none.some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝ : β
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind none fun a => Option.map (Prod.mk a) (some val✝)) =
    Option.bind none fun a => Option.map (f a) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case some.none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝ : α
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind (some val✝) fun a => Option.map (Prod.mk a) none) =
    Option.bind (some val✝) fun a => Option.map (f a) none
[PROOFSTEP]
rfl
[GOAL]
case some.some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝¹ : α
val✝ : β
⊢ Option.map (fun p => f p.fst p.snd) (Option.bind (some val✝¹) fun a => Option.map (Prod.mk a) (some val✝)) =
    Option.bind (some val✝¹) fun a => Option.map (f a) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
this :
  ∀ (a : Option α) (b : Option β),
    Option.map (fun p => f p.fst p.snd) (Option.bind a fun a => Option.map (Prod.mk a) b) =
      Option.bind a fun a => Option.map (f a) b
⊢ Primrec₂ f ↔
    Nat.Primrec (Nat.unpaired fun m n => encode (Option.bind (decode m) fun a => Option.map (f a) (decode n)))
[PROOFSTEP]
simp [Primrec₂, Primrec, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired
            (fun z n =>
              Nat.rec (encode (Option.map f (decode z)))
                (fun y IH =>
                  encode
                    (Option.map (fun p => g p.fst p.snd)
                      (decode
                        (Nat.pair (Nat.unpair (Nat.pair z (Nat.pair y IH))).fst
                          (Nat.pair (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).snd).fst
                            (Nat.pred (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).snd).snd))))))
                n)
            (Nat.pair (Nat.unpair (Nat.pair z y)).snd (Nat.unpair (Nat.unpair (Nat.pair z y)).fst).snd))
      (Nat.pair (id n) (encode (decode (Nat.unpair n).fst))) =
    Nat.unpaired
      (fun m n =>
        encode
          (Option.bind (decode m) fun a => Option.map (fun n => Nat.rec (f a) (fun n IH => g a (n, IH)) n) (decode n)))
      n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.fst p.snd)
                (Option.bind (decode n_1) fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH)))))
          (Nat.unpair n).snd)
      (encode (decode (Nat.unpair n).fst)) =
    encode
      (Option.bind (decode (Nat.unpair n).fst) fun a =>
        some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).snd))
[PROOFSTEP]
cases' @decode α _ n.unpair.1 with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.fst p.snd)
                (Option.bind (decode n_1) fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH)))))
          (Nat.unpair n).snd)
      (encode none) =
    encode (Option.bind none fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).snd))
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.fst p.snd)
                (Option.bind (decode n_1) fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH)))))
          (Nat.unpair n).snd)
      (encode (some a)) =
    encode (Option.bind (some a) fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).snd))
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (Nat.succ (encode (f a)))
      (fun y IH => encode (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH))))
      (Nat.unpair n).snd =
    Nat.succ (encode (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).snd))
[PROOFSTEP]
induction' n.unpair.2 with m
[GOAL]
case some.zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (Nat.succ (encode (f a)))
      (fun y IH => encode (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH))))
      Nat.zero =
    Nat.succ (encode (Nat.rec (f a) (fun n IH => g a (n, IH)) Nat.zero))
[PROOFSTEP]
simp [encodek]
[GOAL]
case some.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
m : ℕ
n_ih✝ :
  Nat.rec (Nat.succ (encode (f a)))
      (fun y IH => encode (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH)))) m =
    Nat.succ (encode (Nat.rec (f a) (fun n IH => g a (n, IH)) m))
⊢ Nat.rec (Nat.succ (encode (f a)))
      (fun y IH => encode (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH))))
      (Nat.succ m) =
    Nat.succ (encode (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.succ m)))
[PROOFSTEP]
simp [encodek]
[GOAL]
case some.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
m : ℕ
n_ih✝ :
  Nat.rec (Nat.succ (encode (f a)))
      (fun y IH => encode (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH)))) m =
    Nat.succ (encode (Nat.rec (f a) (fun n IH => g a (n, IH)) m))
⊢ encode
      (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk m)
        (decode
          (Nat.pred
            (Nat.rec (Nat.succ (encode (f a)))
              (fun y IH =>
                encode (Option.map ((fun p => g p.fst p.snd) ∘ Prod.mk a ∘ Prod.mk y) (decode (Nat.pred IH))))
              m)))) =
    Nat.succ (encode (g a (m, Nat.rec (f a) (fun n IH => g a (n, IH)) m)))
[PROOFSTEP]
simp [*, encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH => h a (n, IH).snd) (f a) = (h a)^[f a] (g a)
[PROOFSTEP]
induction f a
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH => h a (n, IH).snd) Nat.zero = (h a)^[Nat.zero] (g a)
[PROOFSTEP]
simp [*, -Function.iterate_succ, Function.iterate_succ']
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
n✝ : ℕ
n_ih✝ : Nat.rec (g a) (fun n IH => h a (n, IH).snd) n✝ = (h a)^[n✝] (g a)
⊢ Nat.rec (g a) (fun n IH => h a (n, IH).snd) (Nat.succ n✝) = (h a)^[Nat.succ n✝] (g a)
[PROOFSTEP]
simp [*, -Function.iterate_succ, Function.iterate_succ']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (encode (f a)) fun b =>
      Nat.pred (encode (Option.bind (decode (encode (a, b).fst)) fun a => Option.map (g a) (decode b)))) =
    encode (Option.casesOn (o a) (f a) (g a))
[PROOFSTEP]
cases' o a with b
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (encode none) (encode (f a)) fun b =>
      Nat.pred (encode (Option.bind (decode (encode (a, b).fst)) fun a => Option.map (g a) (decode b)))) =
    encode (Option.casesOn none (f a) (g a))
[PROOFSTEP]
simp [encodek]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
b : β
⊢ (Nat.casesOn (encode (some b)) (encode (f a)) fun b =>
      Nat.pred (encode (Option.bind (decode (encode (a, b).fst)) fun a => Option.map (g a) (decode b)))) =
    encode (Option.casesOn (some b) (f a) (g a))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn (f a) none (g a) = Option.bind (f a) (g a)
[PROOFSTEP]
cases f a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn none none (g a) = Option.bind none (g a)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
val✝ : β
⊢ Option.casesOn (some val✝) none (g a) = Option.bind (some val✝) (g a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (Option.bind (f x) fun b => some (g x b)) = Option.map (g x) (f x)
[PROOFSTEP]
cases f x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (Option.bind none fun b => some (g x b)) = Option.map (g x) none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
val✝ : β
⊢ (Option.bind (some val✝) fun b => some (g x b)) = Option.map (g x) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Inhabited α
o : Option α
⊢ (Option.casesOn (id o) default fun b => b) = Option.iget o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Inhabited α
⊢ (Option.casesOn (id none) default fun b => b) = Option.iget none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Inhabited α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) default fun b => b) = Option.iget (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
o : Option α
⊢ (Option.casesOn (id o) false fun b => true) = Option.isSome o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ (Option.casesOn (id none) false fun b => true) = Option.isSome none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
val✝ : α
⊢ (Option.casesOn (id (some val✝)) false fun b => true) = Option.isSome (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × α
o : Option α
a : α
⊢ (Option.casesOn ((fun a x => a) (o, a).fst (o, a).snd) ((fun x b => b) (o, a).fst (o, a).snd) fun b => b) =
    Option.getD (o, a).fst (o, a).snd
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × α
a : α
⊢ (Option.casesOn ((fun a x => a) (none, a).fst (none, a).snd) ((fun x b => b) (none, a).fst (none, a).snd) fun b =>
      b) =
    Option.getD (none, a).fst (none, a).snd
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × α
a val✝ : α
⊢ (Option.casesOn ((fun a x => a) (some val✝, a).fst (some val✝, a).snd)
      ((fun x b => b) (some val✝, a).fst (some val✝, a).snd) fun b => b) =
    Option.getD (some val✝, a).fst (some val✝, a).snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → Option σ
h : Primrec₂ fun a n => Option.bind (decode n) (f a)
⊢ Primrec₂ f
[PROOFSTEP]
simpa [encodek] using h.comp fst ((@Primrec.encode β _).comp snd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => Option.map (f a) (decode n)) ↔ Primrec₂ f
[PROOFSTEP]
simp only [Option.map_eq_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f
[PROOFSTEP]
exact bind_decode_iff.trans Primrec₂.option_some_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (encode (c a)) (g a) fun b => f (a, b).fst) = bif c a then f a else g a
[PROOFSTEP]
cases c a
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (encode false) (g a) fun b => f (a, b).fst) = bif false then f a else g a
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (encode true) (g a) fun b => f (a, b).fst) = bif true then f a else g a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
c : α → Prop
inst✝ : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec fun a => if c a then f a else g a
[PROOFSTEP]
simpa using cond hc hf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ (Nat.casesOn ((fun x x_1 => x - x_1) p.fst p.snd) true fun b => false) =
    (fun a b => decide ((fun x x_1 => x ≤ x_1) a b)) p.fst p.snd
[PROOFSTEP]
dsimp [swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ Nat.rec true (fun n n_ih => false) (p.fst - p.snd) = decide (p.fst ≤ p.snd)
[PROOFSTEP]
cases' e : p.1 - p.2 with n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
e : p.fst - p.snd = Nat.zero
⊢ Nat.rec true (fun n n_ih => false) Nat.zero = decide (p.fst ≤ p.snd)
[PROOFSTEP]
simp [tsub_eq_zero_iff_le.1 e]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
n : ℕ
e : p.fst - p.snd = Nat.succ n
⊢ Nat.rec true (fun n n_ih => false) (Nat.succ n) = decide (p.fst ≤ p.snd)
[PROOFSTEP]
simp [not_le.2 (Nat.lt_of_sub_eq_succ e)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → α
b : Bool
⊢ (bif id b then f true else f false) = f b
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → α
⊢ (bif id false then f true else f false) = f false
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → α
⊢ (bif id true then f true else f false) = f true
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → Bool → α
x✝ : Bool × Bool
a b : Bool
⊢ (bif (a, b).fst then f true (a, b).snd else f false (a, b).snd) = f (a, b).fst (a, b).snd
[PROOFSTEP]
cases a
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (false, b).fst then f true (false, b).snd else f false (false, b).snd) = f (false, b).fst (false, b).snd
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (true, b).fst then f true (true, b).snd else f false (true, b).snd) = f (true, b).fst (true, b).snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
n : α
⊢ (!decide (p n)) = decide ((fun a => ¬p a) n)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable β
inst✝⁴ : Primcodable γ
inst✝³ : Primcodable δ
inst✝² : Primcodable σ
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : PrimrecPred p
hq : PrimrecPred q
n : α
⊢ (decide (p n) && decide (q n)) = decide ((fun a => p a ∧ q a) n)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable β
inst✝⁴ : Primcodable γ
inst✝³ : Primcodable δ
inst✝² : Primcodable σ
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hp : PrimrecPred p
hq : PrimrecPred q
n : α
⊢ (decide (p n) || decide (q n)) = decide ((fun a => p a ∨ q a) n)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
a : ℕ × ℕ
⊢ (fun x x_1 => x ≤ x_1) a.fst a.snd ∧ (fun x x_1 => x ≤ x_1) a.snd a.fst ↔ (fun a b => a = b) a.fst a.snd
[PROOFSTEP]
simp [le_antisymm_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : ℕ × ℕ
⊢ ¬p.snd ≤ p.fst ↔ (fun x x_1 => x < x_1) p.fst p.snd
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
o₁ o₂ : Option α
⊢ (Option.casesOn (o₁, o₂).fst (o₁, o₂).snd fun b => ((o₁, o₂), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (o₁, o₂).fst (o₁, o₂).snd
[PROOFSTEP]
cases o₁
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
o₂ : Option α
⊢ (Option.casesOn (none, o₂).fst (none, o₂).snd fun b => ((none, o₂), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (none, o₂).fst (none, o₂).snd
[PROOFSTEP]
cases o₂
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
o₂ : Option α
val✝ : α
⊢ (Option.casesOn (some val✝, o₂).fst (some val✝, o₂).snd fun b => ((some val✝, o₂), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (some val✝, o₂).fst (some val✝, o₂).snd
[PROOFSTEP]
cases o₂
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
⊢ (Option.casesOn (none, none).fst (none, none).snd fun b => ((none, none), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (none, none).fst (none, none).snd
[PROOFSTEP]
rfl
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (none, some val✝).fst (none, some val✝).snd fun b => ((none, some val✝), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (none, some val✝).fst (none, some val✝).snd
[PROOFSTEP]
rfl
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (some val✝, none).fst (some val✝, none).snd fun b => ((some val✝, none), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (some val✝, none).fst (some val✝, none).snd
[PROOFSTEP]
rfl
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
val✝¹ val✝ : α
⊢ (Option.casesOn (some val✝¹, some val✝).fst (some val✝¹, some val✝).snd fun b =>
      ((some val✝¹, some val✝), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (some val✝¹, some val✝).fst (some val✝¹, some val✝).snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ Primrec₂ fun p a => encode a
[PROOFSTEP]
exact encode_iff.mpr snd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ Primrec₂ fun p a => p.fst
[PROOFSTEP]
exact fst.comp fst
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : α → β → Bool
hp : Primrec₂ p
a : β
l : List β
n : α
⊢ (bif p (id n) a then 0 else Nat.succ (List.findIdx (p n) l)) = List.findIdx (p n) (a :: l)
[PROOFSTEP]
simp [List.findIdx_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
⊢ Primrec fun a => some (f a)
[PROOFSTEP]
haveI := decidableEqOfEncodable α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
this : DecidableEq α
⊢ Primrec fun a => some (f a)
[PROOFSTEP]
refine ((list_get?₁ (l.map f)).comp (list_indexOf₁ l)).of_eq fun a => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Fintype α
f : α → σ
l : List α
left✝ : List.Nodup l
m : ∀ (x : α), x ∈ l
this : DecidableEq α
a : α
⊢ List.get? (List.map f l) (List.indexOf a l) = some (f a)
[PROOFSTEP]
rw [List.get?_map, List.indexOf_get? (m a), Option.map_some']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
f : α → ℕ
p : α → ℕ → Prop
inst✝ : (x : α) → (n : ℕ) → Decidable (p x n)
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH => if p x ((n, IH).fst + 1) then (n, IH).fst + 1 else (n, IH).snd) (f x) =
    Nat.findGreatest (p x) (f x)
[PROOFSTEP]
induction f x
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
f : α → ℕ
p : α → ℕ → Prop
inst✝ : (x : α) → (n : ℕ) → Decidable (p x n)
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH => if p x ((n, IH).fst + 1) then (n, IH).fst + 1 else (n, IH).snd) Nat.zero =
    Nat.findGreatest (p x) Nat.zero
[PROOFSTEP]
simp [Nat.findGreatest, *]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
f : α → ℕ
p : α → ℕ → Prop
inst✝ : (x : α) → (n : ℕ) → Decidable (p x n)
hf : Primrec f
hp : PrimrecRel p
x : α
n✝ : ℕ
n_ih✝ :
  Nat.rec 0 (fun n IH => if p x ((n, IH).fst + 1) then (n, IH).fst + 1 else (n, IH).snd) n✝ = Nat.findGreatest (p x) n✝
⊢ Nat.rec 0 (fun n IH => if p x ((n, IH).fst + 1) then (n, IH).fst + 1 else (n, IH).snd) (Nat.succ n✝) =
    Nat.findGreatest (p x) (Nat.succ n✝)
[PROOFSTEP]
simp [Nat.findGreatest, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b => f a = b
⊢ Primrec f
[PROOFSTEP]
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f
[PROOFSTEP]
refine (nat_findGreatest pg h₂).of_eq fun n => ?_
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b => f n = b) (g n) = f n
[PROOFSTEP]
exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ Primrec₂ fun x x_1 => x / x_1
[PROOFSTEP]
refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ PrimrecRel fun a b => (fun x x_1 => x / x_1) a.fst a.snd = b
[PROOFSTEP]
have : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) => (a.2 = 0 ∧ b = 0) ∨ (0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2) :=
  PrimrecPred.or (.and (const 0 |> Primrec.eq.comp (fst |> snd.comp)) (const 0 |> Primrec.eq.comp snd))
    (.and (nat_lt.comp (const 0) (fst |> snd.comp)) <|
      .and (nat_le.comp (nat_mul.comp snd (fst |> snd.comp)) (fst |> fst.comp))
        (nat_lt.comp (fst.comp fst) (nat_mul.comp (Primrec.succ.comp snd) (snd.comp fst))))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
⊢ PrimrecRel fun a b => (fun x x_1 => x / x_1) a.fst a.snd = b
[PROOFSTEP]
refine this.of_eq ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
⊢ ∀ (a : ℕ × ℕ) (b : ℕ),
    a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd ↔ (fun x x_1 => x / x_1) a.fst a.snd = b
[PROOFSTEP]
rintro ⟨a, k⟩ q
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
a k q : ℕ
⊢ (a, k).snd = 0 ∧ q = 0 ∨ 0 < (a, k).snd ∧ q * (a, k).snd ≤ (a, k).fst ∧ (a, k).fst < (q + 1) * (a, k).snd ↔
    (fun x x_1 => x / x_1) (a, k).fst (a, k).snd = q
[PROOFSTEP]
if H : k = 0 then simp [H, eq_comm]
else
  have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
    rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le' (Nat.pos_of_ne_zero H),
      Nat.div_lt_iff_lt_mul' (Nat.pos_of_ne_zero H)]
  simpa [H, zero_lt_iff, eq_comm (b := q)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
a k q : ℕ
H : k = 0
⊢ (a, k).snd = 0 ∧ q = 0 ∨ 0 < (a, k).snd ∧ q * (a, k).snd ≤ (a, k).fst ∧ (a, k).fst < (q + 1) * (a, k).snd ↔
    (fun x x_1 => x / x_1) (a, k).fst (a, k).snd = q
[PROOFSTEP]
simp [H, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
a k q : ℕ
H : ¬k = 0
⊢ (a, k).snd = 0 ∧ q = 0 ∨ 0 < (a, k).snd ∧ q * (a, k).snd ≤ (a, k).fst ∧ (a, k).fst < (q + 1) * (a, k).snd ↔
    (fun x x_1 => x / x_1) (a, k).fst (a, k).snd = q
[PROOFSTEP]
have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
  rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le' (Nat.pos_of_ne_zero H),
    Nat.div_lt_iff_lt_mul' (Nat.pos_of_ne_zero H)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
a k q : ℕ
H : ¬k = 0
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
[PROOFSTEP]
rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le' (Nat.pos_of_ne_zero H),
  Nat.div_lt_iff_lt_mul' (Nat.pos_of_ne_zero H)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
this✝ : PrimrecRel fun a b => a.snd = 0 ∧ b = 0 ∨ 0 < a.snd ∧ b * a.snd ≤ a.fst ∧ a.fst < (b + 1) * a.snd
a k q : ℕ
H : ¬k = 0
this : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
⊢ (a, k).snd = 0 ∧ q = 0 ∨ 0 < (a, k).snd ∧ q * (a, k).snd ≤ (a, k).fst ∧ (a, k).fst < (q + 1) * (a, k).snd ↔
    (fun x x_1 => x / x_1) (a, k).fst (a, k).snd = q
[PROOFSTEP]
simpa [H, zero_lt_iff, eq_comm (b := q)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
m n : ℕ
⊢ (m, n).fst - (m, n).snd * (fun x x_1 => x / x_1) (m, n).fst (m, n).snd = m % n
[PROOFSTEP]
apply Nat.sub_eq_of_eq_add
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
m n : ℕ
⊢ (m, n).fst = m % n + (m, n).snd * (fun x x_1 => x / x_1) (m, n).fst (m, n).snd
[PROOFSTEP]
simp [add_comm (m % n), Nat.div_add_mod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
n : ℕ
⊢ (id n % 2 == 1) = Nat.bodd n
[PROOFSTEP]
cases H : n.bodd
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
n : ℕ
H : Nat.bodd n = false
⊢ (id n % 2 == 1) = false
[PROOFSTEP]
simp [Nat.mod_two_of_bodd, H]
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
n : ℕ
H : Nat.bodd n = true
⊢ (id n % 2 == 1) = true
[PROOFSTEP]
simp [Nat.mod_two_of_bodd, H]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a => Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a))) =
    some (List.casesOn (f a) (g a) fun b l => h a (b, l))
[PROOFSTEP]
cases' f a with b l
[GOAL]
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a => Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode [])) =
    some (List.casesOn [] (g a) fun b l => h a (b, l))
[PROOFSTEP]
simp [encodek]
[GOAL]
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a => Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
b : β
l : List β
⊢ Option.map (fun o => Option.casesOn o (g a) (h a)) (decode (encode (b :: l))) =
    some (List.casesOn (b :: l) (g a) fun b l => h a (b, l))
[PROOFSTEP]
simp [encodek]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
letI := prim H
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
let G (a : α) (IH : σ × List β) : σ × List β := List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
have hG : Primrec₂ G :=
  list_casesOn' H (snd.comp snd) snd <|
    to₂ <| pair (hh.comp (fst.comp fst) <| pair ((fst.comp snd).comp fst) (fst.comp snd)) (snd.comp snd)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
let F := fun (a : α) (n : ℕ) => (G a)^[n] (g a, f a)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
have hF : Primrec fun a => (F a (encode (f a))).1 := (fst.comp <| nat_iterate (encode_iff.2 hf) (pair hg hf) <| hG)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
suffices : ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n)
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
this : ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
refine hF.of_eq fun a => ?_
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
this : ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
a : α
⊢ (F a (encode (f a))).fst = List.foldl (fun s b => h a (s, b)) (g a) (f a)
[PROOFSTEP]
rw [this, List.take_all_of_le (length_le_encode _)]
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
⊢ ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
[PROOFSTEP]
introv
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
n : ℕ
⊢ F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
[PROOFSTEP]
dsimp only
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
n : ℕ
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (g a, f a) =
    (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
[PROOFSTEP]
generalize f a = l
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
n : ℕ
l : List β
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (g a, l) =
    (List.foldl (fun s b => h a (s, b)) (g a) (List.take n l), List.drop n l)
[PROOFSTEP]
generalize g a = x
[GOAL]
case this
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
n : ℕ
l : List β
x : σ
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (x, l) =
    (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)
[PROOFSTEP]
induction' n with n IH generalizing l x
[GOAL]
case this.zero
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
l✝ : List β
x✝ : σ
l : List β
x : σ
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[Nat.zero] (x, l) =
    (List.foldl (fun s b => h a (s, b)) x (List.take Nat.zero l), List.drop Nat.zero l)
[PROOFSTEP]
rfl
[GOAL]
case this.succ
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
l✝ : List β
x✝ : σ
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (x, l) =
      (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[Nat.succ n] (x, l) =
    (List.foldl (fun s b => h a (s, b)) x (List.take (Nat.succ n) l), List.drop (Nat.succ n) l)
[PROOFSTEP]
simp
[GOAL]
case this.succ
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
l✝ : List β
x✝ : σ
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (x, l) =
      (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)
l : List β
x : σ
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n]
      (List.rec (x, l) (fun head tail tail_ih => (h a (x, head), tail)) l) =
    (List.foldl (fun s b => h a (s, b)) x (List.take (Nat.succ n) l), List.drop (Nat.succ n) l)
[PROOFSTEP]
cases' l with b l
[GOAL]
case this.succ.nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
l : List β
x✝ : σ
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (x, l) =
      (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)
x : σ
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n]
      (List.rec (x, []) (fun head tail tail_ih => (h a (x, head), tail)) []) =
    (List.foldl (fun s b => h a (s, b)) x (List.take (Nat.succ n) []), List.drop (Nat.succ n) [])
[PROOFSTEP]
simp [IH]
[GOAL]
case this.succ.cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.snd IH fun b l => (h a (IH.fst, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).fst
a : α
l✝ : List β
x✝ : σ
n : ℕ
IH :
  ∀ (l : List β) (x : σ),
    (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n] (x, l) =
      (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)
x : σ
b : β
l : List β
⊢ (fun IH => List.rec IH (fun head tail tail_ih => (h a (IH.fst, head), tail)) IH.snd)^[n]
      (List.rec (x, b :: l) (fun head tail tail_ih => (h a (x, head), tail)) (b :: l)) =
    (List.foldl (fun s b => h a (s, b)) x (List.take (Nat.succ n) (b :: l)), List.drop (Nat.succ n) (b :: l))
[PROOFSTEP]
simp [IH]
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
this : Primcodable (List β) := prim H
l : List β
⊢ ∀ (r : List β), List.foldl (fun s b => b :: s) r l = List.reverseAux l r
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
this : Primcodable (List β) := prim H
⊢ ∀ (r : List β), List.foldl (fun s b => b :: s) r [] = List.reverseAux [] r
[PROOFSTEP]
simp [*, List.reverseAux]
[GOAL]
case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
this : Primcodable (List β) := prim H
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (r : List β), List.foldl (fun s b => b :: s) r tail✝ = List.reverseAux tail✝ r
⊢ ∀ (r : List β), List.foldl (fun s b => b :: s) r (head✝ :: tail✝) = List.reverseAux (head✝ :: tail✝) r
[PROOFSTEP]
simp [*, List.reverseAux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif Nat.bodd n then Option.map (fun b => 2 * encode (n, b).snd + 1) (decode (Nat.div2 n))
      else Option.map (fun b => 2 * encode (n, b).snd) (decode (Nat.div2 n))) =
    encode (decodeSum n)
[PROOFSTEP]
simp [decodeSum]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif Nat.bodd n then Option.map (fun b => 2 * encode b + 1) (decode (Nat.div2 n))
      else Option.map (fun b => 2 * encode b) (decode (Nat.div2 n))) =
    encode
      (match (Nat.bodd n, Nat.div2 n) with
      | (false, m) => Option.map Sum.inl (decode m)
      | (fst, m) => Option.map Sum.inr (decode m))
[PROOFSTEP]
cases Nat.bodd n
[GOAL]
case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif false then Option.map (fun b => 2 * encode b + 1) (decode (Nat.div2 n))
      else Option.map (fun b => 2 * encode b) (decode (Nat.div2 n))) =
    encode
      (match (false, Nat.div2 n) with
      | (false, m) => Option.map Sum.inl (decode m)
      | (fst, m) => Option.map Sum.inr (decode m))
[PROOFSTEP]
simp [decodeSum]
[GOAL]
case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif true then Option.map (fun b => 2 * encode b + 1) (decode (Nat.div2 n))
      else Option.map (fun b => 2 * encode b) (decode (Nat.div2 n))) =
    encode
      (match (true, Nat.div2 n) with
      | (false, m) => Option.map Sum.inl (decode m)
      | (fst, m) => Option.map Sum.inr (decode m))
[PROOFSTEP]
simp [decodeSum]
[GOAL]
case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b => 2 * encode b) (decode (Nat.div2 n))) = encode (Option.map Sum.inl (decode (Nat.div2 n)))
[PROOFSTEP]
cases @decode α _ n.div2
[GOAL]
case false.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b => 2 * encode b) none) = encode (Option.map Sum.inl none)
[PROOFSTEP]
rfl
[GOAL]
case false.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ encode (Option.map (fun b => 2 * encode b) (some val✝)) = encode (Option.map Sum.inl (some val✝))
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b => 2 * encode b + 1) (decode (Nat.div2 n))) =
    encode (Option.map Sum.inr (decode (Nat.div2 n)))
[PROOFSTEP]
cases @decode β _ n.div2
[GOAL]
case true.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b => 2 * encode b + 1) none) = encode (Option.map Sum.inr none)
[PROOFSTEP]
rfl
[GOAL]
case true.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : β
⊢ encode (Option.map (fun b => 2 * encode b + 1) (some val✝)) = encode (Option.map Sum.inr (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ encode
      (List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
        (List.reverse (ofNat (List ℕ) n))) =
    encode (decode n)
[PROOFSTEP]
rw [List.foldl_reverse]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ encode
      (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) n)) =
    encode (decode n)
[PROOFSTEP]
apply Nat.case_strong_induction_on n
[GOAL]
case hz
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ encode
      (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) 0)) =
    encode (decode 0)
[PROOFSTEP]
simp
[GOAL]
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m ≤ n →
          encode
              (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
                (ofNat (List ℕ) m)) =
            encode (decode m)) →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (Nat.succ n))) =
        encode (decode (Nat.succ n))
[PROOFSTEP]
intro n IH
[GOAL]
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
⊢ encode
      (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) (Nat.succ n))) =
    encode (decode (Nat.succ n))
[PROOFSTEP]
simp
[GOAL]
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
⊢ encode
      (Option.bind (decode (Nat.unpair n).fst) fun a =>
        Option.map (List.cons (encode a))
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (Nat.unpair n).snd))) =
    encode (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode (Nat.unpair n).fst)) fun x => decode (Nat.unpair n).snd)
[PROOFSTEP]
cases' @decode α _ n.unpair.1 with a
[GOAL]
case hi.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
⊢ encode
      (Option.bind none fun a =>
        Option.map (List.cons (encode a))
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (Nat.unpair n).snd))) =
    encode (Seq.seq (Option.map (fun x x_1 => x :: x_1) none) fun x => decode (Nat.unpair n).snd)
[PROOFSTEP]
rfl
[GOAL]
case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
⊢ encode
      (Option.bind (some a) fun a =>
        Option.map (List.cons (encode a))
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (Nat.unpair n).snd))) =
    encode (Seq.seq (Option.map (fun x x_1 => x :: x_1) (some a)) fun x => decode (Nat.unpair n).snd)
[PROOFSTEP]
simp only [decode_eq_ofNat, Option.some.injEq, Option.some_bind, Option.map_some']
[GOAL]
case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
⊢ encode
      (Option.map (List.cons (encode a))
        (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) (Nat.unpair n).snd))) =
    encode (Seq.seq (some fun x => a :: x) fun x => decode (Nat.unpair n).snd)
[PROOFSTEP]
suffices :
  ∀ (o : Option (List ℕ)) (p) (_ : encode o = encode p),
    encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
[GOAL]
case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝¹ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this✝ :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
this :
  ∀ (o : Option (List ℕ)) (p : Option (List α)),
    encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
⊢ encode
      (Option.map (List.cons (encode a))
        (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) (Nat.unpair n).snd))) =
    encode (Seq.seq (some fun x => a :: x) fun x => decode (Nat.unpair n).snd)
case this
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
⊢ ∀ (o : Option (List ℕ)) (p : Option (List α)),
    encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
[PROOFSTEP]
exact this _ _ (IH _ (Nat.unpair_right_le n))
[GOAL]
case this
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
⊢ ∀ (o : Option (List ℕ)) (p : Option (List α)),
    encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
[PROOFSTEP]
intro o p IH
[GOAL]
case this
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
o : Option (List ℕ)
p : Option (List α)
IH : encode o = encode p
⊢ encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
[PROOFSTEP]
cases o
[GOAL]
case this.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
p : Option (List α)
IH : encode none = encode p
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)
[PROOFSTEP]
cases p
[GOAL]
case this.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
p : Option (List α)
val✝ : List ℕ
IH : encode (some val✝) = encode p
⊢ encode (Option.map (List.cons (encode a)) (some val✝)) = encode (Option.map (List.cons a) p)
[PROOFSTEP]
cases p
[GOAL]
case this.none.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
IH : encode none = encode none
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) none)
[PROOFSTEP]
rfl
[GOAL]
case this.none.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
val✝ : List α
IH : encode none = encode (some val✝)
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) (some val✝))
[PROOFSTEP]
injection IH
[GOAL]
case this.some.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
val✝ : List ℕ
IH : encode (some val✝) = encode none
⊢ encode (Option.map (List.cons (encode a)) (some val✝)) = encode (Option.map (List.cons a) none)
[PROOFSTEP]
injection IH
[GOAL]
case this.some.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n) := prim
this✝ : Primrec₂ fun a o => Option.map (List.cons (encode a)) o
this :
  Primrec fun n =>
    List.foldl (fun o m => Option.bind (decode m) fun a => Option.map (List.cons (encode a)) o) (some [])
      (List.reverse (ofNat (List ℕ) n))
n✝ n : ℕ
IH✝ :
  ∀ (m : ℕ),
    m ≤ n →
      encode
          (List.foldr (fun x y => Option.bind (decode x) fun a => Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) m)) =
        encode (decode m)
a : α
val✝¹ : List ℕ
val✝ : List α
IH : encode (some val✝¹) = encode (some val✝)
⊢ encode (Option.map (List.cons (encode a)) (some val✝¹)) = encode (Option.map (List.cons a) (some val✝))
[PROOFSTEP]
exact congr_arg (fun k => (Nat.pair (encode a) k).succ.succ) (Nat.succ.inj IH)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
⊢ (bif Nat.bodd (encode (f a)) then Option.map (h a) (decode (Nat.div2 (encode (f a))))
    else Option.map (g a) (decode (Nat.div2 (encode (f a))))) =
    some (Sum.casesOn (f a) (g a) (h a))
[PROOFSTEP]
cases' f a with b c
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
b : β
⊢ (bif Nat.bodd (encode (Sum.inl b)) then Option.map (h a) (decode (Nat.div2 (encode (Sum.inl b))))
    else Option.map (g a) (decode (Nat.div2 (encode (Sum.inl b))))) =
    some (Sum.casesOn (Sum.inl b) (g a) (h a))
[PROOFSTEP]
simp [Nat.div2_val, encodek]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
c : γ
⊢ (bif Nat.bodd (encode (Sum.inr c)) then Option.map (h a) (decode (Nat.div2 (encode (Sum.inr c))))
    else Option.map (g a) (decode (Nat.div2 (encode (Sum.inr c))))) =
    some (Sum.casesOn (Sum.inr c) (g a) (h a))
[PROOFSTEP]
simp [Nat.div2_val, encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ List.foldl (fun s b => h (a, s, b).fst ((a, s, b).snd.snd, (a, s, b).snd.fst)) (g a) (List.reverse (f a)) =
    List.foldr (fun b s => h a (b, s)) (g a) (f a)
[PROOFSTEP]
simp [List.foldl_reverse]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ (List.casesOn (id l) none fun b l_1 => some (l, b, l_1).snd.fst) = List.head? l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ (List.casesOn (id []) none fun b l => some ([], b, l).snd.fst) = List.head? []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) none fun b l => some (head✝ :: tail✝, b, l).snd.fst) = List.head? (head✝ :: tail✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ (List.casesOn (id l) [] fun b l_1 => (l, b, l_1).snd.snd) = List.tail l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ (List.casesOn (id []) [] fun b l => ([], b, l).snd.snd) = List.tail []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) [] fun b l => (head✝ :: tail✝, b, l).snd.snd) = List.tail (head✝ :: tail✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ (F a).snd = List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)
[PROOFSTEP]
suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this✝ : Primrec F
a : α
this : F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))
⊢ (F a).snd = List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a) =
    (f a, List.rec (g a) (fun b l IH => h a (b, l, IH)) (f a))
[PROOFSTEP]
induction' f a with b l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) [] = ([], List.rec (g a) (fun b l IH => h a (b, l, IH)) [])
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
b : β
l : List β
IH : List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) l = (l, List.rec (g a) (fun b l IH => h a (b, l, IH)) l)
⊢ List.foldr (fun b s => (b :: s.fst, h a (b, s))) ([], g a) (b :: l) =
    (b :: l, List.rec (g a) (fun b l IH => h a (b, l, IH)) (b :: l))
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.casesOn (F (l, n).fst (l, n).snd) (fun x => none) some = List.get? l n
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) l) =
    List.get? l n
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
l : List α
n : ℕ
⊢ List.get? l n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) l)
[PROOFSTEP]
induction' l with a l IH generalizing n
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ n : ℕ
⊢ List.get? [] n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
n : ℕ
⊢ List.get? (a :: l) n =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl n) (a :: l))
[PROOFSTEP]
cases' n with n
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
⊢ List.get? (a :: l) Nat.zero =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl Nat.zero) (a :: l))
[PROOFSTEP]
dsimp
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
[PROOFSTEP]
clear IH
[GOAL]
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
l : List α
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
[PROOFSTEP]
induction' l with _ l IH
[GOAL]
case cons.zero.nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a : α
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) [])
[PROOFSTEP]
simp [*]
[GOAL]
case cons.zero.cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n : ℕ
a head✝ : α
l : List α
IH :
  some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) l)
⊢ some a =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inr a) (head✝ :: l))
[PROOFSTEP]
simp [*]
[GOAL]
case cons.succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
F : List α → ℕ → ℕ ⊕ α :=
  fun l n => List.foldl (fun s a => Sum.casesOn s (fun x => Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p => Sum.casesOn (F p.fst p.snd) (fun x => none) some
n✝ : ℕ
a : α
l : List α
IH :
  ∀ (n : ℕ),
    List.get? l n =
      Sum.rec (fun val => none) (fun val => some val)
        (List.foldl
          (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
          (Sum.inl n) l)
n : ℕ
⊢ List.get? (a :: l) (Nat.succ n) =
    Sum.rec (fun val => none) (fun val => some val)
      (List.foldl
        (fun s a => Sum.rec (fun val => Nat.rec (Sum.inr a) (fun n n_ih => Sum.inl n) val) (fun val => Sum.inr val) s)
        (Sum.inl (Nat.succ n)) (a :: l))
[PROOFSTEP]
apply IH
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
d : α
⊢ Primrec₂ fun l n => List.getD l n d
[PROOFSTEP]
simp only [List.getD_eq_getD_get?]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
d : α
⊢ Primrec₂ fun l n => Option.getD (List.get? l n) d
[PROOFSTEP]
exact option_getD.comp₂ list_get? (const _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l₁ l₂ : List α
⊢ List.foldr (fun b s => ((l₁, l₂), b, s).snd.fst :: ((l₁, l₂), b, s).snd.snd) (l₁, l₂).snd (l₁, l₂).fst = l₁ ++ l₂
[PROOFSTEP]
induction l₁
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l₂ : List α
⊢ List.foldr (fun b s => (([], l₂), b, s).snd.fst :: (([], l₂), b, s).snd.snd) ([], l₂).snd ([], l₂).fst = [] ++ l₂
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.foldr (fun b s => ((tail✝, l₂), b, s).snd.fst :: ((tail✝, l₂), b, s).snd.snd) (tail✝, l₂).snd (tail✝, l₂).fst =
    tail✝ ++ l₂
⊢ List.foldr (fun b s => ((head✝ :: tail✝, l₂), b, s).snd.fst :: ((head✝ :: tail✝, l₂), b, s).snd.snd)
      (head✝ :: tail✝, l₂).snd (head✝ :: tail✝, l₂).fst =
    head✝ :: tail✝ ++ l₂
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s => g (a, b, s).fst (a, b, s).snd.fst :: (a, b, s).snd.snd) [] (f a) = List.map (g a) (f a)
[PROOFSTEP]
induction f a
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s => g (a, b, s).fst (a, b, s).snd.fst :: (a, b, s).snd.snd) [] [] = List.map (g a) []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
head✝ : β
tail✝ : List β
tail_ih✝ :
  List.foldr (fun b s => g (a, b, s).fst (a, b, s).snd.fst :: (a, b, s).snd.snd) [] tail✝ = List.map (g a) tail✝
⊢ List.foldr (fun b s => g (a, b, s).fst (a, b, s).snd.fst :: (a, b, s).snd.snd) [] (head✝ :: tail✝) =
    List.map (g a) (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Nat.rec [] (fun n_1 IH => (n, n_1, IH).snd.snd ++ [(n, n_1, IH).snd.fst]) (id n) = List.range n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Nat.rec [] (fun n IH => IH ++ [n]) n = List.range n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ Nat.rec [] (fun n IH => IH ++ [n]) Nat.zero = List.range Nat.zero
[PROOFSTEP]
simp [*, List.range_succ]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n✝ : ℕ
n_ih✝ : Nat.rec [] (fun n IH => IH ++ [n]) n✝ = List.range n✝
⊢ Nat.rec [] (fun n IH => IH ++ [n]) (Nat.succ n✝) = List.range (Nat.succ n✝)
[PROOFSTEP]
simp [*, List.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List (List α)
⊢ List.foldr (fun b s => (fun x x_1 => x ++ x_1) (l, b, s).snd.fst (l, b, s).snd.snd) [] (id l) = List.join l
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List (List α)
⊢ List.foldr (fun b s => b ++ s) [] l = List.join l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ List.foldr (fun b s => b ++ s) [] [] = List.join []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : List.foldr (fun b s => b ++ s) [] tail✝ = List.join tail✝
⊢ List.foldr (fun b s => b ++ s) [] (head✝ :: tail✝) = List.join (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ List.foldr (fun b s => (fun a b => Nat.succ (a, b).snd.snd) (l, b, s).fst (l, b, s).snd) 0 (id l) = List.length l
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ List.foldr (fun b s => Nat.succ s) 0 l = List.length l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ List.foldr (fun b s => Nat.succ s) 0 [] = List.length []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun b s => Nat.succ s) 0 tail✝ = List.length tail✝
⊢ List.foldr (fun b s => Nat.succ s) 0 (head✝ :: tail✝) = List.length (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p (a, b, s).fst (a, b, s).snd.fst then 0 else Nat.succ (a, b, s).snd.snd) 0 (f a) =
    List.findIdx (p a) (f a)
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p a b then 0 else Nat.succ s) 0 (f a) = List.findIdx (p a) (f a)
[PROOFSTEP]
induction f a
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s => bif p a b then 0 else Nat.succ s) 0 [] = List.findIdx (p a) []
[PROOFSTEP]
simp [List.findIdx_cons, *]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
head✝ : β
tail✝ : List β
tail_ih✝ : List.foldr (fun b s => bif p a b then 0 else Nat.succ s) 0 tail✝ = List.findIdx (p a) tail✝
⊢ List.foldr (fun b s => bif p a b then 0 else Nat.succ s) 0 (head✝ :: tail✝) = List.findIdx (p a) (head✝ :: tail✝)
[PROOFSTEP]
simp [List.findIdx_cons, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some [])
      (fun n IH =>
        Option.bind (a, n, IH).snd.snd fun b =>
          Option.map (fun b_1 => (((a, n, IH), b), b_1).fst.snd ++ [(((a, n, IH), b), b_1).snd])
            (g ((a, n, IH), b).fst.fst ((a, n, IH), b).snd))
      n =
    some (List.map (f a) (List.range n))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) n =
    some (List.map (f a) (List.range n))
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) Nat.zero =
    some (List.map (f a) (List.range Nat.zero))
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
IH :
  Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) n =
    some (List.map (f a) (List.range n))
⊢ Nat.rec (some []) (fun n IH => Option.bind IH fun b => Option.map (fun b_1 => b ++ [b_1]) (g a b)) (Nat.succ n) =
    some (List.map (f a) (List.range (Nat.succ n)))
[PROOFSTEP]
simp [IH, H, List.range_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
this : Primrec₂ fun a n => List.map (f a) (List.range n)
a : α
n : ℕ
⊢ List.get? (List.map (f (a, n).fst) (List.range (Nat.succ (a, n).snd))) (a, n).snd = some (f a n)
[PROOFSTEP]
simp [List.get?_range (Nat.lt_succ_self n)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
⊢ encode (Option.bind (decode n) fun a => Option.guard p a) =
    encode
      (Option.bind (decode n) fun a =>
        if h : (fun a => (fun a => p a) a) a then some { val := a, property := h } else none)
[PROOFSTEP]
cases' @decode α _ n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
⊢ encode (Option.bind none fun a => Option.guard p a) =
    encode
      (Option.bind none fun a => if h : (fun a => (fun a => p a) a) a then some { val := a, property := h } else none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
a : α
⊢ encode (Option.bind (some a) fun a => Option.guard p a) =
    encode
      (Option.bind (some a) fun a =>
        if h : (fun a => (fun a => p a) a) a then some { val := a, property := h } else none)
[PROOFSTEP]
dsimp [Option.guard]
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
a : α
⊢ encode (if p a then some a else none) = encode (if h : p a then some { val := a, property := h } else none)
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
a : α
h : p a
⊢ encode (if p a then some a else none) = encode (if h : p a then some { val := a, property := h } else none)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
a : α
h : ¬p a
⊢ encode (if p a then some a else none) = encode (if h : p a then some { val := a, property := h } else none)
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n => Option.bind (decode n) fun a => Option.guard p a
n : ℕ
a : α
h : p a
⊢ encode a = encode { val := a, property := (_ : p a) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec Subtype.val
[PROOFSTEP]
letI := Primcodable.subtype hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ Primrec Subtype.val
[PROOFSTEP]
refine' (@Primcodable.prim (Subtype p)).of_eq fun n => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode (decode n) = encode (Option.map Subtype.val (decode n))
[PROOFSTEP]
rcases@decode (Subtype p) _ n with (_ | ⟨a, h⟩)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode none = encode (Option.map Subtype.val none)
[PROOFSTEP]
rfl
[GOAL]
case some.mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
a : α
h : p a
⊢ encode (some { val := a, property := h }) = encode (Option.map Subtype.val (some { val := a, property := h }))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
[PROOFSTEP]
letI := Primcodable.subtype hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
[PROOFSTEP]
refine' ⟨fun h => _, fun hf => subtype_val.comp hf⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
⊢ Primrec f
[PROOFSTEP]
refine' Nat.Primrec.of_eq h fun n => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a => ↑(f a)) (decode n)) = encode (Option.map f (decode n))
[PROOFSTEP]
cases' @decode α _ n with a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a => ↑(f a)) none) = encode (Option.map f none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
a : α
⊢ encode (Option.map (fun a => ↑(f a)) (some a)) = encode (Option.map f (some a))
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
a : α
⊢ Nat.succ (encode ↑(f a)) = encode (some (f a))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
⊢ Primrec f → Primrec fun a => Option.get (f a) (_ : Option.isSome (f a) = true)
[PROOFSTEP]
intro hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
⊢ Primrec fun a => Option.get (f a) (_ : Option.isSome (f a) = true)
[PROOFSTEP]
refine' (Nat.Primrec.pred.comp hf).of_eq fun n => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
⊢ Nat.pred (encode (Option.map f (decode n))) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) (decode n))
[PROOFSTEP]
generalize hx : @decode α _ n = x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ Nat.pred (encode (Option.map f x)) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) x)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
hx : decode n = none
⊢ Nat.pred (encode (Option.map f none)) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) none)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
val✝ : α
hx : decode n = some val✝
⊢ Nat.pred (encode (Option.map f (some val✝))) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) (some val✝))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
[PROOFSTEP]
letI : Primcodable { a // id a < n } := Primcodable.subtype (nat_lt.comp .id (const _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype (_ : PrimrecPred fun a => id a < n)
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f
[PROOFSTEP]
exact (Iff.trans (by rfl) subtype_val_iff).trans (of_equiv_iff _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n
this : Primcodable { a // id a < n } := Primcodable.subtype (_ : PrimrecPred fun a => id a < n)
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec fun a => ↑(↑Fin.equivSubtype (f a))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => ↑(Fin.succ a)
[PROOFSTEP]
simp [succ.comp fin_val]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => Vector.toList (a.fst ::ᵥ a.snd)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => a.fst :: Vector.toList a.snd
[PROOFSTEP]
exact list_cons.comp fst (vector_toList_iff.2 snd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
x✝ : Vector α n
l : List α
h : List.length l = n
⊢ List.tail (Vector.toList { val := l, property := h }) = Vector.toList (Vector.tail { val := l, property := h })
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
x✝ : Vector α n
h : List.length [] = n
⊢ List.tail (Vector.toList { val := [], property := h }) = Vector.toList (Vector.tail { val := [], property := h })
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
x✝ : Vector α n
head✝ : α
tail✝ : List α
h : List.length (head✝ :: tail✝) = n
⊢ List.tail (Vector.toList { val := head✝ :: tail✝, property := h }) =
    Vector.toList (Vector.tail { val := head✝ :: tail✝, property := h })
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
a : Vector α n × Fin n
⊢ List.get? (Vector.toList a.fst) ↑a.snd = some (Vector.get a.fst a.snd)
[PROOFSTEP]
rw [Vector.get_eq_get, ← List.get?_eq_get]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
a : Vector α n × Fin n
⊢ List.get? (Vector.toList a.fst) ↑a.snd =
    List.get? (Vector.toList a.fst) ↑(↑(Fin.castIso (_ : n = List.length (Vector.toList a.fst))) a.snd)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a => List.ofFn fun i => f i a
[PROOFSTEP]
simp [List.ofFn_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a => f 0 a :: List.ofFn fun i => f (Fin.succ i) a
[PROOFSTEP]
exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Primrec (f i)
⊢ Primrec fun a => Vector.toList (Vector.ofFn fun i => f i a)
[PROOFSTEP]
simp [list_ofFn hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
x✝ : (Fin n → σ) × Fin n
v : Fin n → σ
i : Fin n
⊢ Vector.get (Vector.ofFn (v, i).fst) (v, i).snd = id (v, i).fst (v, i).snd
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
h : ∀ (i : Fin n), Primrec (f i)
a : Fin n × α
⊢ Vector.get (Vector.ofFn fun i => f i a.snd) a.fst = f a.fst a.snd
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
⊢ Vector.get (Vector.ofFn fun i => f a i) = f a
[PROOFSTEP]
funext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
i : Fin n
⊢ Vector.get (Vector.ofFn fun i => f a i) i = f a i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
pf : Primrec' f
⊢ Primrec f
[PROOFSTEP]
induction pf
[GOAL]
case zero
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun x => 0
case succ
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun v => Nat.succ (head v)
case get
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Primrec fun v => Vector.get v i✝
case comp
n : ℕ
f : Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
a_ih✝¹ : Primrec f✝
a_ih✝ : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a => f✝ (ofFn fun i => g✝ i a)
case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Primrec f✝
a_ih✝ : Primrec g✝
⊢ Primrec fun v => Nat.rec (f✝ (tail v)) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
case zero => exact .const 0
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun x => 0
[PROOFSTEP]
case zero => exact .const 0
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun x => 0
[PROOFSTEP]
exact .const 0
[GOAL]
case succ
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun v => Nat.succ (head v)
case get
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Primrec fun v => Vector.get v i✝
case comp
n : ℕ
f : Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
a_ih✝¹ : Primrec f✝
a_ih✝ : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a => f✝ (ofFn fun i => g✝ i a)
case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Primrec f✝
a_ih✝ : Primrec g✝
⊢ Primrec fun v => Nat.rec (f✝ (tail v)) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
case succ => exact _root_.Primrec.succ.comp .vector_head
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun v => Nat.succ (head v)
[PROOFSTEP]
case succ => exact _root_.Primrec.succ.comp .vector_head
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
⊢ Primrec fun v => Nat.succ (head v)
[PROOFSTEP]
exact _root_.Primrec.succ.comp .vector_head
[GOAL]
case get
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Primrec fun v => Vector.get v i✝
case comp
n : ℕ
f : Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
a_ih✝¹ : Primrec f✝
a_ih✝ : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a => f✝ (ofFn fun i => g✝ i a)
case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Primrec f✝
a_ih✝ : Primrec g✝
⊢ Primrec fun v => Nat.rec (f✝ (tail v)) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
case get n i => exact Primrec.vector_get.comp .id (.const i)
[GOAL]
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
n : ℕ
i : Fin n
⊢ Primrec fun v => Vector.get v i
[PROOFSTEP]
case get n i => exact Primrec.vector_get.comp .id (.const i)
[GOAL]
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
n : ℕ
i : Fin n
⊢ Primrec fun v => Vector.get v i
[PROOFSTEP]
exact Primrec.vector_get.comp .id (.const i)
[GOAL]
case comp
n : ℕ
f : Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
a_ih✝¹ : Primrec f✝
a_ih✝ : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a => f✝ (ofFn fun i => g✝ i a)
case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Primrec f✝
a_ih✝ : Primrec g✝
⊢ Primrec fun v => Nat.rec (f✝ (tail v)) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
case comp m n f g _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
m n : ℕ
f : Vector ℕ n → ℕ
g : Fin n → Vector ℕ m → ℕ
a✝¹ : Primrec' f
a✝ : ∀ (i : Fin n), Primrec' (g i)
hf : Primrec f
hg : ∀ (i : Fin n), Primrec (g i)
⊢ Primrec fun a => f (ofFn fun i => g i a)
[PROOFSTEP]
case comp m n f g _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
m n : ℕ
f : Vector ℕ n → ℕ
g : Fin n → Vector ℕ m → ℕ
a✝¹ : Primrec' f
a✝ : ∀ (i : Fin n), Primrec' (g i)
hf : Primrec f
hg : ∀ (i : Fin n), Primrec (g i)
⊢ Primrec fun a => f (ofFn fun i => g i a)
[PROOFSTEP]
exact hf.comp (.vector_ofFn fun i => hg i)
[GOAL]
case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Primrec f✝
a_ih✝ : Primrec g✝
⊢ Primrec fun v => Nat.rec (f✝ (tail v)) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
case prec n f g _ _ hf hg =>
  exact
    .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
      (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
            Primrec.vector_cons.comp (Primrec.snd.comp .snd) <| (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
a✝¹ : Primrec' f
a✝ : Primrec' g
hf : Primrec f
hg : Primrec g
⊢ Primrec fun v => Nat.rec (f (tail v)) (fun y IH => g (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
case prec n f g _ _ hf hg =>
  exact
    .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
      (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
            Primrec.vector_cons.comp (Primrec.snd.comp .snd) <| (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
[GOAL]
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
a✝¹ : Primrec' f
a✝ : Primrec' g
hf : Primrec f
hg : Primrec g
⊢ Primrec fun v => Nat.rec (f (tail v)) (fun y IH => g (y ::ᵥ IH ::ᵥ tail v)) (head v)
[PROOFSTEP]
exact
  .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
    (hg.comp <|
        Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <| (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
[GOAL]
n : ℕ
v : Vector ℕ (Nat.succ n)
⊢ Vector.get v 0 = Vector.head v
[PROOFSTEP]
simp [get_zero]
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
v : Vector ℕ (Nat.succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (Vector.tail v)
[PROOFSTEP]
rw [← ofFn_get v.tail]
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
v : Vector ℕ (Nat.succ n)
⊢ f (ofFn fun i => Vector.get v (Fin.succ i)) = f (ofFn (Vector.get (Vector.tail v)))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
v : Vector ℕ (Nat.succ n)
⊢ (fun i => Vector.get v (Fin.succ i)) = Vector.get (Vector.tail v)
[PROOFSTEP]
funext i
[GOAL]
case e_a.e_a.h
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
v : Vector ℕ (Nat.succ n)
i : Fin n
⊢ Vector.get v (Fin.succ i) = Vector.get (Vector.tail v) i
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Primrec' f
hg : Vec g
i : Fin (Nat.succ m)
⊢ Primrec' fun v => Vector.get ((fun v => f v ::ᵥ g v) v) 0
[PROOFSTEP]
simp [*]
[GOAL]
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Primrec' f
hg : Vec g
i✝ : Fin (Nat.succ m)
i : Fin m
⊢ Primrec' fun v => Vector.get ((fun v => f v ::ᵥ g v) v) (Fin.succ i)
[PROOFSTEP]
simp [hg i]
[GOAL]
n m : ℕ
f : Vector ℕ m → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Primrec' f
hg : Vec g
v : Vector ℕ n
⊢ f (ofFn fun i => Vector.get (g v) i) = f (g v)
[PROOFSTEP]
simp
[GOAL]
f : ℕ → ℕ → ℕ
hf : Primrec' fun v => f (Vector.head v) (Vector.head (Vector.tail v))
n : ℕ
g h : Vector ℕ n → ℕ
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v => f (g v) (h v)
[PROOFSTEP]
simpa using hf.comp' (hg.cons <| hh.cons Primrec'.nil)
[GOAL]
n : ℕ
f g : Vector ℕ n → ℕ
h : Vector ℕ (n + 2) → ℕ
hf : Primrec' f
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)
[PROOFSTEP]
simpa using comp' (prec hg hh) (hf.cons idv)
[GOAL]
v : Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => Vector.head (y ::ᵥ IH ::ᵥ v)) (Vector.head v) = Nat.pred (Vector.head v)
[PROOFSTEP]
simp
[GOAL]
v : Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => y) (Vector.head v) = Nat.pred (Vector.head v)
[PROOFSTEP]
cases v.head
[GOAL]
case zero
v : Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => y) Nat.zero = Nat.pred Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
v : Vector ℕ (Nat.succ 0)
n✝ : ℕ
⊢ Nat.rec 0 (fun y IH => y) (Nat.succ n✝) = Nat.pred (Nat.succ n✝)
[PROOFSTEP]
rfl
[GOAL]
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ (Vector.head (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v))))
      (Vector.head v) =
    Vector.head v + Vector.head (Vector.tail v)
[PROOFSTEP]
simp
[GOAL]
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ IH) (Vector.head v) =
    Vector.head v + Vector.head (Vector.tail v)
[PROOFSTEP]
induction v.head
[GOAL]
case zero
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ IH) Nat.zero = Nat.zero + Vector.head (Vector.tail v)
[PROOFSTEP]
simp [*, Nat.succ_add]
[GOAL]
case succ
v : Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
n_ih✝ : Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ IH) n✝ = n✝ + Vector.head (Vector.tail v)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ IH) (Nat.succ n✝) =
    Nat.succ n✝ + Vector.head (Vector.tail v)
[PROOFSTEP]
simp [*, Nat.succ_add]
[GOAL]
⊢ Primrec' fun v => Vector.head v - Vector.head (Vector.tail v)
[PROOFSTEP]
suffices
[GOAL]
this : ?m.372029
⊢ Primrec' fun v => Vector.head v - Vector.head (Vector.tail v)
case this ⊢ ?m.372029
[PROOFSTEP]
simpa using comp₂ (fun a b => b - a) this (tail head) head
[GOAL]
case this
⊢ Primrec' fun v => (fun a b => b - a) (Vector.head v) (Vector.head (Vector.tail v))
[PROOFSTEP]
refine' (prec head (pred.comp₁ _ (tail head))).of_eq fun v => _
[GOAL]
case this
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred (Vector.head (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v))))
      (Vector.head v) =
    (fun a b => b - a) (Vector.head v) (Vector.head (Vector.tail v))
[PROOFSTEP]
simp
[GOAL]
case this
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred IH) (Vector.head v) =
    Vector.head (Vector.tail v) - Vector.head v
[PROOFSTEP]
induction v.head
[GOAL]
case this.zero
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred IH) Nat.zero = Vector.head (Vector.tail v) - Nat.zero
[PROOFSTEP]
simp [*, Nat.sub_succ]
[GOAL]
case this.succ
v : Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
n_ih✝ : Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred IH) n✝ = Vector.head (Vector.tail v) - n✝
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.pred IH) (Nat.succ n✝) =
    Vector.head (Vector.tail v) - Nat.succ n✝
[PROOFSTEP]
simp [*, Nat.sub_succ]
[GOAL]
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0
      (fun y IH =>
        Vector.head (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v))) +
          Vector.head (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v)))
      (Vector.head v) =
    Vector.head v * Vector.head (Vector.tail v)
[PROOFSTEP]
simp
[GOAL]
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH => Vector.head (Vector.tail v) + IH) (Vector.head v) = Vector.head v * Vector.head (Vector.tail v)
[PROOFSTEP]
induction v.head
[GOAL]
case zero
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH => Vector.head (Vector.tail v) + IH) Nat.zero = Nat.zero * Vector.head (Vector.tail v)
[PROOFSTEP]
simp [*, Nat.succ_mul]
[GOAL]
case succ
v : Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
n_ih✝ : Nat.rec 0 (fun y IH => Vector.head (Vector.tail v) + IH) n✝ = n✝ * Vector.head (Vector.tail v)
⊢ Nat.rec 0 (fun y IH => Vector.head (Vector.tail v) + IH) (Nat.succ n✝) = Nat.succ n✝ * Vector.head (Vector.tail v)
[PROOFSTEP]
simp [*, Nat.succ_mul]
[GOAL]
case succ
v : Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
n_ih✝ : Nat.rec 0 (fun y IH => Vector.head (Vector.tail v) + IH) n✝ = n✝ * Vector.head (Vector.tail v)
⊢ Vector.head (Vector.tail v) + n✝ * Vector.head (Vector.tail v) =
    n✝ * Vector.head (Vector.tail v) + Vector.head (Vector.tail v)
[PROOFSTEP]
rw [add_comm]
[GOAL]
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) (b v - a v) =
    if a v < b v then f v else g v
[PROOFSTEP]
cases e : b v - a v
[GOAL]
case zero
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
e : b v - a v = Nat.zero
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) Nat.zero = if a v < b v then f v else g v
[PROOFSTEP]
simp [not_lt.2 (tsub_eq_zero_iff_le.mp e)]
[GOAL]
case succ
n : ℕ
a b f g : Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : Vector ℕ n
n✝ : ℕ
e : b v - a v = Nat.succ n✝
⊢ Nat.rec (g v) (fun y IH => f (Vector.tail (Vector.tail (y ::ᵥ IH ::ᵥ v)))) (Nat.succ n✝) =
    if a v < b v then f v else g v
[PROOFSTEP]
simp [Nat.lt_of_sub_eq_succ e]
[GOAL]
v : Vector ℕ 0
⊢ 0 = encode v
[PROOFSTEP]
rw [v.eq_nil]
[GOAL]
v : Vector ℕ 0
⊢ 0 = encode nil
[PROOFSTEP]
rfl
[GOAL]
⊢ Primrec' fun v => Nat.sqrt (Vector.head v)
[PROOFSTEP]
suffices H : ∀ n : ℕ, n.sqrt = n.rec 0 fun x y => if x.succ < y.succ * y.succ then y else y.succ
[GOAL]
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v => Nat.sqrt (Vector.head v)
[PROOFSTEP]
simp [H]
[GOAL]
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v =>
    Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Vector.head v)
[PROOFSTEP]
have :=
  @prec' 1 _ _
    (fun v => by have x := v.head; have y := v.tail.head; exact if x.succ < y.succ * y.succ then y else y.succ) head
    (const 0) ?_
[GOAL]
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
⊢ ℕ
[PROOFSTEP]
have x := v.head
[GOAL]
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
x : ℕ
⊢ ℕ
[PROOFSTEP]
have y := v.tail.head
[GOAL]
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
v : Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ
[PROOFSTEP]
exact if x.succ < y.succ * y.succ then y else y.succ
[GOAL]
case refine_2
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
this :
  Primrec' fun v =>
    Nat.rec 0
      (fun y IH =>
        (fun v =>
            let_fun x := Vector.head v;
            let_fun y := Vector.head (Vector.tail v);
            if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y)
          (y ::ᵥ IH ::ᵥ v))
      (Vector.head v)
⊢ Primrec' fun v =>
    Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Vector.head v)
[PROOFSTEP]
exact this
[GOAL]
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
[PROOFSTEP]
have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
[GOAL]
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
x1 : Primrec' fun v => Nat.succ (Vector.head v)
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
[PROOFSTEP]
have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)
[GOAL]
case refine_1
H : ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
x1 : Primrec' fun v => Nat.succ (Vector.head v)
y1 : Primrec' fun v => Nat.succ (Vector.head (Vector.tail v))
⊢ Primrec' fun v =>
    let_fun x := Vector.head v;
    let_fun y := Vector.head (Vector.tail v);
    if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y
[PROOFSTEP]
exact if_lt x1 (mul.comp₂ _ y1 y1) (tail head) y1
[GOAL]
case H
⊢ ∀ (n : ℕ), Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
[PROOFSTEP]
introv
[GOAL]
case H
n : ℕ
⊢ Nat.sqrt n = Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
[PROOFSTEP]
symm
[GOAL]
case H
n : ℕ
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case H.zero
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) Nat.zero = Nat.sqrt Nat.zero
[PROOFSTEP]
simp
[GOAL]
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) (Nat.succ n) =
    Nat.sqrt (Nat.succ n)
[PROOFSTEP]
dsimp
[GOAL]
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ (if
        Nat.succ n <
          Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n) *
            Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n) then
      Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n
    else Nat.succ (Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n)) =
    Nat.sqrt (Nat.succ n)
[PROOFSTEP]
rw [IH]
[GOAL]
case H.succ
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
⊢ (if Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n) then Nat.sqrt n else Nat.succ (Nat.sqrt n)) =
    Nat.sqrt (Nat.succ n)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
h : Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)
⊢ Nat.sqrt n = Nat.sqrt (Nat.succ n)
[PROOFSTEP]
exact le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)
[GOAL]
case neg
n : ℕ
IH : Nat.rec 0 (fun x y => if Nat.succ x < Nat.succ y * Nat.succ y then y else Nat.succ y) n = Nat.sqrt n
h : ¬Nat.succ n < Nat.succ (Nat.sqrt n) * Nat.succ (Nat.sqrt n)
⊢ Nat.succ (Nat.sqrt n) = Nat.sqrt (Nat.succ n)
[PROOFSTEP]
exact Nat.eq_sqrt.2 ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v => (unpair (f v)).fst
[PROOFSTEP]
have s := sqrt.comp₁ _ hf
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).fst
[PROOFSTEP]
have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).fst
[PROOFSTEP]
refine' (if_lt fss s fss s).of_eq fun v => _
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then f v - Nat.sqrt (f v) * Nat.sqrt (f v)
    else Nat.sqrt (f v)) =
    (unpair (f v)).fst
[PROOFSTEP]
simp [Nat.unpair]
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then f v - Nat.sqrt (f v) * Nat.sqrt (f v)
    else Nat.sqrt (f v)) =
    (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then
        (f v - Nat.sqrt (f v) * Nat.sqrt (f v), Nat.sqrt (f v))
      else (Nat.sqrt (f v), f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v))).fst
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
h✝ : f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v)
⊢ f v - Nat.sqrt (f v) * Nat.sqrt (f v) = (f v - Nat.sqrt (f v) * Nat.sqrt (f v), Nat.sqrt (f v)).fst
[PROOFSTEP]
rfl
[GOAL]
case neg
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
h✝ : ¬f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v)
⊢ Nat.sqrt (f v) = (Nat.sqrt (f v), f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v)).fst
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v => (unpair (f v)).snd
[PROOFSTEP]
have s := sqrt.comp₁ _ hf
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).snd
[PROOFSTEP]
have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
⊢ Primrec' fun v => (unpair (f v)).snd
[PROOFSTEP]
refine' (if_lt fss s s (sub.comp₂ _ fss s)).of_eq fun v => _
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then Nat.sqrt (f v)
    else f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v)) =
    (unpair (f v)).snd
[PROOFSTEP]
simp [Nat.unpair]
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
⊢ (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then Nat.sqrt (f v)
    else f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v)) =
    (if f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v) then
        (f v - Nat.sqrt (f v) * Nat.sqrt (f v), Nat.sqrt (f v))
      else (Nat.sqrt (f v), f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v))).snd
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
h✝ : f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v)
⊢ Nat.sqrt (f v) = (f v - Nat.sqrt (f v) * Nat.sqrt (f v), Nat.sqrt (f v)).snd
[PROOFSTEP]
rfl
[GOAL]
case neg
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => Nat.sqrt (f v)
fss : Primrec' fun v => f v - Nat.sqrt (f v) * Nat.sqrt (f v)
v : Vector ℕ n
h✝ : ¬f v - Nat.sqrt (f v) * Nat.sqrt (f v) < Nat.sqrt (f v)
⊢ f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v) =
    (Nat.sqrt (f v), f v - Nat.sqrt (f v) * Nat.sqrt (f v) - Nat.sqrt (f v)).snd
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Primrec' fun v => f (Vector.head v)
[PROOFSTEP]
induction hf
[GOAL]
case zero
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) (Vector.head v)
case succ
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)
case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)
case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case zero => exact const 0
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) (Vector.head v)
[PROOFSTEP]
case zero => exact const 0
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) (Vector.head v)
[PROOFSTEP]
exact const 0
[GOAL]
case succ
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)
case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)
case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case succ => exact succ
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)
[PROOFSTEP]
case succ => exact succ
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => Nat.succ (Vector.head v)
[PROOFSTEP]
exact succ
[GOAL]
case left
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)
case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case left => exact unpair₁ head
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)
[PROOFSTEP]
case left => exact unpair₁ head
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).fst) (Vector.head v)
[PROOFSTEP]
exact unpair₁ head
[GOAL]
case right
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case right => exact unpair₂ head
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
[PROOFSTEP]
case right => exact unpair₂ head
[GOAL]
n : ℕ
f✝ : Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).snd) (Vector.head v)
[PROOFSTEP]
exact unpair₂ head
[GOAL]
case pair
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) (Vector.head v)
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case pair f g _ _ hf hg => exact natPair.comp₂ _ hf hg
[GOAL]
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f n) (g n)) (Vector.head v)
[PROOFSTEP]
case pair f g _ _ hf hg => exact natPair.comp₂ _ hf hg
[GOAL]
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => (fun n => pair (f n) (g n)) (Vector.head v)
[PROOFSTEP]
exact natPair.comp₂ _ hf hg
[GOAL]
case comp
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) (Vector.head v)
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case comp f g _ _ hf hg => exact hf.comp₁ _ hg
[GOAL]
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => (fun n => f (g n)) (Vector.head v)
[PROOFSTEP]
case comp f g _ _ hf hg => exact hf.comp₁ _ hg
[GOAL]
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => (fun n => f (g n)) (Vector.head v)
[PROOFSTEP]
exact hf.comp₁ _ hg
[GOAL]
case prec
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
a_ih✝¹ : Primrec' fun v => f✝ (Vector.head v)
a_ih✝ : Primrec' fun v => g✝ (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case prec f g _ _ hf hg =>
  simpa using
    prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
      (hg.comp₁ _ <| natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
[GOAL]
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f z) (fun y IH => g (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
case prec f g _ _ hf hg =>
  simpa using
    prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
      (hg.comp₁ _ <| natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
[GOAL]
n : ℕ
f✝¹ : Vector ℕ n → ℕ
f✝ f g : ℕ → ℕ
a✝¹ : Nat.Primrec f
a✝ : Nat.Primrec g
hf : Primrec' fun v => f (Vector.head v)
hg : Primrec' fun v => g (Vector.head v)
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f z) (fun y IH => g (pair z (pair y IH))) n) (Vector.head v)
[PROOFSTEP]
simpa using
  prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
    (hg.comp₁ _ <| natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))
[GOAL]
n : ℕ
f : Vector ℕ n → ℕ
this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' fun v => f (Vector.head v)
hf : Primrec f
i : Vector ℕ n
⊢ Nat.pred ((fun m => encode (Option.map f (decode m))) (encode i)) = f i
[PROOFSTEP]
simp [encodek]
[GOAL]
f : ℕ → ℕ
h : Primrec fun v => f (Vector.head v)
v : ℕ
⊢ f (Vector.head (ofFn fun i => id v)) = f v
[PROOFSTEP]
simp
[GOAL]
f : ℕ → ℕ → ℕ
h : Primrec fun v => f (Vector.head v) (Vector.head (Vector.tail v))
v : ℕ × ℕ
⊢ f (Vector.head (v.fst ::ᵥ v.snd ::ᵥ nil)) (Vector.head (Vector.tail (v.fst ::ᵥ v.snd ::ᵥ nil))) = f v.fst v.snd
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
f : Vector ℕ m → Vector ℕ n
h : Vec f
⊢ Primrec f
[PROOFSTEP]
simpa using Primrec.vector_ofFn fun i => to_prim (h i)