- Timestamp:
- Jun 27, 2012, 4:28:11 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r2124 r2125 1678 1678 ] 1679 1679 qed. 1680 1681 (* this is in the stdlib, but commented out, why? *) 1682 theorem 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 *) 1686 lemma 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 ] 1693 qed. 1694 1695 lemma sth_not_s: ∀x.x ≠ S x. 1696 #x cases x 1697 [ // | #y // ] 1698 qed. 1699 1700 lemma 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 ] 1713 qed. 1714 1715 lemma 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 ] 1725 qed. 1726
Note: See TracChangeset
for help on using the changeset viewer.