internlm/Lean-Github huggingface dataset:
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema [("final", Nat)]
Tactic:
apply IsQuizSchema.consNonQuiz (by decide)
Proof state after:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ String.startsWith "final" "quiz" = false
Tactic:
decide
Proof state after:
no goals
Theorem: gradebook_schema_is_quiz_schema
Proof state before:
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema []
Tactic:
apply IsQuizSchema.nil
Proof state after:
no goals
Theorem: nrows_groupBySubtractive
Proof state before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
⊢ nrows (groupBySubtractive t c) ≤ nrows t
Tactic:
have h_gbs := groupBySubtractive_spec7 t c hc
Proof state after:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ nrows (groupBySubtractive t c) ≤ nrows t
Theorem: nrows_groupBySubtractive
Proof state before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ nrows (groupBySubtractive t c) ≤ nrows t
Tactic:
rw [h_gbs]
Proof state after:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ nrows t
Theorem: nrows_groupBySubtractive
Proof state before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ nrows t
Tactic:
rw [←getColumn2_spec2 t c hc]
Proof state after:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ List.length (getColumn2 t c)
Theorem: nrows_groupBySubtractive
Proof state before:
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ List.length (List.unique (getColumn2 t c)) ≤ List.length (getColumn2 t c)
Tactic:
apply List.length_unique_le
Proof state after:
no goals
Theorem: Schema.lookup_of_colImpliesName
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
ss : List Header
⊢ lookup ((nm, τ) :: ss) { fst := nm, snd := colImpliesName HasCol.hd } = (nm, τ)
Tactic:
rw [colImpliesName_eq_1 (sch' := ss) (hdr := (nm, τ)),
    lookup_eq_1]
Proof state after:
no goals
Theorem: Schema.lookup_of_colImpliesName
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup (head✝ :: ss) { fst := nm, snd := colImpliesName (HasCol.tl h) } = (nm, τ)
Tactic:
rw [colImpliesName_eq_2, lookup_eq_2]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup ss { fst := nm, snd := colImpliesName h } = (nm, τ)
Theorem: Schema.lookup_of_colImpliesName
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup ss { fst := nm, snd := colImpliesName h } = (nm, τ)
Tactic:
apply lookup_of_colImpliesName
Proof state after:
no goals
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
cn : CertifiedName s
⊢ lookupType s cn = (lookup s cn).snd
Tactic:
cases cn with | mk nm pf =>
induction pf with
| hd =>
  simp only [lookupType]
  rw [lookup_eq_1]
| tl h ih =>
  simp only [lookupType]
  rw [lookup_eq_2]
  apply ih
Proof state after:
no goals
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
case mk
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
pf : HasName nm s
⊢ lookupType s { fst := nm, snd := pf } = (lookup s { fst := nm, snd := pf }).snd
Tactic:
induction pf with
| hd =>
  simp only [lookupType]
  rw [lookup_eq_1]
| tl h ih =>
  simp only [lookupType]
  rw [lookup_eq_2]
  apply ih
Proof state after:
no goals
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
case mk.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookupType ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    (lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd }).snd
Tactic:
simp only [lookupType]
Proof state after:
case mk.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ τ✝ = (lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd }).snd
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
case mk.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ τ✝ = (lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd }).snd
Tactic:
rw [lookup_eq_1]
Proof state after:
no goals
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h } =
    (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd
Tactic:
simp only [lookupType]
Proof state after:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd
Tactic:
rw [lookup_eq_2]
Proof state after:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
Theorem: Schema.lookupType_eq_snd_lookup
Proof state before:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
Tactic:
apply ih
Proof state after:
no goals
Theorem: addRows_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (rs : List (Row sch)), nrows (addRows t rs) = nrows t + List.length rs
Tactic:
intro t rs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
rs : List (Row sch)
⊢ nrows (addRows t rs) = nrows t + List.length rs
Theorem: addRows_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
rs : List (Row sch)
⊢ nrows (addRows t rs) = nrows t + List.length rs
Tactic:
simp only [nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
rs : List (Row sch)
⊢ List.length (addRows t rs).rows = List.length t.rows + List.length rs
Theorem: addRows_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
rs : List (Row sch)
⊢ List.length (addRows t rs).rows = List.length t.rows + List.length rs
Tactic:
exact List.length_append t.rows rs
Proof state after:
no goals
Theorem: addColumn_spec1
Proof 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
Proof 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]
Theorem: addColumn_spec1
Proof 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]
Proof 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]
Theorem: addColumn_spec1
Proof 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 _
Proof state after:
no goals
Theorem: addColumn_spec1
Proof 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]
Proof state after:
no goals
Theorem: addColumn_spec1
Proof 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]
Proof 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]
Theorem: addColumn_spec1
Proof 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]
Proof 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
Theorem: addColumn_spec1
Proof 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]
Proof 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
Theorem: addColumn_spec1
Proof 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 _
Proof state after:
no goals
Theorem: addColumn_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (vs : List (Option τ)),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
      τ
