Library ATBR.Numbers
This file describes an interface NUM for abstract numbers and a
functor that gives properties about them. One specificity of this
interface is that we require an implemantation of both FSet and
FMap on our numbers.
This interface is then instanciated with positive, and we are able to use positive maps in our development.
In NUMUTILS we define a tactic num_omega (and its couterparts num_omega_false), that reflects equalities and inequalities from num into nat and then calls omega. This tactic is implemented with autorewrite libraires.
In NUMUTILS, we also define tactics num_analyse and num_prop which respectively performs case analysis on function calls, and reflection from boolean functions into the underlying relations. (See BoolView.v for more details)
This interface is then instanciated with positive, and we are able to use positive maps in our development.
In NUMUTILS we define a tactic num_omega (and its couterparts num_omega_false), that reflects equalities and inequalities from num into nat and then calls omega. This tactic is implemented with autorewrite libraires.
In NUMUTILS, we also define tactics num_analyse and num_prop which respectively performs case analysis on function calls, and reflection from boolean functions into the underlying relations. (See BoolView.v for more details)
Require Import Common.
Require Import BoolView.
Require Import MyFSets MyFSetProperties MyFMapProperties FSetPositive FMapPositive.
Module Type NUM.
Variable num : Type.
Parameter nat_of_num : num -> nat.
Parameter num_of_nat : nat -> num.
Parameter leb : num -> num -> bool.
Parameter ltb : num -> num -> bool.
Parameter eqb : num -> num -> bool.
Parameter compare : num -> num -> comparison.
Parameter le : num -> num -> Prop.
Parameter lt : num -> num -> Prop.
Parameter S : num -> num.
Parameter max: num -> num -> num.
Parameter fold_num : forall A, (num -> A -> A) -> num -> A -> A.
Parameter fold_num_sum : forall E T, (num -> T -> T + E) -> num -> T -> (T + E).
Parameter pi0: num -> num.
Parameter pi1: num -> num.
Parameter pimatch: num -> num + num.
Declare Module NumOTA: OrderedTypeAlt with Definition t := num.
Declare Module NumSet: FSetInterface.S with Definition E.t := num.
Declare Module NumMap: FMapInterface.S with Definition E.t := num.
Parameter code: NumSet.t -> num.
Notation "0" := (num_of_nat O).
Notation "n < m" := (lt n m) (at level 70).
Notation "n <= m" := (le n m) (at level 70).
Hypothesis id_num : forall n, num_of_nat (nat_of_num n) = n.
Hypothesis id_nat : forall n, nat_of_num (num_of_nat n) = n.
Hypothesis le_spec : forall n m, reflect (le n m) (leb n m).
Hypothesis lt_spec : forall n m, reflect (lt n m) (ltb n m).
Hypothesis eq_spec : forall n m, reflect (n = m) (eqb n m).
Hypothesis compare_spec : forall n m, compare_spec eq lt n m (compare n m).
Hypothesis S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
Hypothesis max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
Hypothesis le_nat_spec : forall n m, n <= m <-> (nat_of_num n <= nat_of_num m)%nat.
Hypothesis lt_nat_spec : forall n m, n < m <-> (nat_of_num n < nat_of_num m)%nat.
Hypothesis set_eq_spec : forall x y, NumSet.E.eq x y <-> x = y.
Hypothesis map_eq_spec : forall x y, NumMap.E.eq x y <-> x = y.
Hypothesis fold_num_O: forall A (a: A) f, fold_num f 0 a = a.
Hypothesis fold_num_S: forall A (a: A) f n, fold_num f (S n) a = fold_num f n (f n a).
Hypothesis fold_num_sum_O: forall E T a f, @fold_num_sum E T f 0 a = inl a.
Hypothesis fold_num_sum_S: forall E T a f n, @fold_num_sum E T f (S n) a =
match f n a with
| inl a => fold_num_sum f n a
| e => e
end.
Hypothesis match_pi0: forall n, pimatch (pi0 n) = inl n.
Hypothesis match_pi1: forall n, pimatch (pi1 n) = inr n.
Hypothesis lt_pi0: forall n m, n < m -> pi0 n < pi0 m.
Hypothesis lt_pi1: forall n m, n < m -> pi1 n < pi1 m.
End NUM.
Variable num : Type.
Parameter nat_of_num : num -> nat.
Parameter num_of_nat : nat -> num.
Parameter leb : num -> num -> bool.
Parameter ltb : num -> num -> bool.
Parameter eqb : num -> num -> bool.
Parameter compare : num -> num -> comparison.
Parameter le : num -> num -> Prop.
Parameter lt : num -> num -> Prop.
Parameter S : num -> num.
Parameter max: num -> num -> num.
Parameter fold_num : forall A, (num -> A -> A) -> num -> A -> A.
Parameter fold_num_sum : forall E T, (num -> T -> T + E) -> num -> T -> (T + E).
Parameter pi0: num -> num.
Parameter pi1: num -> num.
Parameter pimatch: num -> num + num.
Declare Module NumOTA: OrderedTypeAlt with Definition t := num.
Declare Module NumSet: FSetInterface.S with Definition E.t := num.
Declare Module NumMap: FMapInterface.S with Definition E.t := num.
Parameter code: NumSet.t -> num.
Notation "0" := (num_of_nat O).
Notation "n < m" := (lt n m) (at level 70).
Notation "n <= m" := (le n m) (at level 70).
Hypothesis id_num : forall n, num_of_nat (nat_of_num n) = n.
Hypothesis id_nat : forall n, nat_of_num (num_of_nat n) = n.
Hypothesis le_spec : forall n m, reflect (le n m) (leb n m).
Hypothesis lt_spec : forall n m, reflect (lt n m) (ltb n m).
Hypothesis eq_spec : forall n m, reflect (n = m) (eqb n m).
Hypothesis compare_spec : forall n m, compare_spec eq lt n m (compare n m).
Hypothesis S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
Hypothesis max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
Hypothesis le_nat_spec : forall n m, n <= m <-> (nat_of_num n <= nat_of_num m)%nat.
Hypothesis lt_nat_spec : forall n m, n < m <-> (nat_of_num n < nat_of_num m)%nat.
Hypothesis set_eq_spec : forall x y, NumSet.E.eq x y <-> x = y.
Hypothesis map_eq_spec : forall x y, NumMap.E.eq x y <-> x = y.
Hypothesis fold_num_O: forall A (a: A) f, fold_num f 0 a = a.
Hypothesis fold_num_S: forall A (a: A) f n, fold_num f (S n) a = fold_num f n (f n a).
Hypothesis fold_num_sum_O: forall E T a f, @fold_num_sum E T f 0 a = inl a.
Hypothesis fold_num_sum_S: forall E T a f n, @fold_num_sum E T f (S n) a =
match f n a with
| inl a => fold_num_sum f n a
| e => e
end.
Hypothesis match_pi0: forall n, pimatch (pi0 n) = inl n.
Hypothesis match_pi1: forall n, pimatch (pi1 n) = inr n.
Hypothesis lt_pi0: forall n m, n < m -> pi0 n < pi0 m.
Hypothesis lt_pi1: forall n m, n < m -> pi1 n < pi1 m.
End NUM.
Module NumUtils (N : NUM).
Export N.
Module NumSetProps := MySetProps NumSet.
Module NumMapProps := MyMapProps NumMap.
Notation "0" := (num_of_nat O) : num_scope.
Notation "1" := (num_of_nat 1) : num_scope.
Notation "2" := (num_of_nat 2) : num_scope.
Notation "3" := (num_of_nat 3) : num_scope.
Notation "5" := (num_of_nat 5) : num_scope.
Notation "7" := (num_of_nat 7) : num_scope.
Notation "n < m" := (lt n m) (at level 70) : num_scope.
Notation "n <= m" := (le n m) (at level 70) : num_scope.
Open Scope num_scope.
Instance le_preorder: PreOrder le.
Instance lt_transitive: Transitive lt.
Lemma num_peano_rec :
forall (P : num -> Type), P (num_of_nat O) -> (forall p, P p -> P (S p)) -> forall p, P p.
Lemma eq_nat_spec : forall n m, n = m <-> nat_of_num n = nat_of_num m.
Coercion num_of_nat : nat >-> num.
Coercion nat_of_num : num >-> nat.
Lemma pi0_inj: forall i j, pi0 i = pi0 j -> i = j.
Lemma pi1_inj: forall i j, pi1 i = pi1 j -> i = j.
Instance fold_num_compat' {A} {R} `{E: Equivalence A R}:
Proper (pointwise_relation num (R ==> R) ==> pointwise_relation num (R ==> R)) (@fold_num A).
Instance fold_num_compat T: Proper
(pointwise_relation num (pointwise_relation T (@eq T))
==>
pointwise_relation num (pointwise_relation T (@eq T))) (@fold_num T).
Export N.
Module NumSetProps := MySetProps NumSet.
Module NumMapProps := MyMapProps NumMap.
Notation "0" := (num_of_nat O) : num_scope.
Notation "1" := (num_of_nat 1) : num_scope.
Notation "2" := (num_of_nat 2) : num_scope.
Notation "3" := (num_of_nat 3) : num_scope.
Notation "5" := (num_of_nat 5) : num_scope.
Notation "7" := (num_of_nat 7) : num_scope.
Notation "n < m" := (lt n m) (at level 70) : num_scope.
Notation "n <= m" := (le n m) (at level 70) : num_scope.
Open Scope num_scope.
Instance le_preorder: PreOrder le.
Instance lt_transitive: Transitive lt.
Lemma num_peano_rec :
forall (P : num -> Type), P (num_of_nat O) -> (forall p, P p -> P (S p)) -> forall p, P p.
Lemma eq_nat_spec : forall n m, n = m <-> nat_of_num n = nat_of_num m.
Coercion num_of_nat : nat >-> num.
Coercion nat_of_num : num >-> nat.
Lemma pi0_inj: forall i j, pi0 i = pi0 j -> i = j.
Lemma pi1_inj: forall i j, pi1 i = pi1 j -> i = j.
Instance fold_num_compat' {A} {R} `{E: Equivalence A R}:
Proper (pointwise_relation num (R ==> R) ==> pointwise_relation num (R ==> R)) (@fold_num A).
Instance fold_num_compat T: Proper
(pointwise_relation num (pointwise_relation T (@eq T))
==>
pointwise_relation num (pointwise_relation T (@eq T))) (@fold_num T).
Instance eqb_view : Type_View eqb := { type_view := eq_spec }.
Instance leb_view : Type_View leb := { type_view := le_spec }.
Instance ltb_view : Type_View ltb := { type_view := lt_spec }.
Ltac num_analyse :=
repeat first [ type_view eqb | type_view leb | type_view ltb ].
Lemma leb_true : forall x y, leb x y = true <-> le x y.
Lemma leb_false : forall x y, leb x y = false <-> lt y x.
Lemma ltb_true : forall x y, ltb x y = true <-> lt x y.
Lemma ltb_false : forall x y, ltb x y = false <-> le y x.
Lemma eqb_true : forall x y, eqb x y = true <-> x = y.
Lemma eqb_false : forall x y, eqb x y = false <-> x <> y.
Lemma eq_num_dec: forall (n m: num), {n=m} + {n<>m}.
Hint Rewrite
leb_true leb_false
ltb_true ltb_false
eqb_true eqb_false : num_prop.
Ltac num_prop := autorewrite with num_prop in *.
Lemma eqb_refl: forall x, eqb x x = true.
Lemma leb_refl: forall x, leb x x = true.
Hint Rewrite eqb_refl leb_refl id_nat id_num: bool_simpl.
Lemma leb_false : forall x y, leb x y = false <-> lt y x.
Lemma ltb_true : forall x y, ltb x y = true <-> lt x y.
Lemma ltb_false : forall x y, ltb x y = false <-> le y x.
Lemma eqb_true : forall x y, eqb x y = true <-> x = y.
Lemma eqb_false : forall x y, eqb x y = false <-> x <> y.
Lemma eq_num_dec: forall (n m: num), {n=m} + {n<>m}.
Hint Rewrite
leb_true leb_false
ltb_true ltb_false
eqb_true eqb_false : num_prop.
Ltac num_prop := autorewrite with num_prop in *.
Lemma eqb_refl: forall x, eqb x x = true.
Lemma leb_refl: forall x, leb x x = true.
Hint Rewrite eqb_refl leb_refl id_nat id_num: bool_simpl.
Lemma num_of_nat_comm : forall x y, x = num_of_nat y <-> nat_of_num x = y.
Lemma nat_of_num_comm : forall x y, num_of_nat y = x <-> y = nat_of_num x .
Hint Rewrite eq_nat_spec le_nat_spec lt_nat_spec S_nat_spec max_spec : num_omega.
Hint Rewrite nat_of_num_comm num_of_nat_comm : num_omega .
Hint Rewrite id_nat id_num : num_omega.
Ltac num_simpl := autorewrite with num_omega in *.
Ltac num_omega := num_simpl; intuition (subst; omega).
Ltac num_omega_false := exfalso; num_omega.
Lemma eqb_eq_nat_bool: forall i j,
eqb i j = eq_nat_bool (nat_of_num i) (nat_of_num j).
Lemma numseteqb_eq_nat_bool: forall i j,
NumSetProps.eqb i j = eq_nat_bool (nat_of_num i) (nat_of_num j).
Hint Rewrite numseteqb_eq_nat_bool : bool_simpl.
Lemma le_antisym: forall n m: num, n <= m -> m <= n -> n = m.
End NumUtils.
Lemma nat_of_num_comm : forall x y, num_of_nat y = x <-> y = nat_of_num x .
Hint Rewrite eq_nat_spec le_nat_spec lt_nat_spec S_nat_spec max_spec : num_omega.
Hint Rewrite nat_of_num_comm num_of_nat_comm : num_omega .
Hint Rewrite id_nat id_num : num_omega.
Ltac num_simpl := autorewrite with num_omega in *.
Ltac num_omega := num_simpl; intuition (subst; omega).
Ltac num_omega_false := exfalso; num_omega.
Lemma eqb_eq_nat_bool: forall i j,
eqb i j = eq_nat_bool (nat_of_num i) (nat_of_num j).
Lemma numseteqb_eq_nat_bool: forall i j,
NumSetProps.eqb i j = eq_nat_bool (nat_of_num i) (nat_of_num j).
Hint Rewrite numseteqb_eq_nat_bool : bool_simpl.
Lemma le_antisym: forall n m: num, n <= m -> m <= n -> n = m.
End NumUtils.
Module Positive <: NUM.
Definition num := positive.
Definition nat_of_num n := pred (nat_of_P n).
Definition num_of_nat := P_of_succ_nat.
Definition le := Ple.
Definition lt := Plt.
Definition compare n m := Pcompare n m Eq.
Definition leb (n m: num) :=
match Pcompare n m Eq with
| Gt => false
| _ => true
end.
Definition ltb (n m: num) :=
match Pcompare n m Eq with
| Lt => true
| _ => false
end.
Definition eqb := eq_pos_bool.
Definition S := Psucc.
Definition max := Pmax.
Definition fold_num T (f: num -> T -> T) :=
Prect (fun _ => T -> T) (fun acc => acc) (fun a aux acc => aux (f a acc)).
Fixpoint PeanoView_sum_iter E T (f: positive -> T -> T + E) p (q: PeanoView p) a :=
match q with
| PeanoOne => inl a
| PeanoSucc p q =>
match f p a with
| inl a => PeanoView_sum_iter f q a
| e => e
end
end.
Definition fold_num_sum E T (f: num -> T -> T + E) p a := PeanoView_sum_iter f (peanoView p) a.
Definition pi0 := xO.
Definition pi1 := xI.
Definition pimatch i := match i with xO i => inl i | xI i => inr i | xH => inl xH end.
Lemma id_num : forall n, num_of_nat (nat_of_num n) = n.
Lemma id_nat : forall n, nat_of_num (num_of_nat n) = n.
Lemma le_spec : forall n m, reflect (le n m) (leb n m).
Lemma lt_spec : forall n m, reflect (lt n m) (ltb n m).
Definition eq_spec := eq_pos_spec.
Lemma compare_spec : forall n m, compare_spec eq lt n m (compare n m).
Lemma S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
Lemma le_nat_spec : forall n m, le n m <-> (nat_of_num n <= nat_of_num m)%nat.
Lemma lt_nat_spec : forall n m, lt n m <-> (nat_of_num n < nat_of_num m)%nat.
Lemma max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
Lemma fold_num_O: forall A (a: A) f, fold_num f xH a = a.
Lemma fold_num_S: forall A (a: A) f n, fold_num f (S n) a = fold_num f n (f n a).
Lemma fold_num_sum_O: forall E T a f, @fold_num_sum E T f (num_of_nat 0) a = inl a.
Lemma fold_num_sum_S: forall E T a f n, @fold_num_sum E T f (S n) a =
match f n a with
| inl a => fold_num_sum f n a
| e => e
end.
Lemma match_pi0: forall n, pimatch (pi0 n) = inl n.
Lemma match_pi1: forall n, pimatch (pi1 n) = inr n.
Lemma lt_pi0: forall n m, lt n m -> lt (pi0 n) (pi0 m).
Lemma lt_pi1: forall n m, lt n m -> lt (pi1 n) (pi1 m).
Module NumOTA := Pos_as_OTA.
Module NumSet' := FSetPositive.PositiveSet. Module NumSet := FSetHide NumSet'.
Module NumMap' := FMapPositive.PositiveMap. Module NumMap := FMapHide NumMap'.
Local Open Scope positive_scope.
Definition triangle k i :=
match k with
| 1 => i
| k'~0 => k'*Pdouble_minus_one k'+i
| k'~1 => k'*k+i
end.
Definition enc i j := triangle (Ppred (i+j)) i.
Fixpoint code (x: NumSet.t): num :=
match x with
| NumSet'.Leaf => 1
| NumSet'.Node l true r => enc (code l) (code r)~0
| NumSet'.Node l false r => enc (code l) (code r)~1
end.
Ltac psubst :=
(repeat match goal with
| H: Pos_as_OTA.compare _ _ = Eq |- _ => apply Pos_as_OTA.reflect in H
end); subst.
Hint Extern 0 (Pos_as_OTA.compare _ _ = Eq) => apply Pos_as_OT.eq_refl.
Lemma pcompare_prop: forall x y, Pos_as_OTA.compare x y = Eq <-> x = y.
Hint Rewrite pcompare_prop : num_prop.
Lemma set_eq_spec : forall x y, NumSet.E.eq x y <-> x = y.
Lemma map_eq_spec : forall x y, NumMap.E.eq x y <-> x = y.
End Positive.
Module PositiveUtils := NumUtils Positive.
Definition num := positive.
Definition nat_of_num n := pred (nat_of_P n).
Definition num_of_nat := P_of_succ_nat.
Definition le := Ple.
Definition lt := Plt.
Definition compare n m := Pcompare n m Eq.
Definition leb (n m: num) :=
match Pcompare n m Eq with
| Gt => false
| _ => true
end.
Definition ltb (n m: num) :=
match Pcompare n m Eq with
| Lt => true
| _ => false
end.
Definition eqb := eq_pos_bool.
Definition S := Psucc.
Definition max := Pmax.
Definition fold_num T (f: num -> T -> T) :=
Prect (fun _ => T -> T) (fun acc => acc) (fun a aux acc => aux (f a acc)).
Fixpoint PeanoView_sum_iter E T (f: positive -> T -> T + E) p (q: PeanoView p) a :=
match q with
| PeanoOne => inl a
| PeanoSucc p q =>
match f p a with
| inl a => PeanoView_sum_iter f q a
| e => e
end
end.
Definition fold_num_sum E T (f: num -> T -> T + E) p a := PeanoView_sum_iter f (peanoView p) a.
Definition pi0 := xO.
Definition pi1 := xI.
Definition pimatch i := match i with xO i => inl i | xI i => inr i | xH => inl xH end.
Lemma id_num : forall n, num_of_nat (nat_of_num n) = n.
Lemma id_nat : forall n, nat_of_num (num_of_nat n) = n.
Lemma le_spec : forall n m, reflect (le n m) (leb n m).
Lemma lt_spec : forall n m, reflect (lt n m) (ltb n m).
Definition eq_spec := eq_pos_spec.
Lemma compare_spec : forall n m, compare_spec eq lt n m (compare n m).
Lemma S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
Lemma le_nat_spec : forall n m, le n m <-> (nat_of_num n <= nat_of_num m)%nat.
Lemma lt_nat_spec : forall n m, lt n m <-> (nat_of_num n < nat_of_num m)%nat.
Lemma max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
Lemma fold_num_O: forall A (a: A) f, fold_num f xH a = a.
Lemma fold_num_S: forall A (a: A) f n, fold_num f (S n) a = fold_num f n (f n a).
Lemma fold_num_sum_O: forall E T a f, @fold_num_sum E T f (num_of_nat 0) a = inl a.
Lemma fold_num_sum_S: forall E T a f n, @fold_num_sum E T f (S n) a =
match f n a with
| inl a => fold_num_sum f n a
| e => e
end.
Lemma match_pi0: forall n, pimatch (pi0 n) = inl n.
Lemma match_pi1: forall n, pimatch (pi1 n) = inr n.
Lemma lt_pi0: forall n m, lt n m -> lt (pi0 n) (pi0 m).
Lemma lt_pi1: forall n m, lt n m -> lt (pi1 n) (pi1 m).
Module NumOTA := Pos_as_OTA.
Module NumSet' := FSetPositive.PositiveSet. Module NumSet := FSetHide NumSet'.
Module NumMap' := FMapPositive.PositiveMap. Module NumMap := FMapHide NumMap'.
Local Open Scope positive_scope.
Definition triangle k i :=
match k with
| 1 => i
| k'~0 => k'*Pdouble_minus_one k'+i
| k'~1 => k'*k+i
end.
Definition enc i j := triangle (Ppred (i+j)) i.
Fixpoint code (x: NumSet.t): num :=
match x with
| NumSet'.Leaf => 1
| NumSet'.Node l true r => enc (code l) (code r)~0
| NumSet'.Node l false r => enc (code l) (code r)~1
end.
Ltac psubst :=
(repeat match goal with
| H: Pos_as_OTA.compare _ _ = Eq |- _ => apply Pos_as_OTA.reflect in H
end); subst.
Hint Extern 0 (Pos_as_OTA.compare _ _ = Eq) => apply Pos_as_OT.eq_refl.
Lemma pcompare_prop: forall x y, Pos_as_OTA.compare x y = Eq <-> x = y.
Hint Rewrite pcompare_prop : num_prop.
Lemma set_eq_spec : forall x y, NumSet.E.eq x y <-> x = y.
Lemma map_eq_spec : forall x y, NumMap.E.eq x y <-> x = y.
End Positive.
Module PositiveUtils := NumUtils Positive.