internlm/Lean-Github huggingface dataset:
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 (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
have := List.map_append Prod.fst (sch.removeTypedNames cs) [(c1, η), (c2, τ)]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (Schema.removeTypedNames sch cs ++ [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ List.map Prod.fst [(c1, η), (c2, τ)]
⊢ List.map Prod.fst (List.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 : η
this :
  List.map Prod.fst (Schema.removeTypedNames sch cs ++ [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ List.map Prod.fst [(c1, η), (c2, τ)]
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
simp only [HAppend.hAppend, Append.append] at this
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.map Prod.fst (List.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 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
rw [this]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(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 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
rfl
Proof state after:
no goals
Theorem: pivotWider_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
⊢ ∀ (t : Table sch) (c1 c2 : η) (hc1 : Schema.HasCol (c1, η) sch)
    (hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1))
    [inst :
      DecidableEq
        (Row
          (Schema.removeNames sch
            (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
              (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))],
    header (pivotWider t c1 c2) =
      Schema.names
          (Schema.removeNames sch
            (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
              (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
        List.unique (List.somes (getColumn2 t c1))
Tactic:
intro t c1 c2 hc1 hc2 inst
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
⊢ header (pivotWider t c1 c2) =
    Schema.names
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Theorem: pivotWider_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
⊢ header (pivotWider t c1 c2) =
    Schema.names
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Tactic:
simp only [header, Schema.names]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
⊢ List.map Prod.fst
      (Schema.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Theorem: pivotWider_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
⊢ List.map Prod.fst
      (Schema.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Tactic:
rw [Schema.append_eq_List_append]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
⊢ List.map Prod.fst
      (List.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Theorem: pivotWider_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
⊢ List.map Prod.fst
      (List.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Tactic:
have := List.map_append Prod.fst
  (Schema.removeHeaders sch
    (ActionList.cons { fst := (c1, η), snd := hc1 }
      (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
  (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1 hc1))))
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
this :
  List.map Prod.fst
      (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)) ++
        List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1)))) =
    List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))) ++
      List.map Prod.fst (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))
⊢ List.map Prod.fst
      (List.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Theorem: pivotWider_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
c1 c2 : η
hc1 : Schema.HasCol (c1, η) sch
hc2 : Schema.HasCol (c2, τ) (Schema.removeHeader sch hc1)
inst :
  DecidableEq
    (Row
      (Schema.removeNames sch
        (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
          (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))))
this :
  List.map Prod.fst
      (List.append
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil)))
        (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1))))) =
    List.append
      (List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))))
      (List.map Prod.fst (List.map (fun x => (x, τ)) (List.unique (List.somes (getColumn2 t c1)))))
hf : (Prod.fst ∘ fun x => (x, τ)) = id
⊢ List.append
      (List.map Prod.fst
        (Schema.removeHeaders sch
          (ActionList.cons { fst := (c1, η), snd := hc1 }
            (ActionList.cons { fst := (c2, τ), snd := hc2 } ActionList.nil))))
      (List.unique (List.somes (getColumn2 t c1))) =
    List.map Prod.fst
        (Schema.removeNames sch
          (ActionList.cons (Schema.cNameOfCHead { fst := (c1, η), snd := hc1 })
            (ActionList.cons (Schema.cNameOfCHead { fst := (c2, τ), snd := hc2 }) ActionList.nil))) ++
      List.unique (List.somes (getColumn2 t c1))
Tactic:
rfl
Proof state after:
no goals
Theorem: flatten_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : ActionList Schema.flattenList sch), header (flatten t cs) = header t
Tactic:
intros t cs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ header (flatten t cs) = header t
Theorem: flatten_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ header (flatten t cs) = header t
Tactic:
simp only [flatten, header, Schema.names]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ List.map Prod.fst (Schema.flattenLists sch cs) = List.map Prod.fst sch
Theorem: flatten_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ List.map Prod.fst (Schema.flattenLists sch cs) = List.map Prod.fst sch
Tactic:
induction cs with
| nil => rfl
| cons c cs ih =>
  rw [ih]
  simp only [Schema.flattenList]
  apply Schema.retypeColumn_preserves_names
  exact Table.mk []
