internlm/Lean-Github huggingface dataset:
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
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)
Tactic:
have : Computable₂ (fun q₁ q₂ => ((l q₁.1).reverse.get? q₂.1).casesOn false (fun b => p q₁.1 b && q₂.2)
  : α × ℕ → ℕ × Bool → Bool) :=
  to₂' <| option_casesOn
    (list_get?.comp (list_reverse.comp $ hl.comp $ fst.comp fst) (fst.comp snd))
    (const false) (by apply dom_bool₂.comp₂ (hp.comp₂ (fst.comp₂ $ fst.comp₂ .left) .right) (snd.comp₂ $ snd.comp₂ .left))
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
⊢ Computable fun a => (l a).all (p a)
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
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
⊢ Computable fun a => (l a).all (p a)
Tactic:
have hf : Computable₂ f := (nat_rec snd (const true) this).to₂
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
⊢ Computable fun a => (l a).all (p a)
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
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 p_1 val => (fun b => p p_1.1.1 b && p_1.2.2) val
Tactic:
apply dom_bool₂.comp₂ (hp.comp₂ (fst.comp₂ $ fst.comp₂ .left) .right) (snd.comp₂ $ snd.comp₂ .left)
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
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
⊢ ∀ (n : α), f (id n) (l n).length = (l n).all (p n)
Tactic:
intro a
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ f (id a) (l a).length = (l a).all (p a)
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
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ f (id a) (l a).length = (l a).all (p a)
Tactic:
simp [f]
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((l a).reverse.get? m)) (l a).length =
    (l a).all (p a)
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
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((l a).reverse.get? m)) (l a).length =
    (l a).all (p a)
Tactic:
generalize l a = la
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
la : List β
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la.reverse.get? m)) la.length = la.all (p a)
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
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
la : List β
⊢ Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la.reverse.get? m)) la.length = la.all (p a)
Tactic:
induction' la with b la' ih <;> simp
Proof state after:
case cons
α✝ : 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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
Theorem: Computable.list_all
Proof state before:
case cons
α✝ : 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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
Tactic:
have : List.get? (List.reverse la' ++ [b]) la'.length = some b := by
  simpa using List.get?_concat_length la'.reverse b
Proof state after:
case cons
α✝ : 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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
Theorem: Computable.list_all
Proof state before:
case cons
α✝ : 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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ Option.rec false
      (fun val =>
        p a val &&
          Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m))
            la'.length)
      ((la'.reverse ++ [b]).get? la'.length) =
    (p a b && la'.all (p a))
Tactic:
simp [this]
Proof state after:
case cons
α✝ : 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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ (p a b &&
      Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m)) la'.length) =
    (p a b && la'.all (p a))
Theorem: Computable.list_all
Proof state before:
case cons
α✝ : 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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ (p a b &&
      Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m)) la'.length) =
    (p a b && la'.all (p a))
Tactic:
rw [←ih]
Proof state after:
case cons
α✝ : 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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ (p a b &&
      Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) ((la'.reverse ++ [b]).get? m)) la'.length) =
    (p a b && Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length)
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
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
this : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
⊢ (la'.reverse ++ [b]).get? la'.length = some b
Tactic:
simpa using List.get?_concat_length la'.reverse b
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
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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
⊢ ∀ m < la'.length,
    ∀ (a_2 : Bool),
      Option.rec false (fun val => p a val && a_2) ((la'.reverse ++ [b]).get? m) =
        Option.rec false (fun val => p a val && a_2) (la'.reverse.get? m)
Tactic:
intro m hm k
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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)
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
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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)
Tactic:
have : (la'.reverse ++ [b]).get? m = la'.reverse.get? m := List.get?_append (by simp[hm])
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
this✝¹ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this✝ : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
this : (la'.reverse ++ [b]).get? m = la'.reverse.get? m
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)
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
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
this✝¹ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this✝ : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
this : (la'.reverse ++ [b]).get? m = la'.reverse.get? m
⊢ Option.rec false (fun val => p a val && k) ((la'.reverse ++ [b]).get? m) =
    Option.rec false (fun val => p a val && k) (la'.reverse.get? m)
Tactic:
simp [this]
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
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
this✝ : Computable₂ fun q₁ q₂ => Option.casesOn ((l q₁.1).reverse.get? q₂.1) false fun b => p q₁.1 b && q₂.2
hf : Computable₂ f
a : α
b : β
la' : List β
ih :
  Nat.rec true (fun m ih => Option.rec false (fun val => p a val && ih) (la'.reverse.get? m)) la'.length = la'.all (p a)
this : (la'.reverse ++ [b]).get? la'.length = some b
m : ℕ
hm : m < la'.length
k : Bool
⊢ m < la'.reverse.length
Tactic:
simp[hm]
Proof state after:
no goals
Theorem: Partrec.merge_iff
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a
Tactic:
rcases merge hf hg H with ⟨k, _, hk⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
k : α →. σ
left✝ : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a
Theorem: Partrec.merge_iff
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
a : α
x : σ
k : α →. σ
left✝ : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a
Tactic:
exact Classical.epsilon_spec (p := fun k => ∀ a x, x ∈ k a ↔ x ∈ f a ∨ x ∈ g a) ⟨k, hk⟩ a x
Proof state after:
no goals
Theorem: Partrec.mergep
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
⊢ Partrec (f.merge g)
Tactic:
rcases merge hf hg H with ⟨k, pk, hk⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
pk : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ Partrec (f.merge g)
Theorem: Partrec.mergep
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
pk : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
⊢ Partrec (f.merge g)
Tactic:
exact pk.of_eq fun a => by ext a; simp[hk, merge_iff hf hg H]
Proof state after:
no goals
Theorem: Partrec.mergep
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
pk : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
a : α
⊢ k a = f.merge g a
Tactic:
ext a
Proof state after:
case H
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
pk : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
a✝ : α
a : σ
⊢ a ∈ k a✝ ↔ a ∈ f.merge g a✝