numbers.v 1.89 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
Require Export PArith NArith ZArith.
Require Export base decidable fin_collections.

4 5
Infix "≤" := le : nat_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
Instance nat_eq_dec:  x y : nat, Decision (x = y) := eq_nat_dec.
Instance positive_eq_dec:  x y : positive, Decision (x = y) := Pos.eq_dec.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

Infix "≤" := N.le : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.

Instance N_eq_dec:  x y : N, Decision (x = y) := N.eq_dec.
Program Instance N_le_dec (x y : N) : Decision (x  y)%N :=
  match Ncompare x y with
  | Gt => right _
  | _ => left _
  end.
Next Obligation. congruence. Qed.

Infix "≤" := Z.le : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Instance Z_eq_dec:  x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_le_dec:  x y : Z, Decision (x  y)%Z := Z_le_dec.

Definition Z_to_option_N (x : Z) :=
  match x with
  | Z0 => Some N0
  | Zpos p => Some (Npos p)
  | Zneg _ => None
  end.

Definition Nmax `{Elements N C} : C  N := collection_fold Nmax 0%N.

Instance Nmax_proper `{FinCollection N C} : Proper (() ==> (=)) Nmax.
Proof.
  apply collection_fold_proper. intros.
  rewrite !N.max_assoc. f_equal. apply N.max_comm.
Qed.

Lemma Nmax_max `{FinCollection N C} X x : x  X  (x  Nmax X)%N.
Proof.
  change ((λ b X, x  X  (x  b)%N) (collection_fold N.max 0%N X) X).
  apply collection_fold_ind.
46 47 48
  * solve_proper.
  * simplify_elem_of.
  * simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51 52 53 54
Qed.

Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
Proof.
  split.
55 56 57 58 59 60
  * intros. unfold fresh, Nfresh.
    setoid_replace X with Y; [easy |].
    now apply elem_of_equiv.
  * intros X E. assert (1  0)%N as []; [| easy].
    apply N.add_le_mono_r with (Nmax X).
    now apply Nmax_max.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Qed.