Changeset 350


Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (9 years ago)
Author:
mulligan
Message:

less axioms

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

Legend:

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

    r349 r350  
    147147nqed.
    148148
    149 ndefinition full_add:
    150   ∀n: Nat.
    151   ∀b, c: BitVector n.
    152   ∀d: Bit.
    153     fold_left_i ? ? (
    154       λb1, b2: Bool.
    155       λd.
     149ndefinition full_add ≝
     150  λn: Nat.
     151  λb, c: BitVector n.
     152  λd: Bit.
     153    fold_right2_i ? ? ? (
     154      λn.
     155       λb1, b2: Bool.
     156        λd: Bit × (BitVector n).
    156157        let 〈c1,r〉 ≝ d in
    157158          〈inclusive_disjunction (conjunction b1 b2)
    158159                                 (conjunction c1 (inclusive_disjunction b1 b2)),
    159            (exclusive_disjunction (exclusive_disjunction b1 b2) c1) :: r〉)
    160              b c 〈c, [ ]〉.
    161    
    162     (fun b1 b2 (c,r) -> b1 & b2 || c & (b1 || b2),xor (xor b1 b2) c::r) l r (c,[])
     160           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     161     〈d, [[ ]]〉 ? b c.
    163162   
    164163ndefinition half_add ≝
  • Deliverables/D4.1/Matita/List.ma

    r349 r350  
    105105    ##| nnormalize in p;
    106106        nnormalize;
    107         napply (succ_less_than_or_equal_injective ? ?);
    108         nassumption;
     107        /2/;
    109108    ##]
    110109nqed.
  • Deliverables/D4.1/Matita/Nat.ma

    r349 r350  
    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).
     39(*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
     40*)
    4041
    4142ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
     
    4546ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
    4647  λm, n: Nat.
    47     n ≤ m.
     48    less_than_or_equal_b n m.
    4849   
    4950notation "hvbox(n break ≥ m)"
     
    5354
    5455interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
    55 interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
     56(*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
     57*)
    5658
    5759(* Add Boolean versions.                                                      *)
     
    7678 
    7779interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
     80
     81nlet rec less_than_b (m: Nat) (n: Nat) on m ≝
     82  match m with
     83    [ Z ⇒
     84      match n with
     85        [ Z ⇒ false
     86        | S o ⇒ true
     87        ]
     88    | S o ⇒
     89      match n with
     90        [ Z ⇒ false
     91        | S p ⇒ less_than_b o p
     92        ]
     93    ].
     94
     95(* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *)
     96
     97ndefinition greater_than_b ≝
     98  λm, n: Nat.
     99    less_than_b n m.
     100   
     101(* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *)
    78102
    79103(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    125149
    126150nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
    127   match n ≤ p with
     151  match less_than_or_equal_b n p with
    128152    [ true ⇒ Z
    129153    | false ⇒
     
    148172     
    149173nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
    150   match n ≤ p with
     174  match less_than_or_equal_b n p with
    151175    [ true ⇒ n
    152176    | false ⇒
     
    216240    (m + n) - n = m.
    217241   
    218 naxiom less_than_or_equal_monotone:
     242ntheorem less_than_or_equal_monotone:
    219243  ∀m, n: Nat.
    220244    m ≤ n → (S m) ≤ (S n).
    221    
    222 naxiom succ_less_than_or_equal_injective:
     245 #m n H; nelim H; /2/.
     246nqed.
     247
     248nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l.
     249 #n m l H H1; nelim H1; /2/.
     250nqed.
     251
     252ntheorem succ_less_than_or_equal_injective:
    223253  ∀m, n: Nat.
    224254    (S m) ≤ (S n) → m ≤ n.
     255 #m n H;
     256 nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]);
     257 napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]);
     258 nnormalize; /3/.
     259nqed.
    225260   
    226261naxiom plus_minus_inverse_right:
     
    228263    (m - n) + n = m.
    229264
    230 naxiom greater_than_b: Nat → Nat → Bool.
    231 naxiom less_than_b: Nat → Nat → Bool.
    232 
    233 naxiom succ_less_than_injective:
     265ntheorem succ_less_than_injective:
    234266  ∀m, n: Nat.
    235267    less_than_p (S m) (S n) → m < n.
    236    
    237 naxiom nothing_less_than_Z:
     268 /2/.
     269nqed.
     270
     271nlemma not_less_than_S_Z:
     272 ∀m,n: Nat. S m ≤ n → ¬ (n = Z).
     273 #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ]
     274nqed.
     275
     276ntheorem nothing_less_than_Z:
    238277  ∀m: Nat.
    239278    ¬(m < Z).
     279 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
     280nqed.
    240281   
    241282(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Status.ma

    r345 r350  
    526526  λl: Bool.
    527527    let address ≝ nat_of_bitvector … b in
    528       if (decidable_equality address one_hundred_and_twenty_eight) then
     528      if (eq_n address one_hundred_and_twenty_eight) then
    529529        ?
    530       else if (decidable_equality address one_hundred_and_forty_four) then
     530      else if (eq_n address one_hundred_and_forty_four) then
    531531        if l then
    532532          (p1_latch s)
    533533        else
    534534          (get_8051_sfr s SFR_P1)
    535       else if (decidable_equality address one_hundred_and_sixty) then
     535      else if (eq_n address one_hundred_and_sixty) then
    536536        ?
    537       else if (decidable_equality address one_hundred_and_seventy_six) then
     537      else if (eq_n address one_hundred_and_seventy_six) then
    538538        if l then
    539539          (p3_latch s)
    540540        else
    541541          (get_8051_sfr s SFR_P3)
    542       else if (decidable_equality address one_hundred_and_fifty_three) then
     542      else if (eq_n address one_hundred_and_fifty_three) then
    543543        get_8051_sfr s SFR_SBUF
    544       else if (decidable_equality address one_hundred_and_thirty_eight) then
     544      else if (eq_n address one_hundred_and_thirty_eight) then
    545545        get_8051_sfr s SFR_TL0
    546       else if (decidable_equality address one_hundred_and_thirty_nine) then
     546      else if (eq_n address one_hundred_and_thirty_nine) then
    547547        get_8051_sfr s SFR_TL1
    548       else if (decidable_equality address one_hundred_and_forty) then
     548      else if (eq_n address one_hundred_and_forty) then
    549549        get_8051_sfr s SFR_TH0
    550       else if (decidable_equality address one_hundred_and_forty_one) then
     550      else if (eq_n address one_hundred_and_forty_one) then
    551551        get_8051_sfr s SFR_TH1
    552       else if (decidable_equality address two_hundred) then
     552      else if (eq_n address two_hundred) then
    553553        get_8052_sfr s SFR_T2CON
    554       else if (decidable_equality address two_hundred_and_two) then
     554      else if (eq_n address two_hundred_and_two) then
    555555        get_8052_sfr s SFR_RCAP2L
    556       else if (decidable_equality address two_hundred_and_three) then
     556      else if (eq_n address two_hundred_and_three) then
    557557        get_8052_sfr s SFR_RCAP2H
    558       else if (decidable_equality address two_hundred_and_four) then
     558      else if (eq_n address two_hundred_and_four) then
    559559        get_8052_sfr s SFR_TL2
    560       else if (decidable_equality address two_hundred_and_five) then
     560      else if (eq_n address two_hundred_and_five) then
    561561        get_8052_sfr s SFR_TH2
    562       else if (decidable_equality address one_hundred_and_thirty_five) then
     562      else if (eq_n address one_hundred_and_thirty_five) then
    563563        get_8051_sfr s SFR_PCON
    564       else if (decidable_equality address one_hundred_and_thirty_six) then
     564      else if (eq_n address one_hundred_and_thirty_six) then
    565565        get_8051_sfr s SFR_TCON
    566       else if (decidable_equality address one_hundred_and_thirty_seven) then
     566      else if (eq_n address one_hundred_and_thirty_seven) then
    567567        get_8051_sfr s SFR_TMOD
    568       else if (decidable_equality address one_hundred_and_fifty_two) then
     568      else if (eq_n address one_hundred_and_fifty_two) then
    569569        get_8051_sfr s SFR_SCON
    570       else if (decidable_equality address one_hundred_and_sixty_eight) then
     570      else if (eq_n address one_hundred_and_sixty_eight) then
    571571        get_8051_sfr s SFR_IE
    572       else if (decidable_equality address one_hundred_and_eighty_four) then
     572      else if (eq_n address one_hundred_and_eighty_four) then
    573573        get_8051_sfr s SFR_IP
    574       else if (decidable_equality address one_hundred_and_twenty_nine) then
     574      else if (eq_n address one_hundred_and_twenty_nine) then
    575575        get_8051_sfr s SFR_SP
    576       else if (decidable_equality address one_hundred_and_thirty) then
     576      else if (eq_n address one_hundred_and_thirty) then
    577577        get_8051_sfr s SFR_DPL
    578       else if (decidable_equality address one_hundred_and_thirty_one) then
     578      else if (eq_n address one_hundred_and_thirty_one) then
    579579        get_8051_sfr s SFR_DPH
    580       else if (decidable_equality address two_hundred_and_eight) then
     580      else if (eq_n address two_hundred_and_eight) then
    581581        get_8051_sfr s SFR_PSW
    582       else if (decidable_equality address two_hundred_and_twenty_four) then
     582      else if (eq_n address two_hundred_and_twenty_four) then
    583583        get_8051_sfr s SFR_ACC_A
    584       else if (decidable_equality address two_hundred_and_forty) then
     584      else if (eq_n address two_hundred_and_forty) then
    585585        get_8051_sfr s SFR_ACC_B
    586586      else
     
    594594  λv: Byte.
    595595    let address ≝ nat_of_bitvector … b in
    596       if (decidable_equality address one_hundred_and_twenty_eight) then
     596      if (eq_n address one_hundred_and_twenty_eight) then
    597597        ?
    598       else if (decidable_equality address one_hundred_and_forty_four) then
     598      else if (eq_n address one_hundred_and_forty_four) then
    599599        let status_1 ≝ set_8051_sfr s SFR_P1 v in
    600600        let status_2 ≝ set_p1_latch s v in
    601601          status_2
    602       else if (decidable_equality address one_hundred_and_sixty) then
     602      else if (eq_n address one_hundred_and_sixty) then
    603603        ?
    604       else if (decidable_equality address one_hundred_and_seventy_six) then
     604      else if (eq_n address one_hundred_and_seventy_six) then
    605605        let status_1 ≝ set_8051_sfr s SFR_P3 v in
    606606        let status_2 ≝ set_p3_latch s v in
    607607          status_2
    608       else if (decidable_equality address one_hundred_and_fifty_three) then
     608      else if (eq_n address one_hundred_and_fifty_three) then
    609609        set_8051_sfr s SFR_SBUF v
    610       else if (decidable_equality address one_hundred_and_thirty_eight) then
     610      else if (eq_n address one_hundred_and_thirty_eight) then
    611611        set_8051_sfr s SFR_TL0 v
    612       else if (decidable_equality address one_hundred_and_thirty_nine) then
     612      else if (eq_n address one_hundred_and_thirty_nine) then
    613613        set_8051_sfr s SFR_TL1 v
    614       else if (decidable_equality address one_hundred_and_forty) then
     614      else if (eq_n address one_hundred_and_forty) then
    615615        set_8051_sfr s SFR_TH0 v
    616       else if (decidable_equality address one_hundred_and_forty_one) then
     616      else if (eq_n address one_hundred_and_forty_one) then
    617617        set_8051_sfr s SFR_TH1 v
    618       else if (decidable_equality address two_hundred) then
     618      else if (eq_n address two_hundred) then
    619619        set_8052_sfr s SFR_T2CON v
    620       else if (decidable_equality address two_hundred_and_two) then
     620      else if (eq_n address two_hundred_and_two) then
    621621        set_8052_sfr s SFR_RCAP2L v
    622       else if (decidable_equality address two_hundred_and_three) then
     622      else if (eq_n address two_hundred_and_three) then
    623623        set_8052_sfr s SFR_RCAP2H v
    624       else if (decidable_equality address two_hundred_and_four) then
     624      else if (eq_n address two_hundred_and_four) then
    625625        set_8052_sfr s SFR_TL2 v
    626       else if (decidable_equality address two_hundred_and_five) then
     626      else if (eq_n address two_hundred_and_five) then
    627627        set_8052_sfr s SFR_TH2 v
    628       else if (decidable_equality address one_hundred_and_thirty_five) then
     628      else if (eq_n address one_hundred_and_thirty_five) then
    629629        set_8051_sfr s SFR_PCON v
    630       else if (decidable_equality address one_hundred_and_thirty_six) then
     630      else if (eq_n address one_hundred_and_thirty_six) then
    631631        set_8051_sfr s SFR_TCON v
    632       else if (decidable_equality address one_hundred_and_thirty_seven) then
     632      else if (eq_n address one_hundred_and_thirty_seven) then
    633633        set_8051_sfr s SFR_TMOD v
    634       else if (decidable_equality address one_hundred_and_fifty_two) then
     634      else if (eq_n address one_hundred_and_fifty_two) then
    635635        set_8051_sfr s SFR_SCON v
    636       else if (decidable_equality address one_hundred_and_sixty_eight) then
     636      else if (eq_n address one_hundred_and_sixty_eight) then
    637637        set_8051_sfr s SFR_IE v
    638       else if (decidable_equality address one_hundred_and_eighty_four) then
     638      else if (eq_n address one_hundred_and_eighty_four) then
    639639        set_8051_sfr s SFR_IP v
    640       else if (decidable_equality address one_hundred_and_twenty_nine) then
     640      else if (eq_n address one_hundred_and_twenty_nine) then
    641641        set_8051_sfr s SFR_SP v
    642       else if (decidable_equality address one_hundred_and_thirty) then
     642      else if (eq_n address one_hundred_and_thirty) then
    643643        set_8051_sfr s SFR_DPL v
    644       else if (decidable_equality address one_hundred_and_thirty_one) then
     644      else if (eq_n address one_hundred_and_thirty_one) then
    645645        set_8051_sfr s SFR_DPH v
    646       else if (decidable_equality address two_hundred_and_eight) then
     646      else if (eq_n address two_hundred_and_eight) then
    647647        set_8051_sfr s SFR_PSW v
    648       else if (decidable_equality address two_hundred_and_twenty_four) then
     648      else if (eq_n address two_hundred_and_twenty_four) then
    649649        set_8051_sfr s SFR_ACC_A v
    650       else if (decidable_equality address two_hundred_and_forty) then
     650      else if (eq_n address two_hundred_and_forty) then
    651651        set_8051_sfr s SFR_ACC_B v
    652652      else
     
    996996
    997997ndefinition load_code_memory ≝
    998  fold_lefti … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
     998 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
    999999
    10001000ndefinition load ≝
  • Deliverables/D4.1/Matita/Test.ma

    r347 r350  
    164164nqed.
    165165
    166 ndefinition testfinal ≝ execute five teststatus.
     166ndefinition testfinal ≝ execute one teststatus.
     167
     168nlemma hoo: (*half_add ? (program_counter teststatus)*)
     169  (bitvector_of_nat sixteen (S Z)) = (bitvector_of_nat sixteen (S Z)).
     170 (*half_add (code_memory teststatus) (program_counter teststatus). *)
     171 nwhd in ⊢ (??%?);
    167172
    168173nlemma hoo: testfinal = testfinal.
    169  nwhd in ⊢ (???%);
     174 nwhd in ⊢ (??%?);
    170175 nnormalize; @.
    171176nqed.
  • Deliverables/D4.1/Matita/Vector.ma

    r340 r350  
    165165    ].
    166166
    167 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
    168                       (n: Nat) (f: A → B → C → C) (c: C)
    169                       (v: Vector A n) (q: Vector B n) on v
    170   (match v return λx.λ_. x = n → C with
     167nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0])
     168                      (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat)
     169                      (v: Vector A n) (q: Vector B n) on v : C n
     170  (match v return λx.λ_. x = n → C n with
    171171    [ Empty ⇒
    172       match q return λx.λ_. Z = x → C with
     172      match q return λx.λ_. Z = x → C x with
    173173        [ Empty ⇒ λprf: Z = Z. c
    174         | Cons o hd tl ⇒ λabsd. ?
     174        | Cons o hd tl ⇒ λabsd.
    175175        ]
    176176    | Cons o hd tl ⇒
    177       match q return λx.λ_. S o = x → C with
    178         [ Empty ⇒ λabsd: S o = Z. ?
     177      match q return λx.λ_. S o = x → C x with
     178        [ Empty ⇒ λabsd: S o = Z.
    179179        | Cons p hd' tl' ⇒ λprf: S o = S p.
    180             fold_right_i A B C o f (f hd hd' c) tl ?
     180           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉
    181181        ]
    182182    ]) (refl ? n).
    183     ##[##1,2:
    184         ndestruct;
    185     ##| ndestruct (prf);
    186         napply tl';
    187     ##]
     183 ndestruct; //.
    188184nqed.
    189185 
Note: See TracChangeset for help on using the changeset viewer.