Theorem: Primrec.list_lookup (Logic/Vorspiel/OmegaRec.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
⊢ Primrec₂ List.lookup
Tactic:
have : Primrec₂ (fun p q => bif p.1 == q.1.1 then q.1.2 else q.2.2 : α × List (α × β) → (α × β) × List (α × β) × Option β → Option β) :=
  cond (Primrec.beq.comp (fst.comp fst) (fst.comp $ fst.comp snd))
    (option_some.comp $ snd.comp $ fst.comp snd) (snd.comp $ snd.comp snd)
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
⊢ Primrec₂ List.lookup

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
⊢ Primrec₂ List.lookup
Tactic:
have : Primrec₂ (fun a l => List.recOn l none (fun p _ ih => bif a == p.1 then p.2 else ih) : α → List (α × β) → Option β) :=
  to₂ <| list_rec snd (const none) this
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
⊢ Primrec₂ List.lookup

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
⊢ Primrec₂ List.lookup
Tactic:
exact this.of_eq <| fun a ps => by
  induction' ps with p ps <;> simp[List.lookup, *]
  cases ha : a == p.1 <;> simp[ha]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
ps : List (α × β)
⊢ (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
Tactic:
induction' ps with p ps <;> simp[List.lookup, *]
State after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
p : α × β
ps : List (α × β)
tail_ih✝ : (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps

State before:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
p : α × β
ps : List (α × β)
tail_ih✝ : (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps
Tactic:
cases ha : a == p.1 <;> simp[ha]
State after:
no goals