diff options
Diffstat (limited to 'Instances.v')
| -rw-r--r-- | Instances.v | 263 |
1 files changed, 184 insertions, 79 deletions
diff --git a/Instances.v b/Instances.v index 1a2e08f..bb309fe 100644 --- a/Instances.v +++ b/Instances.v @@ -6,60 +6,176 @@ (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) + +Require Export AAC. + (** Instances for aac_rewrite.*) -(* At the moment, all the instances are exported even if they are packaged into modules. *) -Require Export AAC. +(* This one is not declared as an instance: this interferes badly with setoid_rewrite *) +Lemma eq_subr {X} {R} `{@Reflexive X R}: subrelation eq R. +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. - Program Instance aac_plus : @Op_AC nat eq plus 0 := @Build_Op_AC nat (@eq nat) plus 0 _ plus_0_l plus_assoc plus_comm. + Instance aac_plus_Assoc : Associative eq plus := plus_assoc. + Instance aac_plus_Comm : Commutative eq plus := plus_comm. + + Instance aac_mult_Comm : Commutative eq mult := mult_comm. + Instance aac_mult_Assoc : Associative eq mult := mult_assoc. + + Instance aac_min_Comm : Commutative eq min := min_comm. + Instance aac_min_Assoc : Associative eq min := min_assoc. + + Instance aac_max_Comm : Commutative eq max := max_comm. + Instance aac_max_Assoc : Associative eq max := max_assoc. + + Instance aac_one : Unit eq mult 1 := Build_Unit eq mult 1 mult_1_l mult_1_r. + Instance aac_zero_plus : Unit eq plus O := Build_Unit eq plus (O) plus_0_l plus_0_r. + Instance aac_zero_max : Unit eq max O := Build_Unit eq max 0 max_0_l max_0_r. + + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder le := Build_PreOrder _ _ le_refl le_trans. + Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _. - - Program Instance aac_mult : Op_AC eq mult 1 := Build_Op_AC _ _ _ mult_assoc mult_comm. - (* We also declare a default associative operation: this is currently - required to fill reification environments *) - Definition default_a := AC_A aac_plus. Existing Instance default_a. End Peano. + Module Z. - Require Import ZArith. + Require Import ZArith Zminmax. Open Scope Z_scope. - Program Instance aac_plus : Op_AC eq Zplus 0 := Build_Op_AC _ _ _ Zplus_assoc Zplus_comm. - Program Instance aac_mult : Op_AC eq Zmult 1 := Build_Op_AC _ _ Zmult_1_l Zmult_assoc Zmult_comm. - Definition default_a := AC_A aac_plus. Existing Instance default_a. + Instance aac_Zplus_Assoc : Associative eq Zplus := Zplus_assoc. + Instance aac_Zplus_Comm : Commutative eq Zplus := Zplus_comm. + + Instance aac_Zmult_Comm : Commutative eq Zmult := Zmult_comm. + Instance aac_Zmult_Assoc : Associative eq Zmult := Zmult_assoc. + + Instance aac_Zmin_Comm : Commutative eq Zmin := Zmin_comm. + Instance aac_Zmin_Assoc : Associative eq Zmin := Zmin_assoc. + + Instance aac_Zmax_Comm : Commutative eq Zmax := Zmax_comm. + Instance aac_Zmax_Assoc : Associative eq Zmax := Zmax_assoc. + + Instance aac_one : Unit eq Zmult 1 := Build_Unit eq Zmult 1 Zmult_1_l Zmult_1_r. + 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 lift_le_eq : AAC_lift Zle eq := Build_AAC_lift eq_equivalence _. + End Z. +Module Lists. + Require 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). + Proof. + repeat intro. + subst. + reflexivity. + Qed. +End Lists. + + +Module N. + Require Import NArith Nminmax. + Open Scope N_scope. + Instance aac_Nplus_Assoc : Associative eq Nplus := Nplus_assoc. + Instance aac_Nplus_Comm : Commutative eq Nplus := Nplus_comm. + + Instance aac_Nmult_Comm : Commutative eq Nmult := Nmult_comm. + Instance aac_Nmult_Assoc : Associative eq Nmult := Nmult_assoc. + + Instance aac_Nmin_Comm : Commutative eq Nmin := N.min_comm. + Instance aac_Nmin_Assoc : Associative eq Nmin := N.min_assoc. + + Instance aac_Nmax_Comm : Commutative eq Nmax := N.max_comm. + Instance aac_Nmax_Assoc : Associative eq Nmax := N.max_assoc. + + Instance aac_one : Unit eq Nmult (1)%N := Build_Unit eq Nmult (1)%N Nmult_1_l Nmult_1_r. + Instance aac_zero : Unit eq Nplus (0)%N := Build_Unit eq Nplus (0)%N Nplus_0_l Nplus_0_r. + 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 lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _. + +End N. + +Module P. + Require Import NArith Pminmax. + Open Scope positive_scope. + Instance aac_Pplus_Assoc : Associative eq Pplus := Pplus_assoc. + Instance aac_Pplus_Comm : Commutative eq Pplus := Pplus_comm. + + 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_Pmax_Comm : Commutative eq Pmax := P.max_comm. + Instance aac_Pmax_Assoc : Associative eq Pmax := P.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. + + (* 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 lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _. +End P. + Module Q. - Require Import QArith. - Program Instance aac_plus : Op_AC Qeq Qplus 0 := Build_Op_AC _ _ Qplus_0_l Qplus_assoc Qplus_comm. - Program Instance aac_mult : Op_AC Qeq Qmult 1 := Build_Op_AC _ _ Qmult_1_l Qmult_assoc Qmult_comm. - Definition default_a := AC_A aac_plus. Existing Instance default_a. + Require Import QArith Qminmax. + Instance aac_Qplus_Assoc : Associative Qeq Qplus := Qplus_assoc. + Instance aac_Qplus_Comm : Commutative Qeq Qplus := Qplus_comm. + + Instance aac_Qmult_Comm : Commutative Qeq Qmult := Qmult_comm. + Instance aac_Qmult_Assoc : Associative Qeq Qmult := Qmult_assoc. + + Instance aac_Qmin_Comm : Commutative Qeq Qmin := Q.min_comm. + Instance aac_Qmin_Assoc : Associative Qeq Qmin := Q.min_assoc. + + Instance aac_Qmax_Comm : Commutative Qeq Qmax := Q.max_comm. + Instance aac_Qmax_Assoc : Associative Qeq Qmax := Q.max_assoc. + + Instance aac_one : Unit Qeq Qmult 1 := Build_Unit Qeq Qmult 1 Qmult_1_l Qmult_1_r. + 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 lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. + End Q. Module Prop_ops. - Program Instance aac_or : Op_AC iff or False. Solve All Obligations using tauto. - - Program Instance aac_and : Op_AC iff and True. Solve All Obligations using tauto. - - Definition default_a := AC_A aac_and. Existing Instance default_a. - + Instance aac_or_Assoc : Associative iff or. Proof. unfold Associative; tauto. Qed. + Instance aac_or_Comm : Commutative iff or. Proof. unfold Commutative; tauto. Qed. + Instance aac_and_Assoc : Associative iff and. Proof. unfold Associative; tauto. Qed. + Instance aac_and_Comm : Commutative iff and. Proof. unfold Commutative; tauto. Qed. + Instance aac_True : Unit iff or False. Proof. constructor; firstorder. Qed. + 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. + + Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _ _. End Prop_ops. Module Bool. - Program Instance aac_orb : Op_AC eq orb false. - Solve All Obligations using firstorder. - - Program Instance aac_andb : Op_AC eq andb true. - Solve All Obligations using firstorder. - - Definition default_a := AC_A aac_andb. Existing Instance default_a. - - Instance negb_compat : Proper (eq ==> eq) negb. - Proof. intros [|] [|]; auto. Qed. + Instance aac_orb_Assoc : Associative eq orb. Proof. unfold Associative; firstorder. Qed. + Instance aac_orb_Comm : Commutative eq orb. Proof. unfold Commutative; firstorder. Qed. + Instance aac_andb_Assoc : Associative eq andb. Proof. unfold Associative; firstorder. Qed. + Instance aac_andb_Comm : Commutative eq andb. Proof. unfold Commutative; firstorder. Qed. + Instance aac_true : Unit eq orb false. Proof. constructor; firstorder. Qed. + Instance aac_false : Unit eq andb true. Proof. constructor; intros [|];firstorder. Qed. + + Instance negb_compat : Proper (eq ==> eq) negb. Proof. intros [|] [|]; auto. Qed. End Bool. Module Relations. @@ -75,17 +191,20 @@ Module Relations. Definition bot : relation T := fun _ _ => False. Definition top : relation T := fun _ _ => True. End defs. - - Program Instance aac_union T : Op_AC (same_relation T) (union T) (bot T). - Solve All Obligations using compute; [tauto || intuition]. - - Program Instance aac_inter T : Op_AC (same_relation T) (inter T) (top T). - Solve All Obligations using compute; firstorder. - + + Instance eq_same_relation T : Equivalence (same_relation T). Proof. firstorder. Qed. + + Instance aac_union_Comm T : Commutative (same_relation T) (union T). Proof. unfold Commutative; compute; intuition. Qed. + Instance aac_union_Assoc T : Associative (same_relation T) (union T). Proof. unfold Associative; compute; intuition. Qed. + Instance aac_bot T : Unit (same_relation T) (union T) (bot T). Proof. constructor; compute; intuition. Qed. + + Instance aac_inter_Comm T : Commutative (same_relation T) (inter T). Proof. unfold Commutative; compute; intuition. Qed. + Instance aac_inter_Assoc T : Associative (same_relation T) (inter T). Proof. unfold Associative; compute; intuition. Qed. + Instance aac_top T : Unit (same_relation T) (inter T) (top T). Proof. constructor; compute; intuition. Qed. + (* note that we use [eq] directly as a neutral element for composition *) - Program Instance aac_compo T : Op_A (same_relation T) (compo T) eq. - Solve All Obligations using compute; firstorder. - Solve All Obligations using compute; firstorder subst; trivial. + Instance aac_compo T : Associative (same_relation T) (compo T). Proof. unfold Associative; compute; firstorder. Qed. + Instance aac_eq T : Unit (same_relation T) (compo T) (eq). Proof. compute; firstorder subst; trivial. Qed. Instance negr_compat T : Proper (same_relation T ==> same_relation T) (negr T). Proof. compute. firstorder. Qed. @@ -94,57 +213,43 @@ Module Relations. Proof. compute. firstorder. Qed. Instance clos_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_trans T). - Proof. - intros R S H x y Hxy. induction Hxy. + Proof. + intros R S H x y Hxy. induction Hxy. constructor 1. apply H. assumption. - econstructor 2; eauto 3. + econstructor 2; eauto 3. Qed. - Instance clos_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_trans T). - Proof. intros R S H; split; apply clos_trans_incr, H. Qed. + Instance clos_trans_compat T: Proper (same_relation T ==> same_relation T) (clos_trans T). + Proof. intros R S H; split; apply clos_trans_incr, H. Qed. Instance clos_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T). - Proof. - intros R S H x y Hxy. induction Hxy. + Proof. + intros R S H x y Hxy. induction Hxy. constructor 1. apply H. assumption. constructor 2. - econstructor 3; eauto 3. + econstructor 3; eauto 3. Qed. Instance clos_refl_trans_compat T : Proper (same_relation T ==> same_relation T) (clos_refl_trans T). - Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed. - + Proof. intros R S H; split; apply clos_refl_trans_incr, H. Qed. + + Instance preorder_inclusion T : PreOrder (inclusion T). + Proof. constructor; unfold Reflexive, Transitive, inclusion; intuition. Qed. + + Instance lift_inclusion_same_relation T: AAC_lift (inclusion T) (same_relation T) := + Build_AAC_lift (eq_same_relation T) _. + Proof. firstorder. Qed. + End Relations. Module All. Export Peano. Export Z. + Export P. + Export N. Export Prop_ops. Export Bool. Export Relations. End All. - -(* A small test to ensure that everything can live together *) -(* Section test. - Import All. - Require Import ZArith. - Open Scope Z_scope. - Notation "x ^2" := (x*x) (at level 40). - Hypothesis H : forall x y, x^2 + y^2 + x*y + x* y = (x+y)^2. - Goal forall a b c, a*1*(a ^2)*a + c + (b+0)*1*b + a^2*b + a*b*a = (a^2+b)^2+c. - intros. - aac_rewrite H. - aac_rewrite <- H . - symmetry. - aac_rewrite <- H . - aac_reflexivity. - Qed. - Open Scope nat_scope. - Notation "x ^^2" := (x * x) (at level 40). - Hypothesis H' : forall (x y : nat), x^^2 + y^^2 + x*y + x* y = (x+y)^^2. - - Goal forall (a b c : nat), a*1*(a ^^2)*a + c + (b+0)*1*b + a^^2*b + a*b*a = (a^^2+b)^^2+c. - intros. aac_rewrite H'. aac_reflexivity. - Qed. -End test. - -*) - + +(* Here, we should not see any instance of our classes. + Print HintDb typeclass_instances. +*) |