X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2Flist%2Fin.ma;fp=matita%2Flibrary%2Flist%2Fin.ma;h=0e3be3a8f221ffd21a2809ad0cf43518f49af3e5;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/library/list/in.ma b/matita/library/list/in.ma
new file mode 100644
index 000000000..0e3be3a8f
--- /dev/null
+++ b/matita/library/list/in.ma
@@ -0,0 +1,155 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "datatypes/bool.ma".
+include "datatypes/constructors.ma".
+include "list/list.ma".
+
+inductive in_list (A:Type): A → (list A) → Prop ≝
+| in_list_head : ∀ x,l.(in_list A x (x::l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
+
+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.
+  
+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
+  |intros;destruct H4]
+qed.
+
+lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
+                          x = a \lor in_list A x l.
+intros;inversion H;intros
+  [destruct H2;left;reflexivity
+  |destruct H4;right;assumption]
+qed.
+
+lemma in_list_tail : \forall l,x,y.
+      in_list nat x (y::l) \to x \neq y \to in_list nat x l.
+intros 4;elim (in_list_cons_case ? ? ? ? H)
+  [elim (H2 H1)
+  |assumption]
+qed.
+
+lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
+intros;elim (in_list_cons_case ? ? ? ? H)
+  [assumption
+  |elim (not_in_list_nil ? ? H1)]
+qed.
+
+lemma in_list_to_in_list_append_l: \forall A.\forall x:A.
+\forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
+intros.
+elim H;simplify
+  [apply in_list_head
+  |apply in_list_cons;assumption
+  ]
+qed.
+
+lemma in_list_to_in_list_append_r: \forall A.\forall x:A.
+\forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
+intros 3.
+elim l1;simplify
+  [assumption
+  |apply in_list_cons;apply H;assumption
+  ]
+qed.
+
+theorem in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
+\forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
+intros 3.
+elim l
+  [right.apply H
+  |simplify in H1.inversion H1;intros; destruct;
+    [left.apply in_list_head
+    | elim (H l2)
+      [left.apply in_list_cons. assumption
+      |right.assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
+ match l with
+  [ nil ⇒ false
+  | (cons a l') ⇒
+    match eq x a with
+     [ true ⇒ true
+     | false ⇒ mem A eq x l'
+     ]
+  ].
+  
+lemma mem_true_to_in_list :
+  \forall A,equ.
+  (\forall x,y.equ x y = true \to x = y) \to
+  \forall x,l.mem A equ x l = true \to in_list A x l.
+intros 5.elim l
+  [simplify in H1;destruct H1
+  |simplify in H2;apply (bool_elim ? (equ x t))
+     [intro;rewrite > (H ? ? H3);apply in_list_head
+     |intro;rewrite > H3 in H2;simplify in H2;
+      apply in_list_cons;apply H1;assumption]]
+qed.
+
+lemma in_list_to_mem_true :
+  \forall A,equ.
+  (\forall x.equ x x = true) \to
+  \forall x,l.in_list A x l \to mem A equ x l = true.
+intros 5.elim l
+  [elim (not_in_list_nil ? ? H1)
+  |elim H2
+    [simplify;rewrite > H;reflexivity
+    |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;reflexivity]].
+qed.
+
+lemma in_list_filter_to_p_true : \forall l,x,p.
+in_list nat x (filter nat l p) \to p x = true.
+intros 3;elim l
+  [simplify in H;elim (not_in_list_nil ? ? H)
+  |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+   simplify in H1
+     [elim (in_list_cons_case ? ? ? ? H1)
+        [rewrite > H3;assumption
+        |apply (H H3)]
+     |apply (H H1)]]
+qed.
+
+lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
+intros 3;elim l
+  [simplify in H;elim (not_in_list_nil ? ? H)
+  |simplify in H1;apply (bool_elim ? (p t));intro;rewrite > H2 in H1;
+   simplify in H1
+     [elim (in_list_cons_case ? ? ? ? H1)
+        [rewrite > H3;apply in_list_head
+        |apply in_list_cons;apply H;assumption]
+     |apply in_list_cons;apply H;assumption]]
+qed.
+
+lemma in_list_filter_r : \forall l,p,x.
+              in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
+intros 3;elim l
+  [elim (not_in_list_nil ? ? H)
+  |elim (in_list_cons_case ? ? ? ? H1)
+     [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
+     |simplify;apply (bool_elim ? (p t));intro;simplify;
+        [apply in_list_cons;apply H;assumption
+        |apply H;assumption]]]
+qed.
+
+lemma incl_A_A: ∀T,A.incl T A A.
+intros.unfold incl.intros.assumption.
+qed.
\ No newline at end of file