(**************************************************************************)
(*       ___                                                              *)
(*      ||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.