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

diff --git a/matita/matita/broken_lib/binding/fp.ma b/matita/matita/broken_lib/binding/fp.ma
new file mode 100644
index 000000000..14ba2f774
--- /dev/null
+++ b/matita/matita/broken_lib/binding/fp.ma
@@ -0,0 +1,296 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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