internlm/Lean-Github huggingface dataset:
Theorem: head_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
⊢ ¬z < 0
Tactic:
intro hcontra
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
hcontra : z < 0
⊢ False
Theorem: head_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
hcontra : z < 0
⊢ False
Tactic:
cases z with
| ofNat n => contradiction
| negSucc n => contradiction
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
case ofNat
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
prop : Int.abs (Int.ofNat n) < nrows t
h : { val := Int.ofNat n, property := prop }.val ≥ 0
hcontra : Int.ofNat n < 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
case negSucc
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
n : Nat
prop : Int.abs (Int.negSucc n) < nrows t
h : { val := Int.negSucc n, property := prop }.val ≥ 0
hcontra : Int.negSucc n < 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.ofNat (Int.toNat z) = z
Tactic:
exact Int.toNat_of_ofNat_inj z h
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows
Tactic:
unfold nrows at prop
Proof state after:
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows
Theorem: head_spec2
Proof state before:
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows
Tactic:
rw [Int.abs_of_nonneg_eq_toNat] at prop
Proof state after:
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < Schema.length t.rows
prop : Int.toNat z < Schema.length t.rows
h : { val := z, property := prop✝ }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows

case mk.h.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ z ≥ 0
Theorem: head_spec2
Proof state before:
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < Schema.length t.rows
prop : Int.toNat z < Schema.length t.rows
h : { val := z, property := prop✝ }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows

