internlm/Lean-Github huggingface dataset:
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 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]
Proof 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 τ
Theorem: buildColumn_spec2
Proof 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 []
Proof 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 τ
Theorem: buildColumn_spec2
Proof 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))
Proof state after:
no goals
Theorem: buildColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (f : Row sch → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
      τ
Tactic:
intros t c f
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
f : Row sch → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
    τ
Theorem: buildColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
f : Row sch → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { 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
  . exact (dropColumn t _)
  . exact f ∘ (Row.cons Cell.emp)
Proof state after:
no goals
Theorem: buildColumn_spec4
Proof state before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
t : Table []
f : Row [] → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead [] c τ []) } =
    τ
Tactic:
simp only [Schema.lookupType]
Proof state after:
no goals
Theorem: buildColumn_spec4
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { 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 : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
Theorem: buildColumn_spec4
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
Tactic:
apply ih
Proof state after:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Theorem: buildColumn_spec4
Proof state before:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
. exact (dropColumn t _)
Proof state after:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Theorem: buildColumn_spec4
Proof state before:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
. exact f ∘ (Row.cons Cell.emp)
Proof state after:
no goals
Theorem: buildColumn_spec4
Proof state before:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss
Tactic:
exact (dropColumn t _)
Proof state after:
no goals
Theorem: buildColumn_spec4
Proof state before:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
exact f ∘ (Row.cons Cell.emp)
Proof state after:
no goals
Theorem: buildColumn_spec5
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {τ : Type u} (t : Table sch) (c : η) (f : Row sch → Option τ), nrows (buildColumn t c f) = nrows t
Tactic:
intros τ t c f
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ nrows (buildColumn t c f) = nrows t
Theorem: buildColumn_spec5
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ nrows (buildColumn t c f) = nrows t
Tactic:
simp only [nrows, buildColumn, addColumn, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.length (List.map (fun x => Row.addColumn x.fst c x.snd) (List.zip t.rows (List.map f t.rows))) =
    List.length t.rows
Theorem: buildColumn_spec5
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.length (List.map (fun x => Row.addColumn x.fst c x.snd) (List.zip t.rows (List.map f t.rows))) =
    List.length t.rows
Tactic:
rw [List.length_map, List.zip_length_eq_of_length_eq]
Proof state after:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.length t.rows = List.length (List.map f t.rows)
Theorem: buildColumn_spec5
Proof state before:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.length t.rows = List.length (List.map f t.rows)
Tactic:
apply Eq.symm
Proof state after:
case h.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.length (List.map f t.rows) = List.length t.rows
Theorem: buildColumn_spec5
Proof state before:
case h.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
f : Row sch → Option τ
⊢ List.length (List.map f t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: vcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t1 t2 : Table sch), nrows (vcat t1 t2) = nrows t1 + nrows t2
Tactic:
intro t1 t2
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ nrows (vcat t1 t2) = nrows t1 + nrows t2
Theorem: vcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ nrows (vcat t1 t2) = nrows t1 + nrows t2
Tactic:
simp only [nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ List.length (vcat t1 t2).rows = List.length t1.rows + List.length t2.rows
Theorem: vcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ List.length (vcat t1 t2).rows = List.length t1.rows + List.length t2.rows
Tactic:
exact List.length_append t1.rows t2.rows
Proof state after:
no goals
Theorem: hcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {sch₁ sch₂ : Schema} (t₁ : Table sch₁) (t₂ : Table sch₂), nrows t₁ = nrows t₂ → nrows (hcat t₁ t₂) = nrows t₁
Tactic:
intros sch₁ sch₂ t₁ t₂ h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : nrows t₁ = nrows t₂
⊢ nrows (hcat t₁ t₂) = nrows t₁
Theorem: hcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : nrows t₁ = nrows t₂
⊢ nrows (hcat t₁ t₂) = nrows t₁
Tactic:
simp only [nrows, hcat, Schema.length_eq_List_length] at *
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.map (fun x => Row.append x.fst x.snd) (List.zip t₁.rows t₂.rows)) = List.length t₁.rows
Theorem: hcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.map (fun x => Row.append x.fst x.snd) (List.zip t₁.rows t₂.rows)) = List.length t₁.rows
Tactic:
rw [List.length_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.zip t₁.rows t₂.rows) = List.length t₁.rows
Theorem: hcat_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
h : List.length t₁.rows = List.length t₂.rows
⊢ List.length (List.zip t₁.rows t₂.rows) = List.length t₁.rows
Tactic:
apply List.zip_length_eq_of_length_eq _ _ h
Proof state after:
no goals
Theorem: crossJoin_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {sch₁ sch₂ : Schema} (t₁ : Table sch₁) (t₂ : Table sch₂), nrows (crossJoin t₁ t₂) = nrows t₁ * nrows t₂
Tactic:
intros sch₁ sch₂ t₁ t₂
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ nrows (crossJoin t₁ t₂) = nrows t₁ * nrows t₂
Theorem: crossJoin_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ nrows (crossJoin t₁ t₂) = nrows t₁ * nrows t₂
Tactic:
simp only [nrows, crossJoin, List.length_map, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ List.length (List.prod t₁.rows t₂.rows) = List.length t₁.rows * List.length t₂.rows
Theorem: crossJoin_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch₁ sch₂ : Schema
t₁ : Table sch₁
t₂ : Table sch₂
⊢ List.length (List.prod t₁.rows t₂.rows) = List.length t₁.rows * List.length t₂.rows
Tactic:
apply List.length_prod
Proof state after:
no goals
Theorem: getColumn1_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (n : Nat) (h : n < ncols t), List.length (getColumn1 t n) = nrows t
Tactic:
intro t n h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
h : n < ncols t
⊢ List.length (getColumn1 t n) = nrows t
Theorem: getColumn1_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
h : n < ncols t
⊢ List.length (getColumn1 t n) = nrows t
Tactic:
simp only [getColumn1, nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
h : n < ncols t
⊢ List.length (List.map (fun r => Cell.toOption (Row.nth r n h)) t.rows) = List.length t.rows
Theorem: getColumn1_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
h : n < ncols t
⊢ List.length (List.map (fun r => Cell.toOption (Row.nth r n h)) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: getColumn2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {τ : Type u} (t : Table sch) (c : η) (h : Schema.HasCol (c, τ) sch), List.length (getColumn2 t c) = nrows t
Tactic:
intro τ t c h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
h : Schema.HasCol (c, τ) sch
⊢ List.length (getColumn2 t c) = nrows t
Theorem: getColumn2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
h : Schema.HasCol (c, τ) sch
⊢ List.length (getColumn2 t c) = nrows t
Tactic:
simp only [getColumn2, nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
h : Schema.HasCol (c, τ) sch
⊢ List.length (List.map (fun r => getValue r c) t.rows) = List.length t.rows
Theorem: getColumn2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
h : Schema.HasCol (c, τ) sch
⊢ List.length (List.map (fun r => getValue r c) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: selectRows1_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ns : List (Fin (nrows t))), nrows (selectRows1 t ns) = List.length ns
Tactic:
intro t ns
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (nrows t))
⊢ nrows (selectRows1 t ns) = List.length ns
Theorem: selectRows1_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (nrows t))
⊢ nrows (selectRows1 t ns) = List.length ns
Tactic:
rw [selectRows1, nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (nrows t))
⊢ List.length { rows := List.map (fun n => getRow t n.val) ns }.rows = List.length ns
Theorem: selectRows1_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (nrows t))
⊢ List.length { rows := List.map (fun n => getRow t n.val) ns }.rows = List.length ns
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: selectRows2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (bs : List Bool),
    List.length bs = nrows t → nrows (selectRows2 t bs) = List.length (List.removeAllEq bs [false])
Tactic:
intro t bs h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = nrows t
⊢ nrows (selectRows2 t bs) = List.length (List.removeAllEq bs [false])
Theorem: selectRows2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = nrows t
⊢ nrows (selectRows2 t bs) = List.length (List.removeAllEq bs [false])
Tactic:
simp only [nrows, selectRows2, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = nrows t
⊢ List.length (List.sieve bs t.rows) = List.length (List.removeAllEq bs [false])
Theorem: selectRows2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = nrows t
⊢ List.length (List.sieve bs t.rows) = List.length (List.removeAllEq bs [false])
Tactic:
apply List.sieve_removeAllEq
Proof state after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = nrows t
⊢ List.length bs = List.length t.rows
Theorem: selectRows2_spec2
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = nrows t
⊢ List.length bs = List.length t.rows
Tactic:
rw [nrows, Schema.length_eq_List_length] at h
Proof state after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = List.length t.rows
⊢ List.length bs = List.length t.rows
Theorem: selectRows2_spec2
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
h : List.length bs = List.length t.rows
⊢ List.length bs = List.length t.rows
Tactic:
exact h
Proof state after:
no goals
Theorem: selectColumns1_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (bs : List Bool), header (selectColumns1 t bs) <+ header t
Tactic:
intro t bs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ header (selectColumns1 t bs) <+ header t
Theorem: selectColumns1_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ header (selectColumns1 t bs) <+ header t
Tactic:
simp only [header, Schema.names, Schema.sieve_eq_List_sieve]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ List.map Prod.fst (List.sieve bs sch) <+ List.map Prod.fst sch
Theorem: selectColumns1_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ List.map Prod.fst (List.sieve bs sch) <+ List.map Prod.fst sch
Tactic:
exact List.sublist_of_map_sublist _ _ Prod.fst $ List.sieve_sublist bs sch
Proof state after:
no goals
Theorem: ncols_eq_header_length
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch), ncols t = List.length (header t)
Tactic:
intro t
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ ncols t = List.length (header t)
Theorem: ncols_eq_header_length
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ ncols t = List.length (header t)
Tactic:
simp only [ncols, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ List.length sch = List.length (header t)
Theorem: ncols_eq_header_length
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ List.length sch = List.length (header t)
Tactic:
apply Eq.symm
Proof state after:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ List.length (header t) = List.length sch
Theorem: ncols_eq_header_length
Proof state before:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ List.length (header t) = List.length sch
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: selectColumns1_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hu : Schema.Unique sch
t : Table sch
bs : List Bool
h : List.length bs = ncols t
i : Nat
hlt : i < ncols t
⊢ List.get (header t) { val := i, isLt := (_ : i < List.length (header t)) } ∈ header (selectColumns1 t bs) ↔
    List.get bs { val := i, isLt := (_ : i < List.length bs) } = true
Tactic:
simp only [header, Schema.sieve_eq_List_sieve]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hu : Schema.Unique sch
t : Table sch
bs : List Bool
h : List.length bs = ncols t
i : Nat
hlt : i < ncols t
⊢ List.get (Schema.names sch) { val := i, isLt := (_ : i < List.length (header t)) } ∈
      Schema.names (List.sieve bs sch) ↔
    List.get bs { val := i, isLt := (_ : i < List.length bs) } = true