Theorem: groupBy_spec4 (Table/Proofs.lean)

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
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))

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]
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))

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]
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))

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
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)

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
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

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]
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

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
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

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
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

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
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

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
State after:
no goals