Ignore:
Timestamp:
Feb 11, 2013, 4:52:37 PM (8 years ago)
Author:
tranquil
Message:

new step in code semantic lemma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2645 r2655  
    147147  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    148148    bl = Error … [MSG BadFunction].
    149  #F#V#i#p ** #r #id #EQ1 destruct
     149 #F#V#i#p ** #id #EQ1 #EQ2 destruct
    150150 whd in match fetch_internal_function;
    151151  whd in match fetch_function; normalize nodelta
     
    398398  | _ ⇒ Error … [MSG NoSuccessor]
    399399  ].
     400
     401lemma 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.
    400406
    401407definition eval_seq_no_pc :
     
    461467  elim globals [*]
    462468  #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)} ]
    465470qed.
    466471
Note: See TracChangeset for help on using the changeset viewer.