internlm/Lean-Github huggingface dataset:
Theorem: Encodable.encode_fintypeArrow'
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode ∘ fintypeArrowEquivFinArrow f = fintypeArrowEquivFinArrow fun i => encode (f i)
Tactic:
funext i
Proof state after:
case h
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : Fin (Fintype.card ι)
⊢ (encode ∘ fintypeArrowEquivFinArrow f) i = fintypeArrowEquivFinArrow (fun i => encode (f i)) i
Theorem: Encodable.encode_fintypeArrow'
Proof state before:
case h
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : Fin (Fintype.card ι)
⊢ (encode ∘ fintypeArrowEquivFinArrow f) i = fintypeArrowEquivFinArrow (fun i => encode (f i)) i
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.encode_fintypeArrow_isEmpty
Proof state before:
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = 0
Tactic:
have : Fintype.card ι = 0 := Fintype.card_eq_zero
Proof state after:
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
this : Fintype.card ι = 0
⊢ encode f = 0
Theorem: Encodable.encode_fintypeArrow_isEmpty
Proof state before:
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
this : Fintype.card ι = 0
⊢ encode f = 0
Tactic:
simp[encode_fintypeArrow, encode_finArrow, this]
Proof state after:
no goals
Theorem: Encodable.encode_fintypeArrow_card_one
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 1
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : ι
⊢ encode f = encode [f i]
Tactic:
have : Subsingleton ι := Fintype.card_le_one_iff_subsingleton.mp (by simp[hι])
Proof state after:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 1
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : ι
this : Subsingleton ι
⊢ encode f = encode [f i]
Theorem: Encodable.encode_fintypeArrow_card_one
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 1
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : ι
⊢ Fintype.card ι ≤ 1
Tactic:
simp[hι]
Proof state after:
no goals
Theorem: Encodable.encode_fintypeArrow_card_two
Proof state before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 2
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = encode [f (fintypeEquivFin.symm (Fin.cast ⋯ 0)), f (fintypeEquivFin.symm (Fin.cast ⋯ 1))]
Tactic:
simp[encode_fintypeArrow, encode_finArrow, hι]
Proof state after:
no goals
Theorem: Encodable.encode_list_lt
Proof state before:
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
h : b ∈ bs
⊢ encode b < encode bs
Tactic:
induction' bs with b' bs ih
Proof state after:
case nil
β : Type u_1
inst✝ : Encodable β
b : β
h : b ∈ []
⊢ encode b < encode []

