From 242a8dcfbf26336fd69351af169f85924befbe5f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Feb 2021 17:06:41 -0800 Subject: [PATCH] test: `simp` --- tests/lean/run/concatElim.lean | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean index f5ccc730c7..73b93c171f 100644 --- a/tests/lean/run/concatElim.lean +++ b/tests/lean/run/concatElim.lean @@ -18,16 +18,9 @@ variable {α} theorem concatEq (xs : List α) (h : xs ≠ []) : concat (dropLast xs) (last xs h) = xs := by match xs, h with - | [], h => - apply False.elim - apply h rfl + | [], h => exact absurd rfl h | [x], h => rfl - | x₁::x₂::xs, h => - have x₂::xs ≠ [] by intro h; injection h - have ih := concatEq (x₂::xs) this - show x₁ :: concat (dropLast (x₂::xs)) (last (x₂::xs) this) = x₁ :: x₂ :: xs - rewrite ih - rfl + | x₁::x₂::xs, h => simp [concat, last, concatEq (x₂::xs) List.noConfusion] theorem lengthCons {α} (x : α) (xs : List α) : (x::xs).length = xs.length + 1 := let rec aux (a : α) (xs : List α) : (n : Nat) → (a::xs).lengthAux n = xs.lengthAux n + 1 := @@ -53,15 +46,13 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro intro n h cases n with | zero => - rw [lengthCons, lengthCons] at h + simp [lengthCons] at h injection h with h injection h | succ n => - have (x₁ :: x₂ :: xs).length = xs.length + 2 by rw [lengthCons, lengthCons] + have (x₁ :: x₂ :: xs).length = xs.length + 2 by simp [lengthCons] have xs.length = n by rw [this] at h; injection h with h; injection h with h; assumption - have ih : (dropLast (x₂::xs)).length = xs.length from dropLastLen (x₂::xs) xs.length (lengthCons _ _) - show (x₁ :: dropLast (x₂ :: xs)).length = n+1 - rw [lengthCons, ih, this] + simp [dropLast, lengthCons, dropLastLen (x₂::xs) xs.length (lengthCons ..), this] @[inline] def concatElim {α}