# Changeset 350

Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (11 years ago)
Message:

less axioms

Location:
Deliverables/D4.1/Matita
Files:
6 edited

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

 r349 nqed. ndefinition full_add: ∀n: Nat. ∀b, c: BitVector n. ∀d: Bit. fold_left_i ? ? ( λb1, b2: Bool. λd. ndefinition full_add ≝ λn: Nat. λb, c: BitVector n. λd: Bit. fold_right2_i ? ? ? ( λn. λb1, b2: Bool. λd: Bit × (BitVector n). let 〈c1,r〉 ≝ d in 〈inclusive_disjunction (conjunction b1 b2) (conjunction c1 (inclusive_disjunction b1 b2)), (exclusive_disjunction (exclusive_disjunction b1 b2) c1) :: r〉) b c 〈c, [ ]〉. (fun b1 b2 (c,r) -> b1 & b2 || c & (b1 || b2),xor (xor b1 b2) c::r) l r (c,[]) (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) 〈d, [[ ]]〉 ? b c. ndefinition half_add ≝
• ## Deliverables/D4.1/Matita/List.ma

 r349 ##| nnormalize in p; nnormalize; napply (succ_less_than_or_equal_injective ? ?); nassumption; /2/; ##] nqed.
• ## Deliverables/D4.1/Matita/Nat.ma

 r349 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). (*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). *) ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝ λm, n: Nat. n ≤ m. less_than_or_equal_b n m. notation "hvbox(n break ≥ m)" interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). *) (* Add Boolean versions.                                                      *) interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m). nlet rec less_than_b (m: Nat) (n: Nat) on m ≝ match m with [ Z ⇒ match n with [ Z ⇒ false | S o ⇒ true ] | S o ⇒ match n with [ Z ⇒ false | S p ⇒ less_than_b o p ] ]. (* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *) ndefinition greater_than_b ≝ λm, n: Nat. less_than_b n m. (* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ match n ≤ p with match less_than_or_equal_b n p with [ true ⇒ Z | false ⇒ nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ match n ≤ p with match less_than_or_equal_b n p with [ true ⇒ n | false ⇒ (m + n) - n = m. naxiom less_than_or_equal_monotone: ntheorem less_than_or_equal_monotone: ∀m, n: Nat. m ≤ n → (S m) ≤ (S n). naxiom succ_less_than_or_equal_injective: #m n H; nelim H; /2/. nqed. nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l. #n m l H H1; nelim H1; /2/. nqed. ntheorem succ_less_than_or_equal_injective: ∀m, n: Nat. (S m) ≤ (S n) → m ≤ n. #m n H; nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]); napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]); nnormalize; /3/. nqed. naxiom plus_minus_inverse_right: (m - n) + n = m. naxiom greater_than_b: Nat → Nat → Bool. naxiom less_than_b: Nat → Nat → Bool. naxiom succ_less_than_injective: ntheorem succ_less_than_injective: ∀m, n: Nat. less_than_p (S m) (S n) → m < n. naxiom nothing_less_than_Z: /2/. nqed. nlemma not_less_than_S_Z: ∀m,n: Nat. S m ≤ n → ¬ (n = Z). #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ] nqed. ntheorem nothing_less_than_Z: ∀m: Nat. ¬(m < Z). #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)