lean2/tests/lean/run/list_elab1.lean
Leonardo de Moura 364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00

30 lines
1.1 KiB
Text

----------------------------------------------------------------------------------------------------
--- Copyright (c) 2014 Parikshit Khanna. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Authors: Parikshit Khanna, Jeremy Avigad
----------------------------------------------------------------------------------------------------
-- Theory list
-- ===========
--
-- Basic properties of lists.
import data.nat
open nat eq_ops
inductive list (T : Type) : Type :=
nil {} : list T,
cons : T → list T → list T
namespace list
theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=
list.rec Hnil Hind l
definition concat {T : Type} (s t : list T) : list T :=
list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
theorem concat_nil {T : Type} (t : list T) : concat t nil = t :=
list_induction_on t (eq.refl (concat nil nil))
(take (x : T) (l : list T) (H : concat l nil = l),
H ▸ (eq.refl (concat (cons x l) nil)))
end list