Changeset 2125


Ignore:
Timestamp:
Jun 27, 2012, 4:28:11 PM (5 years ago)
Author:
boender
Message:
  • some more displacement from Policy to Util
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2124 r2125  
    16781678 ]
    16791679qed.
     1680
     1681(* this is in the stdlib, but commented out, why? *)
     1682theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
     1683  #n (elim n) normalize /2 by S_pred/ qed.
     1684 
     1685(* these lemmas seem superfluous, but not sure how to replace them *)
     1686lemma double_plus_equal: ∀a,b:ℕ.a + a = b + b → a = b.
     1687 #a elim a
     1688 [ normalize #b //
     1689 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
     1690   <plus_n_Sm <plus_n_Sm #H
     1691   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
     1692 ]
     1693qed.
     1694
     1695lemma sth_not_s: ∀x.x ≠ S x.
     1696 #x cases x
     1697 [ // | #y // ]
     1698qed.
     1699 
     1700lemma le_to_eq_plus: ∀n,z.
     1701  n ≤ z → ∃k.z = n + k.
     1702 #n #z elim z
     1703 [ #H cases (le_to_or_lt_eq … H)
     1704   [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
     1705   | #H2 @(ex_intro … 0) >H2 //
     1706   ]
     1707 | #z' #Hind #H cases (le_to_or_lt_eq … H)
     1708   [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
     1709     >H2 >plus_n_Sm //
     1710   | #H' @(ex_intro … 0) >H' //
     1711   ]
     1712 ]
     1713qed.
     1714
     1715lemma nth_safe_nth:
     1716  ∀A:Type[0].∀l:list A.∀i.∀proof:i < |l|.∀x.nth_safe A i l proof = nth i A l x.
     1717#A #l elim l
     1718[ #i #prf @⊥ @(absurd ? prf) @le_to_not_lt @le_O_n
     1719| -l #h #t #Hind #i elim i
     1720  [ #prf #x normalize @refl
     1721  | -i #i #Hind2 #prf #x whd in match (nth ????); whd in match (tail ??);
     1722    whd in match (nth_safe ????); @Hind
     1723  ]
     1724]
     1725qed.
     1726
Note: See TracChangeset for help on using the changeset viewer.