matita/matita/lib/binding/fp.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 "binding/names.ma".
  16
  17 (* permutations *)
  18 definition finite_perm : ∀X:Nset.(X → X) → Prop ≝
  19  λX,f.injective X X f ∧ surjective X X f ∧ ∃l.∀x.x ∉ l → f x = x.
  20
  21 (* maps a permutation to a list of parameters *)
  22 definition Pi_list : ∀X:Nset.(X → X) → list X → list X ≝
  23  λX,p,xl.map ?? (λx.p x) xl.
  24
  25 interpretation "permutation of X list" 'middot p x = (Pi_list p x).
  26
  27 definition swap : ∀N:Nset.N → N → N → N ≝
  28   λN,u,v,x.match (x == u) with
  29     [true ⇒ v
  30     |false ⇒ match (x == v) with
  31        [true ⇒ u
  32        |false ⇒ x]].
  33
  34 axiom swap_right : ∀N,x,y.swap N x y y = x.
  35 (*
  36 #N x y;nnormalize;nrewrite > (p_eqb3 ? y y …);//;
  37 nlapply (refl ? (y ≟ x));ncases (y ≟ x) in ⊢ (???% → %);nnormalize;//;
  38 #H1;napply p_eqb1;//;
  39 nqed.
  40 *)
  41
  42 axiom swap_left : ∀N,x,y.swap N x y x = y.
  43 (*
  44 #N x y;nnormalize;nrewrite > (p_eqb3 ? x x …);//;
  45 nqed.
  46 *)
  47
  48 axiom swap_other : ∀N,x,y,z.x ≠ z → y ≠ z → swap N x y z = z.
  49 (*
  50 #N x y z H1 H2;nnormalize;nrewrite > (p_eqb4 …);
  51 ##[nrewrite > (p_eqb4 …);//;@;ncases H2;/2/;
  52 ##|@;ncases H1;/2/
  53 ##]
  54 nqed.
  55 *)
  56
  57 axiom swap_inv : ∀N,x,y,z.swap N x y (swap N x y z) = z.
  58 (*
  59 #N x y z;nlapply (refl ? (x ≟ z));ncases (x ≟ z) in ⊢ (???% → ?);#H1
  60 ##[nrewrite > (p_eqb1 … H1);nrewrite > (swap_left …);//;
  61 ##|nlapply (refl ? (y ≟ z));ncases (y ≟ z) in ⊢ (???% → ?);#H2
  62    ##[nrewrite > (p_eqb1 … H2);nrewrite > (swap_right …);//;
  63    ##|nrewrite > (swap_other …) in ⊢ (??(????%)?);/2/;
  64       nrewrite > (swap_other …);/2/;
  65    ##]
  66 ##]
  67 nqed.
  68 *)
  69
  70 axiom swap_fp : ∀N,x1,x2.finite_perm ? (swap N x1 x2).
  71 (*
  72 #N x1 x2;@
  73 ##[@
  74    ##[nwhd;#xa xb;nnormalize;nlapply (refl ? (xa ≟ x1));
  75       ncases (xa ≟ x1) in ⊢ (???% → %);#H1
  76       ##[nrewrite > (p_eqb1 … H1);nlapply (refl ? (xb ≟ x1));
  77          ncases (xb ≟ x1) in ⊢ (???% → %);#H2
  78          ##[nrewrite > (p_eqb1 … H2);//
  79          ##|nlapply (refl ? (xb ≟ x2));
  80             ncases (xb ≟ x2) in ⊢ (???% → %);#H3
  81             ##[nnormalize;#H4;nrewrite > H4 in H3;
  82                #H3;nrewrite > H3 in H2;#H2;ndestruct (H2)
  83             ##|nnormalize;#H4;nrewrite > H4 in H3;
  84                nrewrite > (p_eqb3 …);//;#H5;ndestruct (H5)
  85             ##]
  86          ##]
  87       ##|nlapply (refl ? (xa ≟ x2));
  88          ncases (xa ≟ x2) in ⊢ (???% → %);#H2
  89          ##[nrewrite > (p_eqb1 … H2);nlapply (refl ? (xb ≟ x1));
  90             ncases (xb ≟ x1) in ⊢ (???% → %);#H3
  91             ##[nnormalize;#H4;nrewrite > H4 in H3;
  92                #H3;nrewrite > (p_eqb1 … H3);@
  93             ##|nnormalize;nlapply (refl ? (xb ≟ x2));
  94                ncases (xb ≟ x2) in ⊢ (???% → %);#H4
  95                ##[nrewrite > (p_eqb1 … H4);//
  96                ##|nnormalize;#H5;nrewrite > H5 in H3;
  97                   nrewrite > (p_eqb3 …);//;#H6;ndestruct (H6);
  98                ##]
  99             ##]
 100          ##|nnormalize;nlapply (refl ? (xb ≟ x1));
 101             ncases (xb ≟ x1) in ⊢ (???% → %);#H3
 102             ##[nnormalize;#H4;nrewrite > H4 in H2;nrewrite > (p_eqb3 …);//;
 103                #H5;ndestruct (H5)
 104             ##|nlapply (refl ? (xb ≟ x2));
 105                ncases (xb ≟ x2) in ⊢ (???% → %);#H4
 106                ##[nnormalize;#H5;nrewrite > H5 in H1;nrewrite > (p_eqb3 …);//;
 107                   #H6;ndestruct (H6)
 108                ##|nnormalize;//
 109                ##]
 110             ##]
 111          ##]
 112       ##]
 113    ##|nwhd;#z;nnormalize;nlapply (refl ? (z ≟ x1));
 114       ncases (z ≟ x1) in ⊢ (???% → %);#H1
 115       ##[nlapply (refl ? (z ≟ x2));
 116          ncases (z ≟ x2) in ⊢ (???% → %);#H2
 117          ##[@ z;nrewrite > H1;nrewrite > H2;napply p_eqb1;//
 118          ##|@ x2;nrewrite > (p_eqb4 …);
 119             ##[nrewrite > (p_eqb3 …);//;
 120                nnormalize;napply p_eqb1;//
 121             ##|nrewrite < (p_eqb1 … H1);@;#H3;nrewrite > H3 in H2;
 122                nrewrite > (p_eqb3 …);//;#H2;ndestruct (H2)
 123             ##]
 124          ##]
 125       ##|nlapply (refl ? (z ≟ x2));
 126          ncases (z ≟ x2) in ⊢ (???% → %);#H2
 127          ##[@ x1;nrewrite > (p_eqb3 …);//;
 128             napply p_eqb1;nnormalize;//
 129          ##|@ z;nrewrite > H1;nrewrite > H2;@;
 130          ##]
 131       ##]
 132    ##]
 133 ##|@ [x1;x2];#x0 H1;nrewrite > (swap_other …)
 134    ##[@
 135    ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;/2/;
 136    ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;//;
 137    ##]
 138 ##]
 139 nqed.
 140 *)
 141
 142 axiom inj_swap : ∀N,u,v.injective ?? (swap N u v).
 143 (*
 144 #N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
 145 nqed.
 146 *)
 147
 148 axiom surj_swap : ∀N,u,v.surjective ?? (swap N u v).
 149 (*
 150 #N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
 151 nqed.
 152 *)
 153
 154 axiom finite_swap : ∀N,u,v.∃l.∀x.x ∉ l → swap N u v x = x.
 155 (*
 156 #N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
 157 nqed.
 158 *)
 159
 160 (* swaps two lists of parameters
 161 definition Pi_swap_list : ∀xl,xl':list X.X → X ≝
 162  λxl,xl',x.foldr2 ??? (λu,v,r.swap ? u v r) x xl xl'.
 163
 164 nlemma fp_swap_list :
 165   ∀xl,xl'.finite_perm ? (Pi_swap_list xl xl').
 166 #xl xl';@
 167 ##[@;
 168    ##[ngeneralize in match xl';nelim xl
 169       ##[nnormalize;//;
 170       ##|#x0 xl0;#IH xl'';nelim xl''
 171          ##[nnormalize;//
 172          ##|#x1 xl1 IH1 y0 y1;nchange in ⊢ (??%% → ?) with (swap ????);
 173             #H1;nlapply (inj_swap … H1);#H2;
 174             nlapply (IH … H2);//
 175          ##]
 176       ##]
 177    ##|ngeneralize in match xl';nelim xl
 178       ##[nnormalize;#_;#z;@z;@
 179       ##|#x' xl0 IH xl'';nelim xl''
 180          ##[nnormalize;#z;@z;@
 181          ##|#x1 xl1 IH1 z;
 182             nchange in ⊢ (??(λ_.???%)) with (swap ????);
 183             ncases (surj_swap X x' x1 z);#x2 H1;
 184             ncases (IH xl1 x2);#x3 H2;@ x3;
 185             nrewrite < H2;napply H1
 186          ##]
 187       ##]
 188    ##]
 189 ##|ngeneralize in match xl';nelim xl
 190    ##[#;@ [];#;@
 191    ##|#x0 xl0 IH xl'';ncases xl''
 192       ##[@ [];#;@
 193       ##|#x1 xl1;ncases (IH xl1);#xl2 H1;
 194          ncases (finite_swap X x0 x1);#xl3 H2;
 195          @ (xl2@xl3);#x2 H3;
 196          nchange in ⊢ (??%?) with (swap ????);
 197          nrewrite > (H1 …);
 198          ##[nrewrite > (H2 …);//;@;#H4;ncases H3;#H5;napply H5;
 199             napply in_list_to_in_list_append_r;//
 200          ##|@;#H4;ncases H3;#H5;napply H5;
 201             napply in_list_to_in_list_append_l;//
 202          ##]
 203       ##]
 204    ##]
 205 ##]
 206 nqed.
 207
 208 (* the 'reverse' swap of lists of parameters
 209    composing Pi_swap_list and Pi_swap_list_r yields the identity function
 210    (see the Pi_swap_list_inv lemma) *)
 211 ndefinition Pi_swap_list_r : ∀xl,xl':list X. Pi ≝
 212  λxl,xl',x.foldl2 ??? (λr,u,v.swap ? u v r ) x xl xl'.
 213
 214 nlemma fp_swap_list_r :
 215   ∀xl,xl'.finite_perm ? (Pi_swap_list_r xl xl').
 216 #xl xl';@
 217 ##[@;
 218    ##[ngeneralize in match xl';nelim xl
 219       ##[nnormalize;//;
 220       ##|#x0 xl0;#IH xl'';nelim xl''
 221          ##[nnormalize;//
 222          ##|#x1 xl1 IH1 y0 y1;nwhd in ⊢ (??%% → ?);
 223             #H1;nlapply (IH … H1);#H2;
 224             napply (inj_swap … H2);
 225          ##]
 226       ##]
 227    ##|ngeneralize in match xl';nelim xl
 228       ##[nnormalize;#_;#z;@z;@
 229       ##|#x' xl0 IH xl'';nelim xl''
 230          ##[nnormalize;#z;@z;@
 231          ##|#x1 xl1 IH1 z;nwhd in ⊢ (??(λ_.???%));
 232             ncases (IH xl1 z);#x2 H1;
 233             ncases (surj_swap X x' x1 x2);#x3 H2;
 234             @ x3;nrewrite < H2;napply H1;
 235          ##]
 236       ##]
 237    ##]
 238 ##|ngeneralize in match xl';nelim xl
 239    ##[#;@ [];#;@
 240    ##|#x0 xl0 IH xl'';ncases xl''
 241       ##[@ [];#;@
 242       ##|#x1 xl1;
 243          ncases (IH xl1);#xl2 H1;
 244          ncases (finite_swap X x0 x1);#xl3 H2;
 245          @ (xl2@xl3);#x2 H3;nwhd in ⊢ (??%?);
 246          nrewrite > (H2 …);
 247          ##[nrewrite > (H1 …);//;@;#H4;ncases H3;#H5;napply H5;
 248             napply in_list_to_in_list_append_l;//
 249          ##|@;#H4;ncases H3;#H5;napply H5;
 250             napply in_list_to_in_list_append_r;//
 251          ##]
 252       ##]
 253    ##]
 254 ##]
 255 nqed.
 256
 257 nlemma Pi_swap_list_inv :
 258  ∀xl1,xl2,x.
 259  Pi_swap_list xl1 xl2 (Pi_swap_list_r xl1 xl2 x) = x.
 260 #xl;nelim xl
 261 ##[#;@
 262 ##|#x1 xl1 IH xl';ncases xl'
 263    ##[#;@
 264    ##|#x2 xl2;#x;
 265       nchange in ⊢ (??%?) with
 266         (swap ??? (Pi_swap_list ??
 267                   (Pi_swap_list_r ?? (swap ????))));
 268       nrewrite > (IH xl2 ?);napply swap_inv;
 269    ##]
 270 ##]
 271 nqed.
 272
 273 nlemma Pi_swap_list_fresh :
 274   ∀x,xl1,xl2.x ∉ xl1 → x ∉ xl2 → Pi_swap_list xl1 xl2 x = x.
 275 #x xl1;nelim xl1
 276 ##[#;@
 277 ##|#x3 xl3 IH xl2' H1;ncases xl2'
 278    ##[#;@
 279    ##|#x4 xl4 H2;ncut (x ∉ xl3 ∧ x ∉ xl4);
 280       ##[@
 281          ##[@;#H3;ncases H1;#H4;napply H4;/2/;
 282          ##|@;#H3;ncases H2;#H4;napply H4;/2/
 283          ##]
 284       ##] *; #H1' H2';
 285       nchange in ⊢ (??%?) with (swap ????);
 286       nrewrite > (swap_other …)
 287       ##[napply IH;//;
 288       ##|nchange in ⊢ (?(???%)) with (Pi_swap_list ???);
 289          nrewrite > (IH …);//;@;#H3;ncases H2;#H4;napply H4;//;
 290       ##|nchange in ⊢ (?(???%)) with (Pi_swap_list ???);
 291          nrewrite > (IH …);//;@;#H3;ncases H1;#H4;napply H4;//
 292       ##]
 293    ##]
 294 ##]
 295 nqed.
 296 *)