Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r1545 r1882  
    118118 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
    119119qed.
     120
     121lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
     122  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
     123#P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1
     124#Ptrue #Pfalse
     125whd in match (eq_pointer ??);
     126@eq_region_elim #reg_eq
     127[ @eq_block_elim #block_eq
     128  [ change with (eqZb ??) in match (eq_offset ??);
     129    @eqZb_elim #offset_eq
     130    [ destruct @Ptrue %
     131    ]
     132  ]
     133]
     134@Pfalse % #EQ destruct /2 by absurd/
     135qed.
Note: See TracChangeset for help on using the changeset viewer.