Ignore:
Timestamp:
Oct 13, 2010, 4:27:18 PM (10 years ago)
Author:
campbell
Message:

Sort out some axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/extralib.ma

    r173 r181  
    8383
    8484(* should be proved in nat.ma, but it's not! *)
    85 naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     85nlemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     86#n; nelim n;
     87##[ #m; ncases m; //;
     88##| #n' IH m; ncases m; ##[ /2/; ##| #m'; nwhd in match (eqb (S n') (S m')) in ⊢ %;
     89  nlapply (IH m'); ncases (eqb n' m'); /2/; ##]
     90##] nqed.
    8691
    8792nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
     
    269274##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb)
    270275##] nqed.
     276
     277nlemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
     278#x y; ncases x; ncases y; /2/;
     279#n m; napply (pos_cases … n); napply (pos_cases … m);
     280##[ //;
     281##| #n'; /2/;
     282##| #m'; #H; napply False_ind; nnormalize in H; napply (absurd … (not_le_succ_one m')); /2/;
     283##| #n' m'; #H; nnormalize in H;
     284    nrewrite > (Zsucc_neg_succ n'); nrewrite > (Zsucc_neg_succ m'); /2/;
     285##] nqed.
     286
     287nlemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
     288#x y; ncases x; ncases y;
     289##[ ##1,2,7,8,9: /2/;
     290##| ##3,4: #m; nnormalize; *;
     291##| #m n; napply (pos_cases … n); napply (pos_cases … m);
     292  ##[ ##1,2: /2/;
     293  ##| #n'; nnormalize; #H; napply False_ind; napply (absurd … (not_le_succ_one n')); /2/;
     294  ##| #n' m'; nrewrite > (Zpred_pos_succ n'); nrewrite > (Zpred_pos_succ m'); /2/;
     295  ##]
     296##| #m n; nnormalize; *;
     297##] nqed.
     298
     299nlemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
     300#n; ncases n; //; #n'; #a b H;
     301##[ napply (pos_elim … n');
     302  ##[ nrewrite < (Zsucc_Zplus_pos_O a); nrewrite < (Zsucc_Zplus_pos_O b); /2/;
     303  ##| #n'' H; nrewrite > (?:pos (succ n'') = Zsucc (pos n'')); //;
     304      nrewrite > (Zplus_Zsucc …); nrewrite > (Zplus_Zsucc …); /2/;
     305  ##]
     306##| napply (pos_elim … n');
     307  ##[ nrewrite < (Zpred_Zplus_neg_O a); nrewrite < (Zpred_Zplus_neg_O b); /2/;
     308  ##| #n'' H; nrewrite > (?:neg (succ n'') = Zpred (neg n'')); //;
     309      nrewrite > (Zplus_Zpred …); nrewrite > (Zplus_Zpred …); /2/;
     310  ##]
     311##] nqed.
     312
     313nlemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
     314/2/; nqed.
    271315
    272316nlet rec Z_times (x:Z) (y:Z) : Z ≝
Note: See TracChangeset for help on using the changeset viewer.