Changeset 2565


Ignore:
Timestamp:
Dec 19, 2012, 6:11:23 PM (7 years ago)
Author:
garnier
Message:

Cl to Cm progress.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2510 r2565  
    149149| 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ]
    150150qed.
     151
     152lemma intsize_eq_inversion :
     153  ∀sz,sz'.
     154  ∀A:Type[0].
     155  ∀ok,not_ok.
     156  intsize_eq_elim' sz sz' (λsz,sz'. res A)
     157                          (OK ? ok)
     158                          (Error ? not_ok) = (OK ? ok) →
     159  sz = sz'.
     160* * try // normalize
     161#A #ok #not_ok #Habsurd destruct
     162qed.
     163
     164lemma intsize_eq_elim_dec :
     165  ∀sz1,sz2.
     166  ∀P: ∀sz1,sz2. Type[0].
     167  ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨
     168  ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2).
     169* * #P normalize
     170try /3 by or_introl, conj, refl/
     171%2 @conj try //
     172% #H destruct
     173qed.
     174
     175lemma typ_eq_elim :
     176  ∀t1,t2.
     177  ∀(P: (t1=t2)+(t1≠t2) → Prop).
     178  (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
     179#t1 #t2 #P #Hl #Hr
     180@(match typ_eq t1 t2
     181  with
     182  [ inl H ⇒ Hl H
     183  | inr H ⇒ Hr H ])
     184qed.
     185
     186
     187lemma eq_nat_dec_true : ∀n. eq_nat_dec n n = inl ?? (refl ? n).
     188#n elim n try //
     189#n' #Hind whd in ⊢ (??%?); >Hind @refl
     190qed.
     191
     192lemma type_eq_dec_true : ∀ty. type_eq_dec ty ty = inl ?? (refl ? ty).
     193#ty cases (type_eq_dec ty ty) #H
     194destruct (H) try @refl @False_ind cases H #J @J @refl qed.
     195
     196lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
     197*
     198[ * * normalize @refl
     199| @refl ]
     200qed.
     201
     202lemma intsize_eq_elim_inversion :
     203  ∀A:Type[0].
     204  ∀sz1,sz2.
     205  ∀elt1,f,errmsg,res. 
     206  intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res →
     207  ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
     208#A * * #elt1 #f #errmsg #res normalize #H destruct (H)
     209%{(refl ??)} normalize nodelta >H @refl
     210qed.
     211
     212lemma inttyp_eq_elim_true' :
     213  ∀sz,sg,P,p1,p2.
     214  inttyp_eq_elim' sz sz sg sg P p1 p2 = p1.
     215* * #P #p1 #p2 normalize try @refl
     216qed.
     217
    151218
    152219(* --------------------------------------------------------------------------- *)
     
    575642  ]
    576643qed.
     644
     645axiom commutative_multiplication :
     646  ∀n. ∀v1,v2:BitVector n.
     647  multiplication ? v1 v2 = multiplication ? v2 v1.
     648 
     649lemma commutative_short_multiplication :
     650  ∀n. ∀v1,v2:BitVector n.
     651  short_multiplication ? v1 v2 = short_multiplication ? v2 v1.
     652#n #v1 #v2 whd in ⊢ (??%%); >commutative_multiplication @refl
     653qed.
     654
     655lemma sign_ext_same_size : ∀n,v. sign_ext n n v = v.
     656#n #v whd in match (sign_ext ???); >nat_compare_eq @refl
     657qed.
     658
     659axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2.
     660
     661axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2.
     662
     663axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?).
     664
     665axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
     666
    577667
    578668
  • src/Clight/memoryInjections.ma

    r2554 r2565  
    370370(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
    371371
    372 
    373 (* particulars inversion. *)
     372(* particulars inversions. *)
    374373lemma value_eq_ptr_inversion :
    375374  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
     
    405404| 3: #Hv1 #Hv2 #_ destruct @H3
    406405| 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed.
     406
     407(* Avoids the use of cut in toCminorCorrectness *)
     408lemma value_eq_triangle_diagram :
     409  ∀E,v1,v2,v3.
     410  value_eq E v1 v2 → v2 = v3 → value_eq E v1 v3.
     411#H1 #H2 #H3 #H4 #H5 #H6 destruct //
     412qed. 
     413
    407414
    408415(* If we succeed to load something by value from a 〈b,off〉 location,
     
    436443    Zltb (block_id b) (nextblock m) = true ∧
    437444    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
     445 
    438446    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
    439447#ty #m * #brg #bid #off #v
  • src/Clight/toCminor.ma

    r2554 r2565  
    334334match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    335335[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
    336 (*| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) *)
    337336(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    338337| add_case_pi n ty sz sg ⇒
     
    341340    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    342341| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    343 ].
    344 
     342].
    345343
    346344definition translate_sub ≝
     
    350348match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    351349[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
    352 (* | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) *)
    353350(* XXX could optimise cast as above *)
    354351| sub_case_pi n ty sz sg ⇒
  • src/Clight/toCminorCorrectness.ma

    r2554 r2565  
    269269include "Clight/memoryInjections.ma".
    270270
    271 lemma intsize_eq_inversion :
    272   ∀sz,sz'.
    273   ∀A:Type[0].
    274   ∀ok,not_ok.
    275   intsize_eq_elim' sz sz' (λsz,sz'. res A)
    276                           (OK ? ok)
    277                           (Error ? not_ok) = (OK ? ok) →
    278   sz = sz'.
    279 * * try // normalize
    280 #A #ok #not_ok #Habsurd destruct
    281 qed.
    282 
    283271(* Perhaps we will have to be more precise on what is allocated, etc.
    284272   cf [exec_alloc_variables]. For now this is conveniently hidden in
     
    326314qed.
    327315
     316lemma typ_should_eq_inversion :
     317  ∀ty1,ty2,P,a,x.
     318    typ_should_eq ty1 ty2 P a = OK ? x →
     319    ty1 = ty2 ∧ a ≃ x.
     320* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
     321[ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
     322| 3: cases sz cases sg #P #A #x normalize #H destruct
     323| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
     324cases sz cases sz2 cases sg cases sg2
     325#P #a #x #H normalize in H:(??%?); destruct (H)
     326try @conj try @refl try @refl_jmeq
     327qed.
     328
    328329lemma load_value_of_type_by_ref :
    329330  ∀ty,m,b,off,val.
     
    460461qed.
    461462
    462 lemma intsize_eq_elim_dec :
    463   ∀sz1,sz2.
    464   ∀P: ∀sz1,sz2. Type[0].
    465   ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨
    466   ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2).
    467 * * #P normalize
    468 try /3 by or_introl, conj, refl/
    469 %2 @conj try //
    470 % #H destruct
    471 qed.
    472 
    473 lemma typ_eq_elim :
    474   ∀t1,t2.
    475   ∀(P: (t1=t2)+(t1≠t2) → Prop).
    476   (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
    477 #t1 #t2 #P #Hl #Hr
    478 @(match typ_eq t1 t2
    479   with
    480   [ inl H ⇒ Hl H
    481   | inr H ⇒ Hr H ])
    482 qed.
    483 
    484463
    485464lemma translate_notbool_to_cminor :
     
    614593qed.
    615594
    616 lemma typ_should_eq_inversion : ∀ty1,ty2,P,a,x. typ_should_eq ty1 ty2 P a = OK ? x → ty1 = ty2.
    617 * [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
    618 [ 4: #P #a #x normalize #H destruct (H) @refl
    619 | 3: cases sz cases sg #P #A #x normalize #H destruct
    620 | 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
    621 cases sz cases sz2 cases sg cases sg2
    622 #P #a #x #H normalize in H:(??%?); destruct (H)
    623 try @refl
     595lemma classify_aop_inversion :
     596  ∀ty1,ty2.
     597    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
     598    classify_aop ty1 ty2 = aop_default ty1 ty2.
     599#ty1 #ty2
     600cases (classify_aop ty1 ty2)
     601[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
     602| #ty #ty' %2 @refl ]
    624603qed.
    625604
    626 lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
    627 *
    628 [ * * normalize @refl
    629 | @refl ]
    630 qed.
    631 
    632 lemma intsize_eq_elim_inversion :
    633   ∀A:Type[0].
    634   ∀sz1,sz2.
    635   ∀elt1,f,errmsg,res. 
    636   intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res →
    637   ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
    638 #A * * #elt1 #f #errmsg #res normalize #H destruct (H)
    639 %{(refl ??)} normalize nodelta >H @refl
     605lemma sem_add_ip_inversion :
     606  ∀sz,sg,ty',optlen.
     607  ∀v1,v2,res.
     608  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
     609  ∃sz',i. v1 = Vint sz' i ∧
     610      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') i)) ∨
     611       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     612#tsz #tsg #ty' * [ | #n ]
     613*
     614[ | #sz' #i' | | #p'
     615| | #sz' #i' | | #p' ]
     616#v2 #res
     617whd in ⊢ ((??%?) → ?);
     618#H destruct
     619cases v2 in H;
     620[ | #sz2' #i2' | | #p2'
     621| | #sz2' #i2' | | #p2' ] normalize nodelta
     622#H destruct
     623[ 1,3:
     624  lapply H -H
     625  @(eq_bv_elim … i' (zero ?)) normalize nodelta
     626  #Hi #Heq destruct (Heq)
     627  %{sz'} %{(zero ?)} @conj destruct try @refl
     628  %2 @conj try @conj try @refl
     629| *: %{sz'} %{i'} @conj try @refl
     630  %1 %{p2'} @conj try @refl
     631] qed.
     632
     633(* symmetric of the upper one *)
     634lemma sem_add_pi_inversion :
     635  ∀sz,sg,ty',optlen.
     636  ∀v1,v2,res.
     637  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
     638  ∃sz',i. v2 = Vint sz' i ∧
     639      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') i)) ∨
     640       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
     641#tsz #tsg #ty' * [ | #n ]
     642*
     643[ | #sz' #i' | | #p'
     644| | #sz' #i' | | #p' ]
     645#v2 #res
     646whd in ⊢ ((??%?) → ?);
     647#H destruct
     648cases v2 in H; normalize nodelta
     649[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
     650#H destruct
     651[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
     652  %{p'} @conj try @refl
     653| *: lapply H -H
     654  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
     655  #Hi #Heq destruct (Heq)
     656  %{sz2'} %{(zero ?)} @conj destruct try @refl
     657  %2 @conj try @conj try @refl
     658] qed.
     659
     660(* Know that addition on integers gives an integer. Notice that there is no correlation
     661   between the size in the types and the size of the integer values. *)
     662lemma sem_add_ii_inversion :
     663  ∀sz,sg.
     664  ∀v1,v2,res.
     665  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     666  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     667              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
     668#sz #sg
     669*
     670[ | #sz' #i' | | #p' ]
     671#v2 #res
     672whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
     673cases sz cases sg normalize nodelta
     674#H destruct
     675cases v2 in H; normalize nodelta
     676#H1 destruct
     677#H2 destruct #Heq %{sz'} lapply Heq -Heq
     678cases sz' in i'; #i' 
     679whd in match (intsize_eq_elim ???????);
     680cases H1 in H2; #j' normalize nodelta
     681#Heq destruct (Heq)
     682%{i'} %{j'} @conj try @conj try @conj try @refl
    640683qed.
    641684
     685lemma sem_mul_inversion :
     686  ∀sz,sg.
     687  ∀v1,v2,res.
     688  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
     689  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     690              res = Vint sz' (short_multiplication ? i1 i2).
     691#sz #sg *
     692[ | #sz' #i' | | #p' ]
     693#v2 #res
     694whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     695cases sz cases sg normalize nodelta
     696#H destruct
     697cases v2 in H; normalize nodelta
     698#H1 destruct
     699#H2 destruct #Heq %{sz'} lapply Heq -Heq
     700cases sz' in i'; #i' 
     701whd in match (intsize_eq_elim ???????);
     702cases H1 in H2; #j' normalize nodelta
     703#Heq destruct (Heq)
     704%{i'} %{j'} @conj try @conj try @conj try @refl
     705qed.
     706
     707
     708lemma sem_div_inversion_s :
     709  ∀sz.
     710  ∀v1,v2,res.
     711  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
     712  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     713              match division_s ? i1 i2 with
     714              [ Some q ⇒  res =  (Vint sz' q)
     715              | None ⇒ False ].
     716#sz *
     717[ | #sz' #i' | | #p' ]
     718#v2 #res
     719whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     720>type_eq_dec_true normalize nodelta
     721#H destruct
     722cases v2 in H; normalize nodelta
     723[ | #sz2' #i2' | | #p2' ]
     724#Heq destruct
     725%{sz'}
     726lapply Heq -Heq
     727cases sz' in i'; #i' 
     728whd in match (intsize_eq_elim ???????);
     729cases sz2' in i2'; #i2' normalize nodelta
     730whd in match (option_map ????); #Hdiv destruct
     731%{i'} %{i2'} @conj try @conj try @conj try @refl
     732cases (division_s ???) in Hdiv;
     733[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     734qed.
     735
     736lemma sem_div_inversion_u :
     737  ∀sz.
     738  ∀v1,v2,res.
     739  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
     740  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
     741              match division_u ? i1 i2 with
     742              [ Some q ⇒  res =  (Vint sz' q)
     743              | None ⇒ False ].
     744#sz *
     745[ | #sz' #i' | | #p' ]
     746#v2 #res
     747whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
     748>type_eq_dec_true normalize nodelta
     749#H destruct
     750cases v2 in H; normalize nodelta
     751[ | #sz2' #i2' | | #p2' ]
     752#Heq destruct
     753%{sz'}
     754lapply Heq -Heq
     755cases sz' in i'; #i' 
     756whd in match (intsize_eq_elim ???????);
     757cases sz2' in i2'; #i2' normalize nodelta
     758whd in match (option_map ????); #Hdiv destruct
     759%{i'} %{i2'} @conj try @conj try @conj try @refl
     760cases (division_u ???) in Hdiv;
     761[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
     762qed.
     763
     764lemma expr_vars_fix_ptr_type :
     765  ∀ty',optlen.
     766  ∀e:expr (typ_of_type (ptr_type ty' optlen)).
     767  ∀P.
     768   expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
     769   expr_vars
     770    (typ_of_type
     771        match optlen 
     772        in option 
     773        return λ_:(option ℕ).type with 
     774        [None⇒Tpointer ty'
     775        |Some (n':ℕ)⇒ Tarray ty' n']) e P.
     776#ty' * normalize
     777[ 2: #n ]
     778#e #P
     779@expr_vars_mp //
     780qed.
     781
     782(* This lemma is just noise. *)
     783lemma eval_expr_rewrite_aux :
     784  ∀genv.
     785  ∀optlen.
     786  ∀ty'.
     787  ∀e.
     788  ∀cm_env.
     789  ∀H.
     790  ∀sp.
     791  ∀m.
     792  ∀res.
     793  (eval_expr genv
     794             (typ_of_type
     795                 match optlen in option return λ_:(option ℕ).type with 
     796                 [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
     797             e cm_env (expr_vars_fix_ptr_type ty' optlen e (λid:ident.λty0:typ.present SymbolTag val cm_env id) H) sp m) = OK ? res →
     798   eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
     799#genv * [ 2: #n ] normalize nodelta
     800#ty' normalize in match (typ_of_type ?);
     801#e #cm_env whd in match (fix_ptr_type ???);
     802#H #sp #m #res #H @H
     803qed.
     804
     805
     806(* TODOs : there are some glitches between clight and cminor :
     807 * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
     808      in the shortcut case, the cminor code returns directly the outcome of the
     809      evaluated expr, with a possibly different size.
     810   2) another glitch is for the integer/pointer additions: Clight always performs
     811      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
     812      the sign of i, producing either a sign extension or a zero extension.
     813 *)
    642814lemma eval_expr_sim :
    643815  ∀(inv:clight_cminor_inv).
     
    675847#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
    676848@expr_lvalue_ind_combined
    677 [ 1: (* Integer constant *)
     849[ 7: (* binary ops *)
     850     #ty
     851     #op #e1 #e2
     852     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
     853     cases (bind_inversion ????? Htranslate) -Htranslate
     854     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
     855     cases (bind_inversion ????? Htranslate) -Htranslate
     856     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
     857     whd in ⊢ ((??%?) → ?);
     858     #Htranslate_binop
     859     cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
     860     #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     861     #cl_val #trace #Hyp_present #Hexec
     862     (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
     863     lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
     864     lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
     865     lapply Hyp_present -Hyp_present
     866     lapply Htranslate_lhs -Htranslate_lhs
     867     lapply Htranslate_rhs -Htranslate_rhs
     868     lapply Hexpr_vars_lhs -Hexpr_vars_lhs
     869     lapply Hexpr_vars_rhs -Hexpr_vars_rhs
     870     lapply Hexec -Hexec
     871     lapply Htranslated_binop -Htranslated_binop
     872     lapply rhs -rhs lapply lhs -lhs
     873     (* end of dump *)
     874     cases op
     875     whd in ⊢ (? → ? → (??%?) → ?);
     876     [ 1: (* add *)
     877       lapply (classify_add_inversion (typeof e1) (typeof e2))
     878       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     879       (* trying to factorise as much stuff as possible ... *)
     880       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
     881       * [ 1: * ]
     882       [ 1: * #sz * #sg * *
     883       | 2: * #optlen * #ty' * #sz * #sg * *
     884       | 3: * #optlen * #sz * #sg * #ty' * * ]
     885       whd in match (typeof ?) in ⊢ (% → % → ?);
     886       #Htypeof_e1 #Htypeof_e2
     887       >Htypeof_e1 >Htypeof_e2
     888       #Hclassify
     889       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
     890       normalize nodelta
     891       whd in match (typeof ?) in ⊢ (% → % → %);
     892       whd in match (typ_of_type (Tint ??));
     893       #lhs #rhs #Htyp_should_eq
     894       [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
     895       | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
     896       -Htyp_should_eq
     897       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
     898       <Heq_e' -Heq_e'
     899       #Hexec
     900       #Hexpr_vars_rhs #Hexpr_vars_lhs
     901       #Htranslate_rhs #Htranslate_lhs
     902       * [ #Hyp_present_lhs #Hyp_present_rhs
     903         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
     904         | #Hyp_present_rhs * #Hyp_present_lhs #Hyp_present_cst  ]
     905       whd in match (typeof ?);
     906       #Hind_rhs #Hind_lhs
     907       cases (bind_inversion ????? Hexec) -Hexec
     908       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     909       cases (bind_inversion ????? Hexec) -Hexec
     910       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     911       cases (bind_inversion ????? Hexec) -Hexec
     912       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     913       lapply (opt_to_res_inversion ???? Hsem) -Hsem
     914       whd in match (typeof ?); whd in match (typeof ?);
     915       #Hsem_binary
     916       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
     917       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
     918       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     919       [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
     920       | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
     921       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     922       whd in match (eval_expr ???????);
     923       whd in match (proj1 ???);
     924       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
     925       [ 1,2: >Heval_lhs normalize nodelta
     926              whd in match (eval_expr ???????);
     927              whd in match (eval_expr ???????);
     928              >Heval_rhs normalize nodelta
     929              whd in match (m_bind ?????);
     930       | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
     931            whd in match (eval_expr ???????);
     932            whd in match (eval_expr ???????);
     933            >Heval_lhs normalize nodelta
     934       ]
     935       whd in match (proj1 ???); whd in match (proj2 ???);
     936       [ 2: (* standard int/int addition. *)
     937            whd in match (eval_binop ???????);
     938            whd in Hsem_binary:(??%?);
     939            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     940            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     941            cases (sem_add_ii_inversion … Hsem_binary_translated)
     942            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
     943            #Hcm_lhs #Hcm_rhs #Hcm_val
     944            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
     945            >intsize_eq_elim_true normalize nodelta
     946            %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
     947            @conj try @refl lapply Hsem_binary_translated
     948            whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
     949            >inttyp_eq_elim_true' normalize nodelta
     950            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
     951       | *: (* pointer/int int/pointer addition *)
     952            whd in Hsem_binary:(??%?);
     953            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     954            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     955            [ 1: lapply (sem_add_pi_inversion … Hsem_binary_translated)
     956                 * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
     957                 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
     958                 | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
     959                 destruct
     960                 whd in match (eval_unop ????);
     961                 @(match sg
     962                   return λs. sg = s → ?
     963                   with
     964                   [ Unsigned ⇒ λHsg. ?
     965                   | Signed ⇒ λHsg. ?
     966                   ] (refl ??)) normalize nodelta
     967                   whd in match (eval_binop ???????);
     968                   whd in match (m_bind ?????);
     969                   [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
     970                                   (short_multiplication (bitsize_of_intsize I16)
     971                                   (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
     972                                   (repr I16 (sizeof ty')))))}
     973                   | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
     974                                   (short_multiplication (bitsize_of_intsize I16)
     975                                   (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
     976                                   (repr I16 (sizeof ty')))))} ]
     977                   [ 1,2: @conj whd in match (E0); whd in match (Eapp trace_rhs ?);
     978                          >(append_nil … trace_rhs) try @refl
     979                          @(value_eq_triangle_diagram … Hvalue_eq_res)
     980                          whd in match (shift_pointer_n ????);
     981                          whd in match (shift_offset_n ????);
     982                          >commutative_short_multiplication
     983                          whd in match (shift_pointer ???);
     984                          whd in match (shift_offset ???);
     985                          @cthulhu (* cf problem description at top of lemma. *)
     986                   | 3: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
     987                        >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
     988                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
     989                        normalize >append_nil try @refl
     990                   | 4: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
     991                        >(short_multiplication_zero 16 (repr I16 (sizeof ty')))
     992                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
     993                        normalize >append_nil try @refl ]
     994            | 2: (* integer/pointer add: symmetric to the case above. *) @cthulhu ]
     995       ]
     996     | 2: (* subtraction cases: identical to add *) @cthulhu
     997     | 3: (* mul *)
     998       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
     999       [ 2,4: #Hclassify >Hclassify normalize nodelta
     1000            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     1001       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
     1002       whd in match (typeof ?); #e'
     1003       * #sz * #sg * *
     1004       whd in match (typeof ?) in ⊢ (% → % → ?);
     1005       #Htypeof_e1 #Htypeof_e2
     1006       >Htypeof_e1 >Htypeof_e2
     1007       whd in match (typeof ?) in ⊢ (% → % → % → ?);
     1008       #Hclassify
     1009       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
     1010       normalize nodelta
     1011       whd in match (typ_of_type (Tint ??));
     1012       #lhs #rhs #Htyp_should_eq
     1013       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
     1014       -Htyp_should_eq
     1015       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
     1016       <Heq_e' -Heq_e'
     1017       #Hexec
     1018       #Hexpr_vars_rhs #Hexpr_vars_lhs
     1019       #Htranslate_rhs #Htranslate_lhs
     1020       * #Hyp_present_lhs #Hyp_present_rhs
     1021       #Hind_rhs #Hind_lhs
     1022       cases (bind_inversion ????? Hexec) -Hexec
     1023       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     1024       cases (bind_inversion ????? Hexec) -Hexec
     1025       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     1026       cases (bind_inversion ????? Hexec) -Hexec
     1027       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1028       lapply (opt_to_res_inversion ???? Hsem) -Hsem
     1029       whd in match (typeof ?); whd in match (typeof ?);
     1030       #Hsem_binary
     1031       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
     1032       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1033       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
     1034       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1035       whd in match (eval_expr ???????);
     1036       whd in match (proj1 ???);
     1037       >Heval_lhs normalize nodelta
     1038       >Heval_rhs normalize nodelta
     1039       whd in match (m_bind ?????);
     1040       whd in match (eval_binop ???????);
     1041       whd in Hsem_binary:(??%?);
     1042       lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1043       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1044       cases (sem_mul_inversion … Hsem_binary)
     1045       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
     1046       #Hcm_lhs #Hcm_rhs #Hcm_val
     1047       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
     1048       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
     1049       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
     1050       >intsize_eq_elim_true normalize nodelta
     1051       %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
     1052       @conj try @refl
     1053       whd in Hsem_binary:(??%?);     
     1054       whd in match (classify_aop ??) in Hsem_binary:(??%?);
     1055       >type_eq_dec_true in Hsem_binary; normalize nodelta
     1056       >intsize_eq_elim_true #Heq destruct (Heq)
     1057       %2
     1058     | 4: (* div *)
     1059       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
     1060       [ 2,4: #Hclassify >Hclassify normalize nodelta
     1061            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     1062       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
     1063       whd in match (typeof ?); #e'
     1064       * #sz * * * *
     1065       whd in match (typeof ?) in ⊢ (% → % → ?);
     1066       #Htypeof_e1 #Htypeof_e2
     1067       >Htypeof_e1 >Htypeof_e2
     1068       whd in match (typeof ?) in ⊢ (% → % → % → ?);
     1069       #Hclassify
     1070       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
     1071       normalize nodelta
     1072       whd in match (typ_of_type (Tint ??));
     1073       #lhs #rhs #Htyp_should_eq
     1074       [ cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
     1075       | cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
     1076       -Htyp_should_eq
     1077       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
     1078       <Heq_e' -Heq_e'
     1079       #Hexec
     1080       #Hexpr_vars_rhs #Hexpr_vars_lhs
     1081       #Htranslate_rhs #Htranslate_lhs
     1082       * #Hyp_present_lhs #Hyp_present_rhs
     1083       #Hind_rhs #Hind_lhs
     1084       cases (bind_inversion ????? Hexec) -Hexec
     1085       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
     1086       cases (bind_inversion ????? Hexec) -Hexec
     1087       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
     1088       cases (bind_inversion ????? Hexec) -Hexec
     1089       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1090       lapply (opt_to_res_inversion ???? Hsem) -Hsem
     1091       whd in match (typeof ?); whd in match (typeof ?);
     1092       #Hsem_binary
     1093       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
     1094       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
     1095       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
     1096       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
     1097       whd in match (eval_expr ???????);
     1098       whd in match (proj1 ???);
     1099       >Heval_lhs normalize nodelta
     1100       >Heval_rhs normalize nodelta
     1101       whd in match (m_bind ?????);
     1102       whd in match (eval_binop ???????);
     1103       whd in Hsem_binary:(??%?);
     1104       lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
     1105       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
     1106       [ cases (sem_div_inversion_s … Hsem_binary)
     1107       | cases (sem_div_inversion_u … Hsem_binary) ]
     1108       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
     1109       #Hcm_lhs #Hcm_rhs #Hcm_val
     1110       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
     1111       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
     1112       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
     1113       >intsize_eq_elim_true normalize nodelta
     1114       [ cases (division_s ???) in Hcm_val; normalize nodelta
     1115         [ @False_ind
     1116         | #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ]
     1117       | cases (division_u ???) in Hcm_val; normalize nodelta
     1118         [ @False_ind
     1119         | #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2 ] ]
     1120     | 5: (* mod *) @cthulhu
     1121     | 6: (* and *) @cthulhu
     1122     | 7: (* or *)  @cthulhu
     1123     | 8: (* xor *) @cthulhu
     1124     | 9: (* shl *) @cthulhu
     1125     | 10: (* shr *) @cthulhu
     1126     | 11: (* eq *) @cthulhu
     1127     | 12: (* ne *) @cthulhu
     1128     | 13: (* lt *) @cthulhu
     1129     | 14: (* gt *) @cthulhu
     1130     | 15: (* le *) @cthulhu
     1131     | 16: (* ge *) @cthulhu ]
     1132     
     1133| 1: (* Integer constant *)
    6781134  #csz #ty cases ty
    6791135  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     
    11811637    ]
    11821638  ]
    1183 | 7: (* binary ops *)
    1184      #ty
    1185      letin s ≝ (typ_of_type ty)
    1186      #op #e1 #e2
    1187      #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
    1188      cases (bind_inversion ????? Htranslate) -Htranslate
    1189      * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
    1190      cases (bind_inversion ????? Htranslate) -Htranslate
    1191      * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
    1192      whd in ⊢ ((??%?) → ?);
    1193      cases op whd in match (translate_binop ??????);
    1194      @cthulhu (* PITA *)
    11951639| 8: #ty #ty' * #ed #ety
    11961640  cases ety
     
    12141658  #cast_val * #Hexec_cast
    12151659  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    1216   lapply (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) #Htype_eq
     1660  cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
     1661  #Htype_eq
    12171662  lapply Hexec_cast -Hexec_cast
    1218   lapply Htyp_should_eq -Htyp_should_eq
     1663(*  lapply Htyp_should_eq -Htyp_should_eq *)
    12191664  lapply Htranslate_cast -Htranslate_cast
    12201665  lapply Hexpr_vars_cast -Hexpr_vars_cast
     
    12241669  lapply cm_expr -cm_expr
    12251670  <Htype_eq -Htype_eq
    1226   whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?); >typ_eq_refl normalize nodelta
     1671  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
     1672  whd in match (typeof ?); normalize nodelta
    12271673  cases ty'
    12281674  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
    12291675  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
    12301676  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
    1231   #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast
    1232   whd in match (typ_of_type ?) in cm_castee cm_expr Hexpr_vars_castee;
    1233   whd in match (typeof ?) in Htranslate_cast Hexec_cast;
    1234   #Heq destruct (Heq)
     1677  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
     1678  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
    12351679  whd in Htranslate_cast:(??%%);
    12361680  whd in Hexpr_vars;
     
    12381682  [ 1,2,3,4,7:
    12391683    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
    1240     * #cm_val' * #Heval_castee #Hvalue_eq #Hexec_cast
    1241     lapply Hvalue_eq -Hvalue_eq lapply Hexec_cm -Hexec_cm
     1684    * #cm_val' * #Heval_castee
     1685    lapply Hexec_cm -Hexec_cm
    12421686    whd in Hexec_cast:(??%%);
    12431687    cases cm_val in Hexec_cast; normalize nodelta
     
    12881732 | *:
    12891733    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
    1290     * #cm_val' * #Heval_expr #Hvalue_eq #Hexec_cast >Heval_expr
     1734    * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
    12911735    %{cm_val'} @conj try @refl
    1292     lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq 
     1736    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
    12931737    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
    12941738    cases cm_val
     
    13011745    [ 1,5,9,13: destruct (Hexec_cast) ]
    13021746    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
    1303     lapply Hexec_cast -Hexec_cast 
     1747    lapply Hexec_cast -Hexec_cast
    13041748    normalize cases (eq_v ?????) normalize
    13051749    #Habsurd destruct (Habsurd)
    1306  ]     
     1750 ]
    13071751| 9: (* Econdition *) 
    13081752  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
     
    15652009  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
    15662010  whd in match (typeof ?) in Htyp_should_eq:(??%?);
    1567   lapply (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
     2011  cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
    15682012  #Htyp_eq
    1569   lapply Htyp_should_eq -Htyp_should_eq
    15702013  lapply Htranslate_ind -Htranslate_ind
    15712014  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
     
    15732016  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
    15742017  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
    1575   <(Htyp_eq)
     2018  <Htyp_eq
    15762019  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
    1577   #Htranslate_ind
    1578   whd in ⊢ ((??%?) → ?); >typ_eq_refl normalize nodelta
    1579   whd in ⊢ ((??%%) → ?); #H destruct (H) whd in match (eval_expr ???????);
     2020  #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
     2021  whd in match (eval_expr ???????);
    15802022  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
    15812023  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     
    15832025  #cm_val' * #Heval_expr' #Hvalue_eq
    15842026  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
    1585   (* Inconsistency in clight and cminor executable semantics for expressions~:
    1586      placement of the label is either before or after current trace.
    1587      To be resolved.
    1588    *)
    1589   @cthulhu
     2027  >cons_to_append >(nil_append … cm_trace) @refl
    15902028| 15: *
    15912029  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
Note: See TracChangeset for help on using the changeset viewer.