Changeset 330


Ignore:
Timestamp:
Nov 29, 2010, 2:08:52 PM (9 years ago)
Author:
mulligan
Message:

Fixed segmentation fault in Nat.ma, added get_index and renamed previous get_index to get_index_weak in List.ma.

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

Legend:

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

    r320 r330  
    195195        false) b c.
    196196
    197 naxiom plus_minus_inverse_left:
    198   ∀m, n: Nat.
    199     (m + n) - n = m.
    200    
    201 naxiom plus_minus_inverse_right:
    202   ∀m, n: Nat.
    203     (m - n) + n = m.
    204 
    205 naxiom greater_than_b: Nat → Nat → Bool.
    206 
    207197nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
    208198  let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
  • Deliverables/D4.1/Matita/List.ma

    r329 r330  
    103103        #K;
    104104        ncases (K absd);
    105     ##| ncases (less_than_monoton);
    106    
    107    
     105    ##| nnormalize in p;
     106        nnormalize;
     107        napply (succ_less_than_or_equal_injective ? ?);
     108        nassumption;
     109    ##]
     110nqed.
     111       
    108112nlet rec get_index_weak (A: Type[0]) (l: List A) (n: Nat) on n ≝
    109113  match n with
     
    116120      match l with
    117121        [ Empty ⇒ Nothing A
    118         | Cons hd tl ⇒ get_index A tl o
     122        | Cons hd tl ⇒ get_index_weak A tl o
    119123        ]
    120124    ].
  • Deliverables/D4.1/Matita/Nat.ma

    r329 r330  
    209209
    210210(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    211 (* Lemmas.                                                                    *)
    212 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     211(* Axioms.                                                                    *)
     212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     213
     214naxiom plus_minus_inverse_left:
     215  ∀m, n: Nat.
     216    (m + n) - n = m.
     217   
     218naxiom less_than_or_equal_monotone:
     219  ∀m, n: Nat.
     220    m ≤ n → (S m) ≤ (S n).
     221   
     222naxiom succ_less_than_or_equal_injective:
     223  ∀m, n: Nat.
     224    (S m) ≤ (S n) → m ≤ n.
     225   
     226naxiom plus_minus_inverse_right:
     227  ∀m, n: Nat.
     228    (m - n) + n = m.
     229
     230naxiom greater_than_b: Nat → Nat → Bool.
    213231
    214232naxiom succ_less_than_injective:
     
    219237  ∀m: Nat.
    220238    ¬(m < Z).
     239   
     240(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     241(* Lemmas.                                                                    *)
     242(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    221243   
    222244nlemma less_than_or_equal_zero:
     
    347369  nnormalize.
    348370  nrewrite > H.
    349   napplyS succ_plus.
     371  napply succ_plus.
    350372nqed.
    351373
Note: See TracChangeset for help on using the changeset viewer.