Changeset 1159 for src/ASM/Util.ma

Timestamp:

Aug 31, 2011, 12:30:13 PM (8 years ago)

Author:

boender

Message:

• added 'nth' theorems
• moved up \bot a bit

File:

• src/ASM/Util.ma (modified) (3 diffs)

src/ASM/Util.ma

@@ -10 +10 @@
 example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
 example not_implemented: False. cases daemon qed.
+
+notation "⊥" with precedence 90
+  for @{ match ? in False with [ ] }.
 
 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
@@ -614 +617 @@
   ]
 qed.
+
+lemma nth_append_first:
+ ∀A:Type[0].
+ ∀n:nat.∀l1,l2:list A.∀d:A.
+   n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
+ #A #n #l1 #l2 #d
+ generalize in match n; -n; elim l1
+ [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
+ | #h #t #Hind #k normalize
+   cases k -k 
+   [ #Hk normalize @refl
+   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
+   ]  
+ ]
+qed.
+
+lemma nth_append_second: 
+ ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
+  nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
+ #A #n #l1 #l2 #d
+ generalize in match n; -n; elim l1
+ [ normalize #k #Hk <(minus_n_O) @refl
+ | #h #t #Hind #k normalize 
+   cases k -k;
+   [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
+   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
+   ] 
+ ]
+qed.
+
     
 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
@@ -699 +732 @@
 qed.
 
-
-notation "⊥" with precedence 90
-  for @{ match ? in False with [ ] }.
 
 let rec exclusive_disjunction (b: bool) (c: bool) on b ≝