Theorem: buildColumn_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {τ : Type u} (t : Table sch) (c : η) (f : Row sch → Option τ),
    header (buildColumn t c f) = List.append (header t) [c]
Tactic:
intros τ t c f
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ header (buildColumn t c f) = List.append (header t) [c]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ header (buildColumn t c f) = List.append (header t) [c]
Tactic:
simp [header, Schema.names]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.map Prod.fst (Schema.append sch [(c, τ)]) = List.map Prod.fst sch ++ [c]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.map Prod.fst (Schema.append sch [(c, τ)]) = List.map Prod.fst sch ++ [c]
Tactic:
induction sch with
| nil => simp [List.map, List.append]
| cons s ss ih =>
 simp only [List.map]
 rw [ih]
 simp [List.append]
 exact Table.mk []
 exact (λ x => f (Row.cons Cell.emp x))
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
t : Table []
f : Row [] → Option τ
⊢ List.map Prod.fst (Schema.append [] [(c, τ)]) = List.map Prod.fst [] ++ [c]
Tactic:
simp [List.map, List.append]
State after:
no goals

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ List.map Prod.fst (Schema.append (s :: ss) [(c, τ)]) = List.map Prod.fst (s :: ss) ++ [c]
Tactic:
simp only [List.map]
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ s.fst :: List.map Prod.fst (Schema.append ss [(c, τ)]) = s.fst :: List.map Prod.fst ss ++ [c]

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ s.fst :: List.map Prod.fst (Schema.append ss [(c, τ)]) = s.fst :: List.map Prod.fst ss ++ [c]
Tactic:
rw [ih]
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ s.fst :: (List.map Prod.fst ss ++ [c]) = s.fst :: List.map Prod.fst ss ++ [c]

case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ s.fst :: (List.map Prod.fst ss ++ [c]) = s.fst :: List.map Prod.fst ss ++ [c]

case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
simp [List.append]
State after:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ

State before:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
exact Table.mk []
State after:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ

State before:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
c : η
s : Header
ss : List Header
ih : Table ss → (Row ss → Option τ) → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
exact (λ x => f (Row.cons Cell.emp x))
State after:
no goals