Theorem: head_spec2 (Table/Proofs.lean)

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

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
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
⊢ Int.ofNat (nrows (head t { val := z, property := prop }.val)) = { val := z, property := prop }.val
Tactic:
simp only [head]
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

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

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

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

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

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

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

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

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

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

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
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
h_not_neg : ¬z < 0
⊢ Int.ofNat (Int.toNat z) = z
Tactic:
exact Int.toNat_of_ofNat_inj z h
State after:
no goals

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

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

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

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

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

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