Changeset 2655 for src/joint/joint_semantics.ma
 Timestamp:
 Feb 11, 2013, 4:52:37 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/joint_semantics.ma
r2645 r2655 147 147 fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p) 148 148 bl = Error … [MSG BadFunction]. 149 #F#V#i#p ** # r #id #EQ1destruct149 #F#V#i#p ** #id #EQ1 #EQ2 destruct 150 150 whd in match fetch_internal_function; 151 151 whd in match fetch_function; normalize nodelta … … 398 398  _ ⇒ Error … [MSG NoSuccessor] 399 399 ]. 400 401 lemma deq_elim : ∀A : DeqSet.∀P : bool → Prop.∀x,y : A. 402 (x = y → P true) → (x ≠ y → P false) → P (x == y). 403 #A #P #x #y #H1 #H2 inversion (x == y) #EQ 404 [ @H1 @(proj1 … (eqb_true … ) EQ)  @H2 % #EQ' destruct 405 >(proj2 … (eqb_true …) (refl …)) in EQ; #ABS destruct ] qed. 400 406 401 407 definition eval_seq_no_pc : … … 461 467 elim globals [*] 462 468 #hd #tl #IH #H elim (orb_Prop_true … H) H 463 [@eq_identifier_elim #H * >H %1 % ] 464 #G %2 @IH @G 469 [ @deq_elim #H * destruct %1 %  #H %2{(IH … H)} ] 465 470 qed. 466 471
Note: See TracChangeset
for help on using the changeset viewer.