]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Fsub/util.ma
new version, using new tacticals
[helm.git] / helm / software / matita / library / Fsub / util.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 set "baseuri" "cic:/matita/Fsub/util".
16 include "logic/equality.ma".
17 include "nat/compare.ma".
18 include "list/list.ma".
19
20 (*** useful definitions and lemmas not really related to Fsub ***)
21
22 lemma eqb_case : \forall x,y.(eqb x y) = true \lor (eqb x y) = false.
23 intros;elim (eqb x y);auto;
24 qed.
25        
26 lemma eq_eqb_case : \forall x,y.((x = y) \land (eqb x y) = true) \lor
27                                 ((x \neq y) \land (eqb x y) = false).
28 intros;lapply (eqb_to_Prop x y);elim (eqb_case x y)
29   [rewrite > H in Hletin;simplify in Hletin;left;auto
30   |rewrite > H in Hletin;simplify in Hletin;right;auto]
31 qed.
32
33 let rec max m n \def
34   match (leb m n) with
35      [true \Rightarrow n
36      |false \Rightarrow m]. 
37
38 inductive in_list (A : Set) : A \to (list A) \to Prop \def
39   | in_Base : \forall x:A.\forall l:(list A).
40               (in_list A x (x :: l))
41   | in_Skip : \forall x,y:A.\forall l:(list A).
42               (in_list A x l) \to (in_list A x (y :: l)).
43
44 definition incl : \forall A.(list A) \to (list A) \to Prop \def
45   \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m).               
46               
47 (* FIXME: use the map in library/list (when there will be one) *)
48 definition map : \forall A,B,f.((list A) \to (list B)) \def
49   \lambda A,B,f.let rec map (l : (list A)) : (list B) \def
50     match l in list return \lambda l0:(list A).(list B) with
51       [nil \Rightarrow (nil B)
52       |(cons (a:A) (t:(list A))) \Rightarrow 
53         (cons B (f a) (map t))] in map.
54
55 definition swap : nat \to nat \to nat \to nat \def
56   \lambda u,v,x.match (eqb x u) with
57     [true \Rightarrow v
58     |false \Rightarrow match (eqb x v) with
59        [true \Rightarrow u
60        |false \Rightarrow x]].
61
62 lemma in_list_nil : \forall A,x.\lnot (in_list A x []).
63 intros.unfold.intro.inversion H
64   [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = [])
65      [assumption|apply nil_cons]
66   |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = [])
67      [assumption|apply nil_cons]]
68 qed.
69
70 lemma notin_cons : \forall A,x,y,l.\lnot (in_list A x (y::l)) \to
71                       (y \neq x) \land \lnot (in_list A x l).
72 intros.split
73   [unfold;intro;apply H;rewrite > H1;constructor 1
74   |unfold;intro;apply H;constructor 2;assumption]
75 qed.
76
77 lemma swap_left : \forall x,y.(swap x y x) = y.
78 intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
79 qed.
80
81 lemma swap_right : \forall x,y.(swap x y y) = x.
82 intros;unfold swap;elim (eq_eqb_case y x)
83   [elim H;rewrite > H2;simplify;rewrite > H1;reflexivity
84   |elim H;rewrite > H2;simplify;rewrite > eqb_n_n;simplify;reflexivity]
85 qed.
86
87 lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
88 intros;unfold swap;elim (eq_eqb_case z x)
89   [elim H2;lapply (H H3);elim Hletin
90   |elim H2;rewrite > H4;simplify;elim (eq_eqb_case z y)
91      [elim H5;lapply (H1 H6);elim Hletin
92      |elim H5;rewrite > H7;simplify;reflexivity]]
93 qed. 
94
95 lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
96 intros;unfold in match (swap u v x);elim (eq_eqb_case x u)
97   [elim H;rewrite > H2;simplify;rewrite > H1;apply swap_right
98   |elim H;rewrite > H2;simplify;elim (eq_eqb_case x v)
99      [elim H3;rewrite > H5;simplify;rewrite > H4;apply swap_left
100      |elim H3;rewrite > H5;simplify;apply (swap_other ? ? ? H1 H4)]]
101 qed.
102
103 lemma swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y.
104 intros;unfold swap in H;elim (eq_eqb_case x u)
105   [elim H1;elim (eq_eqb_case y u)
106      [elim H4;rewrite > H5;assumption
107      |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
108       elim (eq_eqb_case y v)
109         [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8;
110          lapply (H5 H8);elim Hletin
111         |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]]
112   |elim H1;elim (eq_eqb_case y u)
113      [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
114       elim (eq_eqb_case x v)
115         [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8;
116          elim H2;assumption
117         |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption]
118      |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
119       elim (eq_eqb_case x v)
120         [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
121            [elim H10;rewrite > H11;assumption
122            |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry;
123             assumption]
124         |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
125            [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption
126            |elim H10;rewrite > H12 in H;simplify in H;assumption]]]]
127 qed.
128
129 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
130       [ false \Rightarrow n
131       | true \Rightarrow m ].
132 intros;elim m;simplify;reflexivity;
133 qed.