Changeset 2055 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 13, 2012, 12:11:21 PM (7 years ago)
Author:
sacerdot
Message:

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2037 r2055  
    225225  ]
    226226qed.
     227
     228lemma shift_nth_safe:
     229 ∀T,i,l2,l1,K1,K2.
     230  nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
     231 #T #i #l2 elim l2 normalize
     232  [ #l1 #K1 <plus_n_O #K2 %
     233  | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
     234    whd in ⊢ (???%); @IH ]
     235qed.
     236
     237lemma shift_nth_prefix:
     238 ∀T,l1,i,l2,K1,K2.
     239  nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.
     240  #T #l1 elim l1 normalize
     241  [
     242    #i #l1 #K1 cases(lt_to_not_zero … K1)
     243  |
     244    #hd #tl #IH #i #l2
     245    cases i
     246    [
     247      //
     248    |
     249      #i' #K1 #K2 whd in ⊢ (??%%);
     250      @IH
     251    ]
     252  ]
     253qed.
     254
    227255
    228256definition last_safe ≝
Note: See TracChangeset for help on using the changeset viewer.