diff options
Diffstat (limited to 'Instances.v')
| -rw-r--r-- | Instances.v | 31 |
1 files changed, 18 insertions, 13 deletions
diff --git a/Instances.v b/Instances.v index 8ddf9e4..55dffbb 100644 --- a/Instances.v +++ b/Instances.v @@ -6,6 +6,11 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) +Require List. +Require Arith NArith Max Min. +Require ZArith Zminmax. +Require QArith Qminmax. +Require Relations. Require Export AAC. @@ -19,7 +24,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 Min. + Import Arith NArith Max Min. Instance aac_plus_Assoc : Associative eq plus := plus_assoc. Instance aac_plus_Comm : Commutative eq plus := plus_comm. @@ -38,14 +43,14 @@ Module Peano. (* We also provide liftings from le to eq *) - Instance preorder_le : PreOrder le := Build_PreOrder _ _ le_refl le_trans. + Instance preorder_le : PreOrder le := Build_PreOrder _ le_refl le_trans. Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _. End Peano. Module Z. - Require Import ZArith Zminmax. + Import ZArith Zminmax. Open Scope Z_scope. Instance aac_Zplus_Assoc : Associative eq Zplus := Zplus_assoc. Instance aac_Zplus_Comm : Commutative eq Zplus := Zplus_comm. @@ -63,13 +68,13 @@ Module Z. Instance aac_zero_Zplus : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r. (* We also provide liftings from le to eq *) - Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ _ Zle_refl Zle_trans. + Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ Zle_refl Zle_trans. Instance lift_le_eq : AAC_lift Zle eq := Build_AAC_lift eq_equivalence _. End Z. Module Lists. - Require Import List. + Import List. Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A. Instance aac_nil_append {A} : @Unit (list A) eq (@app A) (@nil A) := Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A). Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A). @@ -82,7 +87,7 @@ End Lists. Module N. - Require Import NArith. + 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 +106,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.le_refl N.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. + Import NArith. Open Scope positive_scope. Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. @@ -126,12 +131,12 @@ Module P. 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 Pos.le_refl Pos.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. Module Q. - Require Import QArith Qminmax. + Import QArith Qminmax. Instance aac_Qplus_Assoc : Associative Qeq Qplus := Qplus_assoc. Instance aac_Qplus_Comm : Commutative Qeq Qplus := Qplus_comm. @@ -148,7 +153,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 Qle_refl Qle_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. @@ -162,7 +167,7 @@ Module Prop_ops. Instance aac_False : Unit iff and True. Proof. constructor; firstorder. Qed. Program Instance aac_not_compat : Proper (iff ==> iff) not. - Solve All Obligations using firstorder. + Solve All Obligations with firstorder. Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _ _. End Prop_ops. @@ -179,7 +184,7 @@ Module Bool. End Bool. Module Relations. - Require Import Relations. + Import Relations.Relations. Section defs. Variable T : Type. Variables R S: relation T. |