case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
⊢ encode b < encode (b' :: bs)
Theorem: Encodable.encode_list_lt
Proof state before:
case nil
β : Type u_1
inst✝ : Encodable β
b : β
h : b ∈ []
⊢ encode b < encode []
Tactic:
simp at h
Proof state after:
no goals
Theorem: Encodable.encode_list_lt
Proof state before:
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
⊢ encode b < encode (b' :: bs)
Tactic:
have : b = b' ∨ b ∈ bs := by simpa using h
Proof state after:
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
this : b = b' ∨ b ∈ bs
⊢ encode b < encode (b' :: bs)
Theorem: Encodable.encode_list_lt
Proof state before:
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
this : b = b' ∨ b ∈ bs
⊢ encode b < encode (b' :: bs)
Tactic:
rcases this with (rfl | lt) <;> simp
Proof state after:
case cons.inl
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b :: bs
⊢ encode b < (encode b).pair (encode bs) + 1

case cons.inr
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
lt : b ∈ bs
⊢ encode b < (encode b').pair (encode bs) + 1
Theorem: Encodable.encode_list_lt
Proof state before:
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
⊢ b = b' ∨ b ∈ bs
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Encodable.encode_list_lt
Proof state before:
case cons.inl
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b :: bs
⊢ encode b < (encode b).pair (encode bs) + 1
Tactic:
exact Nat.lt_succ.mpr (Nat.left_le_pair (encode b) (encode bs))
Proof state after:
no goals
Theorem: Encodable.encode_list_lt
Proof state before:
case cons.inr
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
lt : b ∈ bs
⊢ encode b < (encode b').pair (encode bs) + 1
Tactic:
exact Nat.lt.step <| lt_of_lt_of_le (ih lt) (Nat.right_le_pair (encode b') (encode bs))
Proof state after:
no goals
Theorem: Primrec.finArrow_list_ofFn
Proof state before:
σ : Type u_1
α✝ : Type u_2
β : α✝ → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α✝
inst✝⁵ : (a : α✝) → Fintype (β a)
inst✝⁴ : (a : α✝) → DecidableEq (β a)
inst✝³ : (a : α✝) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
k : ℕ
α : Type u_5
inst✝ : Primcodable α
this : Primrec fun e => encode (decode e)
e : ℕ
⊢ encode (decode e) = encode (Option.map List.ofFn (decode e))
Tactic:
rcases (Encodable.decode e) <;> simp[Encodable.encode_finArrow]
Proof state after:
no goals
Theorem: Primrec.sigma_finArrow_list_ofFn
Proof state before:
σ : Type u_1
α✝ : Type u_2
β : α✝ → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α✝
inst✝⁵ : (a : α✝) → Fintype (β a)
inst✝⁴ : (a : α✝) → DecidableEq (β a)
inst✝³ : (a : α✝) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
α : Type u_5
inst✝ : Primcodable α
this : Primrec fun p => (encode p).unpair.2
x✝ : (k : ℕ) × (Fin k → α)
k : ℕ
v : Fin k → α
⊢ (encode ⟨k, v⟩).unpair.2 = encode (List.ofFn ⟨k, v⟩.snd)
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
Theorem: Primrec.sigma_fst
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
⊢ ∀ (n : ℕ),
    ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
      Option.map Sigma.fst (decode n)
Tactic:
intro n
Proof state after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst (decode n)
Theorem: Primrec.sigma_fst
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst (decode n)
Tactic:
simp
Proof state after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst ((decode n.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode n.unpair.2))
Theorem: Primrec.sigma_fst
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst ((decode n.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode n.unpair.2))
Tactic:
rcases (decode n.unpair.1) with (_ | a) <;> simp
Proof state after:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)
Theorem: Primrec.sigma_fst
Proof state before:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)
Tactic:
{ simp[encodeDecode_eq_encode_map_decode, Function.comp] }
Proof state after:
no goals
Theorem: Primrec.sigma_fst
Proof state before:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)
Tactic:
simp[encodeDecode_eq_encode_map_decode, Function.comp]
Proof state after:
no goals
Theorem: Primrec.sigma_prod_left
Proof state before:
σ : Type u_1
α✝ : Type u_2
β✝ : α✝ → Type u_3
γ✝ : Type u_4
inst✝¹¹ : Primcodable σ
inst✝¹⁰ : Primcodable α✝
inst✝⁹ : (a : α✝) → Fintype (β✝ a)
inst✝⁸ : (a : α✝) → DecidableEq (β✝ a)
inst✝⁷ : (a : α✝) → Primcodable (β✝ a)
inst✝⁶ : PrimrecCard β✝
inst✝⁵ : Primcodable γ✝
α : Type u_7
β : α → Type u_5
γ : α → Type u_6
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : (a : α) → Primcodable (γ a)
inst✝¹ : UniformlyPrimcodable β
inst✝ : UniformlyPrimcodable γ
this : Primrec fun p => (encode p).unpair.1.pair (encode p).unpair.2.unpair.1
x✝ : (a : α) × β a × γ a
k : α
b : β k
v : γ k
⊢ (encode ⟨k, (b, v)⟩).unpair.1.pair (encode ⟨k, (b, v)⟩).unpair.2.unpair.1 =
    encode ⟨⟨k, (b, v)⟩.fst, ⟨k, (b, v)⟩.snd.1⟩
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
Theorem: Primrec.sigma_prod_right
Proof state before:
σ : Type u_1
α✝ : Type u_2
β✝ : α✝ → Type u_3
γ✝ : Type u_4
inst✝¹¹ : Primcodable σ
inst✝¹⁰ : Primcodable α✝
inst✝⁹ : (a : α✝) → Fintype (β✝ a)
inst✝⁸ : (a : α✝) → DecidableEq (β✝ a)
inst✝⁷ : (a : α✝) → Primcodable (β✝ a)
inst✝⁶ : PrimrecCard β✝
inst✝⁵ : Primcodable γ✝
α : Type u_7
β : α → Type u_5
γ : α → Type u_6
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : (a : α) → Primcodable (γ a)
inst✝¹ : UniformlyPrimcodable β
inst✝ : UniformlyPrimcodable γ
this : Primrec fun p => (encode p).unpair.1.pair (encode p).unpair.2.unpair.2
x✝ : (a : α) × β a × γ a
k : α
b : β k
v : γ k
⊢ (encode ⟨k, (b, v)⟩).unpair.1.pair (encode ⟨k, (b, v)⟩).unpair.2.unpair.2 =
    encode ⟨⟨k, (b, v)⟩.fst, ⟨k, (b, v)⟩.snd.2⟩
Tactic:
simp[encode_finArrow]
Proof state after:
no goals
Theorem: Primrec.sigma_pair
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
a : α
⊢ Primrec fun a_1 => encode ⟨a, a_1⟩
Tactic:
simp
Proof state after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
a : α
⊢ Primrec fun a_1 => (encode a).pair (encode a_1)
Theorem: Primrec.sigma_pair
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
a : α
⊢ Primrec fun a_1 => (encode a).pair (encode a_1)
Tactic:
exact Primrec₂.natPair.comp (const _) Primrec.encode
Proof state after:
no goals
Theorem: Primrec.encode_of_uniform
Proof state before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
⊢ Primrec fun x => encode (b x).snd
Tactic:
have : Primrec (fun x => (Nat.unpair (encode (b x))).2) := snd.comp (unpair.comp $ Primrec.encode.comp hb)
Proof state after:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ Primrec fun x => encode (b x).snd
Theorem: Primrec.encode_of_uniform
Proof state before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ Primrec fun x => encode (b x).snd
Tactic:
exact this.of_eq <| by
  intro x
  rcases b x with ⟨a, b⟩
  simp[encode_sigma_val]
Proof state after:
no goals
Theorem: Primrec.encode_of_uniform
Proof state before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ ∀ (n : σ), (encode (b n)).unpair.2 = encode (b n).snd
Tactic:
intro x
Proof state after:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
x : σ
⊢ (encode (b x)).unpair.2 = encode (b x).snd
Theorem: Primrec.encode_of_uniform
Proof state before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
x : σ
⊢ (encode (b x)).unpair.2 = encode (b x).snd
Tactic:
rcases b x with ⟨a, b⟩
Proof state after:
case mk
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b✝ : σ → (a : α) × β a
hb : Primrec b✝
this : Primrec fun x => (encode (b✝ x)).unpair.2
x : σ
a : α
b : β a
⊢ (encode ⟨a, b⟩).unpair.2 = encode ⟨a, b⟩.snd
Theorem: Primrec.encode_of_uniform
Proof state before:
case mk
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b✝ : σ → (a : α) × β a
hb : Primrec b✝
this : Primrec fun x => (encode (b✝ x)).unpair.2
x : σ
a : α
b : β a
⊢ (encode ⟨a, b⟩).unpair.2 = encode ⟨a, b⟩.snd
Tactic:
simp[encode_sigma_val]
Proof state after:
no goals
Theorem: Primrec.finArrow_map
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
⊢ Primrec fun v i => f (v i)
Tactic:
have : Primrec (fun e => encode $ ((encodeDecode (Fin k → α) e).bind
  $ fun c => (decode c : Option (List α)).map (fun l => l.map f)) : ℕ → ℕ) :=
  (Primrec.encode.comp $ option_bind Primrec.encodeDecode
    (option_map (Primrec.decode.comp snd) (by apply list_map snd (hf.comp₂ Primrec₂.right))))
Proof state after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
⊢ Primrec fun v i => f (v i)
Theorem: Primrec.finArrow_map
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
⊢ Primrec fun v i => f (v i)
Tactic:
exact decode_iff.mp (encode_iff.mp $ this.of_eq $ fun e => by
  simp[encodeDecode_eq_encode_map_decode, decode_finArrow]
  rcases (decode e) with (_ | as) <;> simp [Function.comp]
  { rcases (as.toVector k) with (_ | v) <;> simp
    { simp[encode_finArrow, Function.comp] } })
Proof state after:
no goals
Theorem: Primrec.finArrow_map
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
⊢ Primrec₂ fun p l => List.map f l
Tactic:
apply list_map snd (hf.comp₂ Primrec₂.right)
Proof state after:
no goals
Theorem: Primrec.finArrow_map
Proof state before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
⊢ encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c)) =
    encode (Option.map (fun v i => f (v i)) (decode e))
Tactic:
simp[encodeDecode_eq_encode_map_decode, decode_finArrow]
Proof state after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
e : ℕ
⊢ encode
      ((Option.map encode ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l))).bind
        fun a => Option.map (fun l => List.map f l) (decode a)) =
    encode
      (Option.map (fun v i => f (v i))
        ((decode e).bind fun l => Option.map (⇑(Equiv.vectorEquivFin α k)) (List.toVector k l)))