Ignore:
Timestamp:
Dec 3, 2010, 11:52:05 PM (9 years ago)
Author:
sacerdot
Message:

No more axioms! All proofs completed.
(Interrupts, I/O and timers not ported to Matita yet)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Interpret.ma

    r370 r372  
    88nlemma inclusive_disjunction_true:
    99  ∀b, c: Bool.
    10     ((inclusive_disjunction b c) = true) → ((b = true) ∨ (c = true)).
     10    inclusive_disjunction b c = true → b = true ∨ c = true.
    1111  #b c;
    1212  nelim b
     
    1414  ##| nnormalize; /2/;
    1515  ##]
     16nqed.
     17
     18nlemma conjunction_true:
     19  ∀b, c: Bool.
     20    conjunction b c = true → b = true ∧ c = true.
     21  #b c;
     22  nelim b; nnormalize
     23    [ /2/ | #K; ndestruct ]
     24nqed.
     25
     26nlemma eq_true_false: false=true → False.
     27 #K; ndestruct.
     28nqed.
     29
     30nlemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
     31 #a; #b; ncases a; ncases b; nnormalize; //; #K; ncases (eq_true_false K).
     32nqed.
     33
     34nlemma inclusive_disjunction_b_true: ∀b. inclusive_disjunction b true = true.
     35 #b; ncases b; @.
     36nqed.
     37
     38nlemma is_a_to_mem_to_is_in:
     39 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
     40 #he a m q; nelim q
     41  [ nnormalize; #_; #K; nassumption
     42  | #m' t q' II H1 H2; nnormalize;
     43    nchange in H2:(??%?) with (inclusive_disjunction ??);
     44    ncases (inclusive_disjunction_true … H2)
     45     [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @
     46     | #K; nrewrite > II; ntry nassumption; // ]
    1647nqed.
    1748
     
    3566       [ #K1; #_;
    3667        nchange in K1 with ((conjunction ? (subvector_with …)) = true);
    37         nlapply (inclusive_disjunction_true (is_a he a) (is_in n' tl a));
    38         #K2;
    39         nlapply (K2 K);
    40         #K3;
     68        ncases (conjunction_true … K1); #K3; #K4;
     69        ncases (inclusive_disjunction_true … K); #K2
     70         [ nrewrite > (is_a_to_mem_to_is_in … K2 K3); @
     71         | napply II [ nrewrite > K2; @ | nrewrite > K4; @]##]
    4172     ##| #K1 K2; nnormalize in K2; ncases K2 ]
    4273   ##| #K1 K2; nnormalize in K2; ncases K2 ]
    43 
    44 
    45 nlet rec execute_1_technical
    46  (m: Nat)
    47  (a: addressing_mode)
    48  (q: Vector addressing_mode_tag (S m))
    49  (n: Nat)
    50  (v: Vector addressing_mode_tag (S n))
    51  on v : bool_to_Prop (is_in ? v a) →
    52         bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    53         bool_to_Prop (is_in ? q a) ≝
    54  match v with
    55   [ Empty ⇒ ?
    56   | Cons o he tl ⇒ ?
    57   ].
    58 ##[ @ | ndestruct |
    59     nlapply (S_inj … H); #H2;
    60     nrewrite > H2 in H1; #K2;
    61  
    62  
    63   #n; nelim n
    64    [ #m v; ninversion v [ #K; ncases (?: False);
    65  
    66  
    67   nelim v
    68    [ nnormalize;
    69      #H1 H2;
    70      ncases (is_in m q a);
    71      nnormalize
    72       [ @ | //;
    73   //.
    74 
    75   #N H V IH H1 H2.
    76   nnormalize.
    77   ncases (is_in m q a).
    78   nnormalize.
    79   napply I.
    80   nnormalize.
    81   //.
    82 nqed.
    83 
    84 nlemma execute_1_technical:
    85   ∀n,m: Nat.
    86   ∀v: Vector addressing_mode_tag (S n).
    87   ∀q: Vector addressing_mode_tag (S m).
    88   ∀a: addressing_mode.
    89     bool_to_Prop (is_in ? v a) →
    90     bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    91     bool_to_Prop (is_in ? q a).
    92   #n; nelim n
    93    [ #m v; ninversion v [ #K; ncases (?: False);
    94  
    95  
    96   nelim v
    97    [ nnormalize;
    98      #H1 H2;
    99      ncases (is_in m q a);
    100      nnormalize
    101       [ @ | //;
    102   //.
    103 
    104   #N H V IH H1 H2.
    105   nnormalize.
    106   ncases (is_in m q a).
    107   nnormalize.
    108   napply I.
    109   nnormalize.
    110   //.
    11174nqed.
    11275   
Note: See TracChangeset for help on using the changeset viewer.