internlm/Lean-Github huggingface dataset:
Theorem: sortByColumns_spec1
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t
Tactic:
. intros x acc h
  rw [←h]
  apply tsort_spec1 (inst := x.snd.snd)
Proof state after:
no goals
Theorem: sortByColumns_spec1
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows t = nrows t
Tactic:
rfl
Proof state after:
no goals
Theorem: sortByColumns_spec1
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t
Tactic:
intros x acc h
Proof state after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows t
Theorem: sortByColumns_spec1
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows t
Tactic:
rw [←h]
Proof state after:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows acc
Theorem: sortByColumns_spec1
Proof state before:
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
x : (h : Header) × Schema.HasCol h sch × Ord h.snd
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows acc
Tactic:
apply tsort_spec1 (inst := x.snd.snd)
Proof state after:
no goals
Theorem: orderBy_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cmps : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))), nrows (orderBy t cmps) = nrows t
Tactic:
intro t _
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ nrows (orderBy t cmps✝) = nrows t
Theorem: orderBy_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ nrows (orderBy t cmps✝) = nrows t
Tactic:
simp only [nrows, orderBy, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ List.length
      (List.mergeSortWith
        (fun r₁ r₂ =>
          match List.find? (fun x => !Prod.snd x.2 (Prod.fst x.2 r₁) (Prod.fst x.2 r₂)) cmps✝ with
          | none => Ordering.lt
          | x => Ordering.gt)
        t.rows) =
    List.length t.rows
Theorem: orderBy_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ List.length
      (List.mergeSortWith
        (fun r₁ r₂ =>
          match List.find? (fun x => !Prod.snd x.2 (Prod.fst x.2 r₁) (Prod.fst x.2 r₂)) cmps✝ with
          | none => Ordering.lt
          | x => Ordering.gt)
        t.rows) =
    List.length t.rows
Tactic:
exact List.length_mergeSortWith _ t.rows
Proof state after:
no goals
Theorem: count_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type
inst✝ : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (hc : Schema.HasCol (c, τ) sch),
    nrows (count t c) = List.length (List.unique (getColumn2 t c))
Tactic:
intro t c hc
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type
inst✝ : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ nrows (count t c) = List.length (List.unique (getColumn2 t c))
Theorem: count_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type
inst✝ : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ nrows (count t c) = List.length (List.unique (getColumn2 t c))
Tactic:
simp only [nrows, count, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type
inst✝ : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (count.pairsToRow (List.counts (getColumn2 t c))) = List.length (List.unique (getColumn2 t c))
Theorem: count_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type
inst✝ : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (count.pairsToRow (List.counts (getColumn2 t c))) = List.length (List.unique (getColumn2 t c))
Tactic:
exact Eq.trans (length_count_pairsToRow _) (List.length_counts _)
Proof state after:
no goals
Theorem: pivotTable_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)) [inst : DecidableEq (Row (Schema.fromCHeaders cs))]
    (aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))),
    header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Tactic:
intro t cs inst aggs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Theorem: pivotTable_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Tactic:
simp only [header, Schema.names, Schema.fromCHeaders,
           Schema.append_eq_List_append, Schema.map_eq_List_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ List.map Prod.fst (List.append (List.map Sigma.fst cs) (List.map (fun x => x.fst) aggs)) =
    List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Theorem: pivotTable_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ List.map Prod.fst (List.append (List.map Sigma.fst cs) (List.map (fun x => x.fst) aggs)) =
    List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Tactic:
exact List.map_map_append cs aggs Prod.fst Sigma.fst Sigma.fst
Proof state after:
no goals
Theorem: pivotTable_spec3_aux
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.fromCHeaders ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := { fst := nm, snd := Schema.HasName.hd }.fst,
        snd := Schema.hasNameOfAppend { fst := nm, snd := Schema.HasName.hd }.snd } =
    Schema.lookup sch
      { fst := { fst := nm, snd := Schema.HasName.hd }.fst,
        snd := Schema.hasNameOfFromCHeaders { fst := nm, snd := Schema.HasName.hd }.snd }
Tactic:
simp only [Schema.fromCHeaders, List.map, List.append, Schema.hasNameOfAppend]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.hd } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders Schema.HasName.hd }
Theorem: pivotTable_spec3_aux
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.hd } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders Schema.HasName.hd }
Tactic:
rw [Schema.lookup_eq_1,
    Schema.hasNameOfFromCHeaders_eq_1,
    Schema.lookup_of_colImpliesName]
Proof state after:
no goals
Theorem: pivotTable_spec3_aux
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup
      (Schema.append (Schema.fromCHeaders ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := { fst := nm, snd := Schema.HasName.tl a✝ }.fst,
        snd := Schema.hasNameOfAppend { fst := nm, snd := Schema.HasName.tl a✝ }.snd } =
    Schema.lookup sch
      { fst := { fst := nm, snd := Schema.HasName.tl a✝ }.fst,
        snd := Schema.hasNameOfFromCHeaders { fst := nm, snd := Schema.HasName.tl a✝ }.snd }
Tactic:
simp only [Schema.fromCHeaders, List.map, List.append, Schema.hasNameOfAppend]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.tl (Schema.hasNameOfAppend a✝) } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders (Schema.HasName.tl a✝) }
Theorem: pivotTable_spec3_aux
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.tl (Schema.hasNameOfAppend a✝) } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders (Schema.HasName.tl a✝) }
Tactic:
rw [Schema.lookup_eq_2,
    Schema.hasNameOfFromCHeaders_eq_2]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup (Schema.append (Schema.map Sigma.fst cs) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.hasNameOfAppend a✝ } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders a✝ }
