(**************************************************************************) (* ___ *) (* ||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 "joint/Joint.ma". lemma list_map_opt_All2 : ∀A,A',B,B',P,Q,f,g,l1,l2. (∀x,y.P x y → match f x with [ Some x' ⇒ match g y with [ Some y' ⇒ Q x' y' | None ⇒ False ] | None ⇒ match g y with [ Some _ ⇒ False | None ⇒ True ] ]) → All2 A B P l1 l2 → All2 A' B' Q (list_map_opt A A' f l1) (list_map_opt B B' g l2). #A #A' #B #B' #P #Q #f #g #l1 #l2 #H lapply l2 -l2 elim l1 -l1 [ * [2: #hd #tl * ] #_ % ] #hd #tl #IH * [*] #hd' #tl' * #H1 #H2 lapply (H … H1) whd in match (list_map_opt A ???); whd in match (list_map_opt B ???); cases (f hd) [2: #y] normalize nodelta cases (g hd') [2,4: #y'] normalize nodelta try * [ #H1' %{H1'} ] @IH assumption qed. lemma All2_of_map : ∀A,B,P,f,l.(∀x.P x (f x)) → All2 A B P l (map A B f l). #A #B #P #f #l #H elim l -l [%] #hd #tl #IH %{IH} @H qed. definition stack_cost_model_le : relation stack_cost_model ≝ All2 … (λx,y.\fst x = \fst y ∧ le (\snd x) (\snd y)). lemma transitive_All2 : ∀A.∀R : relation A.transitive … R → transitive … (All2 … R). #A #R #trans #l1 elim l1 -l1 [2: #hd1 #tl1 #IH] * [2,4: #hd2 #tl2 ] #l3 * [ #H1 #G1 ] cases l3 -l3 [2,4: #hd3 #tl3 ] * [ #H2 #G2 ] % [ @(trans … H1 H2) | @(IH … G1 G2) ] qed. lemma transitive_stack_cost_model_le : transitive … stack_cost_model_le ≝ transitive_All2 …. * #id1 #n1 * #id2 #n2 * #id3 #n3 ** #H1 ** #H2 % [%] @(transitive_le … H1 H2) qed.