case mk.h.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ z ≥ 0
Tactic:
. exact Schema.length_eq_List_length ▸ prop
Proof state after:
case mk.h.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ z ≥ 0
Theorem: head_spec2
Proof state before:
case mk.h.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ z ≥ 0
Tactic:
. exact h
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
case mk.h
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < Schema.length t.rows
prop : Int.toNat z < Schema.length t.rows
h : { val := z, property := prop✝ }.val ≥ 0
h_not_neg : ¬z < 0
⊢ Int.toNat z < List.length t.rows
Tactic:
exact Schema.length_eq_List_length ▸ prop
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
case mk.h.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < Schema.length t.rows
h : { val := z, property := prop }.val ≥ 0
h_not_neg : ¬z < 0
⊢ z ≥ 0
Tactic:
exact h
Proof state after:
no goals
Theorem: head_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (z : { z // Int.abs z < nrows t }), z.val < 0 → nrows (head t z.val) = nrows t - Int.abs z.val
Tactic:
intros t z h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : { z // Int.abs z < nrows t }
h : z.val < 0
⊢ nrows (head t z.val) = nrows t - Int.abs z.val
Theorem: head_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : { z // Int.abs z < nrows t }
h : z.val < 0
⊢ nrows (head t z.val) = nrows t - Int.abs z.val
Tactic:
cases z with | mk z prop =>
simp only at h
simp only [nrows, Schema.length_eq_List_length] at prop
simp only [head, nrows, List.dropLastN, Function.comp, h,
           Schema.length_eq_List_length, ite_true]
rw [List.length_reverse, List.length_drop, List.length_reverse]
rw [List.length_reverse]
exact prop
Proof state after:
no goals
Theorem: head_spec3
Proof state before:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : { val := z, property := prop }.val < 0
⊢ nrows (head t { val := z, property := prop }.val) = nrows t - Int.abs { val := z, property := prop }.val
Tactic:
simp only at h
Proof state after:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : z < 0
⊢ nrows (head t { val := z, property := prop }.val) = nrows t - Int.abs { val := z, property := prop }.val
Theorem: head_spec3
Proof state before:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop : Int.abs z < nrows t
h : z < 0
⊢ nrows (head t { val := z, property := prop }.val) = nrows t - Int.abs { val := z, property := prop }.val
Tactic:
simp only [nrows, Schema.length_eq_List_length] at prop
Proof state after:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ nrows (head t { val := z, property := prop✝ }.val) = nrows t - Int.abs { val := z, property := prop✝ }.val
Theorem: head_spec3
Proof state before:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ nrows (head t { val := z, property := prop✝ }.val) = nrows t - Int.abs { val := z, property := prop✝ }.val
Tactic:
simp only [head, nrows, List.dropLastN, Function.comp, h,
           Schema.length_eq_List_length, ite_true]
Proof state after:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ List.length (List.reverse (List.drop (Int.abs z) (List.reverse t.rows))) = List.length t.rows - Int.abs z
Theorem: head_spec3
Proof state before:
case mk
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ List.length (List.reverse (List.drop (Int.abs z) (List.reverse t.rows))) = List.length t.rows - Int.abs z
Tactic:
rw [List.length_reverse, List.length_drop, List.length_reverse]
Proof state after:
case mk.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ Int.abs z < List.length (List.reverse t.rows)
Theorem: head_spec3
Proof state before:
case mk.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ Int.abs z < List.length (List.reverse t.rows)
Tactic:
rw [List.length_reverse]
Proof state after:
case mk.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ Int.abs z < List.length t.rows
Theorem: head_spec3
Proof state before:
case mk.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : Int
prop✝ : Int.abs z < nrows t
h : z < 0
prop : Int.abs z < List.length t.rows
⊢ Int.abs z < List.length t.rows
Tactic:
exact prop
Proof state after:
no goals
Theorem: dropColumn_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (c : η) (hc : Schema.HasName c sch), nrows (dropColumn t c) = nrows t
Tactic:
intros
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
c✝ : η
hc✝ : Schema.HasName c✝ sch
⊢ nrows (dropColumn t✝ c✝) = nrows t✝
Theorem: dropColumn_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
c✝ : η
hc✝ : Schema.HasName c✝ sch
⊢ nrows (dropColumn t✝ c✝) = nrows t✝
Tactic:
simp only [nrows, dropColumn, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
c✝ : η
hc✝ : Schema.HasName c✝ sch
⊢ List.length (List.map (Row.removeColumn hc✝) t✝.rows) = List.length t✝.rows
Theorem: dropColumn_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t✝ : Table sch
c✝ : η
hc✝ : Schema.HasName c✝ sch
⊢ List.length (List.map (Row.removeColumn hc✝) t✝.rows) = List.length t✝.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ Schema.Unique sch →
    ∀ (t : Table sch) (c : η) (hc : Schema.HasName c sch), header (dropColumn t c) = List.removeAllEq (header t) [c]
Tactic:
intro hsch t c hc
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ header (dropColumn t c) = List.removeAllEq (header t) [c]
Theorem: dropColumn_spec2_unique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ header (dropColumn t c) = List.removeAllEq (header t) [c]
Tactic:
simp only [List.removeAllEq, header]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
Theorem: dropColumn_spec2_unique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : Schema.Unique sch
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
Tactic:
unfold Schema.Unique at hsch
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : List.Unique (Schema.names sch)
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
Theorem: dropColumn_spec2_unique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hsch : List.Unique (Schema.names sch)
t : Table sch
c : η
hc : Schema.HasName c sch
⊢ Schema.names (Schema.removeName sch hc) = List.filter (fun x => decide ¬x ∈ [c]) (Schema.names sch)
Tactic:
induction hc with
| @hd nm s' τ =>
  simp only [List.filter, List.notElem, List.elem]
  cases hsch with | cons hnmem hu =>
  simp only at hnmem
  have : (decide (nm ∉ [nm])) = false :=
    by simp only [decide_not, List.mem_singleton_iff, decide_True,
                  decide_False, not]
  rw [this]
  simp only
  simp only [Schema.names, List.map]
  have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
          = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
  rw [this]
  rw [List.removeAllEq_singleton_nonelem_eq]
  exact hnmem
| @tl hdr nm s' h ih =>
  simp only [Schema.names, List.map]
  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 hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names ((nm, τ) :: s'))
Tactic:
simp only [List.filter, List.notElem, List.elem]
Proof state after:
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
hsch : List.Unique (Schema.names ((nm, τ) :: s'))
t : Table ((nm, τ) :: s')
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
cases hsch with | cons hnmem hu =>
simp only at hnmem
have : (decide (nm ∉ [nm])) = false :=
  by simp only [decide_not, List.mem_singleton_iff, decide_True,
                decide_False, not]
rw [this]
simp only
simp only [Schema.names, List.map]
have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
        = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
rw [this]
rw [List.removeAllEq_singleton_nonelem_eq]
exact hnmem
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬(nm, τ).fst ∈ List.map Prod.fst s'
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
simp only at hnmem
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
have : (decide (nm ∉ [nm])) = false :=
  by simp only [decide_not, List.mem_singleton_iff, decide_True,
                decide_False, not]
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match decide ¬nm ∈ [nm] with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
rw [this]
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match false with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    match false with
    | true => nm :: List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
    | false => List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
simp only
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ Schema.names (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
simp only [Schema.names, List.map]
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : (decide ¬nm ∈ [nm]) = false
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
have : List.filter (λ x => x ∉ [nm]) (List.map Prod.fst s')
        = List.removeAllEq (List.map Prod.fst s') [nm] := rfl
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) =
    List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s')
Tactic:
rw [this]
Proof state after:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) = List.removeAllEq (List.map Prod.fst s') [nm]
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ List.map Prod.fst (Schema.removeName ((nm, τ) :: s') Schema.HasName.hd) = List.removeAllEq (List.map Prod.fst s') [nm]
Tactic:
rw [List.removeAllEq_singleton_nonelem_eq]
Proof state after:
case hd.cons.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ ¬nm ∈ List.map Prod.fst s'
Theorem: dropColumn_spec2_unique
Proof state before:
case hd.cons.a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this✝ : (decide ¬nm ∈ [nm]) = false
this : List.filter (fun x => decide ¬x ∈ [nm]) (List.map Prod.fst s') = List.removeAllEq (List.map Prod.fst s') [nm]
⊢ ¬nm ∈ List.map Prod.fst s'
Tactic:
exact hnmem
Proof state after:
no goals
Theorem: dropColumn_spec2_unique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (decide ¬nm ∈ [nm]) = false
Tactic:
simp only [decide_not, List.mem_singleton_iff, decide_True,
           decide_False, not]
Proof state after:
no goals