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
\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))
+ |simplify in H2;apply (bool_elim ? (equ x a))
[intro;rewrite > (H ? ? H3);apply in_list_head
|intro;rewrite > H3 in H2;simplify in H2;
apply in_list_cons;apply H1;assumption]]
[elim (not_in_list_nil ? ? H1)
|elim H2
[simplify;rewrite > H;reflexivity
- |simplify;rewrite > H4;apply (bool_elim ? (equ a a1));intro;reflexivity]].
+ |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));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;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
simplify in H1
[elim (in_list_cons_case ? ? ? ? H1)
[rewrite > H3;assumption
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;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
simplify in H1
[elim (in_list_cons_case ? ? ? ? H1)
[rewrite > H3;apply in_list_head
[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;
+ |simplify;apply (bool_elim ? (p a));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
+qed.
+
+lemma incl_append_l : ∀T,A,B.incl T A (A @ B).
+unfold incl; intros;autobatch.
+qed.
+
+lemma incl_append_r : ∀T,A,B.incl T B (A @ B).
+unfold incl; intros;autobatch.
+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.
+