Changeset 2470 for src/joint/semanticsUtils.ma
 Timestamp:
 Nov 15, 2012, 7:06:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils.ma
r2457 r2470 67 67 (******************************** GRAPHS **************************************) 68 68 69 definition bitvector_from_pos :70 ∀n.Pos → BitVector n ≝71 λn,p.bitvector_of_Z n (Zpred (pos p)).72 73 definition pos_from_bitvector :74 ∀n.BitVector n → Pos ≝75 λn,v.76 match Zsucc (Z_of_unsigned_bitvector n v)77 return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?78 with79 [ OZ ⇒ λprf.⊥80  pos x ⇒ λ_. x81  neg x ⇒ λprf.⊥82 ] (refl …).83 @hide_prf84 elim v in prf;85 [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.86 87 lemma pos_pos_from_bitvector :88 ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).89 #n #bv elim bv n90 [ %91  #n * #bv #IH [ %  @IH ]92 ]93 qed.94 95 lemma bitvector_from_pos_from_bitvector :96 ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.97 #n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector98 >Zpred_Zsucc //99 qed.100 101 lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.102 (∀q,r.103 ppos m = natp_plus (natp_times q (ppos n)) r →104 natp_lt r n →105 P (〈q,r〉)) →106 P (divide m n).107 #P #m #n #H108 lapply (refl … (divide m n))109 cases (divide ??) in ⊢ (???%→%);110 #q #r #EQ elim (divide_ok … EQ) EQ @H111 qed.112 113 lemma lt_divisor_to_eq_mod : ∀p,q : Pos.114 p < q → \snd (divide p q) = ppos p.115 #p #q #H @divide_elim * [2: #quot ]116 * [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]117 @⊥ elim (lt_to_not_le ?? H) #H @H H H118 [ @(transitive_le … (quot*q)) ] /2 by /119 qed.120 121 lemma pos_from_bitvector_from_pos :122 ∀n,p.123 p ≤ two_power_nat n →124 pos_from_bitvector n (bitvector_from_pos n p) = p.125 #n #p #H126 cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)127 [2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]128 >pos_pos_from_bitvector129 whd in match (bitvector_from_pos ??);130 >Z_of_unsigned_bitvector_of_Z131 cases p in H ⊢ %;132 [ #_ %133 *: #p' #H134 whd in match (Zpred ?);135 whd in match (Z_two_power_nat ?);136 whd in ⊢ (??(?%)?);137 >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]138 whd139 <succ_pred_n try assumption % #ABS destruct(ABS)140 ]141 qed.142 143 lemma pos_from_bitvector_max : ∀n,bv.144 pos_from_bitvector n bv ≤ two_power_nat n.145 #n #bv146 change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)147 >pos_pos_from_bitvector148 @Zlt_to_Zle149 @bv_Z_unsigned_max150 qed.151 152 definition graph_offset_of_label : label → option offset ≝153 λl.let p ≝ word_of_identifier … l in154 if leb p (two_power_nat offset_size) then155 return mk_offset (bitvector_from_pos … p)156 else157 None ?.158 159 definition graph_label_of_offset: offset → label ≝160 λo.an_identifier ? (pos_from_bitvector ? (offv o)).161 162 69 definition make_sem_graph_params : 163 70 ∀pars : unserialized_params. … … 171 78 g_pars 172 79 (spars ?) 173 graph_offset_of_label174 graph_label_of_offset175 ? ?80 (word_of_identifier ?) 81 (an_identifier ?) 82 ? (refl …) 176 83 ). 177 whd in match graph_label_of_offset; 178 whd in match graph_offset_of_label; 179 whd in match word_of_identifier; 180 normalize nodelta * #x 181 @(leb_elim ? (two_power_nat ?)) normalize nodelta 182 [ #_ >bitvector_from_pos_from_bitvector % 183  #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max 184  #H whd >(pos_from_bitvector_from_pos … H) % 185  #_ % 186 ] 187 qed. 84 * #p % qed. 188 85 189 86 (******************************** LINEAR **************************************) 190 87 191 definition lin_offset_of_nat : ℕ → option offset ≝ 192 λn. 193 if leb (S n) (2^offset_size) then 194 return mk_offset (bitvector_of_nat ? n) 195 else 196 None ?. 88 lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p. 89 @pos_elim [%] 90 #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed. 197 91 198 definition lin_nat_of_offset : offset → ℕ ≝199 λo.nat_of_bitvector ? (offv o).200 92 201 93 definition make_sem_lin_params : … … 210 102 lin_pars 211 103 (spars ?) 212 lin_offset_of_nat213 lin_nat_of_offset104 succ_pos_of_nat 105 (λp.pred (nat_of_pos p)) 214 106 ?? 215 107 ). 216 [ * ] #x 217 whd in match lin_offset_of_nat; 218 whd in match lin_nat_of_offset; 219 normalize nodelta 220 @leb_elim normalize nodelta #H 221 [ >bitvector_of_nat_inverse_nat_of_bitvector % 222  @⊥ cases H #H @H H H // 223  whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) % 224  % 225 ] 226 qed. 108 [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 109  #n >nat_succ_pos % 110 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.