source: LTS/utils.ma @ 3586

Last change on this file since 3586 was 3579, checked in by piccolo, 4 years ago
File size: 13.6 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/lists/listb.ma".
16include "../src/utilities/hide.ma".
17include "../src/ASM/Util.ma".
18include "../src/utilities/option.ma".
19
20definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝
21λA,B,f,a,b,x.if x == a then b else f x.
22
23lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
24∀f : A → option B.∀y : B.
25! x ← m; f x = return y →
26∃ x.(m = return x) ∧ (f x = return y).
27#A #B * [| #a] #f #y normalize #EQ [destruct]
28%{a} %{(refl …)} //
29qed.
30
31(*NO DUPLICATES in lists*)
32
33let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
34match l with
35[ nil ⇒ True
36| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
37].
38
39lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
40no_duplicates … l2.
41#A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/
42qed.
43
44lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
45no_duplicates … l1.
46#A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ]
47inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_
48% inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1;
49#EQ destruct(EQ)
50qed.
51
52lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A.
53no_duplicates … (l1 @ l2) →
54no_duplicates … (l2 @ l1).
55#A #l1 elim l1
56[ #l2 >append_nil //]
57#x #xs #IH #l2 * #H1 #H2 lapply(IH … H2) lapply H1 -H1 -IH -H2
58elim l2 -l1
59[ >append_nil #H1 #H2 % // ]
60#y #ys #IH * #H1 * #H2 #H3 %
61[2: @IH
62   [ % #H4 @H1 cases(memb_append … H4)
63     [ #H5 >memb_append_l1 //
64     | #H5 >memb_append_l2 // @orb_Prop_r >H5 //
65     ]
66   | //
67   ]
68| % #H4 cases(memb_append … H4)
69  [ #H5 @(absurd ?? H2) >memb_append_l1 //
70  | whd in match (memb ???); inversion(y==x)
71    [ #H5 #_ <(\P H5) in H1; #H1 @H1 >memb_append_l2 //
72    | #_ normalize nodelta #H5 @(absurd ?? H2) >memb_append_l2 //
73    ]
74  ]
75]
76qed.
77
78lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D.
79x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false.
80#D #l1 elim l1
81[ #l2 #x #_ #H @H ]
82#x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta
83[ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1
84normalize nodelta @IH //
85qed.
86
87lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
88no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
89#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
90inversion (x == x1) normalize nodelta
91[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
92| #_ @IH //
93]
94qed.
95
96(* subset *)
97
98let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝
99match l1 with
100[ nil ⇒ True
101| cons x xs ⇒ mem … x l2 ∧ subset … xs l2
102].
103
104interpretation "subset" 'subseteq a b = (subset ? a b).
105
106lemma subset_append_l2 : ∀A,l2,l1.subset A l2 (l1 @ l2).
107#A #l2 elim l2 // normalize #x #xs #IH #l1 % // @mem_append_l2 whd /2/
108qed.
109
110lemma refl_subset : ∀A.reflexive … (subset A).
111#A #l1 elim l1 // #x #xs #IH normalize % /2/ change with ([?]@xs) in match (x :: xs);
112@subset_append_l2
113qed.
114
115lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2.
116#A #l1 elim l1 // #x #xs #IH #l2 #H %
117[ @memb_to_mem >H // >memb_hd //
118| @IH #y #H1 @H >memb_cons // >H1 //
119]
120qed.
121
122lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3.
123#A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/
124qed.
125
126lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2.
127#A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y *
128[ #EQ destruct // | #H3 @IH // ]
129qed.
130
131lemma transitive_subset : ∀A.transitive … (subset A).
132#A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 %
133[ @(subset_def_inv … H3) // | @IH // ]
134qed.
135
136lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2).
137#A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 // | @IH // ]
138qed.
139
140lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3).
141#A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 %
142[ @mem_append_l2 // | @IH // ]
143qed.
144
145(* some useful deqsets *)
146
147definition DeqUnit ≝ mk_DeqSet unit (λ_.λ_.true) ?.
148@hide_prf ** % // qed.
149
150definition DeqFalse ≝ mk_DeqSet False (λ_.λ_.true) ?.
151@hide_prf * qed.
152
153(* list of elements with decidable equality *)
154
155let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝
156match l1 with
157[ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ]
158| cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ]
159].
160
161lemma eqb_list_elim : ∀P : bool → Prop.
162∀D,l1,l2.(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eqb_list D l1 l2).
163#P #D #l1 lapply P -P elim l1
164[ #P * /2/ #x #xs #H1 #H2 @H2 % #EQ destruct]
165#x #xs #IH #P * /2/ #y #ys #H1 #H2 normalize
166inversion(?==?) #EQ normalize [2: @H2 % #EQ1 destruct >(\b (refl …)) in EQ; #EQ destruct]
167@IH [ #EQ1 destruct @H1 >(\P EQ) % | * #H @H2 % #EQ1 destruct @H %]
168qed.
169
170definition DeqSet_List : DeqSet → DeqSet ≝
171λX.mk_DeqSet (list X) (eqb_list …) ?.
172#x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x
173#x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y)
174#EQ normalize nodelta
175[ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption
176| #EQ destruct
177| #EQ1 destruct @(proj2 … (IH …)) %
178| #EQ1 destruct <EQ @(proj2 … (eqb_true …)) %
179]
180qed.
181
182unification hint  0 ≔ C;
183    X ≟ DeqSet_List C
184(* ---------------------------------------- *) ⊢
185    list C ≡ carr X.
186
187
188unification hint  0 ≔ D,p1,p2;
189    X ≟ DeqSet_List D
190(* ---------------------------------------- *) ⊢
191    eqb_list D p1 p2 ≡ eqb X p1 p2.
192
193lemma mem_list : ∀A : Type[0].
194∀l : list A.∀x : A.mem … x l →
195∃l1,l2.l=l1 @ [x] @ l2.
196#A #l elim l
197[ #x *]
198#x #xs #IH #y *
199[ #EQ destruct %{[]} %{xs} %
200| #H cases(IH … H) #l1 * #l2 #EQ destruct
201  %{(x :: l1)} %{l2} %
202]
203qed.
204
205(* associative list *)
206
207definition associative_list : DeqSet → Type[0] → Type[0] ≝
208λA,B.list (A × (list B)).
209
210let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B)
211   on l : A → list B → associative_list A B ≝
212λa,b.match l with
213    [ nil ⇒ [〈a,b〉]
214    | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs
215                  else x :: (update_list … xs a b) 
216    ].
217
218let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝
219λa.match l with [ nil ⇒ nil ?
220                | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a
221                ].
222
223let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝
224 match l with
225  [ nil ⇒ []
226  | cons x xs ⇒ \fst x :: domain_of_associative_list … xs
227  ].
228
229lemma get_element_append_l:
230 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
231  x ∈ domain_of_associative_list … l1 →
232   get_element … (l1@l2) x = get_element … l1 x.
233#A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd))
234#H [ >(\b H) | >(\bf H) ] normalize /2/
235qed.
236
237lemma get_element_append_r:
238 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
239  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) →
240   get_element ?? (l1@l2) x = get_element … l2 x.
241#A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd))
242#H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I)
243qed.
244
245lemma get_element_append_l1 :
246 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
247  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) →
248   get_element ?? (l1@l2) x = get_element … l1 x.
249#A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ]
250#l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize
251[ * #H @⊥ @H % ] #H @IH assumption
252qed.
253
254lemma get_element_append_r1 :
255 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
256  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) →
257   get_element ?? (l1@l2) x = get_element … l2 x.
258#A #B #l1 elim l1 normalize // #x #xs #IH #l2 #a cases (?==?)
259normalize [* #H cases H //] #H >IH normalize //
260qed.
261
262lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A.
263¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2).
264#A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y)
265normalize [*] @IH
266qed.
267
268lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A.
269¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1).
270#A #x #l1 elim l1
271[ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ]
272#y #ys #IH #l2 #H1 whd in match (memb ???); >IH //
273qed.
274
275lemma foldr_map_append :
276  ∀A,B:Type[0]. ∀l1, l2 : list A.
277   ∀f:A → list B. ∀seed.
278    foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) =
279     append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1)
280       (foldr  ?? (λx,acc. (f x) @ acc) seed l2).
281#A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/
282qed.
283
284lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l).
285//
286qed.
287
288lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B.
289domain_of_associative_list ?? (l1 @ l2) =
290 (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2).
291#A #B #l1 elim l1 // #x #xs #IH #l2 normalize //
292qed.
293
294(*monoids*)
295
296record monoid: Type[1] ≝
297 { carrier :> DeqSet
298 ; op: carrier → carrier → carrier
299 ; e: carrier
300 ; neutral_r : ∀x. op … x e = x
301 ; neutral_l : ∀x. op … e x = x
302 ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
303 }.
304 
305definition is_abelian ≝ λM : monoid.
306∀x,y : M.op … M x y = op … M y x.
307 
308record monoid_action (I : monoid) (M : Type[0]) : Type[0] ≝
309{ act :2> I → M → M
310; act_neutral : ∀x.act (e …) x = x
311; act_op : ∀i,j,x.act (op … i j) x = act j (act i x)
312}.
313
314(* partial order *)
315
316record partial_order (A : Type[0]) : Type[0] ≝
317{ po_rel :2> A → A → Prop
318; refl_po_rel : reflexive … po_rel
319; antisym_po_rel : ∀x,y : A.po_rel … x y → po_rel … y x → x = y
320; trans_po_rel : transitive … po_rel
321}.
322
323(* fold2 *)
324
325let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B)
326(l2 : list C) (f : A → B → C → A) on l1 : option A≝
327match l1 with
328[ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ]
329| cons x xs ⇒
330        match l2 with
331        [ nil ⇒ None ?
332        | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f);
333                      return f ih x y
334        ]
335].
336
337(* dependent map*)
338
339let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝
340(match l return λx.l=x → ? with
341[ nil ⇒ λ_.nil ?
342| cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)
343])(refl …).
344[ >prf %% | >prf %2 assumption]
345qed.
346
347lemma dependent_map_append : ∀A,B,l1,l2,f.
348dependent_map A B (l1 @ l2) (λa,prf.f a prf) =
349(dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).
350[2: @hide_prf /2/ | 3: @hide_prf /2/]
351#A #B #l1 elim l1 normalize /2/
352qed.
353
354lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.
355        ∀EQ:l1 = l2.
356         dependent_map A B l1 (λa,prf.f a prf) =
357         dependent_map A B l2 (λa,prf.f a ?).
358[2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]
359qed.
360
361definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝
362λA,B,l,f,x,prf.f x prf.
363
364lemma proof_irrelevance_temp :  ∀A,B : Type[0].∀l : list A.
365∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
366applica … f x prf1 = applica … f x prf2.
367//
368qed.
369
370lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A.
371∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
372f x prf1 = f x prf2.
373#A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp
374qed.
375
376lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A.
377∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) →
378dependent_map … l f = dependent_map … l g.
379#A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%);
380@eq_f2 // @IH //
381qed.
382
383(* nth_opt*)
384
385lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| > n → nth_opt … n (l1 @ l2) = nth_opt … n l1.
386#A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/
387qed.
388
389lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| ≤ n → nth_opt …  n (l1 @ l2) = nth_opt … (n - |l1|) l2.
390#A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/
391qed.
392
393(* All2 *)
394
395let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
396match l1 with
397[ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False]
398| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
399].
Note: See TracBrowser for help on using the repository browser.