source: src/joint/joint_stacksizes.ma @ 3145

Last change on this file since 3145 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 2.4 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 "joint/Joint.ma".
16
17lemma 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                 ]) →
22All2 A B P l1 l2 →
23All2 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
27lapply (H … H1)
28whd in match (list_map_opt A ???);
29whd in match (list_map_opt B ???);
30cases (f hd) [2: #y] normalize nodelta
31cases (g hd') [2,4: #y'] normalize nodelta try *
32[ #H1' %{H1'} ] @IH assumption
33qed.
34
35lemma 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
38definition stack_cost_model_le : relation stack_cost_model ≝
39All2 … (λx,y.\fst x = \fst y ∧ le (\snd x) (\snd y)).
40
41lemma 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 ]
44cases l3 -l3 [2,4: #hd3 #tl3 ] * [ #H2 #G2 ] %
45[ @(trans … H1 H2) | @(IH … G1 G2) ]
46qed.
47
48lemma transitive_stack_cost_model_le : transitive … stack_cost_model_le ≝
49transitive_All2 ….
50* #id1 #n1 * #id2 #n2 * #id3 #n3 ** #H1 ** #H2 % [%] @(transitive_le … H1 H2)
51qed.
Note: See TracBrowser for help on using the repository browser.