internlm/Lean-Github huggingface dataset:
Theorem: selectColumns1_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
hu : Schema.Unique sch
t : Table sch
bs : List Bool
h : List.length bs = ncols t
i : Nat
hlt : i < ncols t
⊢ List.get (Schema.names sch) { val := i, isLt := (_ : i < List.length (header t)) } ∈
      Schema.names (List.sieve bs sch) ↔
    List.get bs { val := i, isLt := (_ : i < List.length bs) } = true
Tactic:
exact List.sieve_map_mem_iff_true_unique (Schema.length_eq_List_length ▸ hlt)
        (h.symm ▸ hlt) Prod.fst hu
Proof state after:
no goals
Theorem: selectColumns1_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ schema (selectColumns1 t bs) <+ schema t
Tactic:
simp only [schema, Schema.sieve_eq_List_sieve]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ List.sieve bs sch <+ sch
Theorem: selectColumns1_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ List.sieve bs sch <+ sch
Tactic:
apply List.sieve_sublist
Proof state after:
no goals
Theorem: selectColumns1_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (bs : List Bool), nrows (selectColumns1 t bs) = nrows t
Tactic:
intro t bs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ nrows (selectColumns1 t bs) = nrows t
Theorem: selectColumns1_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ nrows (selectColumns1 t bs) = nrows t
Tactic:
simp only [nrows, selectColumns1, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ List.length (List.map (fun r => Row.sieve bs r) t.rows) = List.length t.rows
Theorem: selectColumns1_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
bs : List Bool
⊢ List.length (List.map (fun r => Row.sieve bs r) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: selectColumns2_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ns : List (Fin (ncols t))), ncols (selectColumns2 t ns) = List.length ns
Tactic:
intro t ns
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ ncols (selectColumns2 t ns) = List.length ns
Theorem: selectColumns2_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ ncols (selectColumns2 t ns) = List.length ns
Tactic:
simp only [ncols, Schema.length_eq_List_length, Schema.nths,
           Schema.map_eq_List_map]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ List.length (List.map (fun n => Schema.nth sch n.val (_ : n.val < Schema.length sch)) ns) = List.length ns
Theorem: selectColumns2_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ List.length (List.map (fun n => Schema.nth sch n.val (_ : n.val < Schema.length sch)) ns) = List.length ns
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: selectColumns2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ns : List (Fin (ncols t))) (i : Nat) (hi : i < List.length ns),
    List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
      List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Tactic:
intro t ns i hi
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Theorem: selectColumns2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Tactic:
simp only [header]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Theorem: selectColumns2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Tactic:
simp only [finHeaderLengthOfFinNcols]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch)
      { val := (List.get ns { val := i, isLt := hi }).val,
        isLt := (_ : (List.get ns { val := i, isLt := hi }).val < List.length (header t)) }
Theorem: selectColumns2_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch)
      { val := (List.get ns { val := i, isLt := hi }).val,
        isLt := (_ : (List.get ns { val := i, isLt := hi }).val < List.length (header t)) }
Tactic:
apply Schema.get_map_nths_eq_get_get
Proof state after:
no goals
Theorem: selectColumns2_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {sch : Schema} (t : Table sch) (ns : List (Fin (ncols t))) (c : CertifiedName (schema (selectColumns2 t ns))),
    Schema.lookupType (schema (selectColumns2 t ns)) c =
      Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Tactic:
intro sch t ns c
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (schema (selectColumns2 t ns))
⊢ Schema.lookupType (schema (selectColumns2 t ns)) c =
    Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Theorem: selectColumns2_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (schema (selectColumns2 t ns))
⊢ Schema.lookupType (schema (selectColumns2 t ns)) c =
    Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Tactic:
unfold schema at *
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (Schema.nths sch ns)
⊢ Schema.lookupType (Schema.nths sch ns) c =
    Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Theorem: selectColumns2_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (Schema.nths sch ns)
⊢ Schema.lookupType (Schema.nths sch ns) c =
    Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Tactic:
apply Schema.lookupType_nths_eq_lookupType
Proof state after:
no goals
Theorem: selectColumns2_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ns : List (Fin (ncols t))), nrows (selectColumns2 t ns) = nrows t
Tactic:
intro t ns
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ nrows (selectColumns2 t ns) = nrows t
Theorem: selectColumns2_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ nrows (selectColumns2 t ns) = nrows t
Tactic:
simp only [nrows, selectColumns2, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ List.length (List.map (Row.nths ns) t.rows) = List.length t.rows
Theorem: selectColumns2_spec4
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
⊢ List.length (List.map (Row.nths ns) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: selectColumns3_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)), header (selectColumns3 t cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
intros t cs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ header (selectColumns3 t cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Theorem: selectColumns3_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ header (selectColumns3 t cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
simp only [header, selectColumns3, Schema.names]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Theorem: selectColumns3_spec1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
induction cs with
| nil => simp only [Schema.pick, List.map]
| cons c cs ih =>
  simp only [Schema.pick, List.map, List.cons.injEq]
  apply And.intro
  . simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
  . exact ih
Proof state after:
no goals
Theorem: selectColumns3_spec1
Proof state before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ List.map Prod.fst (Schema.fromCHeaders []) = List.map (Prod.fst ∘ Sigma.fst) []
Tactic:
simp only [Schema.pick, List.map]
Proof state after:
no goals
Theorem: selectColumns3_spec1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.fromCHeaders (c :: cs)) = List.map (Prod.fst ∘ Sigma.fst) (c :: cs)
Tactic:
simp only [Schema.pick, List.map, List.cons.injEq]
Proof state after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c ∧
    List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Theorem: selectColumns3_spec1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c ∧
    List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
apply And.intro
Proof state after:
case cons.left
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c

case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Theorem: selectColumns3_spec1
Proof state before:
case cons.left
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c

case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
. simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
Proof state after:
case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Theorem: selectColumns3_spec1
Proof state before:
case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
. exact ih
Proof state after:
no goals
Theorem: selectColumns3_spec1
Proof state before:
case cons.left
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c
Tactic:
simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
Proof state after:
no goals
Theorem: selectColumns3_spec1
Proof state before:
case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
exact ih
Proof state after:
no goals
Theorem: selectColumns3_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)) (c : CertifiedName (schema (selectColumns3 t cs))),
    Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
      Schema.lookupType (schema (selectColumns3 t cs)) c
