1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "binding/names.ma".
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.
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.
25 interpretation "permutation of X list" 'middot p x = (Pi_list p x).
27 definition swap : ∀N:Nset.N → N → N → N ≝
28 λN,u,v,x.match (x == u) with
30 |false ⇒ match (x == v) with
34 axiom swap_right : ∀N,x,y.swap N x y y = x.
36 #N x y;nnormalize;nrewrite > (p_eqb3 ? y y …);//;
37 nlapply (refl ? (y ≟ x));ncases (y ≟ x) in ⊢ (???% → %);nnormalize;//;
42 axiom swap_left : ∀N,x,y.swap N x y x = y.
44 #N x y;nnormalize;nrewrite > (p_eqb3 ? x x …);//;
48 axiom swap_other : ∀N,x,y,z.x ≠ z → y ≠ z → swap N x y z = z.
50 #N x y z H1 H2;nnormalize;nrewrite > (p_eqb4 …);
51 ##[nrewrite > (p_eqb4 …);//;@;ncases H2;/2/;
57 axiom swap_inv : ∀N,x,y,z.swap N x y (swap N x y z) = z.
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/;
70 axiom swap_fp : ∀N,x1,x2.finite_perm ? (swap N x1 x2).
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)
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);
100 ##|nnormalize;nlapply (refl ? (xb ≟ x1));
101 ncases (xb ≟ x1) in ⊢ (???% → %);#H3
102 ##[nnormalize;#H4;nrewrite > H4 in H2;nrewrite > (p_eqb3 …);//;
104 ##|nlapply (refl ? (xb ≟ x2));
105 ncases (xb ≟ x2) in ⊢ (???% → %);#H4
106 ##[nnormalize;#H5;nrewrite > H5 in H1;nrewrite > (p_eqb3 …);//;
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)
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;@;
133 ##|@ [x1;x2];#x0 H1;nrewrite > (swap_other …)
135 ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;/2/;
136 ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;//;
142 axiom inj_swap : ∀N,u,v.injective ?? (swap N u v).
144 #N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
148 axiom surj_swap : ∀N,u,v.surjective ?? (swap N u v).
150 #N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
154 axiom finite_swap : ∀N,u,v.∃l.∀x.x ∉ l → swap N u v x = x.
156 #N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
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'.
164 nlemma fp_swap_list :
165 ∀xl,xl'.finite_perm ? (Pi_swap_list xl xl').
168 ##[ngeneralize in match xl';nelim xl
170 ##|#x0 xl0;#IH xl'';nelim xl''
172 ##|#x1 xl1 IH1 y0 y1;nchange in ⊢ (??%% → ?) with (swap ????);
173 #H1;nlapply (inj_swap … H1);#H2;
177 ##|ngeneralize in match xl';nelim xl
178 ##[nnormalize;#_;#z;@z;@
179 ##|#x' xl0 IH xl'';nelim xl''
180 ##[nnormalize;#z;@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
189 ##|ngeneralize in match xl';nelim xl
191 ##|#x0 xl0 IH xl'';ncases xl''
193 ##|#x1 xl1;ncases (IH xl1);#xl2 H1;
194 ncases (finite_swap X x0 x1);#xl3 H2;
196 nchange in ⊢ (??%?) with (swap ????);
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;//
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'.
214 nlemma fp_swap_list_r :
215 ∀xl,xl'.finite_perm ? (Pi_swap_list_r xl xl').
218 ##[ngeneralize in match xl';nelim xl
220 ##|#x0 xl0;#IH xl'';nelim xl''
222 ##|#x1 xl1 IH1 y0 y1;nwhd in ⊢ (??%% → ?);
223 #H1;nlapply (IH … H1);#H2;
224 napply (inj_swap … H2);
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;
238 ##|ngeneralize in match xl';nelim xl
240 ##|#x0 xl0 IH xl'';ncases xl''
243 ncases (IH xl1);#xl2 H1;
244 ncases (finite_swap X x0 x1);#xl3 H2;
245 @ (xl2@xl3);#x2 H3;nwhd in ⊢ (??%?);
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;//
257 nlemma Pi_swap_list_inv :
259 Pi_swap_list xl1 xl2 (Pi_swap_list_r xl1 xl2 x) = x.
262 ##|#x1 xl1 IH xl';ncases xl'
265 nchange in ⊢ (??%?) with
266 (swap ??? (Pi_swap_list ??
267 (Pi_swap_list_r ?? (swap ????))));
268 nrewrite > (IH xl2 ?);napply swap_inv;
273 nlemma Pi_swap_list_fresh :
274 ∀x,xl1,xl2.x ∉ xl1 → x ∉ xl2 → Pi_swap_list xl1 xl2 x = x.
277 ##|#x3 xl3 IH xl2' H1;ncases xl2'
279 ##|#x4 xl4 H2;ncut (x ∉ xl3 ∧ x ∉ xl4);
281 ##[@;#H3;ncases H1;#H4;napply H4;/2/;
282 ##|@;#H3;ncases H2;#H4;napply H4;/2/
285 nchange in ⊢ (??%?) with (swap ????);
286 nrewrite > (swap_other …)
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;//