diff options
Diffstat (limited to 'Instances.v')
| -rw-r--r-- | Instances.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/Instances.v b/Instances.v index bb309fe..8ddf9e4 100644 --- a/Instances.v +++ b/Instances.v @@ -19,7 +19,7 @@ Proof. intros x y ->. reflexivity. Qed. (* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*) Module Peano. - Require Import Arith NArith Max. + Require Import Arith NArith Max Min. Instance aac_plus_Assoc : Associative eq plus := plus_assoc. Instance aac_plus_Comm : Commutative eq plus := plus_comm. @@ -82,7 +82,7 @@ End Lists. Module N. - Require Import NArith Nminmax. + Require Import NArith. Open Scope N_scope. Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc. Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm. @@ -101,13 +101,13 @@ Module N. Instance aac_zero_max : Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.T.le_refl N.T.le_trans. + Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.le_refl N.le_trans. Instance lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _. End N. Module P. - Require Import NArith Pminmax. + Require Import NArith. Open Scope positive_scope. Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. @@ -115,18 +115,18 @@ Module P. Instance aac_Pmult_Comm : Commutative eq Pmult := Pmult_comm. Instance aac_Pmult_Assoc : Associative eq Pmult := Pmult_assoc. - Instance aac_Pmin_Comm : Commutative eq Pmin := P.min_comm. - Instance aac_Pmin_Assoc : Associative eq Pmin := P.min_assoc. + Instance aac_Pmin_Comm : Commutative eq Pmin := Pos.min_comm. + Instance aac_Pmin_Assoc : Associative eq Pmin := Pos.min_assoc. - Instance aac_Pmax_Comm : Commutative eq Pmax := P.max_comm. - Instance aac_Pmax_Assoc : Associative eq Pmax := P.max_assoc. + Instance aac_Pmax_Comm : Commutative eq Pmax := Pos.max_comm. + Instance aac_Pmax_Assoc : Associative eq Pmax := Pos.max_assoc. Instance aac_one : Unit eq Pmult 1 := Build_Unit eq Pmult 1 _ Pmult_1_r. intros; reflexivity. Qed. (* TODO : add this lemma in the stdlib *) - Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 P.max_1_l P.max_1_r. + Instance aac_one_max : Unit eq Pmax 1 := Build_Unit eq Pmax 1 Pos.max_1_l Pos.max_1_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple P.T.le_refl P.T.le_trans. + Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple Pos.le_refl Pos.le_trans. Instance lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _. End P. @@ -148,7 +148,7 @@ Module Q. Instance aac_zero_Qplus : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Q.T.le_refl Q.T.le_trans. + Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Qle_refl Qle_trans. Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. End Q. |