helm/software/matita/library/list/in.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "datatypes/bool.ma".
  16 include "datatypes/constructors.ma".
  17 include "list/list.ma".
  18
  19 inductive in_list (A:Type): A → (list A) → Prop ≝
  20 | in_list_head : ∀ x,l.(in_list A x (x::l))
  21 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
  22
  23 definition incl : \forall A.(list A) \to (list A) \to Prop \def
  24   \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
  25
  26 notation "hvbox(a break ∉ b)" non associative with precedence 45
  27 for @{ 'notmem $a $b }.
  28
  29 interpretation "list member" 'mem x l = (in_list ? x l).
  30 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
  31 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
  32
  33 lemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
  34 intros.unfold.intro.inversion H
  35   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
  36   |intros;destruct H4]
  37 qed.
  38
  39 lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
  40                           x = a \lor in_list A x l.
  41 intros;inversion H;intros
  42   [destruct H2;left;reflexivity
  43   |destruct H4;right;assumption]
  44 qed.
  45
  46 lemma in_list_tail : \forall l,x,y.
  47       in_list nat x (y::l) \to x \neq y \to in_list nat x l.
  48 intros 4;elim (in_list_cons_case ? ? ? ? H)
  49   [elim (H2 H1)
  50   |assumption]
  51 qed.
  52
  53 lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
  54 intros;elim (in_list_cons_case ? ? ? ? H)
  55   [assumption
  56   |elim (not_in_list_nil ? ? H1)]
  57 qed.
  58
  59 lemma in_list_to_in_list_append_l: \forall A.\forall x:A.
  60 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
  61 intros.
  62 elim H;simplify
  63   [apply in_list_head
  64   |apply in_list_cons;assumption
  65   ]
  66 qed.
  67
  68 lemma in_list_to_in_list_append_r: \forall A.\forall x:A.
  69 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
  70 intros 3.
  71 elim l1;simplify
  72   [assumption
  73   |apply in_list_cons;apply H;assumption
  74   ]
  75 qed.
  76
  77 theorem in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
  78 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
  79 intros 3.
  80 elim l
  81   [right.apply H
  82   |simplify in H1.inversion H1;intros; destruct;
  83     [left.apply in_list_head
  84     | elim (H l2)
  85       [left.apply in_list_cons. assumption
  86       |right.assumption
  87       |assumption
  88       ]
  89     ]
  90   ]
  91 qed.
  92
  93 let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
  94  match l with
  95   [ nil ⇒ false
  96   | (cons a l') ⇒
  97     match eq x a with
  98      [ true ⇒ true
  99      | false ⇒ mem A eq x l'
 100      ]
 101   ].
 102
 103 lemma mem_true_to_in_list :
 104   \forall A,equ.
 105   (\forall x,y.equ x y = true \to x = y) \to
 106   \forall x,l.mem A equ x l = true \to in_list A x l.
 107 intros 5.elim l
 108   [simplify in H1;destruct H1
 109   |simplify in H2;apply (bool_elim ? (equ x a))
 110      [intro;rewrite > (H ? ? H3);apply in_list_head
 111      |intro;rewrite > H3 in H2;simplify in H2;
 112       apply in_list_cons;apply H1;assumption]]
 113 qed.
 114
 115 lemma in_list_to_mem_true :
 116   \forall A,equ.
 117   (\forall x.equ x x = true) \to
 118   \forall x,l.in_list A x l \to mem A equ x l = true.
 119 intros 5.elim l
 120   [elim (not_in_list_nil ? ? H1)
 121   |elim H2
 122     [simplify;rewrite > H;reflexivity
 123     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 124 qed.
 125
 126 lemma in_list_filter_to_p_true : \forall l,x,p.
 127 in_list nat x (filter nat l p) \to p x = true.
 128 intros 3;elim l
 129   [simplify in H;elim (not_in_list_nil ? ? H)
 130   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 131    simplify in H1
 132      [elim (in_list_cons_case ? ? ? ? H1)
 133         [rewrite > H3;assumption
 134         |apply (H H3)]
 135      |apply (H H1)]]
 136 qed.
 137
 138 lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
 139 intros 3;elim l
 140   [simplify in H;elim (not_in_list_nil ? ? H)
 141   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 142    simplify in H1
 143      [elim (in_list_cons_case ? ? ? ? H1)
 144         [rewrite > H3;apply in_list_head
 145         |apply in_list_cons;apply H;assumption]
 146      |apply in_list_cons;apply H;assumption]]
 147 qed.
 148
 149 lemma in_list_filter_r : \forall l,p,x.
 150               in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
 151 intros 3;elim l
 152   [elim (not_in_list_nil ? ? H)
 153   |elim (in_list_cons_case ? ? ? ? H1)
 154      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
 155      |simplify;apply (bool_elim ? (p a));intro;simplify;
 156         [apply in_list_cons;apply H;assumption
 157         |apply H;assumption]]]
 158 qed.
 159
 160 lemma incl_A_A: ∀T,A.incl T A A.
 161 intros.unfold incl.intros.assumption.
 162 qed.
 163
 164 lemma incl_append_l : ∀T,A,B.incl T A (A @ B).
 165 unfold incl; intros;autobatch.
 166 qed.
 167
 168 lemma incl_append_r : ∀T,A,B.incl T B (A @ B).
 169 unfold incl; intros;autobatch.
 170 qed.
 171
 172 lemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 173 unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 174 qed.
 175