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.