source: src/Clight/labelSimulation.ma @ 1888

Last change on this file since 1888 was 1888, checked in by campbell, 10 years ago

Show that labelling of expressions works ...
after fixing it to match the prototype.

File size: 8.4 KB
Line 
1
2include "Clight/label.ma".
3include "Clight/Cexec.ma".
4
5(* for the induction principle *)
6include "Clight/CexecSound.ma".
7
8lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D.
9  \fst (let 〈x,y〉 ≝ e in F x y) =  let 〈x,y〉 ≝ e in \fst (F x y).
10#A #B #C #D * //
11qed.
12
13lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
14  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
15#A #B #C #D * //
16qed.
17
18lemma label_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
19  (∀u'. P (F (\fst (label_expr e u)) u')) →
20  P (let 〈e',u'〉 ≝ label_expr e u in F e' u').
21#e #u #T #F #P
22cases (label_expr e u)
23#e' #u' #H @H
24qed.
25
26lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
27  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
28  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
29#e #u #T #F #P #H whd in match (add_cost_expr ??);
30cases (fresh ??) #l #u' @H
31qed.
32
33
34
35lemma label_expr_type : ∀e,u.
36  typeof (\fst (label_expr e u)) = typeof e.
37* #e #ty #u >shift_fst //
38qed.
39
40lemma label_expr_ok : ∀ge,en,m,e,v,tr.
41  exec_expr ge en m e = OK … 〈v,tr〉 →
42  ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉.
43#ge #en #m #e
44@(expr_lvalue_ind ?
45  (λe,ty. ∀b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
46          ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉) … e)
47[ 1,2: normalize /2/
48| * //
49 [ normalize /2 by ex_intro/
50 | #e1 #ty #IH #v #tr #EX #u
51   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
52   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
53   normalize in EXrem; destruct
54   cases (IH … EX1 u) #tr1' #EX1'
55   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (??%?); >EX1'
56   whd in ⊢ (??%?); >EXl @refl
57 | #e1 #id #ty #IH #v #tr #EX #u
58   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
59   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
60   normalize in EXrem; destruct
61   cases (IH … EX1 u) #tr1' #EX1'
62   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (??%?); >EX1'
63   whd in ⊢ (??%?); >EXl @refl
64 ]
65| #v #ty #b #o #tr #EX #u %{tr} @EX
66| #e1 #ty #IH #b #o #tr #EX #u
67  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
68  cases (IH … EX1 u) #tr1' #EX1'
69  %{tr1'} >shift_fst whd in ⊢ (??%?); >EX1'
70  whd in ⊢ (??%?);
71  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct @refl
72| #ty' #e1 #ty #IH #v #tr #EX #u
73  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
74  cases (IH … EX1 u) #tr1' #EX1'
75  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (??%?);
76  whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
77  whd in ⊢ (??%?);
78  cases ty' in EX1rem ⊢ %;
79  [ 4: #r #ty' whd in ⊢ (??%? → ??%?); cases (pointer_compat_dec b1 r)
80       #pc normalize #E destruct @refl
81  | *: normalize #A try #B try #C try #D destruct
82  ]
83| #ty #op #e1 #IH #v #tr #EX #u
84  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
85  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
86  normalize in EXrem; destruct
87  cases (IH … EX1 u) #tr1' #EX1'
88  %{tr1'} >shift_fst
89  whd in ⊢ (??(????(?(???%)?))?);
90  @label_expr_elim #u2
91  whd in ⊢ (??%?); >EX1'
92  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
93| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
94  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
95  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
96  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
97  #u
98  cases (IH1 … EX1 u) #tr1' #EX1'
99  >shift_fst
100  whd in ⊢ (??(λ_.??(????(?(???%)?))?));
101  @label_expr_elim #u2
102  cases (IH2 … EX2 u2) #tr2' #EX2'
103  @label_expr_elim #u3 %{(tr1'⧺tr2')}
104  whd in ⊢ (??%?); >EX1'
105  whd in ⊢ (??%?); >EX2'
106  whd in ⊢ (??%?); >label_expr_type >label_expr_type >EXop
107  normalize in EXop'; destruct @refl
108| #ty #ty' #e1 #IH #v #tr #EX #u
109  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
110  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
111  normalize in EX2rem; destruct
112  cases (IH … EX1 u) #tr1' #EX1'
113  %{tr1'} >shift_fst >shift_fst
114  whd in ⊢ (??%?); >EX1'
115  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
116| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
117  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
118  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
119  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
120  normalize in EX2rem; destruct
121  cases (IH1 … EX1 u) #tr1' #EX1'
122  >shift_fst whd in ⊢ (??(λ_.??(????(?(???%)?))?));
123  @label_expr_elim #u2
124  @label_expr_elim #u3
125  @add_cost_expr_elim #u4 #l4
126  @label_expr_elim #u5
127  @add_cost_expr_elim #u6 #l6
128  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' #EXx'
129  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
130  whd in ⊢ (??%?); >EX1'
131  whd in ⊢ (??%?); >label_expr_type >EXguard
132  whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EXx'
133  normalize @refl
134| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
135  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
136  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
137  >shift_fst whd in ⊢ (??(λ_.??(????(?(???%)?))?));
138  @label_expr_elim #u2
139  @label_expr_elim #u3
140  @add_cost_expr_elim #u4 #l4
141  @add_cost_expr_elim #u5 #l5
142  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
143    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
144    cases (IH1 … EX1 u) #tr1' #EX1'
145    cases (IH2 … EX2 u2) #tr2' #EX2'
146    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
147    whd in ⊢ (??%?); >EX1'
148    whd in ⊢ (??%?); >label_expr_type >EX2' >EXguard
149    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?);
150    whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >EX2'
151    whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >label_expr_type >EX3
152    normalize in EX3rem ⊢ %; destruct @refl
153  | cases (IH1 … EX1 u) #tr1' #EX1'
154    %{(tr1'⧺E0⧺Echarge l5)}
155    whd in ⊢ (??%?); >EX1'
156    whd in ⊢ (??%?); >label_expr_type >EXguard
157    normalize in EXguardrem; destruct @refl
158  ]
159| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
160  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
161  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
162  >shift_fst whd in ⊢ (??(λ_.??(????(?(???%)?))?));
163  @label_expr_elim #u2
164  @add_cost_expr_elim #u4 #l4
165  @label_expr_elim #u3
166  @add_cost_expr_elim #u5 #l5
167  [ cases (IH1 … EX1 u) #tr1' #EX1'
168    %{(tr1'⧺Echarge l4)}
169    whd in ⊢ (??%?); >EX1'
170    whd in ⊢ (??%?); >label_expr_type >EXguard
171    normalize in EXguardrem ⊢ %; destruct @refl
172  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
173    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
174    cases (IH1 … EX1 u) #tr1' #EX1'
175    cases (IH2 … EX2 u4) #tr2' #EX2'
176    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
177    whd in ⊢ (??%?); >EX1'
178    whd in ⊢ (??%?); >label_expr_type >EX2' >EXguard
179    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?);
180    whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >EX2'
181    whd in ⊢ (??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?); >label_expr_type >EX3
182    normalize in EX3rem ⊢ %; destruct @refl
183  ]
184| #ty #ty' #v #tr normalize /2/
185| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
186  [ 7: #id #fl #IH #EX
187    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
188    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
189    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
190    cases (IH … EX1 u) #tr1' #EX1'
191    %{tr1'}
192    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
193    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
194  | 8: #id #fl #IH #EX
195    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
196    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
197    cases (IH … EX1 u) #tr1' #EX1'
198    %{tr1'}
199    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
200    whd in ⊢ (??%?); @refl
201  | *: normalize #A #B try #C try #D try #F destruct
202  ]
203| #ty #l #e1 #IH #v #tr #EX #u
204  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
205  whd in EX1rem:(???%); destruct
206  cases (IH … EX1 u) #tr1' #EX1' %{(tr1'@Echarge l)}
207  >shift_fst >shift_fst whd in ⊢ (??%?); >EX1'
208  whd in ⊢ (??%?); @refl
209| #e1 #ty #NLV #b #o #tr #EX @⊥
210  cases e1 in NLV EX; normalize //
211  #A #B #C try #D try #F destruct
212] qed.
Note: See TracBrowser for help on using the repository browser.