Ignore:
Timestamp:
Dec 3, 2010, 4:47:03 PM (9 years ago)
Author:
mulligan
Message:

Most of critical lemma done. Hole remaining that I can't coax matita into solving.

File:
1 edited

Legend:

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

    r369 r370  
    66    zero eight @@ b.
    77   
     8nlemma inclusive_disjunction_true:
     9  ∀b, c: Bool.
     10    ((inclusive_disjunction b c) = true) → ((b = true) ∨ (c = true)).
     11  #b c;
     12  nelim b
     13    [ nnormalize; #H; napply or_introl; @;
     14  ##| nnormalize; /2/;
     15  ##]
     16nqed.
     17
    818nlemma execute_1_technical:
    919  ∀n,m: Nat.
     
    1424    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    1525    bool_to_Prop (is_in ? q a).
    16   #n m v q a.
    17   nelim v.
     26 #n m v q a; nelim v
     27  [ nnormalize; #K; ncases K
     28  | #n' he tl II;
     29    nwhd in ⊢ (% → ? → ?);
     30    nlapply (refl … (is_in … (he:::tl) a));
     31    ncases (is_in … (he:::tl) a) in ⊢ (???% → %)
     32     [ #K; #_; nnormalize in K; nwhd in ⊢ (% → ?);
     33       nlapply (refl … (subvector_with … eq_a (he:::tl) q));
     34       ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
     35       [ #K1; #_;
     36        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;
     41     ##| #K1 K2; nnormalize in K2; ncases K2 ]
     42   ##| #K1 K2; nnormalize in K2; ncases K2 ]
     43
     44
     45nlet 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.
    1876  nnormalize.
    19   #H1 H2.
    2077  ncases (is_in m q a).
    2178  nnormalize.
     
    2380  nnormalize.
    2481  //.
     82nqed.
     83
     84nlemma 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
    25104  #N H V IH H1 H2.
    26105  nnormalize.
Note: See TracChangeset for help on using the changeset viewer.