Theorem: addColumn_spec1 (Table/Proofs.lean)

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

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
⊢ header (addColumn t c vs) = List.append (header t) [c]
Tactic:
simp [header, addColumn, Schema.names]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (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
inst : DecidableEq τ
t : Table sch
c : η
vs : List (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 dropColumn t _
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
c : η
vs : List (Option τ)
t : Table []
⊢ 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
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ 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
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ 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
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ 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
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ s.fst :: (List.map Prod.fst ss ++ [c]) = s.fst :: List.map Prod.fst ss ++ [c]

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

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

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

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih : Table ss → List.map Prod.fst (Schema.append ss [(c, τ)]) = List.map Prod.fst ss ++ [c]
t : Table (s :: ss)
⊢ Table ss
Tactic:
exact dropColumn t _
State after:
no goals