Commit 50dfc148 authored by Robbert Krebbers's avatar Robbert Krebbers

Many relatively small changes.

Most interestingly:
* Use [lia] instead of [omega] everywhere
* More many generic lemmas on the memory to the theory on finite maps.
* Many additional list lemmas.
* A new interface for a monad for collections, which is now also used by the
  collection tactics.
* Provide an additional finite collection implementation using unordered lists
  without duplicates removed. This implementation forms a monad (just the list
  monad in disguise).
parent e82cda6c
......@@ -4,7 +4,7 @@
These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *)
Require Import Omega Wf_nat.
Require Import Wf_nat.
Require Export tactics base.
(** * Definitions *)
......@@ -101,7 +101,7 @@ Section rtc.
bsteps R n x y bsteps R (m + n) x y.
Proof. apply bsteps_weaken. auto with arith. Qed.
Lemma bsteps_S n x y : bsteps R n x y bsteps R (S n) x y.
Proof. apply bsteps_weaken. omega. Qed.
Proof. apply bsteps_weaken. lia. Qed.
Lemma bsteps_trans n m x y z :
bsteps R n x y bsteps R m y z bsteps R (n + m) x z.
Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed.
......@@ -129,11 +129,11 @@ Section rtc.
induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
intros n p1 H. rewrite <-plus_n_Sm.
apply (IH (S n)); [by eauto using bsteps_r |].
intros [|m'] [??]; [omega |].
intros [|m'] [??]; [lia |].
apply Pstep with x'.
* apply bsteps_weaken with n; intuition omega.
* apply bsteps_weaken with n; intuition lia.
* done.
* apply H; intuition omega.
* apply H; intuition lia.
Qed.
Global Instance tc_trans: Transitive (tc R).
......
This diff is collapsed.
This diff is collapsed.
......@@ -93,12 +93,14 @@ Instance False_dec: Decision False := right (False_rect False).
Section prop_dec.
Context `(P_dec : Decision P) `(Q_dec : Decision Q).
Global Instance not_dec: Decision (¬P).
Proof. refine (cast_if_not P_dec); intuition. Defined.
Global Instance and_dec: Decision (P Q).
Proof. refine (cast_if_and P_dec Q_dec); intuition. Qed.
Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
Global Instance or_dec: Decision (P Q).
Proof. refine (cast_if_or P_dec Q_dec); intuition. Qed.
Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
Global Instance impl_dec: Decision (P Q).
Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Qed.
Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
End prop_dec.
(** Instances of [Decision] for common data types. *)
......
......@@ -4,11 +4,11 @@
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
Require Import Permutation.
Require Export collections listset numbers.
Require Export collections numbers listset.
Instance collection_size `{Elements A C} : Size C := λ X, length (elements X).
Definition collection_fold `{Elements A C} {B} (f : A B B)
(b : B) (X : C) : B := foldr f b (elements X).
Instance collection_size `{Elements A C} : Size C := length elements.
Definition collection_fold `{Elements A C} {B}
(f : A B B) (b : B) : C B := foldr f b elements.
Section fin_collection.
Context `{FinCollection A C}.
......@@ -23,42 +23,44 @@ Qed.
Global Instance collection_size_proper: Proper (() ==> (=)) size.
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
Lemma size_empty : size = 0.
Lemma size_empty : size ( : C) = 0.
Proof.
unfold size, collection_size. rewrite (in_nil_inv (elements )).
unfold size, collection_size. simpl.
rewrite (elem_of_nil_inv (elements )).
* done.
* intro. rewrite <-elements_spec. solve_elem_of.
Qed.
Lemma size_empty_inv X : size X = 0 X .
Lemma size_empty_inv (X : C) : size X = 0 X .
Proof.
intros. apply equiv_empty. intro. rewrite elements_spec.
rewrite (nil_length (elements X)); intuition.
rewrite (nil_length (elements X)). by rewrite elem_of_nil. done.
Qed.
Lemma size_empty_iff X : size X = 0 X .
Lemma size_empty_iff (X : C) : size X = 0 X .
Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
Lemma size_singleton x : size {[ x ]} = 1.
Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof.
change (length (elements {[ x ]}) = length [x]).
apply Permutation_length, NoDup_Permutation.
* apply elements_nodup.
* apply NoDup_singleton.
* intros. rewrite <-elements_spec. esolve_elem_of firstorder.
* intros.
by rewrite <-elements_spec, elem_of_singleton, elem_of_list_singleton.
Qed.
Lemma size_singleton_inv X x y : size X = 1 x X y X x = y.
Proof.
unfold size, collection_size. rewrite !elements_spec.
unfold size, collection_size. simpl. rewrite !elements_spec.
generalize (elements X). intros [|? l].
* done.
* injection 1. intro. rewrite (nil_length l) by done.
simpl. intuition congruence.
simpl. rewrite !elem_of_list_singleton. congruence.
Qed.
Lemma elem_of_or_empty X : ( x, x X) X .
Proof.
destruct (elements X) as [|x xs] eqn:E.
* right. apply equiv_empty. intros x Ex.
by rewrite elements_spec, E in Ex.
by rewrite elements_spec, E, elem_of_nil in Ex.
* left. exists x. rewrite elements_spec, E.
by constructor.
Qed.
......@@ -87,17 +89,17 @@ Qed.
Lemma size_union X Y : X Y size (X Y) = size X + size Y.
Proof.
intros [E _]. unfold size, collection_size. rewrite <-app_length.
intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
* apply elements_nodup.
* apply NoDup_app; try apply elements_nodup.
* apply NoDup_app; repeat split; try apply elements_nodup.
intros x. rewrite <-!elements_spec. esolve_elem_of.
* intros. rewrite in_app_iff, <-!elements_spec. solve_elem_of.
* intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of.
Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x X) | 100.
Proof.
refine (cast_if (decide_rel In x (elements X)));
refine (cast_if (decide_rel () x (elements X)));
by rewrite (elements_spec _).
Defined.
Global Program Instance collection_subseteq_dec_slow (X Y : C) :
......@@ -178,11 +180,12 @@ Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B)
X, P (collection_fold f b X) X.
Proof.
intros ? Hemp Hadd.
cut ( l, NoDup l X, ( x, x X In x l) P (foldr f b l) X).
cut ( l, NoDup l X, ( x, x X x l) P (foldr f b l) X).
{ intros help ?. apply help. apply elements_nodup. apply elements_spec. }
induction 1 as [|x l ?? IHl]; simpl.
* intros X HX. rewrite equiv_empty; firstorder.
* intros X HX.
induction 1 as [|x l ?? IHl].
* intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty; firstorder.
* intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
rewrite <-union_difference.
apply Hadd. solve_elem_of. apply IHl.
......@@ -191,25 +194,32 @@ Proof.
+ esolve_elem_of.
Qed.
Lemma collection_fold_proper {B} (f : A B B) (b : B) :
( a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b))
Proper (() ==> (=)) (collection_fold f b).
Proof. intros ??? E. apply foldr_permutation. auto. by rewrite E. Qed.
Lemma collection_fold_proper {B} (R : relation B)
`{!Equivalence R}
(f : A B B) (b : B)
`{!Proper ((=) ==> R ==> R) f}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper (() ==> R) (collection_fold f b).
Proof.
intros ?? E. apply (foldr_permutation R f b).
* auto.
* by rewrite E.
Qed.
Global Instance cforall_dec `(P : A Prop)
`{ x, Decision (P x)} X : Decision (cforall P X) | 100.
`{ x, Decision (P x)} X : Decision (cforall P X) | 100.
Proof.
refine (cast_if (decide (Forall P (elements X))));
abstract (unfold cforall; setoid_rewrite elements_spec;
by rewrite <-Forall_forall).
abstract (unfold cforall; setoid_rewrite elements_spec;
by rewrite <-Forall_forall).
Defined.
Global Instance cexists_dec `(P : A Prop) `{ x, Decision (P x)} X :
Decision (cexists P X) | 100.
Proof.
refine (cast_if (decide (Exists P (elements X))));
abstract (unfold cexists; setoid_rewrite elements_spec;
by rewrite <-Exists_exists).
abstract (unfold cexists; setoid_rewrite elements_spec;
by rewrite <-Exists_exists).
Defined.
Global Instance rel_elem_of_dec `{ x y, Decision (R x y)} x X :
......
This diff is collapsed.
......@@ -9,14 +9,14 @@ 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.
apply (collection_fold_proper (=)).
* solve_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.
apply (collection_fold_ind (λ b X, x X (x b)%N)).
* solve_proper.
* solve_elem_of.
* solve_elem_of (eauto using N.le_max_l, N.le_max_r, N.le_trans).
......@@ -26,6 +26,7 @@ Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
Proof.
split.
* apply _.
* intros. unfold fresh, Nfresh.
setoid_replace X with Y; [done |].
by apply elem_of_equiv.
......
This diff is collapsed.
(* Copyright (c) 2012, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
(** This file implements finite as unordered lists without duplicates
removed. This implementation forms a monad. *)
Require Export base decidable collections list.
Definition listset A := sig (@NoDup A).
Record listset A := Listset {
listset_car: list A
}.
Arguments listset_car {_} _.
Arguments Listset {_} _.
Section list_collection.
Context {A : Type} `{ x y : A, Decision (x = y)}.
Section listset.
Context {A : Type}.
Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, In x (`l).
Global Instance listset_empty: Empty (listset A) := []@NoDup_nil _.
Global Instance listset_singleton: Singleton A (listset A) := λ x,
[x]NoDup_singleton x.
Instance listset_elem_of: ElemOf A (listset A) := λ x l,
x listset_car l.
Instance listset_empty: Empty (listset A) :=
Listset [].
Instance listset_singleton: Singleton A (listset A) := λ x,
Listset [x].
Instance listset_union: Union (listset A) := λ l k,
Listset (listset_car l ++ listset_car k).
Fixpoint listset_difference_raw (l k : list A) :=
match l with
| [] => []
| x :: l =>
if decide_rel In x k
then listset_difference_raw l k
else x :: listset_difference_raw l k
end.
Lemma listset_difference_raw_in l k x :
In x (listset_difference_raw l k) In x l ¬In x k.
Global Instance: SimpleCollection A (listset A).
Proof.
split; induction l; simpl; try case_decide; simpl; intuition congruence.
Qed.
Lemma listset_difference_raw_nodup l k :
NoDup l NoDup (listset_difference_raw l k).
Proof.
induction 1; simpl; try case_decide.
* constructor.
* done.
* constructor. rewrite listset_difference_raw_in; intuition. done.
split.
* by apply not_elem_of_nil.
* by apply elem_of_list_singleton.
* intros. apply elem_of_app.
Qed.
Global Instance listset_difference: Difference (listset A) := λ l k,
listset_difference_raw (`l) (`k)
listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
Definition listset_union_raw (l k : list A) := listset_difference_raw l k ++ k.
Lemma listset_union_raw_in l k x :
In x (listset_union_raw l k) In x l In x k.
Proof.
unfold listset_union_raw. rewrite in_app_iff, listset_difference_raw_in.
intuition. case (decide (In x k)); intuition.
Qed.
Lemma listset_union_raw_nodup l k :
NoDup l NoDup k NoDup (listset_union_raw l k).
Proof.
intros. apply NoDup_app.
* by apply listset_difference_raw_nodup.
* done.
* intro. rewrite listset_difference_raw_in. intuition.
Qed.
Global Instance listset_union: Union (listset A) := λ l k,
listset_union_raw (`l) (`k)
listset_union_raw_nodup (`l) (`k) (proj2_sig l) (proj2_sig k).
Context `{ x y : A, Decision (x = y)}.
Fixpoint listset_intersection_raw (l k : list A) :=
match l with
| [] => []
| x :: l =>
if decide_rel In x k
then x :: listset_intersection_raw l k
else listset_intersection_raw l k
end.
Lemma listset_intersection_raw_in l k x :
In x (listset_intersection_raw l k) In x l In x k.
Proof.
split; induction l; simpl; try case_decide; simpl; intuition congruence.
Qed.
Lemma listset_intersection_raw_nodup l k :
NoDup l NoDup (listset_intersection_raw l k).
Proof.
induction 1; simpl; try case_decide.
* constructor.
* constructor. rewrite listset_intersection_raw_in; intuition. done.
* done.
Qed.
Global Instance listset_intersection: Intersection (listset A) := λ l k,
listset_intersection_raw (`l) (`k)
listset_intersection_raw_nodup (`l) (`k) (proj2_sig l).
Instance listset_intersection: Intersection (listset A) := λ l k,
Listset (list_intersection (listset_car l) (listset_car k)).
Instance listset_difference: Difference (listset A) := λ l k,
Listset (list_difference (listset_car l) (listset_car k)).
Definition listset_add_raw x (l : list A) : list A :=
if decide_rel In x l then l else x :: l.
Lemma listset_add_raw_in x l y : In y (listset_add_raw x l) y = x In y l.
Proof. unfold listset_add_raw. case_decide; firstorder congruence. Qed.
Lemma listset_add_raw_nodup x l : NoDup l NoDup (listset_add_raw x l).
Global Instance: Collection A (listset A).
Proof.
unfold listset_add_raw. case_decide; try constructor; firstorder.
split.
* apply _.
* intros. apply elem_of_list_intersection.
* intros. apply elem_of_list_difference.
Qed.
Fixpoint listset_map_raw (f : A A) (l : list A) :=
match l with
| [] => []
| x :: l => listset_add_raw (f x) (listset_map_raw f l)
end.
Lemma listset_map_raw_nodup f l : NoDup (listset_map_raw f l).
Proof. induction l; simpl. constructor. by apply listset_add_raw_nodup. Qed.
Lemma listset_map_raw_in f l x :
In x (listset_map_raw f l) y, x = f y In y l.
Instance listset_elems: Elements A (listset A) :=
remove_dups listset_car.
Global Instance: FinCollection A (listset A).
Proof.
split.
* induction l; simpl; [done |].
rewrite listset_add_raw_in. firstorder.
* intros [?[??]]. subst. induction l; simpl in *; [done |].
rewrite listset_add_raw_in. firstorder congruence.
* apply _.
* symmetry. apply elem_of_remove_dups.
* intros. apply remove_dups_nodup.
Qed.
Global Instance listset_map: Map A (listset A) := λ f l,
listset_map_raw f (`l)listset_map_raw_nodup f (`l).
End listset.
Global Instance: Collection A (listset A).
(** These instances are declared using [Hint Extern] to avoid too
eager type class search. *)
Hint Extern 1 (ElemOf _ (listset _)) =>
eapply @listset_elem_of : typeclass_instances.
Hint Extern 1 (Empty (listset _)) =>
eapply @listset_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (listset _)) =>
eapply @listset_singleton : typeclass_instances.
Hint Extern 1 (Union (listset _)) =>
eapply @listset_union : typeclass_instances.
Hint Extern 1 (Intersection (listset _)) =>
eapply @listset_intersection : typeclass_instances.
Hint Extern 1 (Difference (listset _)) =>
eapply @listset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (listset _)) =>
eapply @listset_elems : typeclass_instances.
Instance listset_ret: MRet listset := λ A x,
{[ x ]}.
Instance listset_fmap: FMap listset := λ A B f l,
Listset (f <$> listset_car l).
Instance listset_bind: MBind listset := λ A B f l,
Listset (mbind (listset_car f) (listset_car l)).
Instance listset_join: MJoin listset := λ A, mbind id.
Instance: CollectionMonad listset.
Proof.
split.
* intros ? [].
* compute. intuition.
* intros. apply listset_union_raw_in.
* intros. apply listset_intersection_raw_in.
* intros. apply listset_difference_raw_in.
* intros. apply listset_map_raw_in.
* intros. apply _.
* intros. apply elem_of_list_bind.
* intros. apply elem_of_list_ret.
* intros. apply elem_of_list_fmap.
* intros ?? [l].
unfold mjoin, listset_join, elem_of, listset_elem_of.
simpl. by rewrite elem_of_list_bind.
Qed.
Global Instance listset_elems: Elements A (listset A) := @proj1_sig _ _.
Global Instance: FinCollection A (listset A).
Proof. split. apply _. done. by intros [??]. Qed.
End list_collection.
......@@ -7,40 +7,40 @@ Require Export prelude fin_maps.
Local Open Scope N_scope.
Record Nmap A := { Nmap_0 : option A; Nmap_pos : Pmap A }.
Record Nmap A := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
Arguments Nmap_0 {_} _.
Arguments Nmap_pos {_} _.
Arguments Build_Nmap {_} _ _.
Arguments NMap {_} _ _.
Global Instance Pmap_dec `{ x y : A, Decision (x = y)} :
Instance Pmap_dec `{ x y : A, Decision (x = y)} :
x y : Nmap A, Decision (x = y).
Proof. solve_decision. Defined.
Global Instance Nempty {A} : Empty (Nmap A) := Build_Nmap None .
Global Instance Nlookup: Lookup N Nmap := λ A i t,
Instance Nempty {A} : Empty (Nmap A) := NMap None .
Instance Nlookup {A} : Lookup N (Nmap A) A := λ i t,
match i with
| N0 => Nmap_0 t
| Npos p => Nmap_pos t !! p
end.
Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
Instance Npartial_alter {A} : PartialAlter N (Nmap A) A := λ f i t,
match i, t with
| N0, Build_Nmap o t => Build_Nmap (f o) t
| Npos p, Build_Nmap o t => Build_Nmap o (partial_alter f p t)
| N0, NMap o t => NMap (f o) t
| Npos p, NMap o t => NMap o (partial_alter f p t)
end.
Global Instance Ndom: Dom N Nmap := λ C _ _ _ _ t,
Instance Ndom {A} : Dom N (Nmap A) := λ C _ _ _ t,
match t with
| Build_Nmap o t => option_case (λ _, {[ 0 ]}) o (Pdom_raw Npos (`t))
| NMap o t => option_case (λ _, {[ 0 ]}) o (Pdom_raw Npos (`t))
end.
Global Instance Nmerge: Merge Nmap := λ A f t1 t2,
Instance Nmerge: Merge Nmap := λ A f t1 t2,
match t1, t2 with
| Build_Nmap o1 t1, Build_Nmap o2 t2 => Build_Nmap (f o1 o2) (merge f t1 t2)
| NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
end.
Global Instance Nfmap {A B} (f : A B) : FMap Nmap f := λ t,
Instance Nfmap: FMap Nmap := λ A B f t,
match t with
| Build_Nmap o t => Build_Nmap (fmap f o) (fmap f t)
| NMap o t => NMap (fmap f o) (fmap f t)
end.
Global Instance: FinMap N Nmap.
Instance: FinMap N Nmap.
Proof.
split.
* intros ? [??] [??] H. f_equal.
......@@ -53,9 +53,9 @@ Proof.
* intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
intros. apply lookup_partial_alter_ne. congruence.
* intros ??? [??] []; simpl. done. apply lookup_fmap.
* intros ?? ???????? [o t] n; simpl.
* intros ?? ??????? [o t] n; simpl.
rewrite elem_of_union, Plookup_raw_dom.
destruct o, n; esolve_elem_of (simplify_is_Some; eauto).
destruct o, n; esolve_elem_of (inv_is_Some; eauto).
* intros ? f ? [o1 t1] [o2 t2] [|?]; simpl.
+ done.
+ apply (merge_spec f t1 t2).
......
......@@ -6,8 +6,25 @@ notations. *)
Require Export PArith NArith ZArith.
Require Export base decidable.
Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y < z" (at level 70, y at next level).
Reserved Notation "x < y < z" (at level 70, y at next level).
Reserved Notation "x < y ≤ z" (at level 70, y at next level).
Infix "≤" := le : nat_scope.
Notation "x ≤ y ≤ z" := (x y y z)%nat : nat_scope.
Notation "x ≤ y < z" := (x y y < z)%nat : nat_scope.
Notation "x < y < z" := (x < y y < z)%nat : nat_scope.
Notation "x < y ≤ z" := (x < y y z)%nat : nat_scope.
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.
Infix "`div`" := NPeano.div (at level 35) : nat_scope.
Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope.
Instance nat_eq_dec: x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_le_dec: x y : nat, Decision (x y) := le_dec.
Instance nat_lt_dec: x y : nat, Decision (x < y) := lt_dec.
Lemma lt_n_SS n : n < S (S n).
Proof. auto with arith. Qed.
......@@ -19,9 +36,16 @@ Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.
Infix "≤" := N.le : N_scope.
Notation "x ≤ y ≤ z" := (x y y z)%N : N_scope.
Notation "x ≤ y < z" := (x y y < z)%N : N_scope.
Notation "x < y < z" := (x < y y < z)%N : N_scope.
Notation "x < y ≤ z" := (x < y y z)%N : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.
Notation "(<)" := N.lt (only parsing) : N_scope.
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : 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
......@@ -37,8 +61,13 @@ Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
Next Obligation. congruence. Qed.
Infix "≤" := Z.le : Z_scope.
Notation "x ≤ y ≤ z" := (x y y z)%Z : Z_scope.
Notation "x ≤ y < z" := (x y y < z)%Z : Z_scope.
Notation "x < y < z" := (x < y y < z)%Z : Z_scope.
Notation "x < y ≤ z" := (x < y y z)%Z : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Notation "(<)" := Z.lt (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.
Instance Z_lt_dec: x y : Z, Decision (x < y)%Z := Z_lt_dec.
......@@ -63,3 +92,61 @@ used for binary relations. It yields one if [R x y] and zero if not [R x y]. *)
Definition Z_decide_rel {A B} (R : A B Prop)
{dec : x y, Decision (R x y)} (x : A) (y : B) : Z :=
(if dec x y then 1 else 0)%Z.
(** Some correspondence lemmas between [nat] and [N] that are not part of the
standard library. We declare a hint database [natify] to rewrite a goal
involving [N] into a corresponding variant involving [nat]. *)
Lemma N_to_nat_lt x y : N.to_nat x < N.to_nat y (x < y)%N.
Proof. by rewrite <-N.compare_lt_iff, nat_compare_lt, N2Nat.inj_compare. Qed.
Lemma N_to_nat_le x y : N.to_nat x N.to_nat y (x y)%N.
Proof. by rewrite <-N.compare_le_iff, nat_compare_le, N2Nat.inj_compare. Qed.
Lemma N_to_nat_0 : N.to_nat 0 = 0.
Proof. done. Qed.
Lemma N_to_nat_1 : N.to_nat 1 = 1.
Proof. done. Qed.
Lemma N_to_nat_div x y : N.to_nat (x `div` y) = N.to_nat x `div` N.to_nat y.
Proof.
destruct (decide (y = 0%N)).
{ subst. by destruct x. }
apply NPeano.Nat.div_unique with (N.to_nat (x `mod` y)).
{ by apply N_to_nat_lt, N.mod_lt. }
rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
Qed.
(* We have [x `mod` 0 = 0] on [nat], and [x `mod` 0 = x] on [N]. *)
Lemma N_to_nat_mod x y :
y 0%N
N.to_nat (x `mod` y) = N.to_nat x `mod` N.to_nat y.
Proof.
intros.
apply NPeano.Nat.mod_unique with (N.to_nat (x `div` y)).
{ by apply N_to_nat_lt, N.mod_lt. }
rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
Qed.
Hint Rewrite <-N2Nat.inj_iff : natify.
Hint Rewrite <-N_to_nat_lt : natify.
Hint Rewrite <-N_to_nat_le : natify.
Hint Rewrite Nat2N.id : natify.
Hint Rewrite N2Nat.inj_add : natify.
Hint Rewrite N2Nat.inj_mul : natify.
Hint Rewrite N2Nat.inj_sub : natify.
Hint Rewrite N2Nat.inj_succ : natify.
Hint Rewrite N2Nat.inj_pred : natify.
Hint Rewrite N_to_nat_div : natify.
Hint Rewrite N_to_nat_0 : natify.
Hint Rewrite N_to_nat_1 : natify.
Ltac natify := repeat autorewrite with natify in *.
Hint Extern 100 (Nlt _ _) => natify : natify.
Hint Extern 100 (Nle _ _) => natify : natify.
Hint Extern 100 (@eq N _ _) => natify : natify.
Hint Extern 100 (lt _ _) => natify : natify.
Hint Extern 100 (le _ _) => natify : natify.
Hint Extern 100 (@eq nat _ _) => natify : natify.
Instance: x, PropHolds (0 < x)%N