Changeset 2125 for src/ASM

Timestamp:

Jun 27, 2012, 4:28:11 PM (8 years ago)

Author:

boender

Message:

• some more displacement from Policy to Util

File:

• src/ASM/Util.ma (modified) (1 diff)

src/ASM/Util.ma

@@ -1678 +1678 @@
  ]
 qed.
+
+(* this is in the stdlib, but commented out, why? *)
+theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
+  #n (elim n) normalize /2 by S_pred/ qed.
+  
+(* these lemmas seem superfluous, but not sure how to replace them *)
+lemma double_plus_equal: ∀a,b:ℕ.a + a = b + b → a = b.
+ #a elim a
+ [ normalize #b //
+ | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
+   <plus_n_Sm <plus_n_Sm #H
+   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
+ ]
+qed.
+
+lemma sth_not_s: ∀x.x ≠ S x.
+ #x cases x
+ [ // | #y // ]
+qed.
+  
+lemma le_to_eq_plus: ∀n,z.
+  n ≤ z → ∃k.z = n + k.
+ #n #z elim z
+ [ #H cases (le_to_or_lt_eq … H)
+   [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
+   | #H2 @(ex_intro … 0) >H2 //
+   ]
+ | #z' #Hind #H cases (le_to_or_lt_eq … H)
+   [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
+     >H2 >plus_n_Sm //
+   | #H' @(ex_intro … 0) >H' //
+   ]
+ ]
+qed.
+
+lemma nth_safe_nth: 
+  ∀A:Type[0].∀l:list A.∀i.∀proof:i < |l|.∀x.nth_safe A i l proof = nth i A l x.
+#A #l elim l
+[ #i #prf @⊥ @(absurd ? prf) @le_to_not_lt @le_O_n
+| -l #h #t #Hind #i elim i
+  [ #prf #x normalize @refl
+  | -i #i #Hind2 #prf #x whd in match (nth ????); whd in match (tail ??);
+    whd in match (nth_safe ????); @Hind
+  ]
+]
+qed.
+