Tactic:
intro t cs c
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (schema (selectColumns3 t cs)) c
Theorem: selectColumns3_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (schema (selectColumns3 t cs)) c
Tactic:
unfold schema
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.fromCHeaders cs) c
Theorem: selectColumns3_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.fromCHeaders cs) c
Tactic:
unfold Schema.fromCHeaders
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c
Theorem: selectColumns3_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c
Tactic:
simp only [schema] at c
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (Schema.fromCHeaders cs)
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c
Theorem: selectColumns3_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (Schema.fromCHeaders cs)
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c
Tactic:
apply Schema.lookupTypeFromCHeadersUnique
Proof state after:
no goals
Theorem: selectColumns3_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)), nrows (selectColumns3 t cs) = nrows t
Tactic:
intro t cs
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ nrows (selectColumns3 t cs) = nrows t
Theorem: selectColumns3_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ nrows (selectColumns3 t cs) = nrows t
Tactic:
simp only [nrows, selectColumns3, Schema.length_eq_List_length]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.length (List.map (fun r => Row.pick r cs) t.rows) = List.length t.rows
Theorem: selectColumns3_spec3
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.length (List.map (fun r => Row.pick r cs) t.rows) = List.length t.rows
Tactic:
apply List.length_map
Proof state after:
no goals
Theorem: head_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (z : { z // Int.abs z < nrows t }), z.val ≥ 0 → Int.ofNat (nrows (head t z.val)) = 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
⊢ Int.ofNat (nrows (head t z.val)) = z.val
Theorem: head_spec2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
z : { z // Int.abs z < nrows t }
h : z.val ≥ 0
⊢ Int.ofNat (nrows (head t z.val)) = z.val
Tactic:
cases z with | mk z prop =>
simp only [head]
have h_not_neg : ¬ (z < 0) := by
  intro hcontra
  cases z with
  | ofNat n => contradiction
  | negSucc n => contradiction
simp only [ite_false, h_not_neg]
simp only [List.take, nrows, Schema.length_eq_List_length]
rw [List.length_take]
. exact Int.toNat_of_ofNat_inj z h
. unfold nrows at prop
  rw [Int.abs_of_nonneg_eq_toNat] at prop
  . exact Schema.length_eq_List_length ▸ prop
  . exact h
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
⊢ Int.ofNat (nrows (head t { val := z, property := prop }.val)) = { val := z, property := prop }.val
Tactic:
simp only [head]
Proof state after:
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
⊢ Int.ofNat (nrows { rows := if z < 0 then List.dropLastN (Int.abs z) t.rows else List.take (Int.toNat z) t.rows }) = z
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
⊢ Int.ofNat (nrows { rows := if z < 0 then List.dropLastN (Int.abs z) t.rows else List.take (Int.toNat z) t.rows }) = z
Tactic:
have h_not_neg : ¬ (z < 0) := by
  intro hcontra
  cases z with
  | ofNat n => contradiction
  | negSucc n => contradiction
Proof state after:
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 (nrows { rows := if z < 0 then List.dropLastN (Int.abs z) t.rows else List.take (Int.toNat z) t.rows }) = z
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 (nrows { rows := if z < 0 then List.dropLastN (Int.abs z) t.rows else List.take (Int.toNat z) t.rows }) = z
Tactic:
simp only [ite_false, h_not_neg]
Proof state after:
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 (nrows { rows := List.take (Int.toNat z) t.rows }) = z
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 (nrows { rows := List.take (Int.toNat z) t.rows }) = z
Tactic:
simp only [List.take, nrows, Schema.length_eq_List_length]
Proof state after:
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 (List.length (List.take (Int.toNat z) t.rows)) = z
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 (List.length (List.take (Int.toNat z) t.rows)) = z
Tactic:
rw [List.length_take]
Proof state after:
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

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

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:
. exact Int.toNat_of_ofNat_inj z h
Proof state after:
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
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
  rw [Int.abs_of_nonneg_eq_toNat] at prop
  . exact Schema.length_eq_List_length ▸ prop
  . exact h
Proof state after:
no goals