helm/software/matita/contribs/POPLmark/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 include "logic/equality.ma".
  16 include "nat/compare.ma".
  17 include "list/list.ma".
  18 include "list/in.ma".
  19
  20 (*** useful definitions and lemmas not really related to Fsub ***)
  21
  22 definition max \def
  23 \lambda m,n.
  24   match (leb m n) with
  25      [true \Rightarrow n
  26      |false \Rightarrow m].
  27
  28 lemma le_n_max_m_n: \forall m,n:nat. n \le max m n.
  29 intros.
  30 unfold max.
  31 apply (leb_elim m n)
  32   [simplify.intros.apply le_n
  33   |simplify.intros.autobatch
  34   ]
  35 qed.
  36
  37 lemma le_m_max_m_n: \forall m,n:nat. m \le max m n.
  38 intros.
  39 unfold max.
  40 apply (leb_elim m n)
  41   [simplify.intro.assumption
  42   |simplify.intros.autobatch
  43   ]
  44 qed.
  45
  46 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
  47       [ true \Rightarrow n
  48       | false \Rightarrow m ].
  49 intros;elim m;simplify;reflexivity;
  50 qed.
  51
  52 definition swap : nat → nat → nat → nat ≝
  53   λu,v,x.match (eqb x u) with
  54     [true ⇒ v
  55     |false ⇒ match (eqb x v) with
  56        [true ⇒ u
  57        |false ⇒ x]].
  58
  59 lemma swap_left : ∀x,y.(swap x y x) = y.
  60 intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
  61 qed.
  62
  63 lemma swap_right : ∀x,y.(swap x y y) = x.
  64 intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch;
  65 qed.
  66
  67 lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
  68 intros;unfold swap;apply (eqb_elim z x);intro;simplify
  69   [elim H;assumption
  70   |rewrite > not_eq_to_eqb_false;autobatch]
  71 qed.
  72
  73 lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
  74 intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify
  75   [autobatch paramodulation
  76   |apply (eqb_elim x v);intro;simplify
  77      [autobatch paramodulation
  78      |apply swap_other;assumption]]
  79 qed.
  80
  81 lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y.
  82 intros 4;unfold swap;apply (eqb_elim x u);simplify;intro
  83   [apply (eqb_elim y u);simplify;intro
  84      [intro;autobatch paramodulation
  85      |apply (eqb_elim y v);simplify;intros
  86         [autobatch paramodulation
  87         |elim H2;symmetry;assumption]]
  88   |apply (eqb_elim y u);simplify;intro
  89      [apply (eqb_elim x v);simplify;intros;
  90         [autobatch paramodulation
  91         |elim H2;assumption]
  92      |apply (eqb_elim x v);simplify;intro
  93         [apply (eqb_elim y v);simplify;intros
  94            [autobatch paramodulation
  95            |elim H1;symmetry;assumption]
  96         |apply (eqb_elim y v);simplify;intros
  97            [elim H;assumption
  98            |assumption]]]]
  99 qed.
 100
 101 definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
 102   \lambda u,v,l.(map ? ? (swap u v) l).
 103
 104 let rec posn l x on l ≝
 105   match l with
 106   [ nil ⇒ O
 107   | (cons (y:nat) l2) ⇒
 108       match (eqb x y) with
 109             [ true ⇒ O
 110             | false ⇒ S (posn l2 x)]].
 111
 112 let rec lookup n l on l ≝
 113   match l with
 114     [ nil ⇒ false
 115     | cons (x:nat) l1 ⇒ match (eqb n x) with
 116               [true ⇒ true
 117               |false ⇒ (lookup n l1)]].
 118
 119 let rec head (A:Type) l on l ≝
 120   match l with
 121   [ nil ⇒ None A
 122   | (cons (x:A) l2) ⇒ Some A x].
 123
 124 definition max_list : (list nat) \to nat \def
 125   \lambda l.let rec aux l0 m on l0 \def
 126     match l0 with
 127       [ nil ⇒ m
 128       | (cons n l2) ⇒ (aux l2 (max m n))]
 129     in aux l O.
 130
 131 let rec remove_nat (x:nat) (l:list nat) on l \def
 132   match l with
 133   [ nil ⇒ (nil nat)
 134   | (cons y l2) ⇒ match (eqb x y) with
 135                   [ true ⇒ (remove_nat x l2)
 136                   | false ⇒ (y :: (remove_nat x l2)) ]].
 137
 138 lemma in_lookup : \forall x,l.x ∈ l \to (lookup x l = true).
 139 intros;elim H;simplify
 140   [rewrite > eqb_n_n;reflexivity
 141   |rewrite > H2;elim (eqb a a1);reflexivity]
 142 qed.
 143
 144 lemma lookup_in : \forall x,l.(lookup x l = true) \to x ∈ l.
 145 intros 2;elim l
 146   [simplify in H;destruct H
 147   |generalize in match H1;simplify;elim (decidable_eq_nat x a)
 148      [applyS in_list_head
 149      |apply in_list_cons;apply H;
 150       rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;assumption]]
 151 qed.
 152
 153 lemma posn_length : \forall x,vars.x ∈ vars →
 154                        (posn vars x) < (length ? vars).
 155 intros 2;elim vars
 156   [elim (not_in_list_nil ? ? H)
 157   |inversion H1;intros;destruct;simplify
 158      [rewrite > eqb_n_n;simplify;
 159       apply lt_O_S
 160      |elim (eqb x a);simplify
 161         [apply lt_O_S
 162         |apply le_S_S;apply H;assumption]]]
 163 qed.
 164
 165 lemma in_remove : \forall a,b,l.(a ≠ b) \to a ∈ l \to
 166                                 a ∈ (remove_nat b l).
 167 intros 4;elim l
 168   [elim (not_in_list_nil ? ? H1)
 169   |inversion H2;intros;destruct;simplify
 170      [rewrite > not_eq_to_eqb_false
 171         [simplify;apply in_list_head
 172         |intro;apply H;symmetry;assumption]
 173      |elim (eqb b a1);simplify
 174         [apply H1;assumption
 175         |apply in_list_cons;apply H1;assumption]]]
 176 qed.
 177
 178 lemma swap_same : \forall x,y.swap x x y = y.
 179 intros;elim (decidable_eq_nat y x)
 180   [autobatch paramodulation
 181   |rewrite > swap_other;autobatch]
 182 qed.
 183
 184 lemma not_nat_in_to_lookup_false : ∀l,X. X ∉ l → lookup X l = false.
 185 intros 2;elim l;simplify
 186   [reflexivity
 187   |elim (decidable_eq_nat X a)
 188      [elim H1;rewrite > H2;apply in_list_head
 189      |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
 190       apply (in_list_cons ? ? ? ? H3);]]
 191 qed.
 192
 193 lemma lookup_swap : ∀a,b,x,vars.
 194                     lookup (swap a b x) (swap_list a b vars) =
 195                     lookup x vars.
 196 intros 4;elim vars;simplify
 197   [reflexivity
 198   |elim (decidable_eq_nat x a1)
 199      [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
 200      |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
 201         [rewrite > H;rewrite > H2;rewrite > swap_left;
 202          elim (decidable_eq_nat b a1)
 203            [rewrite < H3;rewrite > swap_right;
 204             rewrite > (not_eq_to_eqb_false b a)
 205               [reflexivity
 206               |intro;autobatch]
 207            |rewrite > (swap_other a b a1)
 208               [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
 209               |*:intro;autobatch]]
 210         |elim (decidable_eq_nat x b)
 211            [rewrite > H;rewrite > H3;rewrite > swap_right;
 212             elim (decidable_eq_nat a1 a)
 213               [rewrite > H4;rewrite > swap_left;
 214                rewrite > (not_eq_to_eqb_false a b)
 215                  [reflexivity
 216                  |intro;autobatch]
 217               |rewrite > (swap_other a b a1)
 218                  [rewrite > (not_eq_to_eqb_false a a1)
 219                     [reflexivity
 220                     |intro;autobatch]
 221                  |assumption
 222                  |intro;autobatch]]
 223            |rewrite > H;rewrite > (swap_other a b x)
 224               [elim (decidable_eq_nat a a1)
 225                  [rewrite > H4;rewrite > swap_left;
 226                   rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
 227                  |elim (decidable_eq_nat b a1)
 228                     [rewrite > H5;rewrite > swap_right;
 229                      rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
 230                     |rewrite > (swap_other a b a1)
 231                        [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
 232                        |*:intro;autobatch]]]
 233               |*:assumption]]]]]
 234 qed.
 235
 236 lemma posn_swap : ∀a,b,x,vars.
 237                   posn vars x = posn (swap_list a b vars) (swap a b x).
 238 intros 4;elim vars;simplify
 239   [reflexivity
 240   |rewrite < H;elim (decidable_eq_nat x a1)
 241      [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
 242      |elim (decidable_eq_nat (swap a b x) (swap a b a1))
 243         [elim H1;autobatch
 244         |rewrite > (not_eq_to_eqb_false ? ? H1);
 245          rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
 246 qed.
 247
 248 lemma remove_inlist : \forall x,y,l.x ∈ (remove_nat y l) → x ∈ l \land x ≠ y.
 249 intros 3;elim l 0;simplify;intro
 250   [elim (not_in_list_nil ? ? H)
 251   |elim (decidable_eq_nat y a)
 252      [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
 253       rewrite > H in H1;elim (H1 H2);rewrite > H;split
 254         [apply in_list_cons;assumption
 255         |assumption]
 256      |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
 257       inversion H2;intros;destruct;
 258         [split;autobatch
 259         |elim (H1 H3);split;autobatch]]]
 260 qed.
 261
 262 lemma inlist_remove : ∀x,y,l.x ∈ l → x ≠ y → x ∈ (remove_nat y l).
 263 intros 3;elim l
 264   [elim (not_in_list_nil ? ? H);
 265   |simplify;elim (decidable_eq_nat y a)
 266      [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
 267         [inversion H1;intros;destruct;
 268            [elim H2;reflexivity
 269            |assumption]
 270         |assumption]
 271      |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
 272       inversion H1;intros;destruct;autobatch]]
 273 qed.
 274
 275 lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
 276 intros;unfold in match swap;simplify;elim (eqb x u);simplify
 277   [autobatch
 278   |elim (eqb x v);simplify;autobatch]
 279 qed.
 280
 281 definition distinct_list ≝
 282 λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
 283
 284 lemma posn_nth: ∀l,n.distinct_list l → n < length ? l →
 285                     posn l (nth ? l O n) = n.
 286 intro;elim l
 287   [simplify in H1;elim (not_le_Sn_O ? H1)
 288   |simplify in H2;generalize in match H2;elim n
 289      [simplify;rewrite > eqb_n_n;simplify;reflexivity
 290      |simplify;cut (nth ? (a::l1) O (S n1) ≠ nth ? (a::l1) O O)
 291         [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
 292          rewrite > (H n1)
 293            [reflexivity
 294            |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
 295               [simplify in Hletin;assumption
 296               |2,3:simplify;autobatch
 297               |intro;apply H7;destruct H8;reflexivity]
 298            |autobatch]
 299         |intro;apply H1;
 300            [6:apply H5
 301            |skip
 302            |skip
 303            |(*** *:autobatch; *)
 304             apply H4
 305            |simplify;autobatch
 306            |intro;elim (not_eq_O_S n1);symmetry;assumption]]]]
 307 qed.
 308
 309 lemma nth_in_list : ∀l,n. n < length ? l → (nth ? l O n) ∈ l.
 310 intro;elim l
 311   [simplify in H;elim (not_le_Sn_O ? H)
 312   |generalize in match H1;elim n;simplify
 313      [apply in_list_head
 314      |apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
 315 qed.
 316
 317 lemma lookup_nth : \forall l,n.n < length ? l \to
 318                    lookup (nth nat l O n) l = true.
 319 intro;elim l
 320   [elim (not_le_Sn_O ? H);
 321   |generalize in match H1;elim n;simplify
 322      [rewrite > eqb_n_n;reflexivity
 323      |elim (eqb (nth nat l1 O n1) a);simplify;
 324         [reflexivity
 325         |apply H;apply le_S_S_to_le;assumption]]]
 326 qed.