Proof state after:
no goals
Theorem: flatten_spec1
Proof state before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenLists schema✝ ActionList.nil) = List.map Prod.fst schema✝
Tactic:
rfl
Proof state after:
no goals
Theorem: flatten_spec1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenLists schema✝ (ActionList.cons c cs)) = List.map Prod.fst schema✝
Tactic:
rw [ih]
Proof state after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenList schema✝ c) = List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Theorem: flatten_spec1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenList schema✝ c) = List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Tactic:
simp only [Schema.flattenList]
Proof state after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.retypeColumn schema✝ (Schema.colImpliesName c.snd.snd) c.snd.fst) =
    List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Theorem: flatten_spec1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.retypeColumn schema✝ (Schema.colImpliesName c.snd.snd) c.snd.fst) =
    List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Tactic:
apply Schema.retypeColumn_preserves_names
Proof state after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Theorem: flatten_spec1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Tactic:
exact Table.mk []
Proof state after:
no goals
Theorem: transformColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ₁ τ₂ : Type u_1
⊢ ∀ (t : Table sch) (c : η) (f : Option τ₁ → Option τ₂) (hc : Schema.HasCol (c, τ₁) sch),
    nrows (transformColumn t c f) = nrows t
Tactic:
intro t c f hc
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ₁ τ₂ : Type u_1
t : Table sch
c : η
f : Option τ₁ → Option τ₂
hc : Schema.HasCol (c, τ₁) sch
⊢ nrows (transformColumn t c f) = nrows t
Theorem: transformColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ₁ τ₂ : Type u_1
t : Table sch
c : η
f : Option τ₁ → Option τ₂
hc : Schema.HasCol (c, τ₁) sch
⊢ nrows (transformColumn t c f) = nrows t
Tactic:
simp only [nrows, transformColumn, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ₁ τ₂ : Type u_1
t : Table sch
c : η
f : Option τ₁ → Option τ₂
hc : Schema.HasCol (c, τ₁) sch
⊢ List.length (List.map (fun r => Row.retypeCell r hc (Cell.fromOption (f (getValue r c)))) t.rows) = List.length t.rows
Theorem: transformColumn_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ₁ τ₂ : Type u_1
t : Table sch
c : η
f : Option τ₁ → Option τ₂
hc : Schema.HasCol (c, τ₁) sch
⊢ List.length (List.map (fun r => Row.retypeCell r hc (Cell.fromOption (f (getValue r c)))) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: renameColumns_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ccs : ActionList Schema.renameColumnCN sch), nrows (renameColumns t ccs) = nrows t
Tactic:
intros
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
ccs✝ : ActionList Schema.renameColumnCN sch
⊢ nrows (renameColumns t✝ ccs✝) = nrows t✝
Theorem: renameColumns_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
ccs✝ : ActionList Schema.renameColumnCN sch
⊢ nrows (renameColumns t✝ ccs✝) = nrows t✝
Tactic:
simp only [nrows, renameColumns, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
ccs✝ : ActionList Schema.renameColumnCN sch
⊢ List.length (List.map (Row.renameCells ccs✝) t✝.rows) = List.length t✝.rows
Theorem: renameColumns_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
ccs✝ : ActionList Schema.renameColumnCN sch
⊢ List.length (List.map (Row.renameCells ccs✝) t✝.rows) = List.length t✝.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: groupByRetentive_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (hc : Schema.HasCol (c, τ) sch), List.NoDuplicates (getColumn2 (groupByRetentive t c) "key")
Tactic:
intros t c hc
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates (getColumn2 (groupByRetentive t c) "key")