blob: 1a2e08f47922453d8507cff49a434edb60629adb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
(***************************************************************************)
(* 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. *)
(***************************************************************************)
(** Instances for aac_rewrite.*)
(* At the moment, all the instances are exported even if they are packaged into modules. *)
Require Export AAC.
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.
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.
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.
End Z.
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.
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.
Program Instance aac_not_compat : Proper (iff ==> iff) not.
Solve All Obligations using firstorder.
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.
End Bool.
Module Relations.
Require Import 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.
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.
(* 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 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.
End Relations.
Module All.
Export Peano.
Export Z.
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.
*)
|
