X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbinding%2Ffp.ma;fp=matita%2Fmatita%2Flib%2Fbinding%2Ffp.ma;h=0000000000000000000000000000000000000000;hb=600fba840c748f67593838673a6eb40eab9b68e5;hp=14ba2f77495e70971b8cb79ef9c20862e103e6f0;hpb=b4f76b0d8fa0e5365fb48e91474febe200b647a7;p=helm.git

diff --git a/matita/matita/lib/binding/fp.ma b/matita/matita/lib/binding/fp.ma
deleted file mode 100644
index 14ba2f774..000000000
--- a/matita/matita/lib/binding/fp.ma
+++ /dev/null
@@ -1,296 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "binding/names.ma".
-
-(* permutations *)
-definition finite_perm : ∀X:Nset.(X → X) → Prop ≝ 
- λX,f.injective X X f ∧ surjective X X f ∧ ∃l.∀x.x ∉ l → f x = x.
-
-(* maps a permutation to a list of parameters *)
-definition Pi_list : ∀X:Nset.(X → X) → list X → list X ≝ 
- λX,p,xl.map ?? (λx.p x) xl.
-
-interpretation "permutation of X list" 'middot p x = (Pi_list p x).
-
-definition swap : ∀N:Nset.N → N → N → N ≝
-  λN,u,v,x.match (x == u) with
-    [true ⇒ v
-    |false ⇒ match (x == v) with
-       [true ⇒ u
-       |false ⇒ x]].
-       
-axiom swap_right : ∀N,x,y.swap N x y y = x.
-(*
-#N x y;nnormalize;nrewrite > (p_eqb3 ? y y …);//;
-nlapply (refl ? (y ≟ x));ncases (y ≟ x) in ⊢ (???% → %);nnormalize;//;
-#H1;napply p_eqb1;//;
-nqed.
-*)
-
-axiom swap_left : ∀N,x,y.swap N x y x = y.
-(*
-#N x y;nnormalize;nrewrite > (p_eqb3 ? x x …);//;
-nqed.
-*)
-
-axiom swap_other : ∀N,x,y,z.x ≠ z → y ≠ z → swap N x y z = z.
-(*
-#N x y z H1 H2;nnormalize;nrewrite > (p_eqb4 …);
-##[nrewrite > (p_eqb4 …);//;@;ncases H2;/2/;
-##|@;ncases H1;/2/
-##]
-nqed.
-*)
-
-axiom swap_inv : ∀N,x,y,z.swap N x y (swap N x y z) = z.
-(*
-#N x y z;nlapply (refl ? (x ≟ z));ncases (x ≟ z) in ⊢ (???% → ?);#H1
-##[nrewrite > (p_eqb1 … H1);nrewrite > (swap_left …);//;
-##|nlapply (refl ? (y ≟ z));ncases (y ≟ z) in ⊢ (???% → ?);#H2
-   ##[nrewrite > (p_eqb1 … H2);nrewrite > (swap_right …);//;
-   ##|nrewrite > (swap_other …) in ⊢ (??(????%)?);/2/;
-      nrewrite > (swap_other …);/2/;
-   ##]
-##]
-nqed.
-*)
-
-axiom swap_fp : ∀N,x1,x2.finite_perm ? (swap N x1 x2).
-(*
-#N x1 x2;@
-##[@
-   ##[nwhd;#xa xb;nnormalize;nlapply (refl ? (xa ≟ x1));
-      ncases (xa ≟ x1) in ⊢ (???% → %);#H1
-      ##[nrewrite > (p_eqb1 … H1);nlapply (refl ? (xb ≟ x1));
-         ncases (xb ≟ x1) in ⊢ (???% → %);#H2
-         ##[nrewrite > (p_eqb1 … H2);//
-         ##|nlapply (refl ? (xb ≟ x2));
-            ncases (xb ≟ x2) in ⊢ (???% → %);#H3
-            ##[nnormalize;#H4;nrewrite > H4 in H3;
-               #H3;nrewrite > H3 in H2;#H2;ndestruct (H2)
-            ##|nnormalize;#H4;nrewrite > H4 in H3;
-               nrewrite > (p_eqb3 …);//;#H5;ndestruct (H5)
-            ##]
-         ##]
-      ##|nlapply (refl ? (xa ≟ x2));
-         ncases (xa ≟ x2) in ⊢ (???% → %);#H2
-         ##[nrewrite > (p_eqb1 … H2);nlapply (refl ? (xb ≟ x1));
-            ncases (xb ≟ x1) in ⊢ (???% → %);#H3
-            ##[nnormalize;#H4;nrewrite > H4 in H3;
-               #H3;nrewrite > (p_eqb1 … H3);@
-            ##|nnormalize;nlapply (refl ? (xb ≟ x2));
-               ncases (xb ≟ x2) in ⊢ (???% → %);#H4
-               ##[nrewrite > (p_eqb1 … H4);//
-               ##|nnormalize;#H5;nrewrite > H5 in H3;
-                  nrewrite > (p_eqb3 …);//;#H6;ndestruct (H6);
-               ##]
-            ##]
-         ##|nnormalize;nlapply (refl ? (xb ≟ x1));
-            ncases (xb ≟ x1) in ⊢ (???% → %);#H3
-            ##[nnormalize;#H4;nrewrite > H4 in H2;nrewrite > (p_eqb3 …);//;
-               #H5;ndestruct (H5)
-            ##|nlapply (refl ? (xb ≟ x2));
-               ncases (xb ≟ x2) in ⊢ (???% → %);#H4
-               ##[nnormalize;#H5;nrewrite > H5 in H1;nrewrite > (p_eqb3 …);//;
-                  #H6;ndestruct (H6)
-               ##|nnormalize;//
-               ##]
-            ##]
-         ##]
-      ##]
-   ##|nwhd;#z;nnormalize;nlapply (refl ? (z ≟ x1));
-      ncases (z ≟ x1) in ⊢ (???% → %);#H1
-      ##[nlapply (refl ? (z ≟ x2));
-         ncases (z ≟ x2) in ⊢ (???% → %);#H2
-         ##[@ z;nrewrite > H1;nrewrite > H2;napply p_eqb1;//
-         ##|@ x2;nrewrite > (p_eqb4 …);
-            ##[nrewrite > (p_eqb3 …);//;
-               nnormalize;napply p_eqb1;//
-            ##|nrewrite < (p_eqb1 … H1);@;#H3;nrewrite > H3 in H2;
-               nrewrite > (p_eqb3 …);//;#H2;ndestruct (H2)
-            ##]
-         ##]
-      ##|nlapply (refl ? (z ≟ x2));
-         ncases (z ≟ x2) in ⊢ (???% → %);#H2
-         ##[@ x1;nrewrite > (p_eqb3 …);//;
-            napply p_eqb1;nnormalize;//
-         ##|@ z;nrewrite > H1;nrewrite > H2;@;
-         ##]
-      ##]
-   ##]
-##|@ [x1;x2];#x0 H1;nrewrite > (swap_other …)
-   ##[@
-   ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;/2/;
-   ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;//;
-   ##]
-##]
-nqed.
-*)
-
-axiom inj_swap : ∀N,u,v.injective ?? (swap N u v).
-(*
-#N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
-nqed.
-*)
-
-axiom surj_swap : ∀N,u,v.surjective ?? (swap N u v).
-(*
-#N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
-nqed.
-*)
-
-axiom finite_swap : ∀N,u,v.∃l.∀x.x ∉ l → swap N u v x = x.
-(*
-#N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
-nqed.
-*)
-
-(* swaps two lists of parameters 
-definition Pi_swap_list : ∀xl,xl':list X.X → X ≝ 
- λxl,xl',x.foldr2 ??? (λu,v,r.swap ? u v r) x xl xl'.
-
-nlemma fp_swap_list : 
-  ∀xl,xl'.finite_perm ? (Pi_swap_list xl xl').
-#xl xl';@
-##[@;
-   ##[ngeneralize in match xl';nelim xl
-      ##[nnormalize;//;
-      ##|#x0 xl0;#IH xl'';nelim xl''
-         ##[nnormalize;//
-         ##|#x1 xl1 IH1 y0 y1;nchange in ⊢ (??%% → ?) with (swap ????);
-            #H1;nlapply (inj_swap … H1);#H2;
-            nlapply (IH … H2);//
-         ##]
-      ##]
-   ##|ngeneralize in match xl';nelim xl
-      ##[nnormalize;#_;#z;@z;@
-      ##|#x' xl0 IH xl'';nelim xl''
-         ##[nnormalize;#z;@z;@
-         ##|#x1 xl1 IH1 z;
-            nchange in ⊢ (??(λ_.???%)) with (swap ????);
-            ncases (surj_swap X x' x1 z);#x2 H1;
-            ncases (IH xl1 x2);#x3 H2;@ x3;
-            nrewrite < H2;napply H1
-         ##]
-      ##]
-   ##]
-##|ngeneralize in match xl';nelim xl
-   ##[#;@ [];#;@
-   ##|#x0 xl0 IH xl'';ncases xl''
-      ##[@ [];#;@
-      ##|#x1 xl1;ncases (IH xl1);#xl2 H1;
-         ncases (finite_swap X x0 x1);#xl3 H2;
-         @ (xl2@xl3);#x2 H3;
-         nchange in ⊢ (??%?) with (swap ????);
-         nrewrite > (H1 …);
-         ##[nrewrite > (H2 …);//;@;#H4;ncases H3;#H5;napply H5;
-            napply in_list_to_in_list_append_r;//
-         ##|@;#H4;ncases H3;#H5;napply H5;
-            napply in_list_to_in_list_append_l;//
-         ##]
-      ##]
-   ##]
-##]
-nqed.
-
-(* the 'reverse' swap of lists of parameters 
-   composing Pi_swap_list and Pi_swap_list_r yields the identity function
-   (see the Pi_swap_list_inv lemma) *)
-ndefinition Pi_swap_list_r : ∀xl,xl':list X. Pi ≝ 
- λxl,xl',x.foldl2 ??? (λr,u,v.swap ? u v r ) x xl xl'.
-
-nlemma fp_swap_list_r : 
-  ∀xl,xl'.finite_perm ? (Pi_swap_list_r xl xl').
-#xl xl';@
-##[@;
-   ##[ngeneralize in match xl';nelim xl
-      ##[nnormalize;//;
-      ##|#x0 xl0;#IH xl'';nelim xl''
-         ##[nnormalize;//
-         ##|#x1 xl1 IH1 y0 y1;nwhd in ⊢ (??%% → ?);
-            #H1;nlapply (IH … H1);#H2;
-            napply (inj_swap … H2);
-         ##]
-      ##]
-   ##|ngeneralize in match xl';nelim xl
-      ##[nnormalize;#_;#z;@z;@
-      ##|#x' xl0 IH xl'';nelim xl''
-         ##[nnormalize;#z;@z;@
-         ##|#x1 xl1 IH1 z;nwhd in ⊢ (??(λ_.???%));
-            ncases (IH xl1 z);#x2 H1;
-            ncases (surj_swap X x' x1 x2);#x3 H2;
-            @ x3;nrewrite < H2;napply H1;
-         ##]
-      ##]
-   ##]
-##|ngeneralize in match xl';nelim xl
-   ##[#;@ [];#;@
-   ##|#x0 xl0 IH xl'';ncases xl''
-      ##[@ [];#;@
-      ##|#x1 xl1;
-         ncases (IH xl1);#xl2 H1;
-         ncases (finite_swap X x0 x1);#xl3 H2;
-         @ (xl2@xl3);#x2 H3;nwhd in ⊢ (??%?);
-         nrewrite > (H2 …);
-         ##[nrewrite > (H1 …);//;@;#H4;ncases H3;#H5;napply H5;
-            napply in_list_to_in_list_append_l;//
-         ##|@;#H4;ncases H3;#H5;napply H5;
-            napply in_list_to_in_list_append_r;//
-         ##]
-      ##]
-   ##]
-##]
-nqed.
-
-nlemma Pi_swap_list_inv :
- ∀xl1,xl2,x.
- Pi_swap_list xl1 xl2 (Pi_swap_list_r xl1 xl2 x) = x.
-#xl;nelim xl
-##[#;@
-##|#x1 xl1 IH xl';ncases xl'
-   ##[#;@
-   ##|#x2 xl2;#x;
-      nchange in ⊢ (??%?) with 
-        (swap ??? (Pi_swap_list ?? 
-                  (Pi_swap_list_r ?? (swap ????))));
-      nrewrite > (IH xl2 ?);napply swap_inv;
-   ##]
-##]
-nqed.
-
-nlemma Pi_swap_list_fresh :
-  ∀x,xl1,xl2.x ∉ xl1 → x ∉ xl2 → Pi_swap_list xl1 xl2 x = x.
-#x xl1;nelim xl1
-##[#;@
-##|#x3 xl3 IH xl2' H1;ncases xl2'
-   ##[#;@
-   ##|#x4 xl4 H2;ncut (x ∉ xl3 ∧ x ∉ xl4);
-      ##[@
-         ##[@;#H3;ncases H1;#H4;napply H4;/2/;
-         ##|@;#H3;ncases H2;#H4;napply H4;/2/
-         ##]
-      ##] *; #H1' H2';
-      nchange in ⊢ (??%?) with (swap ????);
-      nrewrite > (swap_other …)
-      ##[napply IH;//;
-      ##|nchange in ⊢ (?(???%)) with (Pi_swap_list ???);
-         nrewrite > (IH …);//;@;#H3;ncases H2;#H4;napply H4;//;
-      ##|nchange in ⊢ (?(???%)) with (Pi_swap_list ???);
-         nrewrite > (IH …);//;@;#H3;ncases H1;#H4;napply H4;//
-      ##]
-   ##]
-##]
-nqed.
-*)
\ No newline at end of file