# Changeset 372 for Deliverables/D4.1/Matita/Interpret.ma

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

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

File:
1 edited

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

 r370 nlemma inclusive_disjunction_true: ∀b, c: Bool. ((inclusive_disjunction b c) = true) → ((b = true) ∨ (c = true)). inclusive_disjunction b c = true → b = true ∨ c = true. #b c; nelim b ##| nnormalize; /2/; ##] nqed. nlemma conjunction_true: ∀b, c: Bool. conjunction b c = true → b = true ∧ c = true. #b c; nelim b; nnormalize [ /2/ | #K; ndestruct ] nqed. nlemma eq_true_false: false=true → False. #K; ndestruct. nqed. nlemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b. #a; #b; ncases a; ncases b; nnormalize; //; #K; ncases (eq_true_false K). nqed. nlemma inclusive_disjunction_b_true: ∀b. inclusive_disjunction b true = true. #b; ncases b; @. nqed. nlemma is_a_to_mem_to_is_in: ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. #he a m q; nelim q [ nnormalize; #_; #K; nassumption | #m' t q' II H1 H2; nnormalize; nchange in H2:(??%?) with (inclusive_disjunction ??); ncases (inclusive_disjunction_true … H2) [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @ | #K; nrewrite > II; ntry nassumption; // ] nqed. [ #K1; #_; nchange in K1 with ((conjunction ? (subvector_with …)) = true); nlapply (inclusive_disjunction_true (is_a he a) (is_in n' tl a)); #K2; nlapply (K2 K); #K3; ncases (conjunction_true … K1); #K3; #K4; ncases (inclusive_disjunction_true … K); #K2 [ nrewrite > (is_a_to_mem_to_is_in … K2 K3); @ | napply II [ nrewrite > K2; @ | nrewrite > K4; @]##] ##| #K1 K2; nnormalize in K2; ncases K2 ] ##| #K1 K2; nnormalize in K2; ncases K2 ] nlet rec execute_1_technical (m: Nat) (a: addressing_mode) (q: Vector addressing_mode_tag (S m)) (n: Nat) (v: Vector addressing_mode_tag (S n)) on v : bool_to_Prop (is_in ? v a) → bool_to_Prop (subvector_with ? ? ? eq_a v q) → bool_to_Prop (is_in ? q a) ≝ match v with [ Empty ⇒ ? | Cons o he tl ⇒ ? ]. ##[ @ | ndestruct | nlapply (S_inj … H); #H2; nrewrite > H2 in H1; #K2; #n; nelim n [ #m v; ninversion v [ #K; ncases (?: False); nelim v [ nnormalize; #H1 H2; ncases (is_in m q a); nnormalize [ @ | //; //. #N H V IH H1 H2. nnormalize. ncases (is_in m q a). nnormalize. napply I. nnormalize. //. nqed. nlemma execute_1_technical: ∀n,m: Nat. ∀v: Vector addressing_mode_tag (S n). ∀q: Vector addressing_mode_tag (S m). ∀a: addressing_mode. bool_to_Prop (is_in ? v a) → bool_to_Prop (subvector_with ? ? ? eq_a v q) → bool_to_Prop (is_in ? q a). #n; nelim n [ #m v; ninversion v [ #K; ncases (?: False); nelim v [ nnormalize; #H1 H2; ncases (is_in m q a); nnormalize [ @ | //; //. #N H V IH H1 H2. nnormalize. ncases (is_in m q a). nnormalize. napply I. nnormalize. //. nqed.
Note: See TracChangeset for help on using the changeset viewer.