Changeset 2111 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 26, 2012, 5:30:41 PM (7 years ago)
Author:
sacerdot
Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2055 r2111  
    253253qed.
    254254
     255(*CSC: practically equal to shift_nth_safe but for commutation
     256  of addition. One of the two lemmas should disappear. *)
     257lemma nth_safe_prepend:
     258 ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
     259  nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
     260 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe
     261qed.
     262
     263lemma nth_safe_cons:
     264 ∀A,hd,tl,l2,j,j_ok,Sj_ok.
     265  nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.
     266//
     267qed.
     268
     269lemma eq_nth_safe_proof_irrelevant:
     270 ∀A,l,i,i_ok,i_ok'.
     271  nth_safe A l i i_ok = nth_safe A l i i_ok'.
     272#A #l #i #i_ok #i_ok' %
     273qed.
     274
     275lemma nth_safe_append:
     276 ∀A,l,n,n_ok.
     277  ∃pre,suff.
     278   (pre @ [nth_safe A n l n_ok]) @ suff = l.
     279#A #l elim l normalize
     280 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
     281 | #hd #tl #IH #n cases n normalize
     282   [ #_ %{[]} /2/
     283   | #m #m_ok cases (IH m ?)
     284     [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]
     285qed.
    255286
    256287definition last_safe ≝
Note: See TracChangeset for help on using the changeset viewer.