| 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 | |
|---|
| 15 | include "joint/Joint.ma". |
|---|
| 16 | |
|---|
| 17 | lemma list_map_opt_All2 : ∀A,A',B,B',P,Q,f,g,l1,l2. |
|---|
| 18 | (∀x,y.P x y → |
|---|
| 19 | match f x with [ Some x' ⇒ match g y with [ Some y' ⇒ Q x' y' | None ⇒ False ] |
|---|
| 20 | | None ⇒ match g y with [ Some _ ⇒ False | None ⇒ True ] |
|---|
| 21 | ]) → |
|---|
| 22 | All2 A B P l1 l2 → |
|---|
| 23 | All2 A' B' Q (list_map_opt A A' f l1) (list_map_opt B B' g l2). |
|---|
| 24 | #A #A' #B #B' #P #Q #f #g #l1 #l2 #H lapply l2 -l2 elim l1 -l1 |
|---|
| 25 | [ * [2: #hd #tl * ] #_ % ] |
|---|
| 26 | #hd #tl #IH * [*] #hd' #tl' * #H1 #H2 |
|---|
| 27 | lapply (H … H1) |
|---|
| 28 | whd in match (list_map_opt A ???); |
|---|
| 29 | whd in match (list_map_opt B ???); |
|---|
| 30 | cases (f hd) [2: #y] normalize nodelta |
|---|
| 31 | cases (g hd') [2,4: #y'] normalize nodelta try * |
|---|
| 32 | [ #H1' %{H1'} ] @IH assumption |
|---|
| 33 | qed. |
|---|
| 34 | |
|---|
| 35 | lemma All2_of_map : ∀A,B,P,f,l.(∀x.P x (f x)) → All2 A B P l (map A B f l). |
|---|
| 36 | #A #B #P #f #l #H elim l -l [%] #hd #tl #IH %{IH} @H qed. |
|---|
| 37 | |
|---|
| 38 | definition stack_cost_model_le : relation stack_cost_model ≝ |
|---|
| 39 | All2 … (λx,y.\fst x = \fst y ∧ le (\snd x) (\snd y)). |
|---|
| 40 | |
|---|
| 41 | lemma transitive_All2 : ∀A.∀R : relation A.transitive … R → transitive … (All2 … R). |
|---|
| 42 | #A #R #trans #l1 elim l1 -l1 |
|---|
| 43 | [2: #hd1 #tl1 #IH] * [2,4: #hd2 #tl2 ] #l3 * [ #H1 #G1 ] |
|---|
| 44 | cases l3 -l3 [2,4: #hd3 #tl3 ] * [ #H2 #G2 ] % |
|---|
| 45 | [ @(trans … H1 H2) | @(IH … G1 G2) ] |
|---|
| 46 | qed. |
|---|
| 47 | |
|---|
| 48 | lemma transitive_stack_cost_model_le : transitive … stack_cost_model_le ≝ |
|---|
| 49 | transitive_All2 …. |
|---|
| 50 | * #id1 #n1 * #id2 #n2 * #id3 #n3 ** #H1 ** #H2 % [%] @(transitive_le … H1 H2) |
|---|
| 51 | qed. |
|---|