Theorem: pivotTable_spec3_aux
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup (Schema.append (Schema.map Sigma.fst cs) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.hasNameOfAppend a✝ } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders a✝ }
Tactic:
apply pivotTable_spec3_aux cs aggs ⟨nm, _⟩
Proof state after:
no goals
Theorem: groupBy_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
⊢ ∀ (t : Table sch) (key : Row sch → κ) (project : Row sch → ν) (aggregate : κ → List ν → Row sch'),
    nrows (groupBy t key project aggregate) = List.length (List.unique (List.map key t.rows))
Tactic:
intros t key proj agg
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ nrows (groupBy t key proj agg) = List.length (List.unique (List.map key t.rows))
Theorem: groupBy_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ nrows (groupBy t key proj agg) = List.length (List.unique (List.map key t.rows))
Tactic:
simp only [nrows, groupBy, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.length
      (List.map (fun klv => agg klv.fst klv.snd) (List.groupByKey (List.map (fun r => (key r, proj r)) t.rows))) =
    List.length (List.unique (List.map key t.rows))
Theorem: groupBy_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.length
      (List.map (fun klv => agg klv.fst klv.snd) (List.groupByKey (List.map (fun r => (key r, proj r)) t.rows))) =
    List.length (List.unique (List.map key t.rows))
Tactic:
rw [List.length_map, List.length_groupByKey]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.length (List.unique (List.map Prod.fst (List.map (fun r => (key r, proj r)) t.rows))) =
    List.length (List.unique (List.map key t.rows))
Theorem: groupBy_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.length (List.unique (List.map Prod.fst (List.map (fun r => (key r, proj r)) t.rows))) =
    List.length (List.unique (List.map key t.rows))
Tactic:
apply congrArg
Proof state after:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.unique (List.map Prod.fst (List.map (fun r => (key r, proj r)) t.rows)) = List.unique (List.map key t.rows)
Theorem: groupBy_spec4
Proof state before:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.unique (List.map Prod.fst (List.map (fun r => (key r, proj r)) t.rows)) = List.unique (List.map key t.rows)
Tactic:
apply congrArg
Proof state after:
case h.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.map Prod.fst (List.map (fun r => (key r, proj r)) t.rows) = List.map key t.rows
Theorem: groupBy_spec4
Proof state before:
case h.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.map Prod.fst (List.map (fun r => (key r, proj r)) t.rows) = List.map key t.rows
Tactic:
rw [List.map_map]
Proof state after:
case h.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.map (Prod.fst ∘ fun r => (key r, proj r)) t.rows = List.map key t.rows
Theorem: groupBy_spec4
Proof state before:
case h.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.map (Prod.fst ∘ fun r => (key r, proj r)) t.rows = List.map key t.rows
Tactic:
apply congr _ rfl
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.map (Prod.fst ∘ fun r => (key r, proj r)) = List.map key
Theorem: groupBy_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.map (Prod.fst ∘ fun r => (key r, proj r)) = List.map key
Tactic:
apply congrArg
Proof state after:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ (Prod.fst ∘ fun r => (key r, proj r)) = key
Theorem: groupBy_spec4
Proof state before:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ (Prod.fst ∘ fun r => (key r, proj r)) = key
Tactic:
unfold Function.comp
Proof state after:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ (fun x => ((fun r => (key r, proj r)) x).fst) = key
Theorem: groupBy_spec4
Proof state before:
case h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ (fun x => ((fun r => (key r, proj r)) x).fst) = key
Tactic:
simp only
Proof state after:
no goals
Theorem: completeCases_spec
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (completeCases t c) = nrows t
Tactic:
simp only [nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (completeCases t c) = List.length t.rows
Theorem: completeCases_spec
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (completeCases t c) = List.length t.rows
Tactic:
exact Eq.trans (List.length_map _ _) (List.length_map _ _)
Proof state after:
no goals
Theorem: fillna_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
⊢ ∀ (t : Table sch) (c : η) (v : τ) (hc : Schema.HasCol (c, τ) sch), nrows (fillna t c v) = nrows t
Tactic:
intros
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ nrows (fillna t✝ c✝ v✝) = nrows t✝
Theorem: fillna_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ nrows (fillna t✝ c✝ v✝) = nrows t✝
Tactic:
simp only [nrows, fillna, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ List.length
      (updateWithoutRetyping [{ fst := (c✝, τ), snd := hc✝ }] t✝ fun r =>
          match Row.getCell r hc✝ with
          | Cell.emp => Row.singleValue v✝
          | Cell.val vOld => Row.singleValue vOld).rows =
    List.length t✝.rows
Theorem: fillna_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
t✝ : Table sch
c✝ : η
v✝ : τ
hc✝ : Schema.HasCol (c✝, τ) sch
⊢ List.length
      (updateWithoutRetyping [{ fst := (c✝, τ), snd := hc✝ }] t✝ fun r =>
          match Row.getCell r hc✝ with
          | Cell.emp => Row.singleValue v✝
          | Cell.val vOld => Row.singleValue vOld).rows =
    List.length t✝.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: pivotLonger_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ header (pivotLonger t cs c1 c2) = Schema.names (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
simp only [header, Schema.names]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (Schema.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Theorem: pivotLonger_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (Schema.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
rw [Schema.append_eq_List_append]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]