Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (9 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r2122 r2124  
    3737qed.
    3838
    39 (*CSC: move elsewhere *)
    40 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
    41   λa, b: addressing_mode.
    42   match a with
    43   [ DIRECT d ⇒
    44     match b with
    45     [ DIRECT e ⇒ eq_bv ? d e
    46     | _ ⇒ false
    47     ]
    48   | INDIRECT b' ⇒
    49     match b with
    50     [ INDIRECT e ⇒ eq_b b' e
    51     | _ ⇒ false
    52     ]
    53   | EXT_INDIRECT b' ⇒
    54     match b with
    55     [ EXT_INDIRECT e ⇒ eq_b b' e
    56     | _ ⇒ false
    57     ]
    58   | REGISTER bv ⇒
    59     match b with
    60     [ REGISTER bv' ⇒ eq_bv ? bv bv'
    61     | _ ⇒ false
    62     ]
    63   | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
    64   | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
    65   | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
    66   | DATA b' ⇒
    67     match b with
    68     [ DATA e ⇒ eq_bv ? b' e
    69     | _ ⇒ false
    70     ]
    71   | DATA16 w ⇒
    72     match b with
    73     [ DATA16 e ⇒ eq_bv ? w e
    74     | _ ⇒ false
    75     ]
    76   | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
    77   | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
    78   | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
    79   | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
    80   | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
    81   | BIT_ADDR b' ⇒
    82     match b with
    83     [ BIT_ADDR e ⇒ eq_bv ? b' e
    84     | _ ⇒ false
    85     ]
    86   | N_BIT_ADDR b' ⇒
    87     match b with
    88     [ N_BIT_ADDR e ⇒ eq_bv ? b' e
    89     | _ ⇒ false
    90     ]
    91   | RELATIVE n ⇒
    92     match b with
    93     [ RELATIVE e ⇒ eq_bv ? n e
    94     | _ ⇒ false
    95     ]
    96   | ADDR11 w ⇒
    97     match b with
    98     [ ADDR11 e ⇒ eq_bv ? w e
    99     | _ ⇒ false
    100     ]
    101   | ADDR16 w ⇒
    102     match b with
    103     [ ADDR16 e ⇒ eq_bv ? w e
    104     | _ ⇒ false
    105     ]
    106   ].
    107 
    108 (*CSC: move elsewhere *)
    109 lemma eq_addressing_mode_refl:
    110   ∀a. eq_addressing_mode a a = true.
    111   #a
    112   cases a try #arg1 try #arg2
    113   try @eq_bv_refl try @eq_b_refl
    114   try normalize %
    115 qed.
    116  
    117 (*CSC: move elsewhere *)
    118 definition eq_sum:
    119     ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
    120   λlt, rt, leq, req, left, right.
    121     match left with
    122     [ inl l ⇒
    123       match right with
    124       [ inl l' ⇒ leq l l'
    125       | _ ⇒ false
    126       ]
    127     | inr r ⇒
    128       match right with
    129       [ inr r' ⇒ req r r'
    130       | _ ⇒ false
    131       ]
    132     ].
    133 
    134 (*CSC: move elsewhere *)
    135 definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
    136   λlt, rt, leq, req, left, right.
    137     let 〈l, r〉 ≝ left in
    138     let 〈l', r'〉 ≝ right in
    139       leq l l' ∧ req r r'.
    140 
    141 (*CSC: move elsewhere *)
    142 definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
    143   λi, j.
    144   match i with
    145   [ ADD arg1 arg2 ⇒
    146     match j with
    147     [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    148     | _ ⇒ false
    149     ]
    150   | ADDC arg1 arg2 ⇒
    151     match j with
    152     [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    153     | _ ⇒ false
    154     ]
    155   | SUBB arg1 arg2 ⇒
    156     match j with
    157     [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    158     | _ ⇒ false
    159     ]
    160   | INC arg ⇒
    161     match j with
    162     [ INC arg' ⇒ eq_addressing_mode arg arg'
    163     | _ ⇒ false
    164     ]
    165   | DEC arg ⇒
    166     match j with
    167     [ DEC arg' ⇒ eq_addressing_mode arg arg'
    168     | _ ⇒ false
    169     ]
    170   | MUL arg1 arg2 ⇒
    171     match j with
    172     [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    173     | _ ⇒ false
    174     ]
    175   | DIV arg1 arg2 ⇒
    176     match j with
    177     [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    178     | _ ⇒ false
    179     ]
    180   | DA arg ⇒
    181     match j with
    182     [ DA arg' ⇒ eq_addressing_mode arg arg'
    183     | _ ⇒ false
    184     ]
    185   | JC arg ⇒
    186     match j with
    187     [ JC arg' ⇒ eq_addressing_mode arg arg'
    188     | _ ⇒ false
    189     ]
    190   | JNC arg ⇒
    191     match j with
    192     [ JNC arg' ⇒ eq_addressing_mode arg arg'
    193     | _ ⇒ false
    194     ]
    195   | JB arg1 arg2 ⇒
    196     match j with
    197     [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    198     | _ ⇒ false
    199     ]
    200   | JNB arg1 arg2 ⇒
    201     match j with
    202     [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    203     | _ ⇒ false
    204     ]
    205   | JBC arg1 arg2 ⇒
    206     match j with
    207     [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    208     | _ ⇒ false
    209     ]
    210   | JZ arg ⇒
    211     match j with
    212     [ JZ arg' ⇒ eq_addressing_mode arg arg'
    213     | _ ⇒ false
    214     ]
    215   | JNZ arg ⇒
    216     match j with
    217     [ JNZ arg' ⇒ eq_addressing_mode arg arg'
    218     | _ ⇒ false
    219     ]
    220   | CJNE arg1 arg2 ⇒
    221     match j with
    222     [ CJNE arg1' arg2' ⇒
    223       let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
    224       let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
    225       let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    226         arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    227     | _ ⇒ false
    228     ]
    229   | DJNZ arg1 arg2 ⇒
    230     match j with
    231     [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    232     | _ ⇒ false
    233     ]
    234   | CLR arg ⇒
    235     match j with
    236     [ CLR arg' ⇒ eq_addressing_mode arg arg'
    237     | _ ⇒ false
    238     ]
    239   | CPL arg ⇒
    240     match j with
    241     [ CPL arg' ⇒ eq_addressing_mode arg arg'
    242     | _ ⇒ false
    243     ]
    244   | RL arg ⇒
    245     match j with
    246     [ RL arg' ⇒ eq_addressing_mode arg arg'
    247     | _ ⇒ false
    248     ]
    249   | RLC arg ⇒
    250     match j with
    251     [ RLC arg' ⇒ eq_addressing_mode arg arg'
    252     | _ ⇒ false
    253     ]
    254   | RR arg ⇒
    255     match j with
    256     [ RR arg' ⇒ eq_addressing_mode arg arg'
    257     | _ ⇒ false
    258     ]
    259   | RRC arg ⇒
    260     match j with
    261     [ RRC arg' ⇒ eq_addressing_mode arg arg'
    262     | _ ⇒ false
    263     ]
    264   | SWAP arg ⇒
    265     match j with
    266     [ SWAP arg' ⇒ eq_addressing_mode arg arg'
    267     | _ ⇒ false
    268     ]
    269   | SETB arg ⇒
    270     match j with
    271     [ SETB arg' ⇒ eq_addressing_mode arg arg'
    272     | _ ⇒ false
    273     ]
    274   | PUSH arg ⇒
    275     match j with
    276     [ PUSH arg' ⇒ eq_addressing_mode arg arg'
    277     | _ ⇒ false
    278     ]
    279   | POP arg ⇒
    280     match j with
    281     [ POP arg' ⇒ eq_addressing_mode arg arg'
    282     | _ ⇒ false
    283     ]
    284   | XCH arg1 arg2 ⇒
    285     match j with
    286     [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    287     | _ ⇒ false
    288     ]
    289   | XCHD arg1 arg2 ⇒
    290     match j with
    291     [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    292     | _ ⇒ false
    293     ]
    294   | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
    295   | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
    296   | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
    297   | MOVX arg ⇒
    298     match j with
    299     [ MOVX arg' ⇒
    300       let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
    301       let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
    302       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    303         sum_eq arg arg'
    304     | _ ⇒ false
    305     ]
    306   | XRL arg ⇒
    307     match j with
    308     [ XRL arg' ⇒
    309       let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
    310       let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
    311       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    312         sum_eq arg arg'
    313     | _ ⇒ false
    314     ]
    315   | ORL arg ⇒
    316     match j with
    317     [ ORL arg' ⇒
    318       let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
    319       let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
    320       let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
    321       let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
    322       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    323         sum_eq arg arg'
    324     | _ ⇒ false
    325     ]
    326   | ANL arg ⇒
    327     match j with
    328     [ ANL arg' ⇒
    329       let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
    330       let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
    331       let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
    332       let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
    333       let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
    334         sum_eq arg arg'
    335     | _ ⇒ false
    336     ]
    337   | MOV arg ⇒
    338     match j with
    339     [ MOV arg' ⇒
    340       let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
    341       let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
    342       let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
    343       let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
    344       let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
    345       let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
    346       let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
    347       let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
    348       let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
    349       let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
    350       let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
    351         sum_eq_5 arg arg'
    352     | _ ⇒ false
    353     ]
    354   ].
    355 
    356 (*CSC: move elsewhere *)
    357 lemma eq_sum_refl:
    358   ∀A, B: Type[0].
    359   ∀leq, req.
    360   ∀s.
    361   ∀leq_refl: (∀t. leq t t = true).
    362   ∀req_refl: (∀u. req u u = true).
    363     eq_sum A B leq req s s = true.
    364   #A #B #leq #req #s #leq_refl #req_refl
    365   cases s assumption
    366 qed.
    367 
    368 (*CSC: move elsewhere *)
    369 lemma eq_prod_refl:
    370   ∀A, B: Type[0].
    371   ∀leq, req.
    372   ∀s.
    373   ∀leq_refl: (∀t. leq t t = true).
    374   ∀req_refl: (∀u. req u u = true).
    375     eq_prod A B leq req s s = true.
    376   #A #B #leq #req #s #leq_refl #req_refl
    377   cases s
    378   whd in ⊢ (? → ? → ??%?);
    379   #l #r
    380   >leq_refl @req_refl
    381 qed.
    382 
    383 (*CSC: move elsewhere *)
    384 lemma eq_preinstruction_refl:
    385   ∀i.
    386     eq_preinstruction i i = true.
    387   #i cases i try #arg1 try #arg2
    388   try @eq_addressing_mode_refl
    389   [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    390     whd in ⊢ (??%?); try %
    391     >eq_addressing_mode_refl
    392     >eq_addressing_mode_refl %
    393   |13,15:
    394     whd in ⊢ (??%?);
    395     cases arg1
    396     [*:
    397       #arg1_left normalize nodelta
    398       >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
    399     ]
    400   |11,12:
    401     whd in ⊢ (??%?);
    402     cases arg1
    403     [1:
    404       #arg1_left normalize nodelta
    405       >(eq_sum_refl …)
    406       [1: % | 2,3: #arg @eq_prod_refl ]
    407       @eq_addressing_mode_refl
    408     |2:
    409       #arg1_left normalize nodelta
    410       @eq_prod_refl [*: @eq_addressing_mode_refl ]
    411     |3:
    412       #arg1_left normalize nodelta
    413       >(eq_sum_refl …)
    414       [1:
    415         %
    416       |2,3:
    417         #arg @eq_prod_refl #arg @eq_addressing_mode_refl
    418       ]
    419     |4:
    420       #arg1_left normalize nodelta
    421       @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
    422     ]
    423   |14:
    424     whd in ⊢ (??%?);
    425     cases arg1
    426     [1:
    427       #arg1_left normalize nodelta
    428       @eq_sum_refl
    429       [1:
    430         #arg @eq_sum_refl
    431         [1:
    432           #arg @eq_sum_refl
    433           [1:
    434             #arg @eq_sum_refl
    435             [1:
    436               #arg @eq_prod_refl
    437               [*:
    438                 @eq_addressing_mode_refl
    439               ]
    440             |2:
    441               #arg @eq_prod_refl
    442               [*:
    443                 #arg @eq_addressing_mode_refl
    444               ]
    445             ]
    446           |2:
    447             #arg @eq_prod_refl
    448             [*:
    449               #arg @eq_addressing_mode_refl
    450             ]
    451           ]
    452         |2:
    453           #arg @eq_prod_refl
    454           [*:
    455             #arg @eq_addressing_mode_refl
    456           ]
    457         ]
    458       |2:
    459         #arg @eq_prod_refl
    460         [*:
    461           #arg @eq_addressing_mode_refl
    462         ]
    463       ]
    464     |2:
    465       #arg1_right normalize nodelta
    466       @eq_prod_refl
    467       [*:
    468         #arg @eq_addressing_mode_refl
    469       ]
    470     ]
    471   |*:
    472     whd in ⊢ (??%?);
    473     cases arg1
    474     [*:
    475       #arg1 >eq_sum_refl
    476       [1,4:
    477         @eq_addressing_mode_refl
    478       |2,3,5,6:
    479         #arg @eq_prod_refl
    480         [*:
    481           #arg @eq_addressing_mode_refl
    482         ]
    483       ]
    484     ]
    485   ]
    486 qed.
    487 
    488 (*CSC: move elsewhere *)
    489 definition eq_instruction: instruction → instruction → bool ≝
    490   λi, j.
    491   match i with
    492   [ ACALL arg ⇒
    493     match j with
    494     [ ACALL arg' ⇒ eq_addressing_mode arg arg'
    495     | _ ⇒ false
    496     ]
    497   | LCALL arg ⇒
    498     match j with
    499     [ LCALL arg' ⇒ eq_addressing_mode arg arg'
    500     | _ ⇒ false
    501     ]
    502   | AJMP arg ⇒
    503     match j with
    504     [ AJMP arg' ⇒ eq_addressing_mode arg arg'
    505     | _ ⇒ false
    506     ]
    507   | LJMP arg ⇒
    508     match j with
    509     [ LJMP arg' ⇒ eq_addressing_mode arg arg'
    510     | _ ⇒ false
    511     ]
    512   | SJMP arg ⇒
    513     match j with
    514     [ SJMP arg' ⇒ eq_addressing_mode arg arg'
    515     | _ ⇒ false
    516     ]
    517   | JMP arg ⇒
    518     match j with
    519     [ JMP arg' ⇒ eq_addressing_mode arg arg'
    520     | _ ⇒ false
    521     ]
    522   | MOVC arg1 arg2 ⇒
    523     match j with
    524     [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    525     | _ ⇒ false
    526     ]
    527   | RealInstruction instr ⇒
    528     match j with
    529     [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
    530     | _ ⇒ false
    531     ]
    532   ].
    533  
    534 (*CSC: move elsewhere *)
    535 lemma eq_instruction_refl:
    536   ∀i. eq_instruction i i = true.
    537   #i cases i [*: #arg1 ]
    538   try @eq_addressing_mode_refl
    539   try @eq_preinstruction_refl
    540   #arg2 whd in ⊢ (??%?);
    541   >eq_addressing_mode_refl >eq_addressing_mode_refl %
    542 qed.
    543 
    544 (*CSC: in is_a_to_mem_to_is_in use vect_member in place of mem … *)
    545 definition vect_member ≝
    546  λA,n,eq,v,a. mem A eq (S n) v a.
    547 
    548 (*CSC: move elsewhere*)
    549 definition is_in_cons_elim:
    550  ∀len.∀hd,tl.∀m:addressing_mode
    551   .is_in (S len) (hd:::tl) m →
    552     (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
    553  #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
    554  cases (is_a hd am) in ISIN; /2/
    555 qed.
    556 
    557 (*CSC: move elsewhere*)
    558 lemma prod_eq_left:
    559   ∀A: Type[0].
    560   ∀p, q, r: A.
    561     p = q → 〈p, r〉 = 〈q, r〉.
    562   #A #p #q #r #hyp
    563   destruct %
    564 qed.
    565 
    566 (*CSC: move elsewhere*)
    567 lemma prod_eq_right:
    568   ∀A: Type[0].
    569   ∀p, q, r: A.
    570     p = q → 〈r, p〉 = 〈r, q〉.
    571   #A #p #q #r #hyp
    572   destruct %
    573 qed.
    574 
    57539let rec encoding_check
    57640  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    … …  
    58347      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
    58448  ].
    585 
    586 (*CSC: move elsewhere *)
    587 lemma add_bitvector_of_nat_Sm:
    588   ∀n, m: nat.
    589     add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
    590       bitvector_of_nat n (S m).
    591  #n #m @add_bitvector_of_nat_plus
    592 qed.
    59349
    59450lemma encoding_check_append:
    … …  
    62278    ]
    62379  ]
    624 qed.
    625 
    626 (*CSC: move elsewhere*)
    627 lemma destruct_bug_fix_1:
    628   ∀n: nat.
    629     S n = 0 → False.
    630   #n #absurd destruct(absurd)
    631 qed.
    632 
    633 (*CSC: move elsewhere*)
    634 lemma destruct_bug_fix_2:
    635   ∀m, n: nat.
    636     S m = S n → m = n.
    637   #m #n #refl destruct %
    638 qed.
    639 
    640 (*CSC: move elsewhere*)
    641 definition bitvector_3_cases:
    642   ∀b: BitVector 3.
    643     ∃l, c, r: bool.
    644       b ≃ [[l; c; r]].
    645   #b
    646   @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
    647   [1:
    648     #absurd @⊥ -b @(destruct_bug_fix_1 2)
    649     >absurd %
    650   |2:
    651     #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
    652     cut (n = 2)
    653     [1:
    654       @destruct_bug_fix_2
    655       >size_refl %
    656     |2:
    657       #n_refl >n_refl in tl; #V
    658       @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
    659       [1:
    660         #absurd @⊥ -V @(destruct_bug_fix_1 1)
    661         >absurd %
    662       |2:
    663         #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
    664         cut (n' = 1)
    665         [1:
    666           @destruct_bug_fix_2 >size_refl' %
    667         |2:
    668           #n_refl' >n_refl' in tl'; #V'
    669           @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
    670           [1:
    671             #absurd @⊥ -V' @(destruct_bug_fix_1 0)
    672             >absurd %
    673           |2:
    674             #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
    675             cut (n'' = 0)
    676             [1:
    677               @destruct_bug_fix_2 >size_refl'' %
    678             |2:
    679               #n_refl'' >n_refl'' in tl''; #tl'''
    680               >(Vector_O … tl''') %
    681             ]
    682           ]
    683         ]
    684       ]
    685     ]
    686   ]
    687 qed.
    688 
    689 (*CSC: move elsewhere*)
    690 lemma bitvector_3_elim_prop:
    691   ∀P: BitVector 3 → Prop.
    692     P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
    693     P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
    694     P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
    695   #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
    696   cases (bitvector_3_cases … H9) #l #assm cases assm
    697   -assm #c #assm cases assm
    698   -assm #r #assm cases assm destruct
    699   cases l cases c cases r assumption
    70080qed.
    70181
    … …  
    750130        fetch_many code_memory final_pc pc' tl)
    751131  ].
    752 
    753 (*CSC: move elsewhere*)
    754 lemma option_destruct_Some:
    755   ∀A: Type[0].
    756   ∀a, b: A.
    757     Some A a = Some A b → a = b.
    758   #A #a #b #EQ
    759   destruct %
    760 qed.
    761 
    762 (*CSC: move elsewhere*)
    763 lemma eq_instruction_to_eq:
    764   ∀i1, i2: instruction.
    765     eq_instruction i1 i2 = true → i1 ≃ i2.
    766   #i1 #i2
    767   cases i1 cases i2 cases daemon (* easy but tedious
    768   [1,10,19,28,37,46:
    769     #arg1 #arg2
    770     whd in match (eq_instruction ??);
    771     cases arg1 #subaddressing_mode
    772     cases subaddressing_mode
    773     try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    774     try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    775     try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
    776     #word11 #irrelevant
    777     cases arg2 #subaddressing_mode
    778     cases subaddressing_mode
    779     try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    780     try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    781     try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
    782     #word11' #irrelevant normalize nodelta
    783     #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
    784 qed.
    785132         
    786133lemma fetch_assembly_pseudo':
    … …  
    1429776     ticks_of0 program sigma policy ppc fetched.
    1430777
    1431 (*CSC: move elsewhere*)
    1432 lemma eq_rect_Type1_r:
    1433   ∀A: Type[1].
    1434   ∀a: A.
    1435   ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    1436   #A #a #P #H #x #p
    1437   generalize in match H;
    1438   generalize in match P;
    1439   cases p //
    1440 qed.
    1441 
    1442778(*
    1443779lemma blah:
    … …  
    1569905*)
    1570906
    1571 (*CSC: move elsewhere*)
    1572 lemma Some_Some_elim:
    1573  ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
    1574  #T #x #y #P #H #K @H @option_destruct_Some //
    1575 qed.
    1576 
    1577 (*CSC: move elsewhere*)
    1578 lemma pair_destruct_right:
    1579   ∀A: Type[0].
    1580   ∀B: Type[0].
    1581   ∀a, c: A.
    1582   ∀b, d: B.
    1583     〈a, b〉 = 〈c, d〉 → b = d.
    1584   #A #B #a #b #c #d //
    1585 qed.
    1586    
    1587907(*CSC: ???*)
    1588908(* XXX: we need a precondition here stating that the PPC is within the
    … …  
    1633953  @pair_elim #lbl #instr #nth_refl normalize nodelta
    1634954  #G cases (pair_destruct_right ?????? G) %
    1635 qed.
    1636 
    1637 (*CSC: move elsewhere*)
    1638 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
    1639   /2/
    1640955qed.
    1641956
Note: See TracChangeset for help on using the changeset viewer.