Changeset 1037 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 23, 2011, 2:56:20 AM (10 years ago)

Author:

sacerdot

Message:

Main theorem: comments are working again.

File:

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

src/ASM/AssemblyProof.ma

@@ -1980 +1980 @@
         pbu)).
 
+lemma Some_Some_elim:
+ ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
+ #T #x #y #P #H #K @H @option_destruct_Some // 
+qed.
+
 theorem main_thm:
  ∀M,M',ps,pol.
@@ -2030 +2035 @@
  change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
  >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
- 
- XX
- 
- whd in match execute_1_pseudo_instruction
- 
- whd in match expand_pseudo_instruction  normalize nodelta; 
- whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0
- normalize in match (\snd 〈preamble,instr_list〉);
- cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ %
- #pi #newppc normalize nodelta; #MAP
- cases pi in MAP; normalize nodelta;
-  [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0]
-    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
-    (*
-    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i
-n H2; whd in ⊢ (% → ?)
-    #H2*) >(eq_bv_eq … H2) >EQ %
+ whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta
+ generalize in match H1; -H1; generalize in match instructions -instructions
+ * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi
+ whd in match ticks_of normalize nodelta <EQ1 >EQ2
+ cases pi in SAFE
+  [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?)
+   @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
+   whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
+   #H2 #EQ %[1,3:@0]
+   <MAP >(eq_bv_eq … H2) >EQ %
 
 lemma main_thm0: