Changeset 2255 for src/Clight/switchRemoval.ma
- Timestamp:
- Jul 24, 2012, 8:12:00 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2234 r2255 1251 1251 pointer_translation p1 E = Some ? p2 → 1252 1252 value_eq E (Vptr p1) (Vptr p2). 1253 1253 1254 1254 (* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t. 1255 1255 * the values are equivalent. *) … … 1257 1257 λ(E : embedding).λ(m1 : mem).λ(m2 : mem). 1258 1258 ∀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 *) 1260 1260 E b1 = Some ? 〈b2,off2〉 → 1261 1261 load_value_of_type ty m1 b1 off1 = Some ? v1 → 1262 1262 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). 1263 1263 1264 definition 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 1264 1272 (* Definition of a memory injection *) 1265 1273 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝ 1266 1274 { (* Load simulation *) 1267 mi_inj : load_sim E m1 m2;1275 mi_inj : load_sim_ptr E m1 m2; 1268 1276 (* Invalid blocks are not mapped *) 1269 1277 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; 1270 1283 (* 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'; *) 1272 1285 (* Regions are preserved *) 1273 1286 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; … … 1283 1296 1284 1297 (* 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. *) 1286 1300 1287 1301 alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)". … … 1289 1303 record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝ 1290 1304 { me_inj : memory_inj E m1 m2; 1305 (* A list of blocks where we can write freely *) 1291 1306 me_writeable : list block; 1307 (* These blocks are valid *) 1292 1308 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) 1297 1314 }. 1298 1315 … … 1420 1437 #E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq 1421 1438 lapply (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. 1439 lapply (refl ? (access_mode ty)) 1440 cases 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 ] 1443 normalize 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/ ] 1446 lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer 1447 lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H 1448 qed. 1438 1449 1439 1450 … … 1523 1534 | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 1524 1535 | 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 1530 1550 | 4: @(mi_region … Hmemory_inj) 1531 1551 | 5: @(mi_disjoint … Hmemory_inj) … … 1547 1567 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1548 1568 /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 ⊢ (% → ?); #Habsurd1554 (* 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; 1556 1576 #contents_m2 #nextblock_m2 #Hnextblock_m2 1557 1577 whd in ⊢ ((??%?) → ?); 1558 1578 #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) 1560 1583 ] qed. 1561 1584 … … 1618 1641 ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 1619 1642 bestorev mB (mk_pointer wb wo) v = Some ? mC → 1620 load_sim E mA mC.1643 load_sim_ptr E mA mC. 1621 1644 #E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd 1622 1645 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload 1623 (* Show that (wb ≠ b2) *)1624 lapply (me_writeable_ok … Hext …Hvalid Hembed) #Hb21646 (* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *) 1647 lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2 1625 1648 lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2 1626 1649 cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false … … 1642 1665 elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok 1643 1666 #Hmem 1644 [ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj1667 [ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint 1645 1668 whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem) 1646 1669 normalize in ⊢ (% → ?); #Hlt_wb 1670 #p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain 1671 normalize in match (valid_pointer ??) in ⊢ (% → %); 1647 1672 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta 1648 1673 cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb))) … … 1650 1675 [ 2: #Habsurd destruct (Habsurd) ] 1651 1676 #Heq destruct (Heq) 1652 #b #b' #o' #Hembed @(Hcodomain … Hembed) 1677 cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta 1678 [ 2: // ] 1679 whd in match (update_block ?????); 1680 cut (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) 1653 1685 qed. 1654 1686 … … 2711 2743 ] qed. 2712 2744 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'. 2745 lemma 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 *) 2754 lemma 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 2756 elim delta #zdelta @sym_eq @Zplus_eq_eq qed. 2757 2758 lemma 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 2760 elim 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.. *) 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). 2721 2772 @cthulhu qed. 2722 2773 2723 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 (* 2724 2803 lemma sem_cmp_value_eq : 2725 2804 ∀E,v1,v2,v1',v2',ty,ty',m1,m2. … … 2731 2810 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 2732 2811 cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????); 2733 [ 1: 2812 [ 1: (* Equality *) 2734 2813 cases (classify_cmp ty ty') normalize nodelta 2735 2814 [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ] … … 2752 2831 | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) 2753 2832 /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 ] 2755 2864 | *: #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 ] 2919 qed.*) 2758 2920 2759 2921 (* Commutation result for binary operators. *)
Note: See TracChangeset
for help on using the changeset viewer.