source: src/Clight/labelSimulation.ma @ 1888

Last change on this file since 1888 was 1888, checked in by campbell, 8 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.