--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
projects / helm.git / blobdiff