From fe63c5efb416a23ee43ea61ee47fa8f4e3f99c52 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Sat, 20 Jun 2009 16:53:44 +0000 Subject: [PATCH] Some notation and additional lemmata. --- helm/software/matita/library/list/in.ma | 10 +++++++++- helm/software/matita/library/list/list.ma | 6 ++++++ 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/list/in.ma b/helm/software/matita/library/list/in.ma index 310c3f369..3285fef2e 100644 --- a/helm/software/matita/library/list/in.ma +++ b/helm/software/matita/library/list/in.ma @@ -23,6 +23,13 @@ inductive in_list (A:Type): A → (list A) → Prop ≝ definition incl : \forall A.(list A) \to (list A) \to Prop \def \lambda A,l,m.\forall x.in_list A x l \to in_list A x m. +notation "hvbox(a break ∉ b)" non associative with precedence 45 +for @{ 'notmem $a $b }. + +interpretation "list member" 'mem x l = (in_list ? x l). +interpretation "list not member" 'notmem x l = (Not (in_list ? x l)). +interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2). + lemma not_in_list_nil : \forall A,x.\lnot in_list A x []. intros.unfold.intro.inversion H [intros;lapply (sym_eq ? ? ? H2);destruct Hletin @@ -164,4 +171,5 @@ qed. lemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. -qed. \ No newline at end of file +qed. + diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index 19866cc29..077e1af6c 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -195,3 +195,9 @@ intros;elim l [simplify;apply le_S_S;assumption |simplify;apply le_S;assumption]] qed. + +lemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m. +intros;elim l +[reflexivity +|simplify;rewrite < H;reflexivity] +qed. -- 2.39.2