source: src/utilities/extranat.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 2.9 KB
Line 
1include "basics/types.ma".
2include "arithmetics/nat.ma".
3
4inductive nat_compared : nat → nat → Type[0] ≝
5| nat_lt : ∀n,m:nat. nat_compared n (n+S m)
6| nat_eq : ∀n:nat.   nat_compared n n
7| nat_gt : ∀n,m:nat. nat_compared (m+S n) m.
8
9let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝
10match n return λx. nat_compared x m with
11[ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ]
12| S n' ⇒
13    match m return λy. nat_compared (S n') y with
14    [ O ⇒ nat_gt n' O
15    | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with
16             [ nat_lt x y ⇒ nat_lt ??
17             | nat_eq x ⇒ nat_eq ?
18             | nat_gt x y ⇒ nat_gt ? (S y)
19             ]
20    ]
21].
22
23lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
24#n elim n
25[ @refl
26| #m #IH whd in ⊢ (??%?) > IH @refl
27] qed.
28
29lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
30#n #m elim n
31[ //
32| #n' #IH whd in ⊢ (??%?) > IH @refl
33] qed.
34
35lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
36#n #m elim m
37[ //
38| #m' #IH whd in ⊢ (??%?) > IH @refl
39] qed.
40
41
42let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
43match n return λn.Sum (n=m) (n≠m) with
44[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
45| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒
46           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
47].
48[ 1,2: % #E destruct
49| >E @refl
50| % #E destruct cases NE /2/
51] qed.
52
53lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
54#m #n #o #H whd in ⊢ (??%) @leb_elim #H'
55[ @(transitive_le ? m ? H H')
56| @H
57] qed.
58
59lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n.
60#m #n #o #H whd in ⊢ (??%) @leb_elim #H'
61[ @H
62| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
63] qed.
64
65
66(* "Fast" proofs:  some proofs get reduced during normalization (in particular,
67   some functions which use a proof for rewriting are applied to constants and
68   get reduced during a proof or while matita is searching for a term;
69   they may also be normalized during testing), and so here are some more
70   efficient versions.  Perhaps they could be replaced using some kind of proof
71   irrelevance? *)
72
73let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
74match n return λn'.∀m.S(n'+m) = n'+S m with
75[ O ⇒ λm.refl ??
76| S n' ⇒ λm. ?
77]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
78
79let rec plus_n_O_faster (n:nat) : n = n + O ≝
80match n return λn.n=n+O with
81[ O ⇒ refl ??
82| S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ]
83].
84
85let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝
86match n return λn.n+m = m+n with
87[ O ⇒ plus_n_O_faster ?
88| S n' ⇒ ?
89]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ])
90@(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed.
91
Note: See TracBrowser for help on using the repository browser.