Changeset 351


Ignore:
Timestamp:
Dec 1, 2010, 4:30:46 PM (9 years ago)
Author:
mulligan
Message:

No more axioms but the paralogisms.

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

Legend:

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

    r350 r351  
    7878    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
    7979                  (modulus c_as_nat ((S (S Z)) * n)) +
    80                   c_as_nat) ((S (S Z)) * n) in
     80                  c_as_nat) ((S (S Z)) * n) in
    8181    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
    8282                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
    83                   c_as_nat) ((S (S Z))^(n - (S Z)))) in
     83                  c_as_nat) ((S (S Z))^(n - (S Z)))) in
    8484    let result ≝ modulus result_old ((S (S Z))^n) in
    85     let cy_flag ≝ (result_old ((S (S Z))^n)) in
     85    let cy_flag ≝ (result_old ((S (S Z))^n)) in
    8686    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    8787      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
     
    9898    let carry_as_nat ≝ nat_of_bool carry in
    9999    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
    100     let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤ carry_as_nat)) in
    101     let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≤ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≤ carry_as_nat)) in
     100    let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in
     101    let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≲ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≲ carry_as_nat)) in
    102102    let old_result_1 ≝ b_as_nat - c_as_nat in
    103103    let old_result_2 ≝ old_result_1 - carry_as_nat in
    104104    let ov_flag ≝ exclusive_disjunction carry bit_six in
    105       match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤ carry_as_nat) with
     105      match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
    106106        [ false ⇒
    107107           let cy_flag ≝ false in
     
    120120  λb: BitVector n.
    121121    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
    122     let overflow ≝ b_as_nat (S (S Z))^n in
     122    let overflow ≝ b_as_nat (S (S Z))^n in
    123123      match overflow with
    124124        [ false ⇒ bitvector_of_nat n b_as_nat
     
    138138
    139139ndefinition bitvector_of_bool:
    140       ∀n: Nat. ∀b: Bool. BitVector n
     140      ∀n: Nat. ∀b: Bool. BitVector (S n)
    141141  λn: Nat.
    142142  λb: Bool.
    143     ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
    144   nrewrite > (plus_minus_inverse_right n ?);
    145   #H;
    146   nassumption;
     143    ? (pad (S n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
     144  nrewrite > plus_minus_inverse_right
     145   [ napply (λx.x) | /2/]
    147146nqed.
    148147
  • Deliverables/D4.1/Matita/BitVector.ma

    r349 r351  
    200200  let bitvector ≝ bitvector_of_list biglist in
    201201  let difference ≝ n - size in
    202     match greater_than_b size n with
    203       [ true ⇒ max n
    204       | false ⇒ ? (pad difference size bitvector)
    205       ].
    206       nnormalize.
    207       nrewrite > (plus_minus_inverse_right n ?).
    208       #H.
    209       nassumption.
     202   less_than_or_equal_b_elim …
     203    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉))
     204    (λH:¬(size ≤ n). max n).
     205 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
    210206nqed.
    211207
  • Deliverables/D4.1/Matita/Exponential.ma

    r268 r351  
    6161nqed.
    6262
     63(*
    6364naxiom exponential_addition_exponential_multiplication:
    6465  ∀m, n, o: Nat.
    6566    (m^n) * (m^o) = m^(n + o).
    6667
    67 (*
    6868nlemma exponential_exponential_multiplication:
    6969  ∀m, n, o: Nat.
  • Deliverables/D4.1/Matita/Interpret.ma

    r347 r351  
    44include "Arithmetic.ma".
    55include "List.ma".
    6 
    7 alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".
    86
    97ndefinition sign_extension: Byte → Word ≝
     
    389387              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
    390388              let 〈nu, nl〉 ≝ split ? four four pc_bu in
    391               let bit ≝ cic:/matita/ng/Vector/get_index.fix(0,3,2) ? ? nl Z ? in
     389              let bit ≝ get_index_bv ? nl Z ? in
    392390              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
    393391              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
  • Deliverables/D4.1/Matita/Nat.ma

    r350 r351  
    3737 
    3838interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
    39 (*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
    40 *)
     39
     40notation "hvbox(n break ≲ m)"
     41  non associative with precedence 47
     42  for @{ 'less_than_or_equalb $n $m }.
     43
     44interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m).
     45
    4146
    4247ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
     
    5459
    5560interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
    56 (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
    57 *)
     61
     62notation "hvbox(n break ≳ m)"
     63  non associative with precedence 47
     64  for @{ 'greater_than_or_equalb $n $m }.
     65
     66interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m).
     67
    5868
    5969(* Add Boolean versions.                                                      *)
     
    236246(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    237247
    238 naxiom plus_minus_inverse_left:
     248(*naxiom plus_minus_inverse_left:
    239249  ∀m, n: Nat.
    240250    (m + n) - n = m.
    241    
     251*)
     252 
    242253ntheorem less_than_or_equal_monotone:
    243254  ∀m, n: Nat.
     
    250261nqed.
    251262
    252 ntheorem succ_less_than_or_equal_injective:
     263ntheorem less_than_or_equal_injective:
    253264  ∀m, n: Nat.
    254265    (S m) ≤ (S n) → m ≤ n.
     
    259270nqed.
    260271   
    261 naxiom plus_minus_inverse_right:
    262   ∀m, n: Nat.
    263     (m - n) + n = m.
    264 
    265272ntheorem succ_less_than_injective:
    266273  ∀m, n: Nat.
     
    279286 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
    280287nqed.
     288
    281289   
    282290(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    294302nqed.
    295303
    296 naxiom less_than_or_equal_injective:
    297   ∀m, n: Nat.
    298     S m ≤ S n → m ≤ n.
    299 
    300304(*
    301305nlemma less_than_or_equal_zero_equal_zero:
     
    548552nqed.
    549553
     554
     555nlemma succ_injective:
     556  ∀m, n: Nat.
     557    S m = S n → m = n.
     558  #m n H;
     559  napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with
     560           [refl ⇒ ? ]);
     561  @;
     562nqed.
     563
     564ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'.
     565 //;
     566nqed.
     567
     568ntheorem plus_minus_inverse_right:
     569  ∀m, n: Nat.
     570   n ≤ m → (m - n) + n = m.
     571 #m; nelim m
     572  [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1);
     573    #K; ncases (K H3)
     574  | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/;
     575    #w; nrewrite < succ_plus; /4/. ##]
     576nqed.
     577
    550578(*
    551 nlemma succ_injective:
    552   ∀m, n: Nat.
    553     S m = S n → m = n.
    554   #m n.
    555   nelim m.
    556   #H.
    557   ninversion H.
    558   #H.
    559   ndestruct
    560579
    561580nlemma plus_minus_associate:
     
    578597  #N H.
    579598*)
     599
     600ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n.
     601 #m; nelim m; //; #y H1 z; ncases z; nnormalize
     602  [ #H; ndestruct | /3/ ]
     603nqed.
     604
     605ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n).
     606 #m; nelim m; nnormalize
     607  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
     608    [ #H; ndestruct | /3/ ] /2/.
     609nqed.
     610
     611ndefinition less_than_or_equal_b_elim:
     612 ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
     613  P (less_than_or_equal_b m n).
     614 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
     615 nlapply (less_than_or_equal_b_complete m n);
     616 ncases (less_than_or_equal_b m n); /3/.
     617nqed.
     618
     619ndefinition greater_than_or_equal_b_elim:
     620 ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) →
     621  P (greater_than_or_equal_b m n).
     622 #m n; napply less_than_or_equal_b_elim;
     623nqed.
     624
     625ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n.
     626 #m; nelim m
     627  [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ]
     628##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K;
     629    napply less_than_or_equal_monotone; napply H; napply K ]
     630nqed.
     631
     632ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n).
     633 #m; nelim m
     634  [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct
     635  | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/.
     636nqed.
     637
     638ndefinition less_than_b_elim:
     639 ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) →
     640  P (less_than_b m n).
     641 #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n);
     642 ncases (less_than_b m n); /3/.
     643nqed.
     644
     645ndefinition greater_than_b_elim:
     646 ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) →
     647  P (greater_than_b m n).
     648 #m n; napply less_than_b_elim.
     649nqed.
  • Deliverables/D4.1/Matita/Status.ma

    r350 r351  
    103103}.
    104104
    105 naxiom sfr8051_index_nineteen:
     105nlemma sfr8051_index_nineteen:
    106106  ∀i: SFR8051.
    107107    sfr_8051_index i < nineteen.
     108 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
     109 napply less_than_or_equal_zero.
     110nqed.
    108111   
    109 naxiom sfr8052_index_five:
     112nlemma sfr8052_index_five:
    110113  ∀i: SFR8052.
    111114    sfr_8052_index i < five.
     115 #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
     116 napply less_than_or_equal_zero.
     117nqed.
    112118   
    113119ndefinition set_clock ≝
     
    180186                old_clock.
    181187
    182 alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
    183188ndefinition get_8051_sfr ≝
    184189  λs: Status.
     
    186191    let sfr ≝ special_function_registers_8051 s in
    187192    let index ≝ sfr_8051_index i in
    188       get_index sfr index ?.
     193      get_index ?? sfr index ?.
    189194    napply (sfr8051_index_nineteen i).
    190195nqed.
     
    195200    let sfr ≝ special_function_registers_8052 s in
    196201    let index ≝ sfr_8052_index i in
    197       get_index sfr index ?.
     202      get_index ?? sfr index ?.
    198203    napply (sfr8052_index_five i).
    199204nqed.
     
    212217    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    213218    let new_special_function_registers_8051 ≝
    214       cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
     219      set_index Byte nineteen old_special_function_registers_8051 index b ? in
    215220    let old_p1_latch ≝ p1_latch s in
    216221    let old_p3_latch ≝ p3_latch s in
     
    242247    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    243248    let new_special_function_registers_8052 ≝
    244       cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
     249      set_index Byte five old_special_function_registers_8052 index b ? in
    245250    let old_p1_latch ≝ p1_latch s in
    246251    let old_p3_latch ≝ p3_latch s in
     
    374379                old_p3_latch
    375380                old_clock.
    376                
    377 naxiom less_than_or_equal_monotone:
    378   ∀m, n: Nat.
    379     m ≤ n → S m ≤ S n.
    380    
    381 alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
    382381               
    383382ndefinition get_cy_flag ≝
     
    887886nqed.
    888887
    889 naxiom modulus_less_than:
    890   ∀m,n: Nat.
    891     (m mod n) < n.
     888ntheorem modulus_less_than:
     889  ∀m,n: Nat. (m mod (S n)) < S n.
     890 #n m; nnormalize; napply less_than_or_equal_monotone;
     891 nlapply (ltoe_refl n);
     892 ngeneralize in ⊢ (?%? → ?(??%?)?);
     893 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
     894  [ nnormalize; #n; napply (less_than_or_equal_b_elim n m); nnormalize
     895     [ // | #H K; ninversion K [ #H1; ndestruct; // | #x H1 H2 H3; ndestruct ]##]
     896##| nnormalize; #y H1 n H2; napply (less_than_or_equal_b_elim n m); nnormalize
     897     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
     898       ncases n; nnormalize; //;
     899       #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m;
     900       nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //;
     901       #q K2; napply H; /3/]
     902nqed.
    892903
    893904ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
     
    9911002          napply less_than_or_equal_zero;
    9921003      ##|##4,5:
    993           napply (modulus_less_than address eight);
     1004          napply modulus_less_than;
    9941005      ##]
    9951006nqed.
Note: See TracChangeset for help on using the changeset viewer.