Tactic:
intros t c vs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
⊢ Schema.lookupType (schema (addColumn t c vs))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
    τ
Theorem: addColumn_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
⊢ Schema.lookupType (schema (addColumn t c vs))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
    τ
Tactic:
induction sch with
| nil =>
  simp only [Schema.lookupType]
| cons s ss ih =>
  simp only [Schema.lookupType]
  apply ih (dropColumn t _)
Proof state after:
no goals
Theorem: addColumn_spec3
Proof state before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
vs : List (Option τ)
t : Table []
⊢ Schema.lookupType (schema (addColumn t c vs))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead [] c τ []) } =
    τ
Tactic:
simp only [Schema.lookupType]
Proof state after:
no goals
Theorem: addColumn_spec3
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih :
  ∀ (t : Table ss),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
⊢ Schema.lookupType (schema (addColumn t c vs))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead (s :: ss) c τ []) } =
    τ
Tactic:
simp only [Schema.lookupType]
Proof state after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih :
  ∀ (t : Table ss),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
Theorem: addColumn_spec3
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
vs : List (Option τ)
s : Header
ss : List Header
ih :
  ∀ (t : Table ss),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
Tactic:
apply ih (dropColumn t _)
Proof state after:
no goals
Theorem: addColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {τ : Type u} [inst : DecidableEq τ] (t : Table sch) (c : η) (vs : List (Option τ)),
    List.length vs = nrows t → nrows (addColumn t c vs) = nrows t
Tactic:
intros τ inst t c vs h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = nrows t
⊢ nrows (addColumn t c vs) = nrows t
Theorem: addColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = nrows t
⊢ nrows (addColumn t c vs) = nrows t
Tactic:
simp only [nrows, addColumn, Schema.length_eq_List_length] at *
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length (List.map (fun x => Row.addColumn x.fst c x.snd) (List.zip t.rows vs)) = List.length t.rows
Theorem: addColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length (List.map (fun x => Row.addColumn x.fst c x.snd) (List.zip t.rows vs)) = List.length t.rows
Tactic:
simp only [List.length_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length (List.zip t.rows vs) = List.length t.rows
Theorem: addColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length (List.zip t.rows vs) = List.length t.rows
Tactic:
rw [List.zip_length_eq_of_length_eq]
Proof state after:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length t.rows = List.length vs
Theorem: addColumn_spec4
Proof state before:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
h : List.length vs = List.length t.rows
⊢ List.length t.rows = List.length vs
Tactic:
exact Eq.symm h
Proof state after:
no goals
Theorem: buildColumn_spec2
Proof 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
Proof 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]
Theorem: buildColumn_spec2
Proof 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]
Proof 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]
Theorem: buildColumn_spec2
Proof 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))
Proof state after:
no goals
Theorem: buildColumn_spec2
Proof 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]
Proof state after:
no goals
Theorem: buildColumn_spec2
Proof 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]
Proof 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]
Theorem: buildColumn_spec2
Proof 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]
Proof 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 τ