1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Fsub/util".
16 include "logic/equality.ma".
17 include "nat/compare.ma".
18 include "list/list.ma".
20 (*** useful definitions and lemmas not really related to Fsub ***)
25 |false \Rightarrow m].
27 inductive in_list (A : Type) : A \to (list A) \to Prop \def
28 | in_Base : \forall x:A.\forall l:(list A).
29 (in_list A x (x :: l))
30 | in_Skip : \forall x,y:A.\forall l:(list A).
31 (in_list A x l) \to (in_list A x (y :: l)).
33 definition incl : \forall A.(list A) \to (list A) \to Prop \def
34 \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m).
36 (* FIXME: use the map in library/list (when there will be one) *)
37 definition map : \forall A,B,f.((list A) \to (list B)) \def
38 \lambda A,B,f.let rec map (l : (list A)) : (list B) \def
39 match l in list return \lambda l0:(list A).(list B) with
40 [nil \Rightarrow (nil B)
41 |(cons (a:A) (t:(list A))) \Rightarrow
42 (cons B (f a) (map t))] in map.
44 lemma in_list_nil : \forall A,x.\lnot (in_list A x []).
45 intros.unfold.intro.inversion H
46 [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = [])
47 [assumption|apply nil_cons]
48 |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = [])
49 [assumption|apply nil_cons]]
52 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
54 | true \Rightarrow m ].
55 intros;elim m;simplify;reflexivity;