source: LTS/Permutation.ma @ 3586

Last change on this file since 3586 was 3552, checked in by piccolo, 5 years ago

closed all daemons

File size: 10.5 KB
Line 
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
15include "basics/deqsets.ma".
16include "arithmetics/nat.ma".
17include "utils.ma".
18
19record multiset (A : DeqSet) : Type[0] ≝
20{ mult : (A → ℕ) }.
21 
22definition m_eq : ∀A.multiset A → multiset A → Prop ≝
23λA,m1,m2.∀a.mult … m1 a = mult … m2 a.
24
25lemma m_eq_reflexive : ∀A.reflexive … (m_eq A).
26//
27qed.
28
29lemma m_eq_symmetric : ∀A.symmetric … (m_eq A).
30//
31qed.
32
33lemma m_eq_transitive : ∀A.transitive … (m_eq A).
34//
35qed.
36
37definition empty_multiset : ∀A.multiset A ≝ λA.mk_multiset … (λ_.O).
38definition singleton : ∀A : DeqSet.A → multiset A ≝ λA,a.mk_multiset … (λx.if x == a then 1 else O).
39definition multiset_union : ∀A.multiset A → multiset A → multiset A ≝
40λA,m1,m2.mk_multiset … (λx.mult … m1 x + mult … m2 x).
41
42notation "hvbox(C break  ⊔ A)" left associative with precedence 55 for @{ 'm_un $C $A }.
43interpretation "m_union" 'm_un x y = (multiset_union ? x y).
44
45notation > "hvbox(C break ⩬ A)" non associative with precedence 45 for @{'m_eq $C $A}.
46interpretation "m_eq" 'm_eq x y = (m_eq ? x y).
47
48notation "ⓧ" with precedence 90 for @{'empty_m}.
49interpretation "empty_mult" 'empty_m = (empty_multiset ?).
50
51notation "❨ term 19 C ❩ " with precedence 10 for @{ 'sing $C}.
52interpretation "singleton_m" 'sing x = (singleton ? x).
53
54lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union ? m1 m2) ⩬ (multiset_union ? m2 m1).
55normalize //
56qed.
57
58lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ⩬ m1 ⊔ (m2 ⊔ m3).
59normalize //
60qed.
61
62lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ⩬ m.
63normalize //
64qed.
65
66lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ⩬ m.
67normalize //
68qed.
69
70include "basics/lists/list.ma".
71
72let rec list_to_multiset (A : DeqSet) (l : list A) on l : multiset A ≝
73match l with
74[ nil ⇒ ⓧ
75| cons x xs ⇒ ❨ x ❩ ⊔ list_to_multiset … xs
76].
77
78lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A.
79m1 ⩬ m2 → m ⊔ m1 ⩬ m ⊔ m2.
80#A #m #m1 #m2 normalize //
81qed.
82
83lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ⩬ m ⊔ m2 → m1 ⩬ m2.
84normalize #A #m #m1 #m2 #H #a /2/
85qed.
86
87lemma list_to_multiset_append : ∀A.∀l1,l2.
88list_to_multiset A (l1 @ l2) ⩬ list_to_multiset … l1 ⊔ list_to_multiset … l2.
89#A #l1 elim l1
90[ normalize //]
91#x #xs #IH #l2 change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (??%?);
92change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (???(??%?));
93whd in match (list_to_multiset ??); @m_eq_symmetric
94@(m_eq_transitive … (m_union_associative …))
95@m_eq_union_left_cancellable @m_eq_symmetric @IH
96qed.
97
98lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
99∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
100#A #l elim l [ #x *] #x #xs #IH #y *
101[ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
102| #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
103]
104qed.
105
106lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
107∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
108#A #l elim l [ #x * #H cases H % ]
109#x #xs #IH #y normalize inversion(y==x) normalize nodelta
110#H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
111qed.
112
113definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝
114λA,l1,l2.list_to_multiset … l1 ⩬ list_to_multiset … l2.
115
116lemma is_permutation_mem : ∀A :DeqSet.
117∀l1,l2 : list A.∀x : A.mem … x l1 →
118is_permutation A l1 l2 → mem … x l2.
119#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
120qed.
121
122lemma is_permutation_eq : ∀A : DeqSet.∀l : list A.is_permutation … l l.
123//
124qed.
125
126lemma is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 →
127                                       is_permutation A (x :: l1) (x :: l2).
128normalize //
129qed.
130
131lemma permute_append_all : ∀A.∀l1,l2,l3,l4.is_permutation A (l1@l2) (l3@l4) →
132is_permutation A (l2 @l1) (l4@l3).
133#A #l1 #l2 #l3 #l4 normalize #H #a >(list_to_multiset_append … a)
134>(list_to_multiset_append … a) >m_union_commutative
135>m_union_commutative in ⊢ (???%); <list_to_multiset_append <list_to_multiset_append @H
136qed.
137
138lemma permute_append_l1 : ∀A.∀l1,l2,l3.is_permutation A l1 (l2 @ l3) →
139is_permutation A l1 (l3 @ l2).
140#A #l1 #l2 #l3 #H #a >list_to_multiset_append >m_union_commutative <list_to_multiset_append @H
141qed.
142
143lemma is_permutation_commutative : ∀A.symmetric … (is_permutation A).
144//
145qed.
146
147lemma is_permutation_transitive : ∀A.transitive … (is_permutation A).
148//
149qed.
150
151lemma is_permutation_append_left_cancellable : ∀A.∀l,l1,l2.is_permutation A l1 l2 →
152is_permutation A (l @ l1) (l @ l2).
153#A #l #l1 #l2 #H #a >list_to_multiset_append >list_to_multiset_append
154@m_eq_union_left_cancellable @H
155qed.
156
157lemma is_permutation_append : ∀A.∀l1,l2,l3,l4.
158is_permutation A l1 l2 → is_permutation A l3 l4 →
159is_permutation A (l1 @ l3) (l2 @ l4).
160#A  #l1 #l2 #l3 #l4 #H1 #H2 #a >list_to_multiset_append
161>list_to_multiset_append normalize >H1 >H2 %
162qed.
163
164lemma permute_equal_right : ∀A.∀l1,l2,l.
165is_permutation A (l1 @ l) (l2 @ l) → is_permutation A l1 l2.
166#A #l1 #l2 #l normalize #H #a lapply(H a) >list_to_multiset_append >list_to_multiset_append
167>m_union_commutative >m_union_commutative in ⊢ (???% → ?);
168normalize //
169qed.
170
171lemma permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y.
172  (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7)
173 →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9)
174 →is_permutation A
175   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
176   (((x ::l4 @y ::l3) @l8) @l9)).
177#A #l1 #l2 #l3 #l4 #l5 #l6 #l7 #l8 #l9 #x #y
178change with ([x] @ ?) in match ([x] @ ?);
179change with ([y] @ ?) in match ([y] @ ?);
180>append_nil #H1 #H2 whd in match (append ???) in ⊢ (???%);
181change with ([x] @ ?) in match ([x] @ ?) in ⊢ (???%);
182change with ([y] @ ?) in match ([y] @ ?) in ⊢ (???%);
183@permute_append_l1 >associative_append in ⊢ (???%);
184<associative_append in ⊢ (???%); <associative_append in ⊢ (???%);
185<associative_append <associative_append <associative_append
186@(is_permutation_transitive … ((((([y]@l4)@l3)@l8)@l9)@[x]))
187[ >associative_append >associative_append >associative_append
188  >associative_append >associative_append >associative_append
189  >associative_append >associative_append >associative_append
190  @is_permutation_append_left_cancellable
191  <associative_append in ⊢ (???%); <associative_append in ⊢ (???%); <associative_append in ⊢ (???%);
192  @permute_append_l1
193  @(is_permutation_transitive … ([x]@l6@l5@l1@l2@l7))
194  [2: @is_permutation_append_left_cancellable
195      @(is_permutation_transitive … ((l5 @ l1) @ ((l6@l2)@l7)))
196      [2: >associative_append in ⊢ (???%); >associative_append in ⊢ (???%);
197         @is_permutation_append
198         [2: <associative_append in ⊢ (???%); assumption
199         | >associative_append in H1 : (??%?); #H1 @permute_equal_right
200           [ @(l6@l7) | >associative_append assumption ]
201         ]
202      | <associative_append in ⊢ (??(???%)?); @is_permutation_commutative
203        @permute_append_l1 >associative_append in ⊢ (???%); @is_permutation_append_left_cancellable
204        >associative_append @permute_append_l1 //
205      ]
206  | <associative_append <associative_append <associative_append in ⊢ (???%);
207    <associative_append in ⊢ (???%); @permute_append_all @is_permutation_append_left_cancellable
208    @permute_append_all @is_permutation_append_left_cancellable @permute_append_l1 //
209  ]
210| @permute_append_all @is_permutation_append_left_cancellable @permute_append_all
211  @is_permutation_append_left_cancellable @permute_append_all
212  @is_permutation_append_left_cancellable @permute_append_all
213  @is_permutation_append_left_cancellable @permute_append_l1 //
214]
215qed.
216
217lemma is_permutation_case : ∀A : DeqSet.
218∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l →
219∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
220#A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
221#l1 * #l2 #EQ destruct %{l1} %{l2} % //
222@(permute_equal_right … [x]) @permute_append_all
223@(is_permutation_transitive … H)
224/4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
225qed.
226
227lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
228∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
229∀perm : is_permutation A l1 l2.
230(∀a : A.
231 ∀prf : mem … a l1.f a prf = g a ?) →
232is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
233[2: @(is_permutation_mem … perm) //]
234#A #B #l1 elim l1 -l1
235[ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
236#x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
237>dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
238whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
239whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
240generalize in ⊢ (? → ???(??(??%)?));
241#prf1 #prf2
242>(proof_irrelevance_all … g x prf1 prf2)
243@is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
244whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
245@(is_permutation_transitive …(IH … (l3@l4) …) )
246[2: assumption
247|3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
248| @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
249]
250>dependent_map_append @is_permutation_append
251[ >dependent_map_extensional [ @is_permutation_eq | // |]
252| >dependent_map_extensional [ @is_permutation_eq | // |]
253]
254qed.
Note: See TracBrowser for help on using the repository browser.