-definition ord_list \def
- \lambda l.
- \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a.
-
-definition in_list \def
- \lambda A.\lambda a:A.\lambda l:list A.
- \exists l1,l2.l = l1@(a::l2).
-
-lemma in_list_filter_to_p_true : \forall l,x,p.in_list nat x (filter nat l p) \to p x = true.
-intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
- [simplify;intro;elim l1
- [simplify in H;destruct H
- |simplify in H1;destruct H1]
- |intros;simplify in H1;apply (bool_elim ? (p t));intro;
- rewrite > H3 in H1;simplify in H1
- [generalize in match H1;elim l2
- [simplify in H4;destruct H4;assumption
- |simplify in H5;destruct H5;apply (H l3);assumption]
- |apply (H l2);assumption]]
-qed.
-
-lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l).
-intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a));
-apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity.
-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;elim H;elim H2;generalize in match H3;elim a
- [simplify in H4;destruct H4;elim H1;reflexivity
- |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1);
- reflexivity]
-qed.
-
-lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
-intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0
- [simplify;intro;elim l1
- [simplify in H3;destruct H3
- |simplify in H4;destruct H4]
- |intros;simplify in H4;apply (bool_elim ? (p t));intro
- [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2
- [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
- simplify;reflexivity
- |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);]
- |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]]
-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;elim H;elim H2;rewrite > H3;elim a
- [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p));
- reflexivity
- |simplify;elim (p t);simplify
- [apply in_list_cons;assumption
- |assumption]]
-qed.
-
-lemma in_list_head : \forall x,l.in_list nat x (x::l).
-intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
-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;elim H;elim H1;clear H H1;generalize in match H2;elim a1
- [simplify in H;destruct H;left;reflexivity
- |simplify in H1;destruct H1;right;
- apply (ex_intro ? ? l1);
- apply (ex_intro ? ? a2);
- reflexivity]
-qed.
-