diff options
Diffstat (limited to 'theories/Instances.v')
| -rw-r--r-- | theories/Instances.v | 261 |
1 files changed, 261 insertions, 0 deletions
diff --git a/theories/Instances.v b/theories/Instances.v new file mode 100644 index 0000000..d007ceb --- /dev/null +++ b/theories/Instances.v @@ -0,0 +1,261 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +Require List. +Require Arith NArith Max Min. +Require ZArith Zminmax. +Require QArith Qminmax. +Require Relations. + +From AAC_tactics +Require Export AAC. + +(** Instances for aac_rewrite.*) + + +(* 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. + Import Arith NArith Max Min. + 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 _. + +End Peano. + + +Module Z. + 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. + + Instance aac_Zmult_Comm : Commutative eq Zmult := Zmult_comm. + Instance aac_Zmult_Assoc : Associative eq Zmult := Zmult_assoc. + + Instance aac_Zmin_Comm : Commutative eq Z.min := Z.min_comm. + Instance aac_Zmin_Assoc : Associative eq Z.min := Z.min_assoc. + + Instance aac_Zmax_Comm : Commutative eq Z.max := Z.max_comm. + Instance aac_Zmax_Assoc : Associative eq Z.max := Z.max_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 Z.le := Build_PreOrder _ Z.le_refl Z.le_trans. + Instance lift_le_eq : AAC_lift Z.le eq := Build_AAC_lift eq_equivalence _. + +End Z. + +Module Lists. + 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. + Import NArith. + 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 N.min := N.min_comm. + Instance aac_Nmin_Assoc : Associative eq N.min := N.min_assoc. + + Instance aac_Nmax_Comm : Commutative eq N.max := N.max_comm. + Instance aac_Nmax_Assoc : Associative eq N.max := 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 N.max 0 := Build_Unit eq N.max 0 N.max_0_l N.max_0_r. + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder N.le := Build_PreOrder N.le N.le_refl N.le_trans. + Instance lift_le_eq : AAC_lift N.le eq := Build_AAC_lift eq_equivalence _. + +End N. + +Module P. + Import NArith. + 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 Pos.min := Pos.min_comm. + Instance aac_Pmin_Assoc : Associative eq Pos.min := Pos.min_assoc. + + Instance aac_Pmax_Comm : Commutative eq Pos.max := Pos.max_comm. + Instance aac_Pmax_Assoc : Associative eq Pos.max := 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 Pos.max 1 := Build_Unit eq Pos.max 1 Pos.max_1_l Pos.max_1_r. + + (* We also provide liftings from le to eq *) + Instance preorder_le : PreOrder Pos.le := Build_PreOrder Pos.le Pos.le_refl Pos.le_trans. + Instance lift_le_eq : AAC_lift Pos.le eq := Build_AAC_lift eq_equivalence _. +End P. + +Module Q. + 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 Qle_refl Qle_trans. + Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _. + +End Q. + +Module Prop_ops. + 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 with firstorder. + + Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _ _. +End Prop_ops. + +Module Bool. + 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. + Import Relations.Relations. + Section defs. + Variable T : Type. + Variables R S: relation T. + Definition inter : relation T := fun x y => R x y /\ S x y. + Definition compo : relation T := fun x y => exists z : T, R x z /\ S z y. + Definition negr : relation T := fun x y => ~ R x y. + (* union and converse are already defined in the standard library *) + + Definition bot : relation T := fun _ _ => False. + Definition top : relation T := fun _ _ => True. + End defs. + + 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 *) + 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. + + Instance transp_compat T : Proper (same_relation T ==> same_relation T) (transp T). + 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. + constructor 1. apply H. assumption. + 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_refl_trans_incr T : Proper (inclusion T ==> inclusion T) (clos_refl_trans T). + Proof. + intros R S H x y Hxy. induction Hxy. + constructor 1. apply H. assumption. + constructor 2. + 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. + + 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. + +(* Here, we should not see any instance of our classes. + Print HintDb typeclass_instances. +*) |