internlm/Lean-Github huggingface dataset:
Theorem: Primrec.of_subtype_iff
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 β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : β → { a // p a }
this : Primcodable (Subtype p) := Primcodable.subtype hp
hf : Primrec fun x => ↑(f x)
b : β
⊢ encode ↑(f b) = encode (f b)
Tactic:
simp[Encodable.Subtype.encode_eq]
Proof state after:
no goals
Theorem: Primrec.nat_toFin
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
⊢ ∀ (n_1 : ℕ), (if id n_1 < n then n_1.succ else 0) = encode (n.toFin n_1)
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if id x < n then x.succ else 0) = encode (n.toFin x)
Theorem: Primrec.nat_toFin
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if id x < n then x.succ else 0) = encode (n.toFin x)
Tactic:
simp[Nat.toFin]
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if x < n then x + 1 else 0) = encode (if hx : x < n then some ⟨x, hx⟩ else none)
Theorem: Primrec.nat_toFin
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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
⊢ (if x < n then x + 1 else 0) = encode (if hx : x < n then some ⟨x, hx⟩ else none)
Tactic:
by_cases hx : x < n <;> simp[hx]
Proof state after:
case pos
σ : 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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
hx : x < n
⊢ x = encode ⟨x, ⋯⟩
Theorem: Primrec.nat_toFin
Proof state before:
case pos
σ : 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 γ
n : ℕ
this : Primrec fun x => if x < n then x + 1 else 0
x : ℕ
hx : x < n
⊢ x = encode ⟨x, ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Primrec.decide_eq_iff
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 γ
p : Prop
inst✝ : Decidable p
b : Bool
⊢ decide p = b ↔ (p ↔ b = true)
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: Primrec.lawfulbeq
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✝¹ : BEq α
inst✝ : LawfulBEq α
⊢ Primrec₂ BEq.beq
Tactic:
haveI : DecidableEq α := Encodable.decidableEqOfEncodable α
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
⊢ Primrec₂ BEq.beq
Theorem: Primrec.lawfulbeq
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
⊢ Primrec₂ BEq.beq
Tactic:
exact Primrec₂.of_eq Primrec.eq (by intro a b; simp[decide_eq_iff])
Proof state after:
no goals
Theorem: Primrec.lawfulbeq
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
⊢ ∀ (a b : α), decide (a = b) = (a == b)
Tactic:
intro a b
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
a b : α
⊢ decide (a = b) = (a == b)
Theorem: Primrec.lawfulbeq
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : DecidableEq α
a b : α
⊢ decide (a = b) = (a == b)
Tactic:
simp[decide_eq_iff]
Proof state after:
no goals
Theorem: Primrec.list_mem
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✝¹ : BEq α
inst✝ : LawfulBEq α
⊢ PrimrecRel fun x x_1 => x ∈ x_1
Tactic:
have : Primrec₂ (fun a l => l.foldr (fun a' ih => (a == a') || ih) false : α → List α → Bool) :=
  to₂' <| list_foldr snd (const false)
    <| (dom_bool₂ Bool.or).comp₂
      (Primrec.lawfulbeq.comp₂ (fst.comp₂ Primrec₂.left) (fst.comp₂ Primrec₂.right))
      (snd.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 γ
inst✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ PrimrecRel fun x x_1 => x ∈ x_1
Theorem: Primrec.list_mem
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ PrimrecRel fun x x_1 => x ∈ x_1
Tactic:
exact this.of_eq <| by intro a as; induction as <;> simp[*]; symm; simp[decide_eq_iff]
Proof state after:
no goals
Theorem: Primrec.list_mem
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
⊢ ∀ (a : α) (b : List α), List.foldr (fun a' ih => a == a' || ih) false b = decide ((fun x x_1 => x ∈ x_1) a b)
Tactic:
intro a as
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a : α
as : List α
⊢ List.foldr (fun a' ih => a == a' || ih) false as = decide ((fun x x_1 => x ∈ x_1) a as)
Theorem: Primrec.list_mem
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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a : α
as : List α
⊢ List.foldr (fun a' ih => a == a' || ih) false as = decide ((fun x x_1 => x ∈ x_1) a as)
Tactic:
induction as <;> simp[*]
Proof state after:
case cons
σ : 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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ (a == head✝ || decide (a ∈ tail✝)) = decide (a ∈ head✝ :: tail✝)
Theorem: Primrec.list_mem
Proof state before:
case cons
σ : 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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ (a == head✝ || decide (a ∈ tail✝)) = decide (a ∈ head✝ :: tail✝)
Tactic:
symm
Proof state after:
case cons
σ : 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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ decide (a ∈ head✝ :: tail✝) = (a == head✝ || decide (a ∈ tail✝))
Theorem: Primrec.list_mem
Proof state before:
case cons
σ : 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✝¹ : BEq α
inst✝ : LawfulBEq α
this : Primrec₂ fun a l => List.foldr (fun a' ih => a == a' || ih) false l
a head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun a' ih => a == a' || ih) false tail✝ = decide ((fun x x_1 => x ∈ x_1) a tail✝)
⊢ decide (a ∈ head✝ :: tail✝) = (a == head✝ || decide (a ∈ tail✝))
Tactic:
simp[decide_eq_iff]
Proof state after:
no goals
Theorem: Primrec.list_subset
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✝ : DecidableEq α
⊢ PrimrecRel fun x x_1 => x ⊆ x_1
Tactic:
have : Primrec₂ (fun l₁ l₂ => l₁.foldr (fun a' ih => a' ∈ l₂ && ih) true : List α → List α → Bool) :=
  to₂' <| list_foldr fst (const true)
    <| (dom_bool₂ _).comp₂
      (list_mem.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.left))
      (snd.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 γ
inst✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
⊢ PrimrecRel fun x x_1 => x ⊆ x_1
Theorem: Primrec.list_subset
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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
⊢ PrimrecRel fun x x_1 => x ⊆ x_1
Tactic:
exact this.of_eq <| by intro l₁ l₂; induction l₁ <;> simp[*]
Proof state after:
no goals
Theorem: Primrec.list_subset
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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
⊢ ∀ (a b : List α), List.foldr (fun a' ih => decide (a' ∈ b) && ih) true a = decide ((fun x x_1 => x ⊆ x_1) a b)
Tactic:
intro l₁ l₂
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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
l₁ l₂ : List α
⊢ List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁ = decide ((fun x x_1 => x ⊆ x_1) l₁ l₂)
Theorem: Primrec.list_subset
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✝ : DecidableEq α
this : Primrec₂ fun l₁ l₂ => List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁
l₁ l₂ : List α
⊢ List.foldr (fun a' ih => decide (a' ∈ l₂) && ih) true l₁ = decide ((fun x x_1 => x ⊆ x_1) l₁ l₂)
Tactic:
induction l₁ <;> simp[*]
Proof state after:
no goals
Theorem: Primrec.list_all
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
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
⊢ ∀ (n : α), List.foldr (fun b s => p n b && s) true (l n) = (l n).all (p n)
Tactic:
intro a
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
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
⊢ List.foldr (fun b s => p a b && s) true (l a) = (l a).all (p a)
Theorem: Primrec.list_all
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
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
⊢ List.foldr (fun b s => p a b && s) true (l a) = (l a).all (p a)
Tactic:
generalize l a = bs
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
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
bs : List β
⊢ List.foldr (fun b s => p a b && s) true bs = bs.all (p a)
Theorem: Primrec.list_all
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
β : Type u_6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Primrec₂ p
hl : Primrec l
this : Primrec fun a => List.foldr (fun b s => p a b && s) true (l a)
a : α
bs : List β
⊢ List.foldr (fun b s => p a b && s) true bs = bs.all (p a)
Tactic:
induction bs <;> simp[*]
Proof state after:
no goals
Theorem: Primrec.list_replicate
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 α
⊢ Primrec₂ List.replicate
Tactic:
have : Primrec₂ (fun p ih => p.2 :: ih.2 : ℕ × α → ℕ × List α → List α) :=
  list_cons.comp₂ (snd.comp₂ .left) (snd.comp₂ .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 γ
α : Type u_5
inst✝ : Primcodable α
this : Primrec₂ fun p ih => p.2 :: ih.2
⊢ Primrec₂ List.replicate
Theorem: Primrec.list_replicate
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 ih => p.2 :: ih.2
⊢ Primrec₂ List.replicate
Tactic:
exact (Primrec.nat_rec' Primrec.fst (.const []) this).of_eq <| by
  rintro ⟨n, a⟩; simp; induction n <;> simp[*]
Proof state after:
no goals
Theorem: Primrec.list_replicate
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 ih => p.2 :: ih.2
⊢ ∀ (n : ℕ × α), Nat.rec [] (fun n_1 IH => n.2 :: (n_1, IH).2) n.1 = List.replicate n.1 n.2
Tactic:
rintro ⟨n, a⟩
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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n_1 IH => (n, a).2 :: (n_1, IH).2) (n, a).1 = List.replicate (n, a).1 (n, a).2
Theorem: Primrec.list_replicate
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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n_1 IH => (n, a).2 :: (n_1, IH).2) (n, a).1 = List.replicate (n, a).1 (n, a).2
Tactic:
simp
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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n IH => a :: IH) n = List.replicate n a
Theorem: Primrec.list_replicate
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 α
this : Primrec₂ fun p ih => p.2 :: ih.2
n : ℕ
a : α
⊢ Nat.rec [] (fun n IH => a :: IH) n = List.replicate n a
Tactic:
induction n <;> simp[*]
Proof state after:
no goals
Theorem: Computable.list_all
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
⊢ Computable fun a => (l a).all (p a)
Tactic:
let f : α → ℕ → Bool := fun a n => n.recOn true (fun m ih => ((l a).reverse.get? m).casesOn false (fun b => p a b && ih))
Proof state after:
α✝ : Type u_1
β✝ : Type u_2
σ : Type u_3
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_4
β : Type u_5
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
l : α → List β
hp : Computable₂ p
hl : Computable l
f : α → ℕ → Bool :=
  fun a n => Nat.recOn n true fun m ih => Option.casesOn ((l a).reverse.get? m) false fun b => p a b && ih
⊢ Computable fun a => (l a).all (p a)