+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
projects / helm.git / blobdiff