internlm/Lean-Github huggingface dataset:
Theorem: dropColumn_spec2_unique
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ Schema.names (Schema.removeName (hdr :: s') (Schema.HasName.tl h)) =
    List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names (hdr :: s'))
Tactic:
simp only [Schema.names, List.map]
Proof state after:
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ hdr.fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) (hdr.fst :: List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c : η
hdr : Header
nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
hsch : List.Unique (Schema.names (hdr :: s'))
t : Table (hdr :: s')
⊢ hdr.fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) (hdr.fst :: List.map Prod.fst s')
Tactic:
cases hdr with | mk nm₁ τ₁ =>
cases Decidable.em (nm₁ = nm) with
| inl heq =>
  rw [heq] at hsch
  cases hsch with | cons hnmem hu =>
  simp only at hnmem
  have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
  contradiction
| inr hneq =>
  rw [←List.removeAllEq]
  rw [List.removeAllEq_singleton_hd_neq]
  . congr
    apply ih
    . cases hsch; assumption
    . exact Table.mk []
  . exact hneq
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
cases Decidable.em (nm₁ = nm) with
| inl heq =>
  rw [heq] at hsch
  cases hsch with | cons hnmem hu =>
  simp only at hnmem
  have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
  contradiction
| inr hneq =>
  rw [←List.removeAllEq]
  rw [List.removeAllEq_singleton_hd_neq]
  . congr
    apply ih
    . cases hsch; assumption
    . exact Table.mk []
  . exact hneq
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
rw [heq] at hsch
Proof state after:
case tl.mk.inl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inl
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
cases hsch with | cons hnmem hu =>
simp only at hnmem
have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
contradiction
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬(nm, τ₁).fst ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
simp only at hnmem
Proof state after:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
Proof state after:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
contradiction
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
Tactic:
rw [←List.removeAllEq]
Proof state after:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.removeAllEq ((nm₁, τ₁).fst :: List.map Prod.fst s') [nm]
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.removeAllEq ((nm₁, τ₁).fst :: List.map Prod.fst s') [nm]
Tactic:
rw [List.removeAllEq_singleton_hd_neq]
Proof state after:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    (nm₁, τ₁).fst :: List.removeAllEq (List.map Prod.fst s') [nm]

case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    (nm₁, τ₁).fst :: List.removeAllEq (List.map Prod.fst s') [nm]

case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Tactic:
. congr
  apply ih
  . cases hsch; assumption
  . exact Table.mk []
Proof state after:
case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Tactic:
. exact hneq
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    (nm₁, τ₁).fst :: List.removeAllEq (List.map Prod.fst s') [nm]
Tactic:
congr
Proof state after:
case tl.mk.inr.e_tail
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.map Prod.fst (Schema.removeName s' h) = List.removeAllEq (List.map Prod.fst s') [nm]
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.e_tail
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.map Prod.fst (Schema.removeName s' h) = List.removeAllEq (List.map Prod.fst s') [nm]
Tactic:
apply ih
Proof state after:
case tl.mk.inr.e_tail.hsch
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.Unique (Schema.names s')

case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.e_tail.hsch
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.Unique (Schema.names s')

case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Tactic:
. cases hsch; assumption
Proof state after:
case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Tactic:
. exact Table.mk []
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.e_tail.hsch
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ List.Unique (Schema.names s')
Tactic:
cases hsch
Proof state after:
case tl.mk.inr.e_tail.hsch.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
a✝¹ : List.Unique (List.map Prod.fst s')
a✝ : ¬(nm₁, τ₁).fst ∈ List.map Prod.fst s'
⊢ List.Unique (Schema.names s')
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.e_tail.hsch.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
a✝¹ : List.Unique (List.map Prod.fst s')
a✝ : ¬(nm₁, τ₁).fst ∈ List.map Prod.fst s'
⊢ List.Unique (Schema.names s')
Tactic:
assumption
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.e_tail.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ Table s'
Tactic:
exact Table.mk []
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case tl.mk.inr.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
hsch : List.Unique (Schema.names ((nm₁, τ₁) :: s'))
t : Table ((nm₁, τ₁) :: s')
hneq : ¬nm₁ = nm
⊢ (nm₁, τ₁).fst ≠ nm
Tactic:
exact hneq
Proof state after:
no goals
Theorem: dropColumns_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : ActionList Schema.removeCertifiedName sch), nrows (dropColumns t cs) = nrows t
Tactic:
intro t cs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.removeCertifiedName sch
⊢ nrows (dropColumns t cs) = nrows t
Theorem: dropColumns_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.removeCertifiedName sch
⊢ nrows (dropColumns t cs) = nrows t
Tactic:
simp only [nrows, dropColumns, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.removeCertifiedName sch
⊢ List.length (List.map (Row.removeColumns cs) t.rows) = List.length t.rows
Theorem: dropColumns_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.removeCertifiedName sch
⊢ List.length (List.map (Row.removeColumns cs) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: tsort_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {τ : Type u} [inst : Ord τ] (t : Table sch) (b : Bool) (c : η) (hc : Schema.HasCol (c, τ) sch),
    nrows (tsort t c b) = nrows t
Tactic:
intro τ _ t b c hc
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : Ord τ
t : Table sch
b : Bool
c : η
hc : Schema.HasCol (c, τ) sch
⊢ nrows (tsort t c b) = nrows t
Theorem: tsort_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : Ord τ
t : Table sch
b : Bool
c : η
hc : Schema.HasCol (c, τ) sch
⊢ nrows (tsort t c b) = nrows t
Tactic:
simp only [nrows, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : Ord τ
t : Table sch
b : Bool
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (tsort t c b).rows = List.length t.rows
Theorem: tsort_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : Ord τ
t : Table sch
b : Bool
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.length (tsort t c b).rows = List.length t.rows
Tactic:
exact List.length_mergeSortWith _ t.rows
Proof state after:
no goals
Theorem: sortByColumns_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)), nrows (sortByColumns t hs) = nrows t
Tactic:
intros t hs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows (sortByColumns t hs) = nrows t
Theorem: sortByColumns_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows (sortByColumns t hs) = nrows t
Tactic:
simp only [nrows, sortByColumns]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ Schema.length (List.foldr (fun ohdr acc => tsort acc ohdr.fst.fst true) t hs).rows = Schema.length t.rows
Theorem: sortByColumns_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ Schema.length (List.foldr (fun ohdr acc => tsort acc ohdr.fst.fst true) t hs).rows = Schema.length t.rows
Tactic:
apply List.foldr_invariant (λ x => nrows x = nrows t)
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)
⊢ nrows t = nrows t

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

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:
. rfl
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) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t