Changeset 972 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 16, 2011, 12:22:57 AM (8 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/AssemblyProof.ma (modified) (2 diffs)

src/ASM/AssemblyProof.ma

@@ -1006 +1006 @@
 qed.
 
+lemma does_not_occur_absurd:
+ ∀id,i,list_instr.
+  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
+ #id #i #list_instr elim list_instr
+  [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
+    >eq_bv_refl %
+  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
+qed.
+
 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
  match l with
@@ -1054 +1063 @@
      [ #H @ (IH H)
      | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
-       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv 16 x id) normalize nodelta;
-       [ #H  | #H @IH @H]
+       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
+       [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
+        /2/ #H >does_not_occur_Some //
+       | #H @IH @H]]]
 qed.