Changeset 2255


Ignore:
Timestamp:
Jul 24, 2012, 8:12:00 PM (7 years ago)
Author:
garnier
Message:

Had to modify the definition of memory injections to prove that valid_pointer is preserved.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2234 r2255  
    12511251  pointer_translation p1 E = Some ? p2 →
    12521252  value_eq E (Vptr p1) (Vptr p2).
    1253  
     1253
    12541254(* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t.
    12551255 * the values are equivalent. *)
     
    12571257λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
    12581258 ∀b1,off1,b2,off2,ty,v1.
    1259   valid_block m1 b1 →
     1259  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
    12601260  E b1 = Some ? 〈b2,off2〉 →
    12611261  load_value_of_type ty m1 b1 off1 = Some ? v1 →
    12621262  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
    12631263
     1264definition load_sim_ptr ≝
     1265λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
     1266 ∀b1,off1,b2,off2,ty,v1.
     1267  valid_pointer m1 (mk_pointer b1 off1) = true →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
     1268  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
     1269  load_value_of_type ty m1 b1 off1 = Some ? v1 →
     1270  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
     1271
    12641272(* Definition of a memory injection *)
    12651273record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
    12661274{ (* Load simulation *)
    1267   mi_inj : load_sim E m1 m2;
     1275  mi_inj : load_sim_ptr E m1 m2;
    12681276  (* Invalid blocks are not mapped *)
    12691277  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
     1278  (* Valid pointers are mapped to valid pointers*)
     1279  mi_valid_pointers : ∀p,p'.
     1280                       valid_pointer m1 p = true →
     1281                       pointer_translation p E = Some ? p' →
     1282                       valid_pointer m2 p' = true;
    12701283  (* Blocks in the codomain are valid *)
    1271   mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
     1284  (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)
    12721285  (* Regions are preserved *)
    12731286  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
     
    12831296
    12841297(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\
    1285  * A memory extension is a [memory_inj] with some particular blocks designated *)
     1298 * A memory extension is a [memory_inj] with some particular blocks designated as
     1299 * being writeable. *)
    12861300
    12871301alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
     
    12891303record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
    12901304{ me_inj : memory_inj E m1 m2;
     1305  (* A list of blocks where we can write freely *)
    12911306  me_writeable : list block;
     1307  (* These blocks are valid *)
    12921308  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
    1293   me_writeable_ok : ∀b,b',o'.
    1294                     valid_block m1 b →
    1295                     E b = Some ? 〈b',o'〉 →
    1296                     ¬ (meml ? b' me_writeable)
     1309  (* And pointers to m1 are oblivious to these blocks *)
     1310  me_writeable_ok : ∀p,p'.
     1311                     valid_pointer m1 p = true →
     1312                     pointer_translation p E = Some ? p' →
     1313                     ¬ (meml ? (pblock p') me_writeable)
    12971314}.
    12981315
     
    14201437#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
    14211438lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
    1422      normalize in Hembed;
    1423      lapply (mi_inj … Hinj b1 off1)
    1424      cases (E b1) in Hembed;
    1425      [ 1: normalize #Habsurd destruct (Habsurd)
    1426      | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
    1427      lapply (refl ? (access_mode ty))
    1428      cases ty
    1429      [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1430      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
    1431      normalize in ⊢ ((???%) → ?); #Hmode #Hyp
    1432      [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
    1433      | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
    1434      #Hload_success
    1435      lapply (load_by_value_success_valid_block … Hmode … Hload_success)
    1436      #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
    1437 qed.
     1439lapply (refl ? (access_mode ty))
     1440cases ty
     1441[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1442| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1443normalize in ⊢ ((???%) → ?); #Hmode #Hyp
     1444[ 1,7,8: normalize in Hyp; destruct (Hyp)
     1445| 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
     1446lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
     1447lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
     1448qed.     
    14381449
    14391450
     
    15231534  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
    15241535| 2: @(mi_freeblock … Hmemory_inj)
    1525 | 3: #b #b' #o' #HE
    1526      lapply (mi_incl … Hmemory_inj … HE)
    1527      elim m2 in Halloc; #contents #nextblock #Hnextblock
    1528      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    1529      whd in match (valid_block ??) in ⊢ (% → %); /2/
     1536| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
     1537     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
     1538     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
     1539     whd in match (valid_pointer ??) in ⊢ (% → %);
     1540     @Zltb_elim_Type0
     1541     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
     1542     #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
     1543     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
     1544     whd in match (high_bound ??) in ⊢ (% → %);
     1545     whd in match (update_block ?????);
     1546     whd in match (eq_block ??);
     1547     cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
     1548     #Hbid_neq >Hbid_neq
     1549     cases (eq_region br' r) normalize #H @H
    15301550| 4: @(mi_region … Hmemory_inj)
    15311551| 5: @(mi_disjoint … Hmemory_inj)
     
    15471567      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    15481568      /2/
    1549 | 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
    1550      normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
    1551      #Heq destruct (Heq) 
    1552      lapply (mi_incl … Hmemory_inj … Hload)
    1553      whd in ⊢ (% → ?); #Habsurd
    1554      (* contradiction car ¬ (valid_block m2 new_block)  *)
    1555      elim m2 in Halloc Habsurd;
     1569| 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %
     1570     normalize in ⊢ (% → ?); * [ 2: #H @H ]
     1571     #Heq destruct (Heq)
     1572     lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)
     1573     whd in ⊢ (% → ?);
     1574     (* contradiction because ¬ (valid_block m2 new_block)  *)
     1575     elim m2 in Halloc;
    15561576     #contents_m2 #nextblock_m2 #Hnextblock_m2
    15571577     whd in ⊢ ((??%?) → ?);
    15581578     #Heq_alloc destruct (Heq_alloc)
    1559      lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
     1579     normalize
     1580     lapply (irreflexive_Zlt nextblock_m2)
     1581     @Zltb_elim_Type0
     1582     [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)
    15601583] qed.
    15611584
     
    16181641  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
    16191642  bestorev mB (mk_pointer wb wo) v = Some ? mC →
    1620   load_sim E mA mC.
     1643  load_sim_ptr E mA mC.
    16211644#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
    16221645#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
    1623 (* Show that (wb ≠ b2) *)
    1624 lapply (me_writeable_ok … Hext Hvalid Hembed) #Hb2
     1646(* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)
     1647lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2
    16251648lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
    16261649cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
     
    16421665elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
    16431666#Hmem
    1644 [ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
     1667[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint
    16451668whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
    16461669normalize in ⊢ (% → ?); #Hlt_wb
     1670#p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain
     1671normalize in match (valid_pointer ??) in ⊢ (% → %);
    16471672>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
    16481673cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
     
    16501675[ 2: #Habsurd destruct (Habsurd) ]
    16511676#Heq destruct (Heq)
    1652 #b #b' #o' #Hembed @(Hcodomain … Hembed)
     1677cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta
     1678[ 2: // ]
     1679whd in match (update_block ?????);
     1680cut (eq_block (pblock p') wb = false)
     1681[ 2: #Heq >Heq normalize nodelta #H @H ]
     1682@neq_block_eq_block_false @sym_neq
     1683@(mem_not_mem_neq writeable … Hmem)
     1684@(Hwriteable_ok … HvalidA Hembed)
    16531685qed.
    16541686
     
    27112743] qed.
    27122744
    2713 (* We want to prove that, but we can't since valid_pointers can in fact be one off outside the block,
    2714    and [memory_inj] handles only stuff that is loadable (i.e. inside a block). TODO *)
    2715 lemma pointer_eq_valid :
    2716 ∀E,m,m',p,p'.
    2717  memory_inj E m m' →
    2718  pointer_translation p E = Some ? p' →
    2719  valid_pointer m p →
    2720  valid_pointer m' p'.
     2745lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta).
     2746#x #y #delta
     2747@eqZb_elim
     2748[ 1: #Heq >Heq >eqZb_z_z @refl
     2749| 2: * #Hneq cut (x+delta ≠ y + delta)
     2750     [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ]
     2751     #H @sym_eq @eqZb_false @H ] qed.
     2752
     2753(* offset equality is invariant by translation *)
     2754lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
     2755#delta #x #y normalize
     2756elim delta #zdelta @sym_eq @Zplus_eq_eq qed.
     2757
     2758lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
     2759#delta #x #y normalize
     2760elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed.
     2761
     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.. *)
     2765lemma 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).
    27212772@cthulhu qed.
    27222773
    2723 
     2774(*           
     2775#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
     2776elim m1 in Hinj; #contents_map1 #nextblock1 #Hnextblock1 #Hinj
     2777cases op whd in match (sem_cmp ??????) in ⊢ (% → ?);
     2778cases (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(*
    27242803lemma sem_cmp_value_eq :
    27252804  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
     
    27312810#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
    27322811cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????);
    2733 [ 1:
     2812[ 1: (* Equality *)
    27342813  cases (classify_cmp ty ty') normalize nodelta
    27352814  [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ]
     
    27522831  | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
    27532832        /3 by ex_intro, conj, vint_eq/
    2754   | 20: @cthulhu (* relies on [pointer_eq_valid] TODO *)   
     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 ]
    27552864  | *: #Habsurd destruct (Habsurd) ]
    2756 | *: @cthulhu ]
    2757 qed.
     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 ]
     2919qed.*)
    27582920 
    27592921(* Commutation result for binary operators. *)
Note: See TracChangeset for help on using the changeset viewer.