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 lemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
  27 intros.unfold.intro.inversion H
  28   [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
  29   |intros;destruct H4]
  30 qed.
  31
  32 lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
  33                           x = a \lor in_list A x l.
  34 intros;inversion H;intros
  35   [destruct H2;left;reflexivity
  36   |destruct H4;right;assumption]
  37 qed.
  38
  39 lemma in_list_tail : \forall l,x,y.
  40       in_list nat x (y::l) \to x \neq y \to in_list nat x l.
  41 intros 4;elim (in_list_cons_case ? ? ? ? H)
  42   [elim (H2 H1)
  43   |assumption]
  44 qed.
  45
  46 lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
  47 intros;elim (in_list_cons_case ? ? ? ? H)
  48   [assumption
  49   |elim (not_in_list_nil ? ? H1)]
  50 qed.
  51
  52 lemma in_list_to_in_list_append_l: \forall A.\forall x:A.
  53 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
  54 intros.
  55 elim H;simplify
  56   [apply in_list_head
  57   |apply in_list_cons;assumption
  58   ]
  59 qed.
  60
  61 lemma in_list_to_in_list_append_r: \forall A.\forall x:A.
  62 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
  63 intros 3.
  64 elim l1;simplify
  65   [assumption
  66   |apply in_list_cons;apply H;assumption
  67   ]
  68 qed.
  69
  70 theorem in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
  71 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
  72 intros 3.
  73 elim l
  74   [right.apply H
  75   |simplify in H1.inversion H1;intros; destruct;
  76     [left.apply in_list_head
  77     | elim (H l2)
  78       [left.apply in_list_cons. assumption
  79       |right.assumption
  80       |assumption
  81       ]
  82     ]
  83   ]
  84 qed.
  85
  86 let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
  87  match l with
  88   [ nil ⇒ false
  89   | (cons a l') ⇒
  90     match eq x a with
  91      [ true ⇒ true
  92      | false ⇒ mem A eq x l'
  93      ]
  94   ].
  95
  96 lemma mem_true_to_in_list :
  97   \forall A,equ.
  98   (\forall x,y.equ x y = true \to x = y) \to
  99   \forall x,l.mem A equ x l = true \to in_list A x l.
 100 intros 5.elim l
 101   [simplify in H1;destruct H1
 102   |simplify in H2;apply (bool_elim ? (equ x a))
 103      [intro;rewrite > (H ? ? H3);apply in_list_head
 104      |intro;rewrite > H3 in H2;simplify in H2;
 105       apply in_list_cons;apply H1;assumption]]
 106 qed.
 107
 108 lemma in_list_to_mem_true :
 109   \forall A,equ.
 110   (\forall x.equ x x = true) \to
 111   \forall x,l.in_list A x l \to mem A equ x l = true.
 112 intros 5.elim l
 113   [elim (not_in_list_nil ? ? H1)
 114   |elim H2
 115     [simplify;rewrite > H;reflexivity
 116     |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
 117 qed.
 118
 119 lemma in_list_filter_to_p_true : \forall l,x,p.
 120 in_list nat x (filter nat l p) \to p x = true.
 121 intros 3;elim l
 122   [simplify in H;elim (not_in_list_nil ? ? H)
 123   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 124    simplify in H1
 125      [elim (in_list_cons_case ? ? ? ? H1)
 126         [rewrite > H3;assumption
 127         |apply (H H3)]
 128      |apply (H H1)]]
 129 qed.
 130
 131 lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
 132 intros 3;elim l
 133   [simplify in H;elim (not_in_list_nil ? ? H)
 134   |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
 135    simplify in H1
 136      [elim (in_list_cons_case ? ? ? ? H1)
 137         [rewrite > H3;apply in_list_head
 138         |apply in_list_cons;apply H;assumption]
 139      |apply in_list_cons;apply H;assumption]]
 140 qed.
 141
 142 lemma in_list_filter_r : \forall l,p,x.
 143               in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
 144 intros 3;elim l
 145   [elim (not_in_list_nil ? ? H)
 146   |elim (in_list_cons_case ? ? ? ? H1)
 147      [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
 148      |simplify;apply (bool_elim ? (p a));intro;simplify;
 149         [apply in_list_cons;apply H;assumption
 150         |apply H;assumption]]]
 151 qed.
 152
 153 lemma incl_A_A: ∀T,A.incl T A A.
 154 intros.unfold incl.intros.assumption.
 155 qed.