Changeset 2263


Ignore:
Timestamp:
Jul 25, 2012, 6:55:36 PM (7 years ago)
Author:
garnier
Message:

Finished proving semantics preservation under memory injections for unary and binary ops. Had to tweak a definition in Csem.ma to circumvent lack of unfold.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2177 r2263  
    327327let rec sem_cmp (c:comparison)
    328328                  (v1: val) (t1: type) (v2: val) (t2: type)
    329                   (m: mem): option val ≝
     329                  (m: mem) on m: option val ≝
    330330  match classify_cmp t1 t2 with
    331331  [ cmp_case_ii _ sg ⇒
  • src/Clight/switchRemoval.ma

    r2255 r2263  
    27432743] qed.
    27442744
     2745lemma monotonic_Zlt_Zsucc: monotonic Z Zlt Zsucc.
     2746whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle)
     2747/3 by monotonic_Zle_Zplus_r, Zle_to_Zlt/ qed.
     2748
     2749lemma monotonic_Zlt_Zpred: monotonic Z Zlt Zpred.
     2750whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle)
     2751/3 by monotonic_Zle_Zpred, Zle_to_Zlt/ qed.
     2752
     2753lemma antimonotonic_Zle_Zsucc: ∀x,y. Zsucc x ≤ Zsucc y → x ≤ y.
     2754#x #y #H lapply (monotonic_Zle_Zpred … H) >Zpred_Zsucc >Zpred_Zsucc #H @H
     2755qed.
     2756
     2757(*
     2758lemma antimonotonic_Zle_Zpred: ∀x,y. Zpred x ≤ Zpred y → x ≤ y.
     2759#x #y #H lapply (monotonic_Zle_Zsucc … H) >Zsucc_Zpred >Zsucc_Zpred #H @H
     2760qed. *)
     2761
     2762lemma antimonotonic_Zlt_Zsucc: ∀x,y. Zsucc x < Zsucc y → x < y.
     2763#x #y #Hlt lapply (Zle_to_Zlt … (antimonotonic_Zle_Zsucc … (Zlt_to_Zle … Hlt)))
     2764>Zpred_Zsucc #H @H
     2765qed.
     2766
     2767lemma antimonotonic_Zlt_Zpred: ∀x,y. Zpred x < Zpred y → x < y.
     2768#x #y #Hlt lapply (monotonic_Zlt_Zsucc … Hlt) >Zsucc_Zpred >Zsucc_Zpred #H @H
     2769qed.
     2770
     2771lemma not_Zlt_to_Zltb_false : ∀n,m. n ≮ m → Zltb n m = false.
     2772#n #m #Hnlt
     2773@Zltb_elim_Type0
     2774[ 1: elim Hnlt #H0 #H1 @(False_ind … (H0 H1))
     2775| 2: #_ @refl ] qed.
     2776
    27452777lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta).
    27462778#x #y #delta
     
    27502782     [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ]
    27512783     #H @sym_eq @eqZb_false @H ] qed.
     2784     
     2785lemma Zltb_Zsucc : ∀x,y. Zltb x y = Zltb (Zsucc x) (Zsucc y).
     2786#x #y
     2787@(Zltb_elim_Type0 … x y)
     2788[ 1: #Hlt @sym_eq lapply (monotonic_Zlt_Zsucc … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt')
     2789| 2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc
     2790      lapply (antimonotonic_Zlt_Zsucc … Hltsucc) #Hlt
     2791      @(absurd … Hlt Hnlt)
     2792] qed.
     2793
     2794lemma Zltb_Zpred : ∀x,y. Zltb x y = Zltb (Zpred x) (Zpred y).
     2795#x #y
     2796@(Zltb_elim_Type0 … x y)
     2797[ 1: #Hlt @sym_eq
     2798lapply (monotonic_Zlt_Zpred … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt')
     2799| 2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc
     2800      lapply (antimonotonic_Zlt_Zpred … Hltsucc) #Hlt
     2801      @(absurd … Hlt Hnlt)
     2802] qed.           
     2803
     2804lemma Zplus_pos_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (pos delta)) (y + (pos delta)).
     2805#x #y #delta @(pos_elim … delta)
     2806[ 1: >(sym_Zplus x) >(sym_Zplus y) <Zsucc_Zplus_pos_O <Zsucc_Zplus_pos_O
     2807     >Zltb_Zsucc @refl
     2808| 2: #n #Hind >Hind >Zltb_Zsucc
     2809     >(sym_Zplus x) >(sym_Zplus y)
     2810     <Zplus_Zsucc <Zplus_Zsucc
     2811     >(sym_Zplus ? x) >(sym_Zplus ? y)
     2812     normalize in match (Zsucc ?); @refl
     2813] qed.
     2814
     2815lemma Zplus_neg_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (neg delta)) (y + (neg delta)).
     2816#x #y #delta @(pos_elim … delta)
     2817[ 1: >(sym_Zplus x) >(sym_Zplus y) <Zpred_Zplus_neg_O <Zpred_Zplus_neg_O
     2818     >Zltb_Zpred @refl
     2819| 2: #n #Hind >Hind >Zltb_Zpred
     2820     >(sym_Zplus x) >(sym_Zplus y)
     2821     <Zplus_Zpred <Zplus_Zpred
     2822     >(sym_Zplus ? x) >(sym_Zplus ? y)
     2823     normalize in match (Zpred ?); @refl
     2824] qed.
     2825
     2826(* I would not be surprised for a simpler proof that mine to exist. *)
     2827lemma Zplus_lt_lt : ∀x,y,delta:Z. Zltb x y = Zltb (x + delta) (y + delta).
     2828#x #y #delta
     2829cases delta
     2830[ 1: >Zplus_z_OZ >Zplus_z_OZ @refl
     2831| 2: #p @Zplus_pos_lt_lt
     2832| 3: #p @Zplus_neg_lt_lt
     2833] qed.
    27522834
    27532835(* offset equality is invariant by translation *)
     
    27602842elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed.
    27612843
    2762 (* The key problem is that [sem_cmp] is a let-rec defined on [op], but we /don't want/ to
    2763    perform a case-analysis on [op]. TODO: try and see if specifying another pseudo-decreasing
    2764    argument is ok. This just won't cut it.. *)
    2765 lemma sem_cmp_value_eq :
    2766   ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
    2767    value_eq E v1 v2 →
    2768    value_eq E v1' v2' →
    2769    memory_inj E m1 m2 →   
    2770    ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
    2771            ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
    2772 @cthulhu qed.
    2773 
    2774 (*           
    2775 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
    2776 elim m1 in Hinj; #contents_map1 #nextblock1 #Hnextblock1 #Hinj
    2777 cases op whd in match (sem_cmp ??????) in ⊢ (% → ?);
    2778 cases (classify_cmp ty ty') normalize nodelta
    2779 [ 1,9,17: #sz #sg
    2780   @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
    2781   [ 1,6,11: #v #Habsurd destruct (Habsurd)
    2782   | 2,7,12: #sz #i @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    2783     [ 1,6,11: #v' #Habsurd destruct (Habsurd)
    2784     | 2,7,12: #sz' #i'
    2785     | 3,8,13: #f #Habsurd destruct (Habsurd)
    2786     | 4,9,14: #Habsurd destruct (Habsurd)
    2787     | 5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ]
    2788 
    2789   | 3,8,13: #f #Habsurd destruct (Habsurd)   
    2790   | 4,9,14: #Habsurd destruct (Habsurd)
    2791   | 5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ]
    2792 | 2,10,18: #n #ty0 | 3,11,19: #fsz | 4,12,20: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
    2793 [ 1,6,11,16,21,26,31,36,41,46,51,56,61,66,71,76,81,86,91,96: #v #Habsurd destruct (Habsurd)
    2794 | 2,7,12,17,22,27,32,37,42,47,52,57,62,67,72,77,82,87,92,97: #sz' #i
    2795 
    2796 |
    2797 | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
    2798 *)
    2799 
    2800 
    2801 (* The proof of the following lemma begs for factorization. *)
    2802 (*
    2803 lemma sem_cmp_value_eq :
     2844lemma cmp_offset_translation : ∀op,delta,x,y.
     2845   cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
     2846* #delta #x #y normalize
     2847elim delta #zdelta
     2848[ 1: @Zplus_eq_eq
     2849| 2: <Zplus_eq_eq @refl
     2850| 3: @Zplus_lt_lt
     2851| 4: <Zplus_lt_lt @refl
     2852| 5: @Zplus_lt_lt
     2853| 6: <Zplus_lt_lt @refl
     2854qed.
     2855
     2856lemma cmp_value_eq :
    28042857  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
    28052858   value_eq E v1 v2 →
     
    28092862           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
    28102863#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
    2811 cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????);
    2812 [ 1: (* Equality *)
    2813   cases (classify_cmp ty ty') normalize nodelta
    2814   [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
    2815   @(value_eq_inversion E … Hvalue_eq1)
    2816   [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
    2817   normalize nodelta
    2818   [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
    2819   @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    2820   [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
    2821   [ 5: elim sg normalize nodelta
    2822        @intsize_eq_elim_elim
    2823        [ 1,3: #_ #Habsurd destruct (Habsurd)
    2824        | 2,4: #Heq destruct (Heq) normalize nodelta
    2825               [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
    2826               | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
     2864elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj
     2865whd in match (sem_cmp ??????) in ⊢ ((??%?) → %);
     2866cases (classify_cmp ty ty') normalize nodelta
     2867[ 1: #tsz #tsg
     2868     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
     2869     [ 1: #v #Habsurd destruct (Habsurd)
     2870     | 3: #f #Habsurd destruct (Habsurd)
     2871     | 4: #Habsurd destruct (Habsurd)
     2872     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
     2873     #sz #i
     2874     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2875     [ 1: #v #Habsurd destruct (Habsurd)
     2876     | 3: #f #Habsurd destruct (Habsurd)
     2877     | 4: #Habsurd destruct (Habsurd)
     2878     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
     2879     #sz' #i' cases tsg normalize nodelta
     2880     @intsize_eq_elim_elim
     2881     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
     2882     | 2,4: #Heq destruct (Heq) normalize nodelta
     2883            #Heq destruct (Heq)     
     2884            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
     2885            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
    28272886              /3 by ex_intro, conj, vint_eq/ ]
    2828   | 10: #Heq destruct (Heq) cases (Fcmp Ceq f f') /3 by ex_intro, conj, vint_eq/
    2829   | 15: whd in match (sem_cmp_match ?); #Heq destruct (Heq)
    2830         /3 by ex_intro, conj, vint_eq/
    2831   | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
    2832         /3 by ex_intro, conj, vint_eq/
    2833   | 20: lapply (mi_valid_pointers … Hinj p1' p2')
    2834         lapply (mi_valid_pointers … Hinj p1 p2)
    2835         cases (valid_pointer m1 p1')
    2836         [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    2837         cases (valid_pointer m1 p1)
    2838         [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    2839         #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
    2840         >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
    2841         elim p1 in Hembed; #b1 #o1
    2842         elim p1' in Hembed'; #b1' #o1'
    2843         whd in match (pointer_translation ??);
    2844         whd in match (pointer_translation ??);
    2845         @(eq_block_elim … b1 b1')
    2846         [ 1: #Heq destruct (Heq)
    2847               cases (E b1')
    2848               [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
    2849               * #eb1' #eo1' normalize nodelta
    2850               #Heq1 #Heq2 #Heq3 destruct
    2851               >eq_block_identity normalize nodelta
    2852               >eq_offset_translation cases (cmp_offset ???)
    2853               /3 by ex_intro, conj, vint_eq/
    2854         | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
    2855              cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    2856              * #eb1 #eo1
    2857              cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
    2858              * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
    2859              lapply (H ???? Hneq (refl ??) (refl ??))
    2860              #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
    2861              #Heq destruct (Heq) whd in match (sem_cmp_mismatch Ceq);
    2862              %{Vfalse} @conj try @refl normalize in Heq; destruct (Heq)
    2863              @vint_eq ]
    2864   | *: #Habsurd destruct (Habsurd) ]
    2865 | 2: (* Inequality *)
    2866   cases (classify_cmp ty ty') normalize nodelta
    2867   [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
    2868   @(value_eq_inversion E … Hvalue_eq1)
    2869   [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ]
    2870   normalize nodelta
    2871   [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ]
    2872   @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
    2873   [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ]
    2874   [ 5: cases sg normalize nodelta
    2875        @intsize_eq_elim_elim
    2876        [ 1,3: #_ #Habsurd destruct (Habsurd)
    2877        | 2,4: #Heq destruct (Heq) normalize nodelta
    2878               [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq)
    2879               | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ]
    2880               /3 by ex_intro, conj, vint_eq/ ]
    2881   | 10: #Heq destruct (Heq) cases (Fcmp Cne f f') /3 by ex_intro, conj, vint_eq/
    2882   | 15: whd in match (sem_cmp_match ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
    2883   | 16,19: whd in match (sem_cmp_mismatch ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
    2884   | 20: lapply (mi_valid_pointers … Hinj p1' p2')
    2885         lapply (mi_valid_pointers … Hinj p1 p2)
    2886         cases (valid_pointer m1 p1')
    2887         [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    2888         cases (valid_pointer m1 p1)
    2889         [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    2890         #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
    2891         >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
    2892         elim p1 in Hembed; #b1 #o1
    2893         elim p1' in Hembed'; #b1' #o1'
    2894         whd in match (pointer_translation ??);
    2895         whd in match (pointer_translation ??);
    2896         @(eq_block_elim … b1 b1')
    2897         [ 1: #Heq destruct (Heq)
    2898               cases (E b1')
    2899               [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
    2900               * #eb1' #eo1' normalize nodelta
    2901               #Heq1 #Heq2 #Heq3 destruct
    2902               >eq_block_identity normalize nodelta
    2903               >neq_offset_translation cases (cmp_offset ???)
    2904               /3 by ex_intro, conj, vint_eq/
    2905         | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
    2906              cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    2907              * #eb1 #eo1
    2908              cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
    2909              * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
    2910              lapply (H ???? Hneq (refl ??) (refl ??))
    2911              #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
    2912              #Heq destruct (Heq) whd in match (sem_cmp_mismatch Cne);
    2913              %{Vtrue} @conj try @refl normalize in Heq; destruct (Heq)
    2914              @vint_eq ]
    2915   | *: #Habsurd destruct (Habsurd) ]
    2916 | 3: (* Less-than *)
    2917  
    2918 | 3: *: @cthulhu ]
    2919 qed.*)
     2887| 3: #fsz
     2888     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
     2889     [ 1: #v #Habsurd destruct (Habsurd)
     2890     | 2: #sz #i #Habsurd destruct (Habsurd)
     2891     | 4: #Habsurd destruct (Habsurd)
     2892     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
     2893     #f
     2894     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2895     [ 1: #v #Habsurd destruct (Habsurd)
     2896     | 2: #sz #i #Habsurd destruct (Habsurd)
     2897     | 4: #Habsurd destruct (Habsurd)
     2898     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
     2899     #f'
     2900     #Heq destruct (Heq) cases (Fcmp op f f')
     2901     /3 by ex_intro, conj, vint_eq/
     2902| 4: #ty1 #ty2 #Habsurd destruct (Habsurd)
     2903| 2: #optn #typ             
     2904     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
     2905     [ 1: #v #Habsurd destruct (Habsurd)
     2906     | 2: #sz #i #Habsurd destruct (Habsurd)
     2907     | 3: #f #Habsurd destruct (Habsurd)
     2908     | 5: #p1 #p2 #Hembed ]
     2909     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     2910     [ 1,6: #v #Habsurd destruct (Habsurd)
     2911     | 2,7: #sz #i #Habsurd destruct (Habsurd)
     2912     | 3,8: #f #Habsurd destruct (Habsurd)
     2913     | 5,10: #p1' #p2' #Hembed' ]
     2914     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
     2915          #Heq destruct (Heq)
     2916          [ 1,3: %{Vfalse} @conj try @refl @vint_eq
     2917          | 2,4: %{Vtrue} @conj try @refl @vint_eq ]
     2918     | 4: cases op whd in match (sem_cmp_match ?);
     2919          #Heq destruct (Heq)
     2920          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
     2921          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
     2922     lapply (mi_valid_pointers … Hinj p1' p2')
     2923     lapply (mi_valid_pointers … Hinj p1 p2)         
     2924     cases (valid_pointer (mk_mem ???) p1')
     2925     [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
     2926     cases (valid_pointer (mk_mem ???) p1)
     2927     [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
     2928     #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
     2929     >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
     2930     elim p1 in Hembed; #b1 #o1
     2931     elim p1' in Hembed'; #b1' #o1'
     2932     whd in match (pointer_translation ??);
     2933     whd in match (pointer_translation ??);
     2934     @(eq_block_elim … b1 b1')
     2935     [ 1: #Heq destruct (Heq)
     2936          cases (E b1') normalize nodelta
     2937          [ 1: #Habsurd destruct (Habsurd) ]
     2938          * #eb1' #eo1' normalize nodelta
     2939          #Heq1 #Heq2 #Heq3 destruct
     2940          >eq_block_identity normalize nodelta
     2941          <cmp_offset_translation
     2942          cases (cmp_offset ???) normalize nodelta         
     2943          /3 by ex_intro, conj, vint_eq/
     2944     | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
     2945          cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
     2946          * #eb1 #eo1
     2947          cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
     2948          * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
     2949          lapply (H ???? Hneq (refl ??) (refl ??))
     2950          #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
     2951          elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
     2952          /3 by ex_intro, conj, vint_eq/
     2953     ]
     2954] qed.               
    29202955 
    29212956(* Commutation result for binary operators. *)
     
    29322967whd in match (sem_binary_operation ??????);
    29332968whd in match (sem_binary_operation ??????);
    2934 @cthulhu
    2935 qed.
     2969[ 1: @add_value_eq try assumption
     2970| 2: @sub_value_eq try assumption
     2971| 3: @mul_value_eq try assumption
     2972| 4: @div_value_eq try assumption
     2973| 5: @mod_value_eq try assumption
     2974| 6: @and_value_eq try assumption
     2975| 7: @or_value_eq try assumption
     2976| 8: @xor_value_eq try assumption
     2977| 9: @shl_value_eq try assumption
     2978| 10: @shr_value_eq try assumption
     2979| *: @cmp_value_eq try assumption
     2980] qed.
    29362981
    29372982 
     
    30393084     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
    30403085           normalize /2/ ]
     3086| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
     3087     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
     3088     cases (exec_expr ge en1 m1 e2) in Hsim2;
     3089     [ 2: #error // ]
     3090     * #val #trace normalize in ⊢ (% → ?); #Hsim2
     3091     elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2
     3092     whd in match (m_bind ?????); whd in match (m_bind ?????);
     3093     lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext))
     3094     cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1)
     3095     [ 1: #_ // ]
     3096     #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq  #Hvalue_eq_opval
     3097     >Hopval_eq normalize destruct /2 by conj/
     3098| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
     3099     #v1 #v2 #trace #Hvalue_eq (* TODO ... *) @cthulhu
    30413100| *: @cthulhu ] qed.
    30423101
Note: See TracChangeset for help on using the changeset viewer.