Theorem: head_spec3 (Table/Proofs.lean)

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

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

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

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

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

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

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

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