Changeset 370 for Deliverables/D4.1/Matita/Interpret.ma
 Timestamp:
 Dec 3, 2010, 4:47:03 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r369 r370 6 6 zero eight @@ b. 7 7 8 nlemma 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 ##] 16 nqed. 17 8 18 nlemma execute_1_technical: 9 19 ∀n,m: Nat. … … 14 24 bool_to_Prop (subvector_with ? ? ? eq_a v q) → 15 25 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 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. 18 76 nnormalize. 19 #H1 H2.20 77 ncases (is_in m q a). 21 78 nnormalize. … … 23 80 nnormalize. 24 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 25 104 #N H V IH H1 H2. 26 105 nnormalize.
Note: See TracChangeset
for help on using the changeset viewer.