michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean/run/blast_ematch_list): blast last_concat

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-12 22:56:28 -08:00
parent 12876ccc20
commit 081ad1212b
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/blast_ematch_list.lean Normal file
View file

@ -0,0 +1,12 @@
import data.list
open list
lemma last_singleton [simp] {A : Type} (a : A) : last [a] !cons_ne_nil = a :=
rfl
lemma last_cons_cons [simp] {A : Type} (a₁ a₂ : A) (l : list A) : last (a₁::a₂::l) !cons_ne_nil = last (a₂::l) !cons_ne_nil :=
rfl
theorem last_concat [simp] {A : Type} {x : A} : ∀ {l : list A}, last (concat x l) !concat_ne_nil = x :=
by rec_inst_simp