From 15dffdc28a4dce5c64f44619c2c9d9381e8bab1b Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 27 Feb 2024 14:12:37 +0000
Subject: [PATCH] Deploy to GitHub pages
---
.nojekyll | 0
docs/coqdoc/AAC_tactics.AAC.html | 1372 +++++++++++++
docs/coqdoc/AAC_tactics.Caveats.html | 760 +++++++
docs/coqdoc/AAC_tactics.Constants.html | 80 +
docs/coqdoc/AAC_tactics.Instances.html | 593 ++++++
docs/coqdoc/AAC_tactics.Tutorial.html | 793 ++++++++
docs/coqdoc/AAC_tactics.Utils.html | 445 +++++
docs/coqdoc/config.js | 79 +
docs/coqdoc/coqdoc.css | 197 ++
docs/coqdoc/coqdocjs.css | 239 +++
docs/coqdoc/coqdocjs.js | 197 ++
docs/coqdoc/indexpage.html | 2411 +++++++++++++++++++++++
docs/coqdoc/toc.html | 223 +++
docs/ocamldoc/Aac_rewrite.html | 39 +
docs/ocamldoc/Coq.Classes.html | 40 +
docs/ocamldoc/Coq.Equivalence.html | 62 +
docs/ocamldoc/Coq.List.html | 46 +
docs/ocamldoc/Coq.Nat.html | 38 +
docs/ocamldoc/Coq.Option.html | 35 +
docs/ocamldoc/Coq.Pair.html | 39 +
docs/ocamldoc/Coq.Pos.html | 38 +
docs/ocamldoc/Coq.Relation.html | 52 +
docs/ocamldoc/Coq.Rewrite.html | 181 ++
docs/ocamldoc/Coq.html | 142 ++
docs/ocamldoc/Helper.CONTROL.html | 30 +
docs/ocamldoc/Helper.Debug.html | 62 +
docs/ocamldoc/Helper.html | 38 +
docs/ocamldoc/Matcher.Subst.html | 47 +
docs/ocamldoc/Matcher.Terms.html | 134 ++
docs/ocamldoc/Matcher.html | 158 ++
docs/ocamldoc/Print.html | 46 +
docs/ocamldoc/Search_monad.html | 83 +
docs/ocamldoc/Theory.Sigma.html | 58 +
docs/ocamldoc/Theory.Stubs.html | 57 +
docs/ocamldoc/Theory.Sym.html | 80 +
docs/ocamldoc/Theory.Trans.html | 157 ++
docs/ocamldoc/Theory.html | 78 +
docs/ocamldoc/index.html | 74 +
docs/ocamldoc/index_attributes.html | 26 +
docs/ocamldoc/index_class_types.html | 26 +
docs/ocamldoc/index_classes.html | 26 +
docs/ocamldoc/index_exceptions.html | 26 +
docs/ocamldoc/index_extensions.html | 26 +
docs/ocamldoc/index_methods.html | 26 +
docs/ocamldoc/index_module_types.html | 29 +
docs/ocamldoc/index_modules.html | 163 ++
docs/ocamldoc/index_types.html | 102 +
docs/ocamldoc/index_values.html | 413 ++++
docs/ocamldoc/style.css | 43 +
docs/ocamldoc/type_Aac_rewrite.html | 31 +
docs/ocamldoc/type_Coq.Classes.html | 25 +
docs/ocamldoc/type_Coq.Equivalence.html | 37 +
docs/ocamldoc/type_Coq.List.html | 22 +
docs/ocamldoc/type_Coq.Nat.html | 19 +
docs/ocamldoc/type_Coq.Option.html | 24 +
docs/ocamldoc/type_Coq.Pair.html | 25 +
docs/ocamldoc/type_Coq.Pos.html | 19 +
docs/ocamldoc/type_Coq.Relation.html | 23 +
docs/ocamldoc/type_Coq.Rewrite.html | 41 +
docs/ocamldoc/type_Coq.html | 141 ++
docs/ocamldoc/type_Helper.CONTROL.html | 19 +
docs/ocamldoc/type_Helper.Debug.html | 28 +
docs/ocamldoc/type_Helper.html | 33 +
docs/ocamldoc/type_Matcher.Subst.html | 24 +
docs/ocamldoc/type_Matcher.Terms.html | 33 +
docs/ocamldoc/type_Matcher.html | 65 +
docs/ocamldoc/type_Print.html | 25 +
docs/ocamldoc/type_Search_monad.html | 34 +
docs/ocamldoc/type_Theory.Sigma.html | 29 +
docs/ocamldoc/type_Theory.Stubs.html | 28 +
docs/ocamldoc/type_Theory.Sym.html | 24 +
docs/ocamldoc/type_Theory.Trans.html | 56 +
docs/ocamldoc/type_Theory.html | 91 +
index.html | 54 +
74 files changed, 11059 insertions(+)
create mode 100644 .nojekyll
create mode 100644 docs/coqdoc/AAC_tactics.AAC.html
create mode 100644 docs/coqdoc/AAC_tactics.Caveats.html
create mode 100644 docs/coqdoc/AAC_tactics.Constants.html
create mode 100644 docs/coqdoc/AAC_tactics.Instances.html
create mode 100644 docs/coqdoc/AAC_tactics.Tutorial.html
create mode 100644 docs/coqdoc/AAC_tactics.Utils.html
create mode 100644 docs/coqdoc/config.js
create mode 100644 docs/coqdoc/coqdoc.css
create mode 100644 docs/coqdoc/coqdocjs.css
create mode 100644 docs/coqdoc/coqdocjs.js
create mode 100644 docs/coqdoc/indexpage.html
create mode 100644 docs/coqdoc/toc.html
create mode 100644 docs/ocamldoc/Aac_rewrite.html
create mode 100644 docs/ocamldoc/Coq.Classes.html
create mode 100644 docs/ocamldoc/Coq.Equivalence.html
create mode 100644 docs/ocamldoc/Coq.List.html
create mode 100644 docs/ocamldoc/Coq.Nat.html
create mode 100644 docs/ocamldoc/Coq.Option.html
create mode 100644 docs/ocamldoc/Coq.Pair.html
create mode 100644 docs/ocamldoc/Coq.Pos.html
create mode 100644 docs/ocamldoc/Coq.Relation.html
create mode 100644 docs/ocamldoc/Coq.Rewrite.html
create mode 100644 docs/ocamldoc/Coq.html
create mode 100644 docs/ocamldoc/Helper.CONTROL.html
create mode 100644 docs/ocamldoc/Helper.Debug.html
create mode 100644 docs/ocamldoc/Helper.html
create mode 100644 docs/ocamldoc/Matcher.Subst.html
create mode 100644 docs/ocamldoc/Matcher.Terms.html
create mode 100644 docs/ocamldoc/Matcher.html
create mode 100644 docs/ocamldoc/Print.html
create mode 100644 docs/ocamldoc/Search_monad.html
create mode 100644 docs/ocamldoc/Theory.Sigma.html
create mode 100644 docs/ocamldoc/Theory.Stubs.html
create mode 100644 docs/ocamldoc/Theory.Sym.html
create mode 100644 docs/ocamldoc/Theory.Trans.html
create mode 100644 docs/ocamldoc/Theory.html
create mode 100644 docs/ocamldoc/index.html
create mode 100644 docs/ocamldoc/index_attributes.html
create mode 100644 docs/ocamldoc/index_class_types.html
create mode 100644 docs/ocamldoc/index_classes.html
create mode 100644 docs/ocamldoc/index_exceptions.html
create mode 100644 docs/ocamldoc/index_extensions.html
create mode 100644 docs/ocamldoc/index_methods.html
create mode 100644 docs/ocamldoc/index_module_types.html
create mode 100644 docs/ocamldoc/index_modules.html
create mode 100644 docs/ocamldoc/index_types.html
create mode 100644 docs/ocamldoc/index_values.html
create mode 100644 docs/ocamldoc/style.css
create mode 100644 docs/ocamldoc/type_Aac_rewrite.html
create mode 100644 docs/ocamldoc/type_Coq.Classes.html
create mode 100644 docs/ocamldoc/type_Coq.Equivalence.html
create mode 100644 docs/ocamldoc/type_Coq.List.html
create mode 100644 docs/ocamldoc/type_Coq.Nat.html
create mode 100644 docs/ocamldoc/type_Coq.Option.html
create mode 100644 docs/ocamldoc/type_Coq.Pair.html
create mode 100644 docs/ocamldoc/type_Coq.Pos.html
create mode 100644 docs/ocamldoc/type_Coq.Relation.html
create mode 100644 docs/ocamldoc/type_Coq.Rewrite.html
create mode 100644 docs/ocamldoc/type_Coq.html
create mode 100644 docs/ocamldoc/type_Helper.CONTROL.html
create mode 100644 docs/ocamldoc/type_Helper.Debug.html
create mode 100644 docs/ocamldoc/type_Helper.html
create mode 100644 docs/ocamldoc/type_Matcher.Subst.html
create mode 100644 docs/ocamldoc/type_Matcher.Terms.html
create mode 100644 docs/ocamldoc/type_Matcher.html
create mode 100644 docs/ocamldoc/type_Print.html
create mode 100644 docs/ocamldoc/type_Search_monad.html
create mode 100644 docs/ocamldoc/type_Theory.Sigma.html
create mode 100644 docs/ocamldoc/type_Theory.Stubs.html
create mode 100644 docs/ocamldoc/type_Theory.Sym.html
create mode 100644 docs/ocamldoc/type_Theory.Trans.html
create mode 100644 docs/ocamldoc/type_Theory.html
create mode 100644 index.html
diff --git a/.nojekyll b/.nojekyll
new file mode 100644
index 0000000..e69de29
diff --git a/docs/coqdoc/AAC_tactics.AAC.html b/docs/coqdoc/AAC_tactics.AAC.html
new file mode 100644
index 0000000..7c30534
--- /dev/null
+++ b/docs/coqdoc/AAC_tactics.AAC.html
@@ -0,0 +1,1372 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Theory for AAC Tactics
+
+
+
+
+ We define several base classes to package associative and possibly
+ commutative/idempotent operators, and define a data-type for reified
+ (or quoted) expressions (with morphisms).
+
+
+
+ We then define a reflexive decision procedure to decide the
+ equality of reified terms: first normalise reified terms, then
+ compare them. This allows us to close transitivity steps
+ automatically, in the
aac_rewrite tactic.
+
+
+
+ We restrict ourselves to the case where all symbols operate on a
+ single fixed type. In particular, this means that we cannot handle
+ situations like
+
+
+
+
H : forall x y , nat_of_pos (pos_of_nat (x ) + y ) + x = ...
+
+
+
+ where one occurrence of
+
operates on
nat while the other one
+ operates on
positive .
+
+
+
+
+
+
Environments for the reification process
+
+
+
+ Positive maps are used to index elements
+
+
+
+
+
Classes for properties of operators
+
+
+
+
+
+ Class used to find the equivalence relation on which operations
+ are A or AC, starting from the relation appearing in the goal
+
+
+
+
+
+Simple instances for when we have a subrelation or an equivalence
+
+
+
+
+
Utilities for the evaluation function
+
+
+
+
+
+copy n x = x+...+x
(n
times)
+
+
+
+
+
Packaging structures
+
+
+
+
Free symbols
+
+
+
+
+
+Type of an arity
+
+
+
+
+Relation to be preserved at an arity
+
+
+
Fixpoint rel_of n :
relation (
type_of n ) :=
+
match n with
+ |
O =>
R
+ |
S n =>
respectful R (
rel_of n )
+
end .
+
+
+
Register type_of as aac_tactics.internal.sym.type_of .
+
Register rel_of as aac_tactics.internal.sym.rel_of .
+
+
+
+
+
+A symbol package contains:
+
+ an arity,
+
+
+ a value of the corresponding type, and
+
+
+ a proof that the value is a proper morphism
+
+
+
+
+
+
+
+Helper to build default values, when filling reification environments
+
+
+
Definition null :
pack :=
mkPack 1 (
fun x =>
x ) (
fun _ _ H =>
H ).
+
+
+
Register null as aac_tactics.sym.null .
+
+
+
End t .
+
+
+
End Sym .
+
+
+
+
+
+
+
+
+See the Instances
module for concrete instances of these classes
+
+
+
+
+
Reification, normalisation, and decision
+
+
+
+
+
+ We use environments to store the various operators
+ and the morphisms
+
+
+
+
+
+Packaging units (depends on
e_bin )
+
+
+
+
+
Almost normalised syntax
+
+
+
+
+ A term in
T is in normal form if:
+
+ sums do not contain sums
+
+
+ products do not contain products
+
+
+ there are no unary sums or products
+
+
+ lists and msets are lexicographically sorted according to the order we define below
+
+
+
+
+
+
+
vT n denotes the set of term vectors of size
n
+ (the mutual dependency could be removed).
+
+
+
+ Note that
T and
vT depend on the
e_sym environment (which
+ contains, among other things, the arity of symbols).
+
+
+
+
+
+
Inductive T :
Type :=
+ |
sum :
idx -> mset T -> T
+ |
prd :
idx -> nelist T -> T
+ |
sym :
forall i ,
vT (
Sym.ar (
e_sym i ))
-> T
+ |
unit :
idx -> T
+
with vT :
nat -> Type :=
+ |
vnil :
vT O
+ |
vcons :
forall n ,
T -> vT n -> vT (
S n ).
+
+
+
Register T as aac_tactics.internal.T .
+
Register sum as aac_tactics.internal.sum .
+
Register prd as aac_tactics.internal.prd .
+
Register sym as aac_tactics.internal.sym .
+
Register unit as aac_tactics.internal.unit .
+
+
+
Register vnil as aac_tactics.internal.vnil .
+
Register vcons as aac_tactics.internal.vcons .
+
+
+
+
+
+Lexicographic rpo over the normalised syntax
+
+
+
Fixpoint compare (
u v :
T ) :=
+
match u ,
v with
+ |
sum i l ,
sum j vs =>
lex (
idx_compare i j ) (
mset_compare compare l vs )
+ |
prd i l ,
prd j vs =>
lex (
idx_compare i j ) (
list_compare compare l vs )
+ |
sym i l ,
sym j vs =>
lex (
idx_compare i j ) (
vcompare l vs )
+ |
unit i ,
unit j =>
idx_compare i j
+ |
unit _ ,
_ =>
Lt
+ |
_ ,
unit _ =>
Gt
+ |
sum _ _ ,
_ =>
Lt
+ |
_ ,
sum _ _ =>
Gt
+ |
prd _ _ ,
_ =>
Lt
+ |
_ ,
prd _ _ =>
Gt
+
+
end
+
with vcompare i j (
us :
vT i ) (
vs :
vT j ) :=
+
match us ,
vs with
+ |
vnil ,
vnil =>
Eq
+ |
vnil ,
_ =>
Lt
+ |
_ ,
vnil =>
Gt
+ |
vcons _ u us ,
vcons _ v vs =>
lex (
compare u v ) (
vcompare us vs )
+
end .
+
+
+
+
+
+
Evaluation from syntax to the abstract domain
+
+
+
+
+
+ We need to show that
compare reflects equality (this is because
+ we work with msets rather than with lists with arities)
+
+
+
+
+
+Is i
a unit for j
?
+
+
+
+
+Is i
commutative?
+
+
+
+
+Is i
idempotent?
+
+
+
+
+
+
+
+This is called Datatypes.sum in the stdlib
+
+
+
+
+Auxiliary functions, to clean up sums
+
+
+
+
+Similar functions for products
+
+
+
+
+
+
+
+Auxiliary lemmas about sums
+
+
+
Section sum_correctness .
+
Variable i :
idx .
+
Variable is_unit :
idx -> bool .
+
Hypothesis is_unit_sum_Unit :
forall j ,
is_unit j = true ->
+ @
Unit X R (
Bin.value (
e_bin i )) (
eval (
unit j )).
+
+
+
Inductive is_sum_spec_ind :
T -> @
discr (
mset T )
-> Prop :=
+ |
is_sum_spec_op :
forall j l ,
j = i -> is_sum_spec_ind (
sum j l ) (
Is_op l )
+ |
is_sum_spec_unit :
forall j ,
is_unit j = true -> is_sum_spec_ind (
unit j ) (
Is_unit j )
+ |
is_sum_spec_nothing :
forall u ,
is_sum_spec_ind u (
Is_nothing ).
+
+
+
Lemma is_sum_spec u :
is_sum_spec_ind u (
is_sum i is_unit u ).
+
Proof .
+
unfold is_sum ;
case u ;
intros ;
try constructor .
+
case_eq (
eq_idx_bool p i );
intros ;
subst ;
try constructor ;
auto .
+
revert H .
case eq_idx_spec ;
try discriminate .
auto .
+
case_eq (
is_unit p );
intros ;
try constructor .
auto .
+
Qed .
+
+
+
Instance assoc : @
Associative X R (
Bin.value (
e_bin i )).
+
Proof .
destruct (
e_bin i ).
simpl .
assumption .
Qed .
+
+
+
Instance proper :
Proper (
R ==> R ==> R )(
Bin.value (
e_bin i )).
+
Proof .
destruct (
e_bin i ).
simpl .
assumption .
Qed .
+
+
+
Hypothesis comm : @
Commutative X R (
Bin.value (
e_bin i )).
+
+
+
Lemma sum'_sum :
forall (
l :
mset T ),
eval (
sum' i l )
== eval (
sum i l ).
+
Proof .
+
intros [[
a n ] | [
a n ]
l ];
destruct n ;
simpl ;
reflexivity .
+
Qed .
+
+
+
Lemma eval_sum_nil x :
eval (
sum i (
nil ( x , xH ) ))
== ( eval x ) .
+
Proof .
rewrite <-
sum'_sum .
reflexivity .
Qed .
+
+
+
Lemma eval_sum_cons :
forall n a (
l :
mset T ),
+
( eval (
sum i (
( a , n ) :: l ))
) == ( @
Bin.value _ _ (
e_bin i )
+ (@
copy _ (@
Bin.value _ _ (
e_bin i ))
n (
eval a )) (
eval (
sum i l ))
) .
+
Proof .
intros n a [[? ? ]|[
b m ]
l ];
simpl ;
reflexivity .
Qed .
+
+
+
Inductive compat_sum_unit : @
m idx (
mset T )
-> Prop :=
+ |
csu_left :
forall x ,
is_unit x = true -> compat_sum_unit (
left x )
+ |
csu_right :
forall m ,
compat_sum_unit (
right m ).
+
+
+
Lemma compat_sum_unit_return x n :
compat_sum_unit (
return_sum i is_unit x n ).
+
Proof .
+
unfold return_sum .
+
case is_sum_spec ;
intros ;
try constructor ;
auto .
+
Qed .
+
+
+
Lemma compat_sum_unit_add :
forall x n h ,
+
compat_sum_unit h ->
+
compat_sum_unit (
add_to_sum i (
is_unit_of i )
x n h ).
+
Proof .
+
unfold add_to_sum ;
intros ;
inversion H ;
+
case_eq (
is_sum i (
is_unit_of i )
x );
+
intros ;
simpl ;
try constructor ||
eauto .
apply H0 .
+
Qed .
+
+
+
+ #[
local ]
Hint Extern 5 (
copy (?
n + ?
m ) (
eval ?
a )
==
+
Bin.value (
copy ?
n (
eval ?
a )) (
copy ?
m (
eval ?
a ))) =>
apply copy_plus :
core .
+ #[
local ]
Hint Extern 5 (?
x == ?
x ) =>
reflexivity :
core .
+ #[
local ]
Hint Extern 5 (
Bin.value ?
x ?
y == Bin.value ?
y ?
x ) =>
apply Bin.comm :
core .
+
+
+
Lemma eval_merge_bin :
forall (
h k :
mset T ),
+
eval (
sum i (
merge_msets compare h k ))
==
+ @
Bin.value _ _ (
e_bin i ) (
eval (
sum i h )) (
eval (
sum i k )).
+
Proof .
+
induction h as [[
a n ]|[
a n ]
h IHh ];
intro k .
+ -
simpl ;
induction k as [[
b m ]|[
b m ]
k IHk ];
simpl .
+ *
destruct (
tcompare_weak_spec a b )
as [
a |
a b |
a b ];
simpl ;
auto .
+
apply copy_plus ;
auto .
+ *
destruct (
tcompare_weak_spec a b )
as [
a |
a b |
a b ];
simpl ;
auto .
+
rewrite copy_plus ,
law_assoc ;
auto .
+
rewrite IHk ;
clear IHk .
rewrite 2
law_assoc .
+
apply proper ; [
apply law_comm |
reflexivity ].
+ -
induction k as [[
b m ]|[
b m ]
k IHk ];
simpl ;
simpl in IHh .
+ *
destruct (
tcompare_weak_spec a b )
as [
a |
a b |
a b ];
simpl .
+
rewrite (
law_comm _ (
copy m (
eval a ))).
+
rewrite law_assoc , <-
copy_plus ,
Pplus_comm ;
auto .
+
rewrite <-
law_assoc ,
IHh .
reflexivity .
+
rewrite law_comm .
reflexivity .
+ *
simpl in IHk .
+
destruct (
tcompare_weak_spec a b )
as [
a |
a b |
a b ];
simpl .
+
rewrite IHh ;
clear IHh .
rewrite 2
law_assoc .
+
rewrite (
law_comm _ (
copy m (
eval a ))).
+
rewrite law_assoc , <-
copy_plus ,
Pplus_comm ;
auto .
+
rewrite IHh ;
clear IHh .
simpl .
rewrite law_assoc .
reflexivity .
+
rewrite 2 (
law_comm (
copy m (
eval b ))).
+
rewrite law_assoc .
apply proper ; [ |
reflexivity ].
+
rewrite <-
IHk .
reflexivity .
+
Qed .
+
+
+
Lemma copy_mset' n (
l :
mset T ) :
+
copy_mset n l = nelist_map (
fun vm =>
let '
( v , m ) :=
vm in ( v , Pmult n m ) )
l .
+
Proof .
+
unfold copy_mset .
destruct n ;
try reflexivity .
+
simpl .
induction l as [|[
a l ]
IHl ];
simpl ;
try congruence .
+
destruct a ;
reflexivity .
+
Qed .
+
+
+
Lemma copy_mset_succ n (
l :
mset T ) :
+
eval (
sum i (
copy_mset (
Pos.succ n )
l ))
==
+ @
Bin.value _ _ (
e_bin i ) (
eval (
sum i l )) (
eval (
sum i (
copy_mset n l ))).
+
Proof .
+
rewrite 2
copy_mset' .
+
induction l as [[
a m ]|[
a m ]
l IHl ].
+
simpl eval .
rewrite <-
copy_plus ;
auto .
+
rewrite Pmult_Sn_m .
reflexivity .
+
simpl nelist_map .
rewrite !
eval_sum_cons .
rewrite IHl .
clear IHl .
+
rewrite Pmult_Sn_m .
rewrite copy_plus ;
auto .
rewrite <- !
law_assoc .
+
apply Binvalue_Proper ;
try reflexivity .
+
rewrite law_comm .
rewrite <- !
law_assoc .
apply proper ;
try reflexivity .
+
apply law_comm .
+
Qed .
+
+
+
Lemma copy_mset_copy :
forall n (
m :
mset T ),
eval (
sum i (
copy_mset n m ))
==
+ @
copy _ (@
Bin.value _ _ (
e_bin i ))
n (
eval (
sum i m )).
+
Proof .
+
induction n using Pind ;
intros .
+ -
unfold copy_mset .
rewrite copy_xH .
reflexivity .
+ -
rewrite copy_mset_succ .
rewrite copy_Psucc .
rewrite IHn .
reflexivity .
+
Qed .
+
+
+
Instance compat_sum_unit_Unit :
forall p ,
compat_sum_unit (
left p )
->
+ @
Unit X R (
Bin.value (
e_bin i )) (
eval (
unit p )).
+
Proof .
intros ;
inversion H ;
subst ;
auto .
Qed .
+
+
+
Lemma copy_n_unit :
forall j n ,
is_unit j = true ->
+
eval (
unit j )
== @
copy _ (
Bin.value (
e_bin i ))
n (
eval (
unit j )).
+
Proof .
+
intros ;
induction n using Prect .
+
rewrite copy_xH .
reflexivity .
+
rewrite copy_Psucc .
rewrite <-
IHn .
+
apply is_unit_sum_Unit in H .
rewrite law_neutral_left .
reflexivity .
+
Qed .
+
+
+
Lemma z0 l r (
H :
compat_sum_unit r ) :
+
eval (
sum i (
run_msets (
comp (
merge_msets compare )
l r )))
==
+
eval (
sum i ((
merge_msets compare ) (
l ) (
run_msets r ))).
+
Proof .
+
unfold comp .
unfold run_msets .
+
case_eq r ;
intros ;
subst ; [|
reflexivity ].
+
rewrite eval_merge_bin ;
auto .
+
rewrite eval_sum_nil .
+
apply compat_sum_unit_Unit in H .
+
rewrite law_neutral_right .
reflexivity .
+
Qed .
+
+
+
Lemma z1 :
forall n x ,
+
eval (
sum i (
run_msets (
return_sum i (
is_unit )
x n )))
==
+ @
copy _ (@
Bin.value _ _ (
e_bin i ))
n (
eval x ).
+
Proof .
+
intros ;
unfold return_sum ,
run_msets .
+
case (
is_sum_spec );
intros ;
subst .
+ -
rewrite copy_mset_copy ;
reflexivity .
+ -
rewrite eval_sum_nil .
apply copy_n_unit .
auto .
+ -
reflexivity .
+
Qed .
+
+
+
Lemma z2 :
forall u n x ,
compat_sum_unit x ->
+
eval (
sum i (
run_msets (
add_to_sum i (
is_unit )
u n x )))
==
+ @
Bin.value _ _ (
e_bin i )
+ (@
copy _ (@
Bin.value _ _ (
e_bin i ))
n (
eval u )) (
eval (
sum i (
run_msets x ))).
+
Proof .
+
intros u n x Hix .
+
unfold add_to_sum .
+
case is_sum_spec ;
intros ;
subst .
+ -
rewrite z0 by auto .
rewrite eval_merge_bin ,
copy_mset_copy .
reflexivity .
+ -
rewrite <-
copy_n_unit by assumption .
apply is_unit_sum_Unit in H .
+
rewrite law_neutral_left .
reflexivity .
+ -
rewrite z0 by auto .
rewrite eval_merge_bin .
reflexivity .
+
Qed .
+
+
+
End sum_correctness .
+
+
+
Lemma eval_norm_msets i norm
+ (
Comm :
Commutative R (
Bin.value (
e_bin i )))
+ (
Hnorm :
forall u ,
eval (
norm u )
== eval u ) :
+
forall h ,
eval (
sum i (
norm_msets norm i h ))
== eval (
sum i h ).
+
Proof .
+
unfold norm_msets .
+
assert (
H :
forall h :
mset T ,
+
eval (
sum i (
run_msets (
norm_msets_ i (
is_unit_of i )
norm h )))
==
+
eval (
sum i h )
/\ compat_sum_unit (
is_unit_of i ) (
norm_msets_ i (
is_unit_of i )
norm h )).
+
induction h as [[
a n ] | [
a n ]
h [
IHh IHh' ]];
simpl norm_msets_ ;
split .
+ -
rewrite z1 by auto .
rewrite Hnorm .
reflexivity .
+ -
apply compat_sum_unit_return .
+ -
rewrite z2 by auto .
rewrite IHh ,
eval_sum_cons ,
Hnorm .
reflexivity .
+ -
apply compat_sum_unit_add ,
IHh' .
+ -
apply H .
+
Defined .
+
+
+
Lemma copy_idem i (
Idem :
Idempotent R (
Bin.value (
e_bin i )))
n x :
+
copy (
plus :=(
Bin.value (
e_bin i )))
n x == x .
+
Proof .
+
induction n using Pos.peano_ind ;
simpl .
+ -
apply copy_xH .
+ -
rewrite copy_Psucc ,
IHn ;
apply law_idem .
+
Qed .
+
+
+
Lemma eval_reduce_msets i (
Idem :
Idempotent R (
Bin.value (
e_bin i )))
m :
+
eval (
sum i (
reduce_mset m ))
== eval (
sum i m ).
+
Proof .
+
induction m as [[
a n ]|[
a n ]
m IH ].
+ -
simpl .
now rewrite 2
copy_idem .
+ -
simpl .
rewrite IH .
now rewrite 2
copy_idem .
+
Qed .
+
+
+
+
+
+Auxiliary lemmas about products
+
+
+
Section prd_correctness .
+
+
+
Variable i :
idx .
+
Variable is_unit :
idx -> bool .
+
Hypothesis is_unit_prd_Unit :
forall j ,
is_unit j = true ->
+ @
Unit X R (
Bin.value (
e_bin i )) (
eval (
unit j )).
+
+
+
Inductive is_prd_spec_ind :
T -> @
discr (
nelist T )
-> Prop :=
+ |
is_prd_spec_op :
+
forall j l ,
j = i -> is_prd_spec_ind (
prd j l ) (
Is_op l )
+ |
is_prd_spec_unit :
+
forall j ,
is_unit j = true -> is_prd_spec_ind (
unit j ) (
Is_unit j )
+ |
is_prd_spec_nothing :
+
forall u ,
is_prd_spec_ind u (
Is_nothing ).
+
+
+
Lemma is_prd_spec u :
is_prd_spec_ind u (
is_prd i is_unit u ).
+
Proof .
+
unfold is_prd ;
case u ;
intros ;
try constructor .
+
case (
eq_idx_spec );
intros ;
subst ;
try constructor ;
auto .
+
case_eq (
is_unit p );
intros ;
try constructor ;
auto .
+
Qed .
+
+
+
Lemma prd'_prd :
forall (
l :
nelist T ),
eval (
prd' i l )
== eval (
prd i l ).
+
Proof .
+
intros [?|? [|? ?]];
simpl ;
reflexivity .
+
Qed .
+
+
+
Lemma eval_prd_nil x :
eval (
prd i (
nil x ))
== eval x .
+
Proof .
+
rewrite <-
prd'_prd .
simpl .
reflexivity .
+
Qed .
+
+
+
Lemma eval_prd_cons a :
forall (
l :
nelist T ),
+
eval (
prd i (
a :: l ))
== @
Bin.value _ _ (
e_bin i ) (
eval a ) (
eval (
prd i l )).
+
Proof .
intros [|
b l ];
simpl ;
reflexivity .
Qed .
+
+
+
Lemma eval_prd_app :
forall (
h k :
nelist T ),
+
eval (
prd i (
h ++ k ))
== @
Bin.value _ _ (
e_bin i ) (
eval (
prd i h )) (
eval (
prd i k )).
+
Proof .
+
induction h ;
intro k .
simpl ;
try reflexivity .
+
simpl appne .
rewrite 2
eval_prd_cons ,
IHh ,
law_assoc .
reflexivity .
+
Qed .
+
+
+
Inductive compat_prd_unit : @
m idx (
nelist T )
-> Prop :=
+ |
cpu_left :
forall x ,
is_unit x = true -> compat_prd_unit (
left x )
+ |
cpu_right :
forall m ,
compat_prd_unit (
right m ).
+
+
+
Lemma compat_prd_unit_return x :
compat_prd_unit (
return_prd i is_unit x ).
+
Proof .
+
unfold return_prd .
+
case (
is_prd_spec );
intros ;
try constructor ;
auto .
+
Qed .
+
+
+
Lemma compat_prd_unit_add :
forall x h ,
compat_prd_unit h ->
+
compat_prd_unit (
add_to_prd i is_unit x h ).
+
Proof .
+
intros ;
unfold add_to_prd ,
comp .
+
case (
is_prd_spec );
intros ;
try constructor ;
auto .
+ -
unfold comp ;
case h ;
try constructor .
+ -
unfold comp ;
case h ;
try constructor .
+
Qed .
+
+
+
Instance compat_prd_Unit :
forall p ,
compat_prd_unit (
left p )
->
+ @
Unit X R (
Bin.value (
e_bin i )) (
eval (
unit p )).
+
Proof .
+
intros .
+
inversion H ;
subst .
apply is_unit_prd_Unit .
assumption .
+
Qed .
+
+
+
Lemma z0' :
forall l (
r : @
m idx (
nelist T )),
compat_prd_unit r ->
+
eval (
prd i (
run_list (
comp (@
appne T )
l r )))
==
+
eval (
prd i ((
appne (
l ) (
run_list r )))).
+
Proof .
+
intros .
+
unfold comp .
unfold run_list .
case_eq r ;
intros ;
auto ;
subst .
+
rewrite eval_prd_app .
+
rewrite eval_prd_nil .
+
apply compat_prd_Unit in H .
rewrite law_neutral_right .
reflexivity .
+
reflexivity .
+
Qed .
+
+
+
Lemma z1' a :
eval (
prd i (
run_list (
return_prd i is_unit a )))
== eval (
prd i (
nil a )).
+
Proof .
+
intros .
unfold return_prd .
unfold run_list .
+
case (
is_prd_spec );
intros ;
subst ;
reflexivity .
+
Qed .
+
+
+
Lemma z2' :
forall u x ,
compat_prd_unit x ->
+
eval (
prd i (
run_list (
add_to_prd i is_unit u x )))
==
+ @
Bin.value _ _ (
e_bin i ) (
eval u ) (
eval (
prd i (
run_list x ))).
+
Proof .
+
intros u x Hix .
+
unfold add_to_prd .
+
case (
is_prd_spec );
intros ;
subst .
+
rewrite z0' by auto .
rewrite eval_prd_app .
reflexivity .
+
apply is_unit_prd_Unit in H .
rewrite law_neutral_left .
reflexivity .
+
rewrite z0' by auto .
rewrite eval_prd_app .
reflexivity .
+
Qed .
+
+
+
End prd_correctness .
+
+
+
Lemma eval_norm_lists i (
Hnorm :
forall u ,
eval (
norm u )
== eval u ) :
+
forall h ,
eval (
prd i (
norm_lists norm i h ))
== eval (
prd i h ).
+
Proof .
+
unfold norm_lists .
+
assert (
H :
forall h :
nelist T ,
+
eval (
prd i (
run_list (
norm_lists_ i (
is_unit_of i )
norm h )))
==
+
eval (
prd i h )
+
/\ compat_prd_unit (
is_unit_of i ) (
norm_lists_ i (
is_unit_of i )
norm h )). {
+
induction h as [
a |
a h [
IHh IHh' ]];
simpl norm_lists_ ;
split .
+
rewrite z1' .
simpl .
apply Hnorm .
+
apply compat_prd_unit_return .
+
rewrite z2' .
rewrite IHh .
rewrite eval_prd_cons .
+
rewrite Hnorm .
reflexivity .
apply is_unit_of_Unit .
+
auto .
+
apply compat_prd_unit_add .
auto .
+ }
+
apply H .
+
Defined .
+
+
+
+
+
+Correctness of the normalisation function
+
+
+
+
+Corollaries, for goal normalisation or decision
+
+
+
+
+
Lemmas for performing transitivity steps given an AAC_lift instance
+
+
+
+
+
+
Section t .
+
+
+
Context `{
AAC_lift }.
+
+
+
Lemma lift_transitivity_left (
y x z :
X ):
E x y -> R y z -> R x z .
+
Proof .
destruct H as [
Hequiv Hproper ];
intros G ;
rewrite G .
trivial .
Qed .
+
+
+
Lemma lift_transitivity_right (
y x z :
X ):
E y z -> R x y -> R x z .
+
Proof .
destruct H as [
Hequiv Hproper ];
intros G .
rewrite G .
trivial .
Qed .
+
+
+
Lemma lift_reflexivity {
HR :
Reflexive R }:
forall x y ,
E x y -> R x y .
+
Proof .
destruct H .
intros ? ?
G .
rewrite G .
reflexivity .
Qed .
+
+
+
Register lift_transitivity_left as aac_tactics.internal.lift_transitivity_left .
+
Register lift_transitivity_right as aac_tactics.internal.lift_transitivity_right .
+
Register lift_reflexivity as aac_tactics.internal.lift_reflexivity .
+
+
+
End t .
+
+
+
Declare ML Module "aac_plugin:coq-aac-tactics.plugin".
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/AAC_tactics.Caveats.html b/docs/coqdoc/AAC_tactics.Caveats.html
new file mode 100644
index 0000000..e47568d
--- /dev/null
+++ b/docs/coqdoc/AAC_tactics.Caveats.html
@@ -0,0 +1,760 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Currently known limitations and caveats of AAC Tactics
+
+
+
+
+
+
Limitations
+
+
+
+
Dependent parameters
+
+
+
+
+ The type of the rewriting hypothesis must be of the form
+
+
+
+
forall (x_1 : T_1 ) ... (x_n : T_n ), R l r
+
+
+
+ where
R
is a relation over some type
T
and such that for all
+ variable
x_i
appearing in the left-hand side (
l
), we actually
+ have
T_i = T
. The goal should be of the form
S g d
, where
+
S
is a relation on
T
.
+
+
+
+ In other words, we cannot instantiate arguments of an exogeneous type.
+
+
+
+
+
+ In
Hf , since the parameter
n has type
nat ,
+ it cannot be instantiated automatically
+
+
+
+
+
+aac_rewrite does not instantiate n automatically
+
+
+
+
+of course, this argument can be given explicitly
+
+
+
aac_rewrite (
Hf k ).
+
aac_reflexivity .
+
Qed .
+
+
+
+
+
+For the same reason, we cannot handle higher-order parameters (here,
g )
+
+
+
+
+
Exogeneous morphisms
+
+
+
+
+ We do not handle "exogeneous" morphisms: morphisms that move from
+ type
T
to some other type
T'
.
+
+
+
+
+
+
+
+
+ More generally, this prevents us from rewriting under
+ propositional contexts
+
+
+
+
+
+a solution is to introduce an evar to replace the part to be
+ rewritten - this tiresome process should be improved in the
+ future; here, it can be done using eapply and the morphism
+
+
+
+
+similarly, we need to bring equations to the toplevel before
+ being able to rewrite
+
+
+
+
+
Treatment of variance with inequations
+
+
+
+
+ We do not take variance into account when we compute the set of
+ solutions to a matching problem modulo AC. As a consequence,
+
aac_instances may propose solutions for which
aac_rewrite will
+ fail, due to the lack of adequate morphisms.
+
+
+
+
+
+this fails because the first solution is not valid (Z.opp is not increasing)
+
+
+
Fail aac_rewrite H .
+
aac_instances H .
+
+
+
+on the contrary, the second solution is valid:
+
+
+
+
+currently, we cannot filter out such invalid solutions in an easy way;
+ this should be fixed in the future
+
+
+
Abort .
+
+
+
End ineq .
+
+
+
+
+
+
Caveats
+
+
+
+
Special treatment for units
+
+
+
+
+
S 0 is considered as a unit for multiplication whenever a
Nat.mul
+ appears in the goal. The downside is that
S x does not match
1 ,
+ and
1 does not match
S (0 + 0) whenever
Nat.mul appears in
+ the goal.
+
+
+
+
+
+OK (no multiplication around),
x is instantiated with
O
+
+
+
aacu_rewrite H .
+
Abort .
+
+
+
Goal 1 * 1 = 1 .
+
+
+
+fails since 1 is seen as a unit, not the application of the
+ morphism
S to the constant
O
+
+
+
+
+OK (no multiplication around),
x is instantiated with
a
+
+
+
+
+fails: although
S (0+0) is understood as the application of
+ the morphism
S to the constant
O , it is not recognised
+ as the unit
S O of multiplication
+
+
+
intro .
Fail aac_rewrite H' .
+
Abort .
+
+
+
+
+
+ More generally, similar counter-intuitive behaviours can appear
+ when declaring an applied morphism as a unit
+
+
+
+
+
+
Existential variables
+
+
+
+
+ We implemented an algorithm for
matching modulo AC, not for
+
unifying modulo AC. As a consequence, existential variables
+ appearing in a goal are considered as constants and will not be
+ instantiated.
+
+
+
+
+this works: x is instantiated with an evar
+
+
+
aac_rewrite idem .
+
instantiate (2 := 0).
+
+
+
+this does work but there are remaining evars in the end
+
+
+
symmetry .
aac_reflexivity .
+
Abort .
+
+
+
Hypothesis H' :
forall x , 3
+ x = x -> P .
+
+
+
Goal P .
+
eapply H' .
+
+
+
+this fails since we do not instantiate evars
+
+
+
Fail aac_rewrite idem .
+
Abort .
+
+
+
End evars .
+
+
+
+
+
+
Distinction between aac_rewrite and aacu_rewrite
+
+
+
+
+
+in some situations, the aac_rewrite tactic allows
+ instantiations of a variable with a unit, when the variable occurs
+ directly under a function symbol:
+
+
+
+
+this behaviour seems desirable in most situations: these
+ solutions with units are less peculiar than the other ones, since
+ the unit comes from the goal; however, this policy is not properly
+ enforced for now (hard to do with the current algorithm):
+
+
+
+
+
+
+
+
aac_rewrite uses the symbols appearing in the goal and the
+ hypothesis to infer the AC and A operations. In the following
+ example,
dot appears neither in the left-hand-side of the goal,
+ nor in the right-hand side of the hypothesis. Hence,
1 is not
+ recognised as a unit. To circumvent this problem, we can force
+
aac_rewrite to take into account a given operation, by giving
+ it an extra argument. This extra argument seems useful only in
+ this peculiar case.
+
+
+
+
+
+
Lemma inv_unique :
forall x y y' ,
x * y == 1
-> y' * x == 1
-> y == y' .
+
Proof .
+
intros x y y' Hxy Hy'x .
+
aac_instances <-
Hy'x [
dot ].
+
aac_rewrite <-
Hy'x at 1 [
dot ].
+
aac_rewrite Hxy .
aac_reflexivity .
+
Qed .
+
+
+
End V .
+
+
+
+
+
+
Rewriting too many things
+
+
+
+
+
+
aac_rewrite finds a pattern modulo AC that matches a given
+ hypothesis, and then makes a call to
setoid_rewrite . This
+
setoid_rewrite can unfortunately make several rewrites (in a
+ non-intuitive way: below, the
1 in the right-hand side is
+ rewritten into
S c )
+
+
+
+
+to this end, we provide a companion tactic to aac_rewrite
+ and aacu_rewrite , that makes the transitivity step, but not the
+ setoid_rewrite; this allows the user to select the relevant
+ occurrences in which to rewrite:
+
+
+
aac_pattern H at 2.
setoid_rewrite H at 1.
+
Abort .
+
+
+
End W .
+
+
+
+
+
+
Rewriting nullifiable patterns
+
+
+
+
+
+ If the pattern of the rewritten hypothesis does not contain "hard"
+ symbols (like constants, function symbols, AC or A symbols without
+ units), there can be infinitely many subterms such that the pattern
+ matches: it is possible to build "subterms" modulo ACU that make the
+ size of the term increase (by making neutral elements appear in a
+ layered fashion). Hence, we settled with heuristics to propose only
+ "some" of these solutions. In such cases, the tactic displays a
+ (conservative) warning.
+
+
+
+
+
+in this case, only three solutions are proposed, while there are
+ infinitely many solutions, for example:
+
+ a+b*c*(1+☐ )
+
+
+ a+b*c*(1+0*(1+ ☐ ))
+
+
+ ...
+
+
+
+
+
+ Abort .
+
+
+
+
+
+
If the pattern is a unit or can be instantiated to be equal to a unit
+
+
+
+
+ The heuristic is to make the unit appear at each possible position
+ in the term, e.g. transforming
a into
1*a and
a *1, but this
+ process is not recursive (we will not transform
1*a ) into
+
(1+0*1)*a .
+
+
+
+
+
+1 solution, we miss solutions like
(a +b +c *(1+0*(1+[]))) and so on
+
+
+
+
+7 solutions, we miss solutions like
(a +b +c +0*(1+0*[]))
+
+
+ Abort .
+
+
+
+
+
+
Another example of the former case
+
+
+
+
+ In the following, the hypothesis can be instantiated
+ to be equal to
1 .
+
+
+
+
+
+here, only one solution if we use the aac_instance tactic
+
+
+
+
+there are 8 solutions using
aacu_instances (but, here,
+ there are infinitely many different solutions); we miss, e.g.,
a *a +b *a
+
+ (x *x + y *x )*c , which seems to be more peculiar
+
+
+
+
+the 7 last solutions are the same as if we were matching 1
+
+
+
aacu_instances H1 .
+
Abort .
+
+
+
+
+
+ The behavior of the tactic is not satisfying in this case. It is
+ still unclear how to handle properly this kind of situation; we plan
+ to investigate this in the future.
+
+
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/AAC_tactics.Constants.html b/docs/coqdoc/AAC_tactics.Constants.html
new file mode 100644
index 0000000..0662f1d
--- /dev/null
+++ b/docs/coqdoc/AAC_tactics.Constants.html
@@ -0,0 +1,80 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Register Init.Datatypes.O as aac_tactics.nat.O .
+
Register Init.Datatypes.S as aac_tactics.nat.S .
+
Register Init.Datatypes.nat as aac_tactics.nat.type .
+
+
+
Register Init.Datatypes.pair as aac_tactics.pair.pair .
+
Register Init.Datatypes.prod as aac_tactics.pair.prod .
+
+
+
Register Init.Datatypes.option as aac_tactics.option.typ .
+
Register Init.Datatypes.Some as aac_tactics.option.Some .
+
Register Init.Datatypes.None as aac_tactics.option.None .
+
+
+
Register Init.Datatypes.list as aac_tactics.list.typ .
+
Register Init.Datatypes.nil as aac_tactics.list.nil .
+
Register Init.Datatypes.cons as aac_tactics.list.cons .
+
+
+
From Coq Require BinNums .
+
Register BinNums.positive as aac_tactics.pos.typ .
+
Register BinNums.xI as aac_tactics.pos.xI .
+
Register BinNums.xO as aac_tactics.pos.xO .
+
Register BinNums.xH as aac_tactics.pos.xH .
+
+
+
From Coq Require Classes.Morphisms .
+
Register Morphisms.Proper as aac_tactics.coq.classes.morphisms.Proper .
+
From Coq Require Classes.RelationClasses .
+
+
+
Register RelationClasses.Equivalence as aac_tactics.coq.RelationClasses.Equivalence .
+
Register RelationClasses.Reflexive as aac_tactics.coq.RelationClasses.Reflexive .
+
Register RelationClasses.Transitive as aac_tactics.coq.RelationClasses.Transitive .
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/AAC_tactics.Instances.html b/docs/coqdoc/AAC_tactics.Instances.html
new file mode 100644
index 0000000..f372a0d
--- /dev/null
+++ b/docs/coqdoc/AAC_tactics.Instances.html
@@ -0,0 +1,593 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Instances for AAC Tactics
+
+
+
+
+
+This one is not declared as an instance; this would interfere badly with setoid_rewrite
+
+
+
+
+
+
+
+We also provide liftings from
Nat.le to
eq
+
+
+
+
+
+
+
+We also provide liftings from
Z.le to
eq
+
+
+
+
+
+
+
+Exported
Morphisms module provides a
Proper instance
+
+
+
+
+
Permutation_app' in the Stdlib provides a
Proper instance
+
+
+
End Lists .
+
+
+
Module N .
+
Import NArith .
+
Open Scope N_scope .
+
+
+
+
+
+
+
+
+
+
+
+We also provide liftings from
Pos.le to
eq
+
+
+
+
+
+
+
+we also provide liftings from le to eq
+
+
+
+
+
+
+
+
+
+
+
+
+
+union and converse are already defined in the standard library
+
+
+
+
+Note that we use
eq directly as a neutral element for composition
+
+
+
+
+ Here, we should not see any instance of our classes:
+ Print HintDb typeclass_instances.
+
+
+
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/AAC_tactics.Tutorial.html b/docs/coqdoc/AAC_tactics.Tutorial.html
new file mode 100644
index 0000000..2215335
--- /dev/null
+++ b/docs/coqdoc/AAC_tactics.Tutorial.html
@@ -0,0 +1,793 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Tutorial for using AAC Tactics
+
+
+
+
+
+
Introductory example
+
+
+
+
+ Here is a first example with relative numbers (
Z ): one can
+ rewrite an universally quantified hypothesis modulo the
+ associativity and commutativity of
Z.add .
+
+
+
+
+note:
+
+ the tactic handles arbitrary function symbols like Z.opp (as
+ long as they are proper morphisms w.r.t. the considered
+ equivalence relation)
+
+
+ here, the ring tactic would have done the job
+
+
+
+
+
+
+ several associative/commutative operations can be used at the same time,
+ here,
Z.mul and
Z.add , which are both associative and commutative (AC)
+
+
+
+
+
+some commutative operations can be declared as idempotent, here Z.max
+ which is taken into account by the aac_normalise and aac_reflexivity tactics;
+ however, aac_rewrite does not match modulo idempotency
+
+
+
+
+
+
Usage
+
+
+
+
+ One can also work in an abstract context, with arbitrary
+ associative and commutative operators. (Note that one can declare
+ several operations of each kind.)
+
+
+
+
+
+in the very first example,
ring would have solved the
+ goal; here, since
dot does not necessarily distribute over
plus ,
+ it is not possible to rely on it
+
+
+
+
+the tactic starts by normalising terms, so that trailing units
+ are always eliminated
+
+
+
+
+the tactic can deal with "proper" morphisms of arbitrary arity
+ (here
f and
g , or
Z.opp earlier): it rewrites under such
+ morphisms (
g ), and, more importantly, it is able to reorder
+ terms modulo AC under these morphisms (
f )
+
+
+
+
+
Selecting what and where to rewrite
+
+
+
+
+ There are sometimes several solutions to the matching problem. We
+ now show how to interact with the tactic to select the desired one.
+
+
+
+
+
+As expected, one can use both keywords together to select the
+ occurrence and the substitution. We also provide a keyword to
+ specify that the rewrite should be done in the right-hand side of
+ the equation.
+
+
+
+
+
+
Distinction between aac_rewrite and aacu_rewrite :
+
+
+
+
+
aac_rewrite rejects solutions in which variables are instantiated
+ by units, while the companion tactic,
aacu_rewrite allows such
+ solutions.
+
+
+
+
+
+
Section dealing_with_units .
+
Variables a b c :
X .
+
Hypothesis H :
forall x ,
a * x * a == x .
+
+
+
Goal a * a == 1 .
+
+
try aac_instances H .
+
+
aacu_instances H .
+
aacu_rewrite H .
+
reflexivity .
+
Qed .
+
+
+
+
+
+we introduced this distinction because it allows us to rule
+ out dummy cases in common situations:
+
+
+
+
+
Declaring instances
+
+
+
+
+ To use one's own operations: it suffices to declare them as
+ instances of our classes. (Note that the following instances are
+ already declared in the Instances module.)
+
+
+
+
+
+Two (or more) operations may share the same units: in the
+ following example, 0 is understood as the unit of Nat.max as well as
+ the unit of Nat.add .
+
+
+
+
+Commutative operations may additionally be declared as idempotent.
+ This does not change the behaviour of aac_rewrite , but this enables
+ more simplifications in aac_normalise and aac_reflexivity .
+
+
+
+
+
+here, we use idempotency:
+
+
+
+
+furthermore, several operators can be mixed:
+
+
+
+
+
Working with inequations
+
+
+
+
+ To be able to use the tactics, the goal must be a relation
R
+ applied to two arguments, and the rewritten hypothesis must end
+ with a relation
Q applied to two arguments. These relations are
+ not necessarily equivalences, but they should be related
+ according to the occurrence where the rewrite takes place; we
+ leave this check to the underlying call to
setoid_rewrite .
+
+
+
+ one can rewrite equations in the left member of inequations:
+
+
+
+
+or in the right member of inequations, using the in_right keyword:
+
+
+
+
+similarly, one can rewrite inequations in inequations:
+
+
+
+
+possibly in the right-hand side:
+
+
+
+
+aac_reflexivity deals with "trivial" inequations too:
+
+
+
+
+In the last three examples, there were no equivalence relations
+ involved in the goal. However, we actually had to guess the
+ equivalence relation with respect to which the operators
+ (
add ,max ,0) were AC. In this case, it was Leibniz equality
+
eq so that it was automatically inferred; more generally, one
+ can specify which equivalence relation to use by declaring
+ instances of the
AAC_lift type class:
+
+
+
+
+
+(This instance is automatically inferred because
eq is always a
+ valid candidate, here for
le .)
+
+
+
+
+
Normalising goals
+
+
+
+
+ We also provide a tactic to normalise terms modulo AC. This
+ normalisation is the one we use internally.
+
+
+
+
+
+
Examples from previous website
+
+
+
+
+
+
Reverse triangle inequality
+
+
+
+
+
+the following morphisms are required to perform the required rewrites:
+
+
+
+
+
+
+
+note: after the
aac_rewrite <- H , one could use
ring to close the proof
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/AAC_tactics.Utils.html b/docs/coqdoc/AAC_tactics.Utils.html
new file mode 100644
index 0000000..ef461c6
--- /dev/null
+++ b/docs/coqdoc/AAC_tactics.Utils.html
@@ -0,0 +1,445 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Utility functions and results for AAC Tactics
+
+
+
+
+
+
Utilities for positive numbers
+
+
+
+
+ We use
positive numbers as:
+
+ indices for morphisms and symbols
+
+
+ multiplicity of terms in sums
+
+
+
+
+
+
+
+
+
Notation idx :=
positive .
+
+
+
Fixpoint eq_idx_bool i j :=
+
match i ,
j with
+ |
xH ,
xH =>
true
+ |
xO i ,
xO j =>
eq_idx_bool i j
+ |
xI i ,
xI j =>
eq_idx_bool i j
+ |
_ ,
_ =>
false
+
end .
+
+
+
Fixpoint idx_compare i j :=
+
match i ,
j with
+ |
xH ,
xH =>
Eq
+ |
xH ,
_ =>
Lt
+ |
_ ,
xH =>
Gt
+ |
xO i ,
xO j =>
idx_compare i j
+ |
xI i ,
xI j =>
idx_compare i j
+ |
xI _ ,
xO _ =>
Gt
+ |
xO _ ,
xI _ =>
Lt
+
end .
+
+
+
Notation pos_compare :=
idx_compare (
only parsing ).
+
+
+
+
+
+Specification predicate for boolean binary functions
+
+
+
+
+ Weak specification predicate for comparison functions:
+ only the
Eq case is specified
+
+
+
+
+
+
Dependent types utilities
+
+
+
+
+
+ These lemmas have to remain transparent to get structural recursion
+ in the lemma
tcompare_weak_spec below
+
+
+
+
+
+
Utilities about (non-empty) lists and multisets
+
+
+
+
+
+Finite multisets are represented with ordered lists with multiplicities
+
+
+
+
+Lexicographic composition of comparisons (this is a notation to keep it lazy)
+
+
+
Notation lex e f := (
match e with Eq =>
f |
_ =>
e end ).
+
+
+
Section lists .
+
+
+
+
+
+Comparison functions
+
+
+
+
+
+
+
+ This lemma has to remain transparent to get structural recursion
+ in the lemma
tcompare_weak_spec below
+
+
+
+
+
+ This lemma has to remain transparent to get structural recursion
+ in the lemma
tcompare_weak_spec below
+
+
+
+
+
+Merging functions (sorted)
+
+
+
Section m .
+
Variable A :
Type .
+
Variable compare :
A -> A -> comparison .
+
Definition insert n1 h1 :=
+
let fix insert_aux l2 :=
+
match l2 with
+ |
nil ( h2 , n2 ) =>
+
match compare h1 h2 with
+ |
Eq =>
nil ( h1 , Pplus n1 n2 )
+ |
Lt =>
( h1 , n1 ) :: nil ( h2 , n2 )
+ |
Gt =>
( h2 , n2 ) :: nil ( h1 , n1 )
+
end
+ |
( h2 , n2 ) :: t2 =>
+
match compare h1 h2 with
+ |
Eq =>
( h1 , Pplus n1 n2 ) :: t2
+ |
Lt =>
( h1 , n1 ) :: l2
+ |
Gt =>
( h2 , n2 ) :: insert_aux t2
+
end
+
end
+
in insert_aux .
+
+
+
Fixpoint merge_msets l1 :=
+
match l1 with
+ |
nil ( h1 , n1 ) =>
fun l2 =>
insert n1 h1 l2
+ |
( h1 , n1 ) :: t1 =>
+
let fix merge_aux l2 :=
+
match l2 with
+ |
nil ( h2 , n2 ) =>
+
match compare h1 h2 with
+ |
Eq =>
( h1 , Pplus n1 n2 ) :: t1
+ |
Lt =>
( h1 , n1 ) :: merge_msets t1 l2
+ |
Gt =>
( h2 , n2 ) :: l1
+
end
+ |
( h2 , n2 ) :: t2 =>
+
match compare h1 h2 with
+ |
Eq =>
( h1 , Pplus n1 n2 ) :: merge_msets t1 t2
+ |
Lt =>
( h1 , n1 ) :: merge_msets t1 l2
+ |
Gt =>
( h2 , n2 ) :: merge_aux t2
+
end
+
end
+
in merge_aux
+
end .
+
+
+
+
+
+Setting all multiplicities to one, in order to implement idempotency
+
+
+
+
+Interpretation of a list with a constant and a binary operation
+
+
+
+
+Mapping and merging
+
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/config.js b/docs/coqdoc/config.js
new file mode 100644
index 0000000..1902b36
--- /dev/null
+++ b/docs/coqdoc/config.js
@@ -0,0 +1,79 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+ "forall": "∀",
+ "exists": "∃",
+ "~": "¬",
+ "/\\": "∧",
+ "\\/": "∨",
+ "->": "→",
+ "<-": "←",
+ "<->": "↔",
+ "=>": "⇒",
+ "<>": "≠",
+ "<=": "≤",
+ ">=": "≥",
+ "el": "∈",
+ "nel": "∉",
+ "<<=": "⊆",
+ "|-": "⊢",
+ ">>": "»",
+ "<<": "⊆",
+ "++": "⧺",
+ "===": "≡",
+ "=/=": "≢",
+ "=~=": "≅",
+ "==>": "⟹",
+ "<==": "⟸",
+ "False": "⊥",
+ "True": "⊤",
+ ":=": "≔",
+ "-|": "⊣",
+ "*": "×",
+ "::": "∷",
+ "lhd": "⊲",
+ "rhd": "⊳",
+ "nat": "ℕ",
+ "alpha": "α",
+ "beta": "β",
+ "gamma": "γ",
+ "delta": "δ",
+ "epsilon": "ε",
+ "eta": "η",
+ "iota": "ι",
+ "kappa": "κ",
+ "lambda": "λ",
+ "mu": "μ",
+ "nu": "ν",
+ "omega": "ω",
+ "phi": "ϕ",
+ "pi": "π",
+ "psi": "ψ",
+ "rho": "ρ",
+ "sigma": "σ",
+ "tau": "τ",
+ "theta": "θ",
+ "xi": "ξ",
+ "zeta": "ζ",
+ "Delta": "Δ",
+ "Gamma": "Γ",
+ "Pi": "Π",
+ "Sigma": "Σ",
+ "Omega": "Ω",
+ "Xi": "Ξ"
+};
+
+coqdocjs.subscr = {
+ "0" : "₀",
+ "1" : "₁",
+ "2" : "₂",
+ "3" : "₃",
+ "4" : "₄",
+ "5" : "₅",
+ "6" : "₆",
+ "7" : "₇",
+ "8" : "₈",
+ "9" : "₉",
+};
+
+coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
diff --git a/docs/coqdoc/coqdoc.css b/docs/coqdoc/coqdoc.css
new file mode 100644
index 0000000..18dad89
--- /dev/null
+++ b/docs/coqdoc/coqdoc.css
@@ -0,0 +1,197 @@
+@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
+
+body{
+ font-family: 'Open Sans', sans-serif;
+ font-size: 14px;
+ color: #2D2D2D
+}
+
+a {
+ text-decoration: none;
+ border-radius: 3px;
+ padding-left: 3px;
+ padding-right: 3px;
+ margin-left: -3px;
+ margin-right: -3px;
+ color: inherit;
+ font-weight: bold;
+}
+
+#main .code a, #main .inlinecode a, #toc a {
+ font-weight: inherit;
+}
+
+a[href]:hover, [clickable]:hover{
+ background-color: rgba(0,0,0,0.1);
+ cursor: pointer;
+}
+
+h, h1, h2, h3, h4, h5 {
+ line-height: 1;
+ color: black;
+ text-rendering: optimizeLegibility;
+ font-weight: normal;
+ letter-spacing: 0.1em;
+ text-align: left;
+}
+
+div + br {
+ display: none;
+}
+
+div:empty{ display: none;}
+
+#main h1 {
+ font-size: 2em;
+}
+
+#main h2 {
+ font-size: 1.667rem;
+}
+
+#main h3 {
+ font-size: 1.333em;
+}
+
+#main h4, #main h5, #main h6 {
+ font-size: 1em;
+}
+
+#toc h2 {
+ padding-bottom: 0;
+}
+
+#main .doc {
+ margin: 0;
+ text-align: justify;
+}
+
+.inlinecode, .code, #main pre {
+ font-family: monospace;
+}
+
+.code > br:first-child {
+ display: none;
+}
+
+.doc + .code{
+ margin-top:0.5em;
+}
+
+.block{
+ display: block;
+ margin-top: 5px;
+ margin-bottom: 5px;
+ padding: 10px;
+ text-align: center;
+}
+
+.block img{
+ margin: 15px;
+}
+
+table.infrule {
+ border: 0px;
+ margin-left: 50px;
+ margin-top: 10px;
+ margin-bottom: 10px;
+}
+
+td.infrule {
+ font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
+ text-align: center;
+ padding: 0;
+ line-height: 1;
+}
+
+tr.infrulemiddle hr {
+ margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+ color: rgb(60%,60%,60%);
+ padding-left: 1em;
+ padding-bottom: 0.1em
+}
+
+.id[type="constructor"], .id[type="projection"], .id[type="method"],
+.id[title="constructor"], .id[title="projection"], .id[title="method"] {
+ color: #A30E16;
+}
+
+.id[type="var"], .id[type="variable"],
+.id[title="var"], .id[title="variable"] {
+ color: inherit;
+}
+
+.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
+.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
+ color: #A6650F;
+}
+
+.id[type="lemma"],
+.id[title="lemma"]{
+ color: #188B0C;
+}
+
+.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
+.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
+ color : #2874AE;
+}
+
+.comment {
+ color: #808080;
+}
+
+/* TOC */
+
+#toc h2{
+ letter-spacing: 0;
+ font-size: 1.333em;
+}
+
+/* Index */
+
+#index {
+ margin: 0;
+ padding: 0;
+ width: 100%;
+}
+
+#index #frontispiece {
+ margin: 1em auto;
+ padding: 1em;
+ width: 60%;
+}
+
+.booktitle { font-size : 140% }
+.authors { font-size : 90%;
+ line-height: 115%; }
+.moreauthors { font-size : 60% }
+
+#index #entrance {
+ text-align: center;
+}
+
+#index #entrance .spacer {
+ margin: 0 30px 0 30px;
+}
+
+ul.doclist {
+ margin-top: 0em;
+ margin-bottom: 0em;
+}
+
+#toc > * {
+ clear: both;
+}
+
+#toc > a {
+ display: block;
+ float: left;
+ margin-top: 1em;
+}
+
+#toc a h2{
+ display: inline;
+}
diff --git a/docs/coqdoc/coqdocjs.css b/docs/coqdoc/coqdocjs.css
new file mode 100644
index 0000000..959b42e
--- /dev/null
+++ b/docs/coqdoc/coqdocjs.css
@@ -0,0 +1,239 @@
+/* replace unicode */
+
+.id[repl] .hidden {
+ font-size: 0;
+}
+
+.id[repl]:before{
+ content: attr(repl);
+}
+
+/* folding proofs */
+
+@keyframes show-proof {
+ 0% {
+ max-height: 1.2em;
+ opacity: 1;
+ }
+ 99% {
+ max-height: 1000em;
+ }
+ 100%{
+ }
+}
+
+@keyframes hide-proof {
+ from {
+ visibility: visible;
+ max-height: 10em;
+ opacity: 1;
+ }
+ to {
+ max-height: 1.2em;
+ }
+}
+
+.proof {
+ cursor: pointer;
+}
+.proof * {
+ cursor: pointer;
+}
+
+.proof {
+ overflow: hidden;
+ position: relative;
+ transition: opacity 1s;
+ display: inline-block;
+}
+
+.proof[show="false"] {
+ max-height: 1.2em;
+ visibility: visible;
+ opacity: 0.3;
+}
+
+.proof[show="false"][animate] {
+ animation-name: hide-proof;
+ animation-duration: 0.25s;
+}
+
+.proof[show="true"] {
+ animation-name: show-proof;
+ animation-duration: 10s;
+}
+
+.proof[show="true"]:before {
+ content: "\25BC"; /* arrow down */
+}
+.proof[show="false"]:before {
+ content: "\25B6"; /* arrow right */
+}
+
+.proof[show="false"]:hover {
+ visibility: visible;
+ opacity: 0.5;
+}
+
+#toggle-proofs[proof-status="no-proofs"] {
+ display: none;
+}
+
+#toggle-proofs[proof-status="some-hidden"]:before {
+ content: "Show Proofs";
+}
+
+#toggle-proofs[proof-status="all-shown"]:before {
+ content: "Hide Proofs";
+}
+
+
+/* page layout */
+
+html, body {
+ height: 100%;
+ margin:0;
+ padding:0;
+}
+
+@media only screen { /* no div with internal scrolling to allow printing of whole content */
+ body {
+ display: flex;
+ flex-direction: column
+ }
+
+ #content {
+ flex: 1;
+ overflow: auto;
+ display: flex;
+ flex-direction: column;
+ }
+}
+
+#content:focus {
+ outline: none; /* prevent glow in OS X */
+}
+
+#main {
+ display: block;
+ padding: 16px;
+ padding-top: 1em;
+ padding-bottom: 2em;
+ margin-left: auto;
+ margin-right: auto;
+ max-width: 60em;
+ flex: 1 0 auto;
+}
+
+.libtitle {
+ display: none;
+}
+
+/* header */
+#header {
+ width:100%;
+ padding: 0;
+ margin: 0;
+ display: flex;
+ align-items: center;
+ background-color: rgb(21,57,105);
+ color: white;
+ font-weight: bold;
+ overflow: hidden;
+}
+
+
+.button {
+ cursor: pointer;
+}
+
+#header * {
+ text-decoration: none;
+ vertical-align: middle;
+ margin-left: 15px;
+ margin-right: 15px;
+}
+
+#header > .right, #header > .left {
+ display: flex;
+ flex: 1;
+ align-items: center;
+}
+#header > .left {
+ text-align: left;
+}
+#header > .right {
+ flex-direction: row-reverse;
+}
+
+#header a, #header .button {
+ color: white;
+ box-sizing: border-box;
+}
+
+#header a {
+ border-radius: 0;
+ padding: 0.2em;
+}
+
+#header .button {
+ background-color: rgb(63, 103, 156);
+ border-radius: 1em;
+ padding-left: 0.5em;
+ padding-right: 0.5em;
+ margin: 0.2em;
+}
+
+#header a:hover, #header .button:hover {
+ background-color: rgb(181, 213, 255);
+ color: black;
+}
+
+#header h1 { padding: 0;
+ margin: 0;}
+
+/* footer */
+#footer {
+ text-align: center;
+ opacity: 0.5;
+ font-size: 75%;
+}
+
+/* hyperlinks */
+
+@keyframes highlight {
+ 50%{
+ background-color: black;
+ }
+}
+
+:target * {
+ animation-name: highlight;
+ animation-duration: 1s;
+}
+
+a[name]:empty {
+ float: right;
+}
+
+/* Proviola */
+
+div.code {
+ width: auto;
+ float: none;
+}
+
+div.goal {
+ position: fixed;
+ left: 75%;
+ width: 25%;
+ top: 3em;
+}
+
+div.doc {
+ clear: both;
+}
+
+span.command:hover {
+ background-color: inherit;
+}
diff --git a/docs/coqdoc/coqdocjs.js b/docs/coqdoc/coqdocjs.js
new file mode 100644
index 0000000..727da8c
--- /dev/null
+++ b/docs/coqdoc/coqdocjs.js
@@ -0,0 +1,197 @@
+var coqdocjs = coqdocjs || {};
+(function(){
+
+function replace(s){
+ var m;
+ if (m = s.match(/^(.+)'/)) {
+ return replace(m[1])+"'";
+ } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) {
+ return replace(m[1])+m[2].replace(/\d/g, function(d){
+ if (coqdocjs.subscr.hasOwnProperty(d)) {
+ return coqdocjs.subscr[d];
+ } else {
+ return d;
+ }
+ });
+ } else if (coqdocjs.repl.hasOwnProperty(s)){
+ return coqdocjs.repl[s]
+ } else {
+ return s;
+ }
+}
+
+function toArray(nl){
+ return Array.prototype.slice.call(nl);
+}
+
+function replInTextNodes() {
+ // Get all the nodes up front.
+ var nodes = Array.from(document.querySelectorAll(".code, .inlinecode"))
+ .flatMap(elem => Array.from(elem.childNodes)
+ .filter(e => e.nodeType == Node.TEXT_NODE)
+ );
+
+ // Create a replacement template node to clone from.
+ var replacementTemplate = document.createElement("span");
+ replacementTemplate.setAttribute("class", "id");
+ replacementTemplate.setAttribute("type", "keyword");
+
+ // Do the replacements.
+ coqdocjs.replInText.forEach(function(toReplace){
+ var replacement = replacementTemplate.cloneNode(true);
+ replacement.appendChild(document.createTextNode(toReplace));
+
+ nodes.forEach(node => {
+ var fragments = node.textContent.split(toReplace);
+ node.textContent = fragments[fragments.length-1];
+ for (var k = 0; k < fragments.length - 1; ++k) {
+ fragments[k] && node.parentNode.insertBefore(document.createTextNode(fragments[k]),node);
+ node.parentNode.insertBefore(replacement.cloneNode(true), node);
+ }
+ });
+ });
+}
+
+function replNodes() {
+ toArray(document.getElementsByClassName("id")).forEach(function(node){
+ if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){
+ var text = node.textContent;
+ var replText = replace(text);
+ if(text != replText) {
+ node.setAttribute("repl", replText);
+ node.setAttribute("title", text);
+ var hidden = document.createElement("span");
+ hidden.setAttribute("class", "hidden");
+ while (node.firstChild) {
+ hidden.appendChild(node.firstChild);
+ }
+ node.appendChild(hidden);
+ }
+ }
+ });
+}
+
+function isVernacStart(l, t){
+ t = t.trim();
+ for(var s of l){
+ if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){
+ return true;
+ }
+ }
+ return false;
+}
+
+function isProofStart(n){
+ return isVernacStart(["Proof"], n.textContent) ||
+ (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent));
+}
+
+function isProofEnd(s){
+ return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s);
+}
+
+function proofStatus(){
+ var proofs = toArray(document.getElementsByClassName("proof"));
+ if(proofs.length) {
+ for(var proof of proofs) {
+ if (proof.getAttribute("show") === "false") {
+ return "some-hidden";
+ }
+ }
+ return "all-shown";
+ }
+ else {
+ return "no-proofs";
+ }
+}
+
+function updateView(){
+ document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus());
+}
+
+function foldProofs() {
+ var hasCommands = true;
+ var nodes = document.getElementsByClassName("command");
+ if(nodes.length == 0) {
+ hasCommands = false;
+ console.log("no command tags found")
+ nodes = document.getElementsByClassName("id");
+ }
+ toArray(nodes).forEach(function(node){
+ if(isProofStart(node)) {
+ var proof = document.createElement("span");
+ proof.setAttribute("class", "proof");
+
+ node.parentNode.insertBefore(proof, node);
+ if(proof.previousSibling.nodeType === Node.TEXT_NODE)
+ proof.appendChild(proof.previousSibling);
+ while(node && !isProofEnd(node.textContent)) {
+ proof.appendChild(node);
+ node = proof.nextSibling;
+ }
+ if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed
+ if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed
+
+ proof.addEventListener("click", function(proof){return function(e){
+ if (e.target.parentNode.tagName.toLowerCase() === "a")
+ return;
+ proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true");
+ proof.setAttribute("animate", "");
+ updateView();
+ };}(proof));
+ proof.setAttribute("show", "false");
+ }
+ });
+}
+
+function toggleProofs(){
+ var someProofsHidden = proofStatus() === "some-hidden";
+ toArray(document.getElementsByClassName("proof")).forEach(function(proof){
+ proof.setAttribute("show", someProofsHidden);
+ proof.setAttribute("animate", "");
+ });
+ updateView();
+}
+
+function repairDom(){
+ // pull whitespace out of command
+ toArray(document.getElementsByClassName("command")).forEach(function(node){
+ while(node.firstChild && node.firstChild.textContent.trim() == ""){
+ console.log("try move");
+ node.parentNode.insertBefore(node.firstChild, node);
+ }
+ });
+ toArray(document.getElementsByClassName("id")).forEach(function(node){
+ node.setAttribute("type", node.getAttribute("title"));
+ });
+ toArray(document.getElementsByClassName("idref")).forEach(function(ref){
+ toArray(ref.childNodes).forEach(function(child){
+ if (["var", "variable"].indexOf(child.getAttribute("type")) > -1)
+ ref.removeAttribute("href");
+ });
+ });
+
+}
+
+function fixTitle(){
+ var url = "/" + window.location.pathname;
+ var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
+ if (basename === "toc") {document.title = "Table of Contents";}
+ else if (basename === "indexpage") {document.title = "Index";}
+ else {document.title = basename;}
+}
+
+function postprocess(){
+ repairDom();
+ replInTextNodes()
+ replNodes();
+ foldProofs();
+ document.getElementById("toggle-proofs").addEventListener("click", toggleProofs);
+ updateView();
+}
+
+fixTitle();
+document.addEventListener('DOMContentLoaded', postprocess);
+
+coqdocjs.toggleProofs = toggleProofs;
+})();
diff --git a/docs/coqdoc/indexpage.html b/docs/coqdoc/indexpage.html
new file mode 100644
index 0000000..12ba892
--- /dev/null
+++ b/docs/coqdoc/indexpage.html
@@ -0,0 +1,2411 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Global Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(663 entries)
+
+
+Notation Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(19 entries)
+
+
+Module Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(13 entries)
+
+
+Variable Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(176 entries)
+
+
+Library Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(6 entries)
+
+
+Lemma Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(54 entries)
+
+
+Constructor Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(31 entries)
+
+
+Inductive Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(14 entries)
+
+
+Projection Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(19 entries)
+
+
+Section Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(39 entries)
+
+
+Instance Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(141 entries)
+
+
+Abbreviation Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(4 entries)
+
+
+Definition Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(138 entries)
+
+
+Record Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(9 entries)
+
+
+
+
Global Index
+
A
+
AAC [library]
+
aac_lift_proper [instance, in
AAC_tactics.AAC ]
+
aac_lift_subrelation [instance, in
AAC_tactics.AAC ]
+
aac_list_proper [projection, in
AAC_tactics.AAC ]
+
aac_lift_equivalence [projection, in
AAC_tactics.AAC ]
+
AAC_lift [record, in
AAC_tactics.AAC ]
+
AAC_normalise.d [variable, in
AAC_tactics.Tutorial ]
+
AAC_normalise.c [variable, in
AAC_tactics.Tutorial ]
+
AAC_normalise.b [variable, in
AAC_tactics.Tutorial ]
+
AAC_normalise.a [variable, in
AAC_tactics.Tutorial ]
+
AAC_normalise [section, in
AAC_tactics.Tutorial ]
+
aac_le_eq_lift [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_max_0_Unit [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_max_Idem [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_max_Assoc [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_max_Comm [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_add_0_Unit [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_mul_1_Unit [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_mul_Assoc [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_mul_Comm [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_add_Comm [instance, in
AAC_tactics.Tutorial ]
+
aac_Nat_add_Assoc [instance, in
AAC_tactics.Tutorial ]
+
All [module, in
AAC_tactics.Instances ]
+
appne [definition, in
AAC_tactics.Utils ]
+
Associative [record, in
AAC_tactics.AAC ]
+
Associative [inductive, in
AAC_tactics.AAC ]
+
B
+
base [section, in
AAC_tactics.Tutorial ]
+
base.both [section, in
AAC_tactics.Tutorial ]
+
base.both.a [variable, in
AAC_tactics.Tutorial ]
+
base.both.b [variable, in
AAC_tactics.Tutorial ]
+
base.both.c [variable, in
AAC_tactics.Tutorial ]
+
base.both.d [variable, in
AAC_tactics.Tutorial ]
+
base.both.H [variable, in
AAC_tactics.Tutorial ]
+
base.both.H' [variable, in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.H' [variable, in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.H [variable, in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.c [variable, in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.b [variable, in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.a [variable, in
AAC_tactics.Tutorial ]
+
base.dealing_with_units [section, in
AAC_tactics.Tutorial ]
+
base.dot [variable, in
AAC_tactics.Tutorial ]
+
base.dot_Proper [variable, in
AAC_tactics.Tutorial ]
+
base.dot_A [variable, in
AAC_tactics.Tutorial ]
+
base.E [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms [section, in
AAC_tactics.Tutorial ]
+
base.morphisms.a [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms.b [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms.f [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms.g [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms.H [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms.Hf [variable, in
AAC_tactics.Tutorial ]
+
base.morphisms.Hg [variable, in
AAC_tactics.Tutorial ]
+
base.occurrence [section, in
AAC_tactics.Tutorial ]
+
base.occurrence.a [variable, in
AAC_tactics.Tutorial ]
+
base.occurrence.f [variable, in
AAC_tactics.Tutorial ]
+
base.occurrence.H [variable, in
AAC_tactics.Tutorial ]
+
base.occurrence.Hf [variable, in
AAC_tactics.Tutorial ]
+
base.One [variable, in
AAC_tactics.Tutorial ]
+
base.one [variable, in
AAC_tactics.Tutorial ]
+
base.plus [variable, in
AAC_tactics.Tutorial ]
+
base.plus_Proper [variable, in
AAC_tactics.Tutorial ]
+
base.plus_C [variable, in
AAC_tactics.Tutorial ]
+
base.plus_A [variable, in
AAC_tactics.Tutorial ]
+
base.R [variable, in
AAC_tactics.Tutorial ]
+
base.reminder [section, in
AAC_tactics.Tutorial ]
+
base.reminder.a [variable, in
AAC_tactics.Tutorial ]
+
base.reminder.b [variable, in
AAC_tactics.Tutorial ]
+
base.reminder.c [variable, in
AAC_tactics.Tutorial ]
+
base.reminder.H [variable, in
AAC_tactics.Tutorial ]
+
base.subst [section, in
AAC_tactics.Tutorial ]
+
base.subst.a [variable, in
AAC_tactics.Tutorial ]
+
base.subst.b [variable, in
AAC_tactics.Tutorial ]
+
base.subst.c [variable, in
AAC_tactics.Tutorial ]
+
base.subst.d [variable, in
AAC_tactics.Tutorial ]
+
base.subst.H [variable, in
AAC_tactics.Tutorial ]
+
base.subst.H' [variable, in
AAC_tactics.Tutorial ]
+
base.X [variable, in
AAC_tactics.Tutorial ]
+
base.Zero [variable, in
AAC_tactics.Tutorial ]
+
base.zero [variable, in
AAC_tactics.Tutorial ]
+
_ + _ [notation, in
AAC_tactics.Tutorial ]
+
_ * _ [notation, in
AAC_tactics.Tutorial ]
+
_ == _ [notation, in
AAC_tactics.Tutorial ]
+
0 [notation, in
AAC_tactics.Tutorial ]
+
1 [notation, in
AAC_tactics.Tutorial ]
+
Bool [module, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_true_Unit [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_false_Unit [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_Idem [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_Comm [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_Assoc [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_Idem [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_Comm [instance, in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_Assoc [instance, in
AAC_tactics.Instances ]
+
Bool.negb_compat [instance, in
AAC_tactics.Instances ]
+
C
+
cast [abbreviation, in
AAC_tactics.Utils ]
+
cast_eq [lemma, in
AAC_tactics.Utils ]
+
Caveats [library]
+
Commutative [record, in
AAC_tactics.AAC ]
+
Commutative [inductive, in
AAC_tactics.AAC ]
+
compare_weak_spec_sind [definition, in
AAC_tactics.Utils ]
+
compare_weak_spec_ind [definition, in
AAC_tactics.Utils ]
+
compare_weak_spec [inductive, in
AAC_tactics.Utils ]
+
cons [constructor, in
AAC_tactics.Utils ]
+
Constants [library]
+
D
+
decide_spec_sind [definition, in
AAC_tactics.Utils ]
+
decide_spec_ind [definition, in
AAC_tactics.Utils ]
+
decide_false [constructor, in
AAC_tactics.Utils ]
+
decide_true [constructor, in
AAC_tactics.Utils ]
+
decide_spec [inductive, in
AAC_tactics.Utils ]
+
dep [section, in
AAC_tactics.Utils ]
+
dep.f [variable, in
AAC_tactics.Utils ]
+
dep.T [variable, in
AAC_tactics.Utils ]
+
dep.U [variable, in
AAC_tactics.Utils ]
+
E
+
eq_idx_spec [lemma, in
AAC_tactics.Utils ]
+
eq_idx_bool [definition, in
AAC_tactics.Utils ]
+
eq_subr [lemma, in
AAC_tactics.Instances ]
+
evars [section, in
AAC_tactics.Caveats ]
+
evars.H [variable, in
AAC_tactics.Caveats ]
+
evars.H' [variable, in
AAC_tactics.Caveats ]
+
evars.idem [variable, in
AAC_tactics.Caveats ]
+
evars.P [variable, in
AAC_tactics.Caveats ]
+
Examples [section, in
AAC_tactics.Tutorial ]
+
Examples.a [variable, in
AAC_tactics.Tutorial ]
+
Examples.b [variable, in
AAC_tactics.Tutorial ]
+
Examples.c [variable, in
AAC_tactics.Tutorial ]
+
Examples.H [variable, in
AAC_tactics.Tutorial ]
+
_ ^2 [notation, in
AAC_tactics.Tutorial ]
+
2 ⋅ _ [notation, in
AAC_tactics.Tutorial ]
+
F
+
fold_map' [definition, in
AAC_tactics.Utils ]
+
fold_map [definition, in
AAC_tactics.Utils ]
+
H
+
Hbin1 [lemma, in
AAC_tactics.Tutorial ]
+
Hbin2 [lemma, in
AAC_tactics.Tutorial ]
+
Hopp [lemma, in
AAC_tactics.Tutorial ]
+
I
+
Idempotent [record, in
AAC_tactics.AAC ]
+
Idempotent [inductive, in
AAC_tactics.AAC ]
+
idx [abbreviation, in
AAC_tactics.Utils ]
+
idx_compare_reflect_eq [lemma, in
AAC_tactics.Utils ]
+
idx_compare [definition, in
AAC_tactics.Utils ]
+
ineq [section, in
AAC_tactics.Caveats ]
+
ineq.H [variable, in
AAC_tactics.Caveats ]
+
insert [definition, in
AAC_tactics.Utils ]
+
Instances [library]
+
Internal [module, in
AAC_tactics.AAC ]
+
Internal.add_to_prd [definition, in
AAC_tactics.AAC ]
+
Internal.add_to_sum [definition, in
AAC_tactics.AAC ]
+
Internal.assoc [instance, in
AAC_tactics.AAC ]
+
Internal.Bin [module, in
AAC_tactics.AAC ]
+
Internal.Binvalue_Proper [instance, in
AAC_tactics.AAC ]
+
Internal.Binvalue_Associative [instance, in
AAC_tactics.AAC ]
+
Internal.Binvalue_Idempotent [instance, in
AAC_tactics.AAC ]
+
Internal.Binvalue_Commutative [instance, in
AAC_tactics.AAC ]
+
Internal.Bin.assoc [projection, in
AAC_tactics.AAC ]
+
Internal.Bin.comm [projection, in
AAC_tactics.AAC ]
+
Internal.Bin.compat [projection, in
AAC_tactics.AAC ]
+
Internal.Bin.idem [projection, in
AAC_tactics.AAC ]
+
Internal.Bin.pack [record, in
AAC_tactics.AAC ]
+
Internal.Bin.t [section, in
AAC_tactics.AAC ]
+
Internal.Bin.t.R [variable, in
AAC_tactics.AAC ]
+
Internal.Bin.t.X [variable, in
AAC_tactics.AAC ]
+
Internal.Bin.value [projection, in
AAC_tactics.AAC ]
+
Internal.comp [definition, in
AAC_tactics.AAC ]
+
Internal.compare [definition, in
AAC_tactics.AAC ]
+
Internal.compare_reflect_eq [lemma, in
AAC_tactics.AAC ]
+
Internal.compat_prd_Unit [instance, in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_add [lemma, in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_return [lemma, in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_sind [definition, in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_ind [definition, in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit [inductive, in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_Unit [instance, in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_add [lemma, in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_return [lemma, in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_sind [definition, in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_ind [definition, in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit [inductive, in
AAC_tactics.AAC ]
+
Internal.copy [definition, in
AAC_tactics.AAC ]
+
Internal.copy [section, in
AAC_tactics.AAC ]
+
Internal.copy_idem [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_n_unit [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_mset_copy [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_mset_succ [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_mset' [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_mset [definition, in
AAC_tactics.AAC ]
+
Internal.copy_compat [instance, in
AAC_tactics.AAC ]
+
Internal.copy_Psucc [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_xH [lemma, in
AAC_tactics.AAC ]
+
Internal.copy_plus [lemma, in
AAC_tactics.AAC ]
+
Internal.copy' [definition, in
AAC_tactics.AAC ]
+
Internal.copy.HR [variable, in
AAC_tactics.AAC ]
+
Internal.copy.op [variable, in
AAC_tactics.AAC ]
+
Internal.copy.op' [variable, in
AAC_tactics.AAC ]
+
Internal.copy.plus [variable, in
AAC_tactics.AAC ]
+
Internal.copy.po [variable, in
AAC_tactics.AAC ]
+
Internal.copy.R [variable, in
AAC_tactics.AAC ]
+
Internal.copy.X [variable, in
AAC_tactics.AAC ]
+
Internal.cpu_right [constructor, in
AAC_tactics.AAC ]
+
Internal.cpu_left [constructor, in
AAC_tactics.AAC ]
+
Internal.csu_right [constructor, in
AAC_tactics.AAC ]
+
Internal.csu_left [constructor, in
AAC_tactics.AAC ]
+
Internal.decide [lemma, in
AAC_tactics.AAC ]
+
Internal.discr [inductive, in
AAC_tactics.AAC ]
+
Internal.discr_sind [definition, in
AAC_tactics.AAC ]
+
Internal.discr_rec [definition, in
AAC_tactics.AAC ]
+
Internal.discr_ind [definition, in
AAC_tactics.AAC ]
+
Internal.discr_rect [definition, in
AAC_tactics.AAC ]
+
Internal.eval [definition, in
AAC_tactics.AAC ]
+
Internal.eval_norm_aux [definition, in
AAC_tactics.AAC ]
+
Internal.eval_norm [definition, in
AAC_tactics.AAC ]
+
Internal.eval_norm_lists [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_prd_app [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_prd_cons [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_prd_nil [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_reduce_msets [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_norm_msets [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_merge_bin [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_sum_cons [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_sum_nil [lemma, in
AAC_tactics.AAC ]
+
Internal.eval_aux_compat [instance, in
AAC_tactics.AAC ]
+
Internal.eval_aux [definition, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec [lemma, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_ind_sind [definition, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_ind_ind [definition, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_nothing [constructor, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_unit [constructor, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_op [constructor, in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_ind [inductive, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec [lemma, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_ind_sind [definition, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_ind_ind [definition, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_nothing [constructor, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_unit [constructor, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_op [constructor, in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_ind [inductive, in
AAC_tactics.AAC ]
+
Internal.is_unit_of_Unit [lemma, in
AAC_tactics.AAC ]
+
Internal.is_prd [definition, in
AAC_tactics.AAC ]
+
Internal.is_sum [definition, in
AAC_tactics.AAC ]
+
Internal.Is_nothing [constructor, in
AAC_tactics.AAC ]
+
Internal.Is_unit [constructor, in
AAC_tactics.AAC ]
+
Internal.Is_op [constructor, in
AAC_tactics.AAC ]
+
Internal.is_idempotent [definition, in
AAC_tactics.AAC ]
+
Internal.is_commutative [definition, in
AAC_tactics.AAC ]
+
Internal.is_unit_of [definition, in
AAC_tactics.AAC ]
+
Internal.left [constructor, in
AAC_tactics.AAC ]
+
Internal.lift_normalise [lemma, in
AAC_tactics.AAC ]
+
Internal.m [inductive, in
AAC_tactics.AAC ]
+
Internal.m_sind [definition, in
AAC_tactics.AAC ]
+
Internal.m_rec [definition, in
AAC_tactics.AAC ]
+
Internal.m_ind [definition, in
AAC_tactics.AAC ]
+
Internal.m_rect [definition, in
AAC_tactics.AAC ]
+
Internal.norm [definition, in
AAC_tactics.AAC ]
+
Internal.normalise [lemma, in
AAC_tactics.AAC ]
+
Internal.norm_msets [definition, in
AAC_tactics.AAC ]
+
Internal.norm_lists [definition, in
AAC_tactics.AAC ]
+
Internal.norm_lists_ [definition, in
AAC_tactics.AAC ]
+
Internal.norm_msets_ [definition, in
AAC_tactics.AAC ]
+
Internal.prd [constructor, in
AAC_tactics.AAC ]
+
Internal.prd' [definition, in
AAC_tactics.AAC ]
+
Internal.prd'_prd [lemma, in
AAC_tactics.AAC ]
+
Internal.proper [instance, in
AAC_tactics.AAC ]
+
Internal.return_prd [definition, in
AAC_tactics.AAC ]
+
Internal.return_sum [definition, in
AAC_tactics.AAC ]
+
Internal.right [constructor, in
AAC_tactics.AAC ]
+
Internal.run_msets [definition, in
AAC_tactics.AAC ]
+
Internal.run_list [definition, in
AAC_tactics.AAC ]
+
Internal.s [section, in
AAC_tactics.AAC ]
+
Internal.sum [constructor, in
AAC_tactics.AAC ]
+
Internal.sum' [definition, in
AAC_tactics.AAC ]
+
Internal.sum'_sum [lemma, in
AAC_tactics.AAC ]
+
Internal.sym [constructor, in
AAC_tactics.AAC ]
+
Internal.Sym [module, in
AAC_tactics.AAC ]
+
Internal.Sym.ar [projection, in
AAC_tactics.AAC ]
+
Internal.Sym.morph [projection, in
AAC_tactics.AAC ]
+
Internal.Sym.null [definition, in
AAC_tactics.AAC ]
+
Internal.Sym.pack [record, in
AAC_tactics.AAC ]
+
Internal.Sym.rel_of [definition, in
AAC_tactics.AAC ]
+
Internal.Sym.t [section, in
AAC_tactics.AAC ]
+
Internal.Sym.type_of [definition, in
AAC_tactics.AAC ]
+
Internal.Sym.t.R [variable, in
AAC_tactics.AAC ]
+
Internal.Sym.t.X [variable, in
AAC_tactics.AAC ]
+
Internal.Sym.value [projection, in
AAC_tactics.AAC ]
+
Internal.s.E [variable, in
AAC_tactics.AAC ]
+
Internal.s.e_unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.e_bin [variable, in
AAC_tactics.AAC ]
+
Internal.s.e_sym [variable, in
AAC_tactics.AAC ]
+
Internal.s.prds [section, in
AAC_tactics.AAC ]
+
Internal.s.prds.i [variable, in
AAC_tactics.AAC ]
+
Internal.s.prds.is_unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness.is_unit_prd_Unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness.is_unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness.i [variable, in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness [section, in
AAC_tactics.AAC ]
+
Internal.s.R [variable, in
AAC_tactics.AAC ]
+
Internal.s.sums [section, in
AAC_tactics.AAC ]
+
Internal.s.sums.i [variable, in
AAC_tactics.AAC ]
+
Internal.s.sums.is_unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.comm [variable, in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.is_unit_sum_Unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.is_unit [variable, in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.i [variable, in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness [section, in
AAC_tactics.AAC ]
+
Internal.s.X [variable, in
AAC_tactics.AAC ]
+
_ == _ [notation, in
AAC_tactics.AAC ]
+
Internal.T [inductive, in
AAC_tactics.AAC ]
+
Internal.tcompare_weak_spec [definition, in
AAC_tactics.AAC ]
+
Internal.T_sind [definition, in
AAC_tactics.AAC ]
+
Internal.T_rec [definition, in
AAC_tactics.AAC ]
+
Internal.T_ind [definition, in
AAC_tactics.AAC ]
+
Internal.T_rect [definition, in
AAC_tactics.AAC ]
+
Internal.uf_desc [projection, in
AAC_tactics.AAC ]
+
Internal.uf_idx [projection, in
AAC_tactics.AAC ]
+
Internal.unit [constructor, in
AAC_tactics.AAC ]
+
Internal.unit_pack [record, in
AAC_tactics.AAC ]
+
Internal.unit_of [record, in
AAC_tactics.AAC ]
+
Internal.u_desc [projection, in
AAC_tactics.AAC ]
+
Internal.u_value [projection, in
AAC_tactics.AAC ]
+
Internal.vcompare [definition, in
AAC_tactics.AAC ]
+
Internal.vcompare_reflect_eqdep [definition, in
AAC_tactics.AAC ]
+
Internal.vcons [constructor, in
AAC_tactics.AAC ]
+
Internal.vnil [constructor, in
AAC_tactics.AAC ]
+
Internal.vnorm [definition, in
AAC_tactics.AAC ]
+
Internal.vT [inductive, in
AAC_tactics.AAC ]
+
Internal.vT_sind [definition, in
AAC_tactics.AAC ]
+
Internal.vT_rec [definition, in
AAC_tactics.AAC ]
+
Internal.vT_ind [definition, in
AAC_tactics.AAC ]
+
Internal.vT_rect [definition, in
AAC_tactics.AAC ]
+
Internal.z0 [lemma, in
AAC_tactics.AAC ]
+
Internal.z0' [lemma, in
AAC_tactics.AAC ]
+
Internal.z1 [lemma, in
AAC_tactics.AAC ]
+
Internal.z1' [lemma, in
AAC_tactics.AAC ]
+
Internal.z2 [lemma, in
AAC_tactics.AAC ]
+
Internal.z2' [lemma, in
AAC_tactics.AAC ]
+
introduction [section, in
AAC_tactics.Tutorial ]
+
introduction.a [variable, in
AAC_tactics.Tutorial ]
+
introduction.b [variable, in
AAC_tactics.Tutorial ]
+
introduction.c [variable, in
AAC_tactics.Tutorial ]
+
introduction.H [variable, in
AAC_tactics.Tutorial ]
+
inv_unique [lemma, in
AAC_tactics.Caveats ]
+
L
+
law_neutral_right [projection, in
AAC_tactics.AAC ]
+
law_neutral_left [projection, in
AAC_tactics.AAC ]
+
law_idem [projection, in
AAC_tactics.AAC ]
+
law_idem [constructor, in
AAC_tactics.AAC ]
+
law_comm [projection, in
AAC_tactics.AAC ]
+
law_comm [constructor, in
AAC_tactics.AAC ]
+
law_assoc [projection, in
AAC_tactics.AAC ]
+
law_assoc [constructor, in
AAC_tactics.AAC ]
+
lex [abbreviation, in
AAC_tactics.Utils ]
+
lift_reflexivity [lemma, in
AAC_tactics.AAC ]
+
lift_transitivity_right [lemma, in
AAC_tactics.AAC ]
+
lift_transitivity_left [lemma, in
AAC_tactics.AAC ]
+
lists [section, in
AAC_tactics.Utils ]
+
Lists [module, in
AAC_tactics.Instances ]
+
Lists [section, in
AAC_tactics.Tutorial ]
+
Lists.aac_List_app_nil_Permutation_Unit [instance, in
AAC_tactics.Instances ]
+
Lists.aac_List_app_Permutation_Comm [instance, in
AAC_tactics.Instances ]
+
Lists.aac_List_app_Permutation_Assoc [instance, in
AAC_tactics.Instances ]
+
Lists.aac_List_app_nil_Unit [instance, in
AAC_tactics.Instances ]
+
Lists.aac_List_app_Assoc [instance, in
AAC_tactics.Instances ]
+
lists.c [section, in
AAC_tactics.Utils ]
+
lists.c.A [variable, in
AAC_tactics.Utils ]
+
lists.c.B [variable, in
AAC_tactics.Utils ]
+
lists.c.compare [variable, in
AAC_tactics.Utils ]
+
Lists.H [variable, in
AAC_tactics.Tutorial ]
+
lists.list_compare_weak_spec.Hcompare [variable, in
AAC_tactics.Utils ]
+
lists.list_compare_weak_spec.compare [variable, in
AAC_tactics.Utils ]
+
lists.list_compare_weak_spec.A [variable, in
AAC_tactics.Utils ]
+
lists.list_compare_weak_spec [section, in
AAC_tactics.Utils ]
+
Lists.l1 [variable, in
AAC_tactics.Tutorial ]
+
Lists.l2 [variable, in
AAC_tactics.Tutorial ]
+
Lists.l3 [variable, in
AAC_tactics.Tutorial ]
+
lists.m [section, in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec.Hcompare [variable, in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec.compare [variable, in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec.A [variable, in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec [section, in
AAC_tactics.Utils ]
+
lists.m.A [variable, in
AAC_tactics.Utils ]
+
lists.m.B [variable, in
AAC_tactics.Utils ]
+
lists.m.bind [variable, in
AAC_tactics.Utils ]
+
lists.m.b2 [variable, in
AAC_tactics.Utils ]
+
lists.m.compare [variable, in
AAC_tactics.Utils ]
+
lists.m.map [variable, in
AAC_tactics.Utils ]
+
lists.m.merge [variable, in
AAC_tactics.Utils ]
+
lists.m.ret [variable, in
AAC_tactics.Utils ]
+
Lists.X [variable, in
AAC_tactics.Tutorial ]
+
list_compare_weak_spec [lemma, in
AAC_tactics.Utils ]
+
list_compare [definition, in
AAC_tactics.Utils ]
+
M
+
merge_map [definition, in
AAC_tactics.Utils ]
+
merge_msets [definition, in
AAC_tactics.Utils ]
+
morphism [section, in
AAC_tactics.Caveats ]
+
morphism.H [variable, in
AAC_tactics.Caveats ]
+
morphism.HP [variable, in
AAC_tactics.Caveats ]
+
morphism.P [variable, in
AAC_tactics.Caveats ]
+
mset [definition, in
AAC_tactics.Utils ]
+
mset_compare_weak_spec [lemma, in
AAC_tactics.Utils ]
+
mset_compare [definition, in
AAC_tactics.Utils ]
+
N
+
N [module, in
AAC_tactics.Instances ]
+
nelist [inductive, in
AAC_tactics.Utils ]
+
nelist_map [definition, in
AAC_tactics.Utils ]
+
nelist_sind [definition, in
AAC_tactics.Utils ]
+
nelist_rec [definition, in
AAC_tactics.Utils ]
+
nelist_ind [definition, in
AAC_tactics.Utils ]
+
nelist_rect [definition, in
AAC_tactics.Utils ]
+
nil [constructor, in
AAC_tactics.Utils ]
+
N.aac_N_le_eq_lift [instance, in
AAC_tactics.Instances ]
+
N.aac_N_max_0_Unit [instance, in
AAC_tactics.Instances ]
+
N.aac_N_add_0_Unit [instance, in
AAC_tactics.Instances ]
+
N.aac_N_mul_1_Unit [instance, in
AAC_tactics.Instances ]
+
N.aac_N_max_Idem [instance, in
AAC_tactics.Instances ]
+
N.aac_N_max_Assoc [instance, in
AAC_tactics.Instances ]
+
N.aac_N_max_Comm [instance, in
AAC_tactics.Instances ]
+
N.aac_N_min_Idem [instance, in
AAC_tactics.Instances ]
+
N.aac_N_min_Assoc [instance, in
AAC_tactics.Instances ]
+
N.aac_N_min_Comm [instance, in
AAC_tactics.Instances ]
+
N.aac_N_mul_Assoc [instance, in
AAC_tactics.Instances ]
+
N.aac_N_mul_Comm [instance, in
AAC_tactics.Instances ]
+
N.aac_N_add_Comm [instance, in
AAC_tactics.Instances ]
+
N.aac_N_add_Assoc [instance, in
AAC_tactics.Instances ]
+
N.N_le_PreOrder [instance, in
AAC_tactics.Instances ]
+
P
+
P [module, in
AAC_tactics.Instances ]
+
parameters [section, in
AAC_tactics.Caveats ]
+
parameters.E [variable, in
AAC_tactics.Caveats ]
+
parameters.f [variable, in
AAC_tactics.Caveats ]
+
parameters.g [variable, in
AAC_tactics.Caveats ]
+
parameters.H [variable, in
AAC_tactics.Caveats ]
+
parameters.Hf [variable, in
AAC_tactics.Caveats ]
+
parameters.Hf' [variable, in
AAC_tactics.Caveats ]
+
parameters.Hg [variable, in
AAC_tactics.Caveats ]
+
parameters.plus [variable, in
AAC_tactics.Caveats ]
+
parameters.plus_Proper [variable, in
AAC_tactics.Caveats ]
+
parameters.plus_C [variable, in
AAC_tactics.Caveats ]
+
parameters.plus_A [variable, in
AAC_tactics.Caveats ]
+
parameters.R [variable, in
AAC_tactics.Caveats ]
+
parameters.X [variable, in
AAC_tactics.Caveats ]
+
parameters.Zero [variable, in
AAC_tactics.Caveats ]
+
parameters.zero [variable, in
AAC_tactics.Caveats ]
+
_ + _ [notation, in
AAC_tactics.Caveats ]
+
_ == _ [notation, in
AAC_tactics.Caveats ]
+
0 [notation, in
AAC_tactics.Caveats ]
+
pcws_gt [constructor, in
AAC_tactics.Utils ]
+
pcws_lt [constructor, in
AAC_tactics.Utils ]
+
pcws_eq [constructor, in
AAC_tactics.Utils ]
+
Peano [section, in
AAC_tactics.Caveats ]
+
Peano [module, in
AAC_tactics.Instances ]
+
Peano [section, in
AAC_tactics.Tutorial ]
+
Peano.a [variable, in
AAC_tactics.Tutorial ]
+
Peano.aac_Nat_le_eq_lift [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_0_Unit [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_add_0_Unit [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_mul_1_Unit [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_Idem [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_Assoc [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_Comm [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_min_Idem [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_min_Assoc [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_min_Comm [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_mul_Assoc [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_mul_Comm [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_add_Comm [instance, in
AAC_tactics.Instances ]
+
Peano.aac_Nat_add_Assoc [instance, in
AAC_tactics.Instances ]
+
Peano.b [variable, in
AAC_tactics.Tutorial ]
+
Peano.c [variable, in
AAC_tactics.Tutorial ]
+
Peano.H [variable, in
AAC_tactics.Caveats ]
+
Peano.H [variable, in
AAC_tactics.Tutorial ]
+
Peano.H' [variable, in
AAC_tactics.Caveats ]
+
Peano.Nat_le_PreOrder [instance, in
AAC_tactics.Instances ]
+
pos_compare_weak_spec [lemma, in
AAC_tactics.Utils ]
+
pos_compare [abbreviation, in
AAC_tactics.Utils ]
+
Props [section, in
AAC_tactics.Tutorial ]
+
Props.P [variable, in
AAC_tactics.Tutorial ]
+
Props.Q [variable, in
AAC_tactics.Tutorial ]
+
Prop_ops.aac_Prop_impl_iff_lift [instance, in
AAC_tactics.Instances ]
+
Prop_ops.not_iff_compat [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_True_iff_Unit [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_False_iff_Unit [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_iff_Idem [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_iff_Comm [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_iff_Assoc [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_iff_Idem [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_iff_Comm [instance, in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_iff_Assoc [instance, in
AAC_tactics.Instances ]
+
Prop_ops [module, in
AAC_tactics.Instances ]
+
P.aac_Pos_le_eq_lift [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_max_1_Unit [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_mul_1_Unit [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_max_Idem [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_max_Assoc [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_max_Comm [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_min_Idem [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_min_Assoc [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_min_Comm [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_mul_Assoc [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_mul_Comm [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_add_Comm [instance, in
AAC_tactics.Instances ]
+
P.aac_Pos_add_Assoc [instance, in
AAC_tactics.Instances ]
+
P.Pos_le_PreOrder [instance, in
AAC_tactics.Instances ]
+
Q
+
Q [module, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qle_eq_lift [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qplus_0_Qeq_Unit [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmult_1_Qeq_Unit [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmax_Qeq_Idem [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmax_Qeq_Assoc [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmax_Qeq_Comm [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmin_Qeq_Idem [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmin_Qeq_Assoc [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmin_Qeq_Comm [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmult_Qeq_Assoc [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmult_Qeq_Comm [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qplus_Qeq_Comm [instance, in
AAC_tactics.Instances ]
+
Q.aac_Q_Qplus_Qeq_Assoc [instance, in
AAC_tactics.Instances ]
+
Q.Q_Qle_PreOrder [instance, in
AAC_tactics.Instances ]
+
R
+
reduce_mset [definition, in
AAC_tactics.Utils ]
+
reflect_eqdep_weak_spec [lemma, in
AAC_tactics.Utils ]
+
reflect_eqdep_eq [lemma, in
AAC_tactics.Utils ]
+
reflect_eqdep [definition, in
AAC_tactics.Utils ]
+
Relations [module, in
AAC_tactics.Instances ]
+
Relations.aac_inclusion_same_relation_lift [instance, in
AAC_tactics.Instances ]
+
Relations.aac_compo_eq_same_relation_Unit [instance, in
AAC_tactics.Instances ]
+
Relations.aac_compo_same_relation_Assoc [instance, in
AAC_tactics.Instances ]
+
Relations.aac_inter_top_same_relation_Unit [instance, in
AAC_tactics.Instances ]
+
Relations.aac_inter_same_relation_Idem [instance, in
AAC_tactics.Instances ]
+
Relations.aac_inter_same_relation_Assoc [instance, in
AAC_tactics.Instances ]
+
Relations.aac_inter_same_relation_Comm [instance, in
AAC_tactics.Instances ]
+
Relations.aac_bot_union_same_relation_Unit [instance, in
AAC_tactics.Instances ]
+
Relations.aac_union_same_relation_Idem [instance, in
AAC_tactics.Instances ]
+
Relations.aac_union_same_relation_Assoc [instance, in
AAC_tactics.Instances ]
+
Relations.aac_union_same_relation_Comm [instance, in
AAC_tactics.Instances ]
+
Relations.bot [definition, in
AAC_tactics.Instances ]
+
Relations.clos_refl_trans_same_relation_compat [instance, in
AAC_tactics.Instances ]
+
Relations.clos_refl_trans_incr [instance, in
AAC_tactics.Instances ]
+
Relations.clos_trans_same_relation_compat [instance, in
AAC_tactics.Instances ]
+
Relations.clos_trans_incr [instance, in
AAC_tactics.Instances ]
+
Relations.compo [definition, in
AAC_tactics.Instances ]
+
Relations.defs [section, in
AAC_tactics.Instances ]
+
Relations.defs.R [variable, in
AAC_tactics.Instances ]
+
Relations.defs.S [variable, in
AAC_tactics.Instances ]
+
Relations.defs.T [variable, in
AAC_tactics.Instances ]
+
Relations.inclusion_PreOrder [instance, in
AAC_tactics.Instances ]
+
Relations.inter [definition, in
AAC_tactics.Instances ]
+
Relations.negr [definition, in
AAC_tactics.Instances ]
+
Relations.negr_same_relation_compat [instance, in
AAC_tactics.Instances ]
+
Relations.same_relation_Equivalence [instance, in
AAC_tactics.Instances ]
+
Relations.top [definition, in
AAC_tactics.Instances ]
+
Relations.transp_same_relation_compat [instance, in
AAC_tactics.Instances ]
+
S
+
sigma [definition, in
AAC_tactics.AAC ]
+
sigma [section, in
AAC_tactics.AAC ]
+
sigma_empty [definition, in
AAC_tactics.AAC ]
+
sigma_add [definition, in
AAC_tactics.AAC ]
+
sigma_get [definition, in
AAC_tactics.AAC ]
+
T
+
t [section, in
AAC_tactics.AAC ]
+
Tutorial [library]
+
U
+
U [section, in
AAC_tactics.Caveats ]
+
Unit [record, in
AAC_tactics.AAC ]
+
Unnamed_thm5 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm5 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm5 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm5 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm4 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm2 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm1 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm1 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm0 [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm [definition, in
AAC_tactics.Caveats ]
+
Unnamed_thm26 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm25 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm24 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm23 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm22 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm21 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm20 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm20 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm20 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm19 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm18 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm17 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm16 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm15 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm14 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm13 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm12 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm11 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm11 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm10 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm9 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm8 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm7 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm6 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm5 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm4 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm3 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm2 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm1 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm0 [definition, in
AAC_tactics.Tutorial ]
+
Unnamed_thm [definition, in
AAC_tactics.Tutorial ]
+
Utils [library]
+
U.dot [variable, in
AAC_tactics.Caveats ]
+
U.dot_inv_right [variable, in
AAC_tactics.Caveats ]
+
U.dot_inv_left [variable, in
AAC_tactics.Caveats ]
+
U.dot_Proper [variable, in
AAC_tactics.Caveats ]
+
U.dot_A [variable, in
AAC_tactics.Caveats ]
+
U.E [variable, in
AAC_tactics.Caveats ]
+
U.f [variable, in
AAC_tactics.Caveats ]
+
U.Hf [variable, in
AAC_tactics.Caveats ]
+
U.One [variable, in
AAC_tactics.Caveats ]
+
U.one [variable, in
AAC_tactics.Caveats ]
+
U.R [variable, in
AAC_tactics.Caveats ]
+
U.X [variable, in
AAC_tactics.Caveats ]
+
_ * _ [notation, in
AAC_tactics.Caveats ]
+
_ == _ [notation, in
AAC_tactics.Caveats ]
+
1 [notation, in
AAC_tactics.Caveats ]
+
V
+
V [section, in
AAC_tactics.Caveats ]
+
V.dot [variable, in
AAC_tactics.Caveats ]
+
V.dot_Proper [variable, in
AAC_tactics.Caveats ]
+
V.dot_A [variable, in
AAC_tactics.Caveats ]
+
V.E [variable, in
AAC_tactics.Caveats ]
+
V.One [variable, in
AAC_tactics.Caveats ]
+
V.one [variable, in
AAC_tactics.Caveats ]
+
V.R [variable, in
AAC_tactics.Caveats ]
+
V.X [variable, in
AAC_tactics.Caveats ]
+
_ * _ [notation, in
AAC_tactics.Caveats ]
+
_ == _ [notation, in
AAC_tactics.Caveats ]
+
1 [notation, in
AAC_tactics.Caveats ]
+
W
+
W [section, in
AAC_tactics.Caveats ]
+
W.a [variable, in
AAC_tactics.Caveats ]
+
W.b [variable, in
AAC_tactics.Caveats ]
+
W.c [variable, in
AAC_tactics.Caveats ]
+
W.H [variable, in
AAC_tactics.Caveats ]
+
Z
+
Z [section, in
AAC_tactics.Caveats ]
+
Z [module, in
AAC_tactics.Instances ]
+
Z_add_incr [instance, in
AAC_tactics.Caveats ]
+
Z_add_le_compat [instance, in
AAC_tactics.Tutorial ]
+
Z_opp_ge_le_compat [instance, in
AAC_tactics.Tutorial ]
+
Z_add_opp_diag_r [lemma, in
AAC_tactics.Tutorial ]
+
Z_abs_triangle [lemma, in
AAC_tactics.Tutorial ]
+
Z.a [variable, in
AAC_tactics.Caveats ]
+
Z.aac_Z_le_eq_lift [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_add_0_Unit [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_mul_1_Unit [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_max_Idem [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_max_Assoc [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_max_Comm [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_min_Idem [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_min_Assoc [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_min_Comm [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_mul_Assoc [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_mul_Comm [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_add_Comm [instance, in
AAC_tactics.Instances ]
+
Z.aac_Z_add_Assoc [instance, in
AAC_tactics.Instances ]
+
Z.b [variable, in
AAC_tactics.Caveats ]
+
Z.c [variable, in
AAC_tactics.Caveats ]
+
Z.f [variable, in
AAC_tactics.Caveats ]
+
Z.H [variable, in
AAC_tactics.Caveats ]
+
Z.H0 [variable, in
AAC_tactics.Caveats ]
+
Z.H1 [variable, in
AAC_tactics.Caveats ]
+
Z.Z_le_PreOrder [instance, in
AAC_tactics.Instances ]
+
other
+
_ ++ _ [notation, in
AAC_tactics.Utils ]
+
_ :: _ [notation, in
AAC_tactics.Utils ]
+
+
Notation Index
+
B
+
_ + _ [in
AAC_tactics.Tutorial ]
+
_ * _ [in
AAC_tactics.Tutorial ]
+
_ == _ [in
AAC_tactics.Tutorial ]
+
0 [in
AAC_tactics.Tutorial ]
+
1 [in
AAC_tactics.Tutorial ]
+
E
+
_ ^2 [in
AAC_tactics.Tutorial ]
+
2 ⋅ _ [in
AAC_tactics.Tutorial ]
+
I
+
_ == _ [in
AAC_tactics.AAC ]
+
P
+
_ + _ [in
AAC_tactics.Caveats ]
+
_ == _ [in
AAC_tactics.Caveats ]
+
0 [in
AAC_tactics.Caveats ]
+
U
+
_ * _ [in
AAC_tactics.Caveats ]
+
_ == _ [in
AAC_tactics.Caveats ]
+
1 [in
AAC_tactics.Caveats ]
+
V
+
_ * _ [in
AAC_tactics.Caveats ]
+
_ == _ [in
AAC_tactics.Caveats ]
+
1 [in
AAC_tactics.Caveats ]
+
other
+
_ ++ _ [in
AAC_tactics.Utils ]
+
_ :: _ [in
AAC_tactics.Utils ]
+
+
Module Index
+
A
+
All [in
AAC_tactics.Instances ]
+
B
+
Bool [in
AAC_tactics.Instances ]
+
I
+
Internal [in
AAC_tactics.AAC ]
+
Internal.Bin [in
AAC_tactics.AAC ]
+
Internal.Sym [in
AAC_tactics.AAC ]
+
L
+
Lists [in
AAC_tactics.Instances ]
+
N
+
N [in
AAC_tactics.Instances ]
+
P
+
P [in
AAC_tactics.Instances ]
+
Peano [in
AAC_tactics.Instances ]
+
Prop_ops [in
AAC_tactics.Instances ]
+
Q
+
Q [in
AAC_tactics.Instances ]
+
R
+
Relations [in
AAC_tactics.Instances ]
+
Z
+
Z [in
AAC_tactics.Instances ]
+
+
Variable Index
+
A
+
AAC_normalise.d [in
AAC_tactics.Tutorial ]
+
AAC_normalise.c [in
AAC_tactics.Tutorial ]
+
AAC_normalise.b [in
AAC_tactics.Tutorial ]
+
AAC_normalise.a [in
AAC_tactics.Tutorial ]
+
B
+
base.both.a [in
AAC_tactics.Tutorial ]
+
base.both.b [in
AAC_tactics.Tutorial ]
+
base.both.c [in
AAC_tactics.Tutorial ]
+
base.both.d [in
AAC_tactics.Tutorial ]
+
base.both.H [in
AAC_tactics.Tutorial ]
+
base.both.H' [in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.H' [in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.H [in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.c [in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.b [in
AAC_tactics.Tutorial ]
+
base.dealing_with_units.a [in
AAC_tactics.Tutorial ]
+
base.dot [in
AAC_tactics.Tutorial ]
+
base.dot_Proper [in
AAC_tactics.Tutorial ]
+
base.dot_A [in
AAC_tactics.Tutorial ]
+
base.E [in
AAC_tactics.Tutorial ]
+
base.morphisms.a [in
AAC_tactics.Tutorial ]
+
base.morphisms.b [in
AAC_tactics.Tutorial ]
+
base.morphisms.f [in
AAC_tactics.Tutorial ]
+
base.morphisms.g [in
AAC_tactics.Tutorial ]
+
base.morphisms.H [in
AAC_tactics.Tutorial ]
+
base.morphisms.Hf [in
AAC_tactics.Tutorial ]
+
base.morphisms.Hg [in
AAC_tactics.Tutorial ]
+
base.occurrence.a [in
AAC_tactics.Tutorial ]
+
base.occurrence.f [in
AAC_tactics.Tutorial ]
+
base.occurrence.H [in
AAC_tactics.Tutorial ]
+
base.occurrence.Hf [in
AAC_tactics.Tutorial ]
+
base.One [in
AAC_tactics.Tutorial ]
+
base.one [in
AAC_tactics.Tutorial ]
+
base.plus [in
AAC_tactics.Tutorial ]
+
base.plus_Proper [in
AAC_tactics.Tutorial ]
+
base.plus_C [in
AAC_tactics.Tutorial ]
+
base.plus_A [in
AAC_tactics.Tutorial ]
+
base.R [in
AAC_tactics.Tutorial ]
+
base.reminder.a [in
AAC_tactics.Tutorial ]
+
base.reminder.b [in
AAC_tactics.Tutorial ]
+
base.reminder.c [in
AAC_tactics.Tutorial ]
+
base.reminder.H [in
AAC_tactics.Tutorial ]
+
base.subst.a [in
AAC_tactics.Tutorial ]
+
base.subst.b [in
AAC_tactics.Tutorial ]
+
base.subst.c [in
AAC_tactics.Tutorial ]
+
base.subst.d [in
AAC_tactics.Tutorial ]
+
base.subst.H [in
AAC_tactics.Tutorial ]
+
base.subst.H' [in
AAC_tactics.Tutorial ]
+
base.X [in
AAC_tactics.Tutorial ]
+
base.Zero [in
AAC_tactics.Tutorial ]
+
base.zero [in
AAC_tactics.Tutorial ]
+
D
+
dep.f [in
AAC_tactics.Utils ]
+
dep.T [in
AAC_tactics.Utils ]
+
dep.U [in
AAC_tactics.Utils ]
+
E
+
evars.H [in
AAC_tactics.Caveats ]
+
evars.H' [in
AAC_tactics.Caveats ]
+
evars.idem [in
AAC_tactics.Caveats ]
+
evars.P [in
AAC_tactics.Caveats ]
+
Examples.a [in
AAC_tactics.Tutorial ]
+
Examples.b [in
AAC_tactics.Tutorial ]
+
Examples.c [in
AAC_tactics.Tutorial ]
+
Examples.H [in
AAC_tactics.Tutorial ]
+
I
+
ineq.H [in
AAC_tactics.Caveats ]
+
Internal.Bin.t.R [in
AAC_tactics.AAC ]
+
Internal.Bin.t.X [in
AAC_tactics.AAC ]
+
Internal.copy.HR [in
AAC_tactics.AAC ]
+
Internal.copy.op [in
AAC_tactics.AAC ]
+
Internal.copy.op' [in
AAC_tactics.AAC ]
+
Internal.copy.plus [in
AAC_tactics.AAC ]
+
Internal.copy.po [in
AAC_tactics.AAC ]
+
Internal.copy.R [in
AAC_tactics.AAC ]
+
Internal.copy.X [in
AAC_tactics.AAC ]
+
Internal.Sym.t.R [in
AAC_tactics.AAC ]
+
Internal.Sym.t.X [in
AAC_tactics.AAC ]
+
Internal.s.E [in
AAC_tactics.AAC ]
+
Internal.s.e_unit [in
AAC_tactics.AAC ]
+
Internal.s.e_bin [in
AAC_tactics.AAC ]
+
Internal.s.e_sym [in
AAC_tactics.AAC ]
+
Internal.s.prds.i [in
AAC_tactics.AAC ]
+
Internal.s.prds.is_unit [in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness.is_unit_prd_Unit [in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness.is_unit [in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness.i [in
AAC_tactics.AAC ]
+
Internal.s.R [in
AAC_tactics.AAC ]
+
Internal.s.sums.i [in
AAC_tactics.AAC ]
+
Internal.s.sums.is_unit [in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.comm [in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.is_unit_sum_Unit [in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.is_unit [in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness.i [in
AAC_tactics.AAC ]
+
Internal.s.X [in
AAC_tactics.AAC ]
+
introduction.a [in
AAC_tactics.Tutorial ]
+
introduction.b [in
AAC_tactics.Tutorial ]
+
introduction.c [in
AAC_tactics.Tutorial ]
+
introduction.H [in
AAC_tactics.Tutorial ]
+
L
+
lists.c.A [in
AAC_tactics.Utils ]
+
lists.c.B [in
AAC_tactics.Utils ]
+
lists.c.compare [in
AAC_tactics.Utils ]
+
Lists.H [in
AAC_tactics.Tutorial ]
+
lists.list_compare_weak_spec.Hcompare [in
AAC_tactics.Utils ]
+
lists.list_compare_weak_spec.compare [in
AAC_tactics.Utils ]
+
lists.list_compare_weak_spec.A [in
AAC_tactics.Utils ]
+
Lists.l1 [in
AAC_tactics.Tutorial ]
+
Lists.l2 [in
AAC_tactics.Tutorial ]
+
Lists.l3 [in
AAC_tactics.Tutorial ]
+
lists.mset_compare_weak_spec.Hcompare [in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec.compare [in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec.A [in
AAC_tactics.Utils ]
+
lists.m.A [in
AAC_tactics.Utils ]
+
lists.m.B [in
AAC_tactics.Utils ]
+
lists.m.bind [in
AAC_tactics.Utils ]
+
lists.m.b2 [in
AAC_tactics.Utils ]
+
lists.m.compare [in
AAC_tactics.Utils ]
+
lists.m.map [in
AAC_tactics.Utils ]
+
lists.m.merge [in
AAC_tactics.Utils ]
+
lists.m.ret [in
AAC_tactics.Utils ]
+
Lists.X [in
AAC_tactics.Tutorial ]
+
M
+
morphism.H [in
AAC_tactics.Caveats ]
+
morphism.HP [in
AAC_tactics.Caveats ]
+
morphism.P [in
AAC_tactics.Caveats ]
+
P
+
parameters.E [in
AAC_tactics.Caveats ]
+
parameters.f [in
AAC_tactics.Caveats ]
+
parameters.g [in
AAC_tactics.Caveats ]
+
parameters.H [in
AAC_tactics.Caveats ]
+
parameters.Hf [in
AAC_tactics.Caveats ]
+
parameters.Hf' [in
AAC_tactics.Caveats ]
+
parameters.Hg [in
AAC_tactics.Caveats ]
+
parameters.plus [in
AAC_tactics.Caveats ]
+
parameters.plus_Proper [in
AAC_tactics.Caveats ]
+
parameters.plus_C [in
AAC_tactics.Caveats ]
+
parameters.plus_A [in
AAC_tactics.Caveats ]
+
parameters.R [in
AAC_tactics.Caveats ]
+
parameters.X [in
AAC_tactics.Caveats ]
+
parameters.Zero [in
AAC_tactics.Caveats ]
+
parameters.zero [in
AAC_tactics.Caveats ]
+
Peano.a [in
AAC_tactics.Tutorial ]
+
Peano.b [in
AAC_tactics.Tutorial ]
+
Peano.c [in
AAC_tactics.Tutorial ]
+
Peano.H [in
AAC_tactics.Caveats ]
+
Peano.H [in
AAC_tactics.Tutorial ]
+
Peano.H' [in
AAC_tactics.Caveats ]
+
Props.P [in
AAC_tactics.Tutorial ]
+
Props.Q [in
AAC_tactics.Tutorial ]
+
R
+
Relations.defs.R [in
AAC_tactics.Instances ]
+
Relations.defs.S [in
AAC_tactics.Instances ]
+
Relations.defs.T [in
AAC_tactics.Instances ]
+
U
+
U.dot [in
AAC_tactics.Caveats ]
+
U.dot_inv_right [in
AAC_tactics.Caveats ]
+
U.dot_inv_left [in
AAC_tactics.Caveats ]
+
U.dot_Proper [in
AAC_tactics.Caveats ]
+
U.dot_A [in
AAC_tactics.Caveats ]
+
U.E [in
AAC_tactics.Caveats ]
+
U.f [in
AAC_tactics.Caveats ]
+
U.Hf [in
AAC_tactics.Caveats ]
+
U.One [in
AAC_tactics.Caveats ]
+
U.one [in
AAC_tactics.Caveats ]
+
U.R [in
AAC_tactics.Caveats ]
+
U.X [in
AAC_tactics.Caveats ]
+
V
+
V.dot [in
AAC_tactics.Caveats ]
+
V.dot_Proper [in
AAC_tactics.Caveats ]
+
V.dot_A [in
AAC_tactics.Caveats ]
+
V.E [in
AAC_tactics.Caveats ]
+
V.One [in
AAC_tactics.Caveats ]
+
V.one [in
AAC_tactics.Caveats ]
+
V.R [in
AAC_tactics.Caveats ]
+
V.X [in
AAC_tactics.Caveats ]
+
W
+
W.a [in
AAC_tactics.Caveats ]
+
W.b [in
AAC_tactics.Caveats ]
+
W.c [in
AAC_tactics.Caveats ]
+
W.H [in
AAC_tactics.Caveats ]
+
Z
+
Z.a [in
AAC_tactics.Caveats ]
+
Z.b [in
AAC_tactics.Caveats ]
+
Z.c [in
AAC_tactics.Caveats ]
+
Z.f [in
AAC_tactics.Caveats ]
+
Z.H [in
AAC_tactics.Caveats ]
+
Z.H0 [in
AAC_tactics.Caveats ]
+
Z.H1 [in
AAC_tactics.Caveats ]
+
+
Library Index
+
A
+
AAC
+
C
+
Caveats
+
Constants
+
I
+
Instances
+
T
+
Tutorial
+
U
+
Utils
+
+
Lemma Index
+
C
+
cast_eq [in
AAC_tactics.Utils ]
+
E
+
eq_idx_spec [in
AAC_tactics.Utils ]
+
eq_subr [in
AAC_tactics.Instances ]
+
H
+
Hbin1 [in
AAC_tactics.Tutorial ]
+
Hbin2 [in
AAC_tactics.Tutorial ]
+
Hopp [in
AAC_tactics.Tutorial ]
+
I
+
idx_compare_reflect_eq [in
AAC_tactics.Utils ]
+
Internal.compare_reflect_eq [in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_add [in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_return [in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_add [in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_return [in
AAC_tactics.AAC ]
+
Internal.copy_idem [in
AAC_tactics.AAC ]
+
Internal.copy_n_unit [in
AAC_tactics.AAC ]
+
Internal.copy_mset_copy [in
AAC_tactics.AAC ]
+
Internal.copy_mset_succ [in
AAC_tactics.AAC ]
+
Internal.copy_mset' [in
AAC_tactics.AAC ]
+
Internal.copy_Psucc [in
AAC_tactics.AAC ]
+
Internal.copy_xH [in
AAC_tactics.AAC ]
+
Internal.copy_plus [in
AAC_tactics.AAC ]
+
Internal.decide [in
AAC_tactics.AAC ]
+
Internal.eval_norm_lists [in
AAC_tactics.AAC ]
+
Internal.eval_prd_app [in
AAC_tactics.AAC ]
+
Internal.eval_prd_cons [in
AAC_tactics.AAC ]
+
Internal.eval_prd_nil [in
AAC_tactics.AAC ]
+
Internal.eval_reduce_msets [in
AAC_tactics.AAC ]
+
Internal.eval_norm_msets [in
AAC_tactics.AAC ]
+
Internal.eval_merge_bin [in
AAC_tactics.AAC ]
+
Internal.eval_sum_cons [in
AAC_tactics.AAC ]
+
Internal.eval_sum_nil [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec [in
AAC_tactics.AAC ]
+
Internal.is_unit_of_Unit [in
AAC_tactics.AAC ]
+
Internal.lift_normalise [in
AAC_tactics.AAC ]
+
Internal.normalise [in
AAC_tactics.AAC ]
+
Internal.prd'_prd [in
AAC_tactics.AAC ]
+
Internal.sum'_sum [in
AAC_tactics.AAC ]
+
Internal.z0 [in
AAC_tactics.AAC ]
+
Internal.z0' [in
AAC_tactics.AAC ]
+
Internal.z1 [in
AAC_tactics.AAC ]
+
Internal.z1' [in
AAC_tactics.AAC ]
+
Internal.z2 [in
AAC_tactics.AAC ]
+
Internal.z2' [in
AAC_tactics.AAC ]
+
inv_unique [in
AAC_tactics.Caveats ]
+
L
+
lift_reflexivity [in
AAC_tactics.AAC ]
+
lift_transitivity_right [in
AAC_tactics.AAC ]
+
lift_transitivity_left [in
AAC_tactics.AAC ]
+
list_compare_weak_spec [in
AAC_tactics.Utils ]
+
M
+
mset_compare_weak_spec [in
AAC_tactics.Utils ]
+
P
+
pos_compare_weak_spec [in
AAC_tactics.Utils ]
+
R
+
reflect_eqdep_weak_spec [in
AAC_tactics.Utils ]
+
reflect_eqdep_eq [in
AAC_tactics.Utils ]
+
Z
+
Z_add_opp_diag_r [in
AAC_tactics.Tutorial ]
+
Z_abs_triangle [in
AAC_tactics.Tutorial ]
+
+
Constructor Index
+
C
+
cons [in
AAC_tactics.Utils ]
+
D
+
decide_false [in
AAC_tactics.Utils ]
+
decide_true [in
AAC_tactics.Utils ]
+
I
+
Internal.cpu_right [in
AAC_tactics.AAC ]
+
Internal.cpu_left [in
AAC_tactics.AAC ]
+
Internal.csu_right [in
AAC_tactics.AAC ]
+
Internal.csu_left [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_nothing [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_unit [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_op [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_nothing [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_unit [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_op [in
AAC_tactics.AAC ]
+
Internal.Is_nothing [in
AAC_tactics.AAC ]
+
Internal.Is_unit [in
AAC_tactics.AAC ]
+
Internal.Is_op [in
AAC_tactics.AAC ]
+
Internal.left [in
AAC_tactics.AAC ]
+
Internal.prd [in
AAC_tactics.AAC ]
+
Internal.right [in
AAC_tactics.AAC ]
+
Internal.sum [in
AAC_tactics.AAC ]
+
Internal.sym [in
AAC_tactics.AAC ]
+
Internal.unit [in
AAC_tactics.AAC ]
+
Internal.vcons [in
AAC_tactics.AAC ]
+
Internal.vnil [in
AAC_tactics.AAC ]
+
L
+
law_idem [in
AAC_tactics.AAC ]
+
law_comm [in
AAC_tactics.AAC ]
+
law_assoc [in
AAC_tactics.AAC ]
+
N
+
nil [in
AAC_tactics.Utils ]
+
P
+
pcws_gt [in
AAC_tactics.Utils ]
+
pcws_lt [in
AAC_tactics.Utils ]
+
pcws_eq [in
AAC_tactics.Utils ]
+
+
Inductive Index
+
A
+
Associative [in
AAC_tactics.AAC ]
+
C
+
Commutative [in
AAC_tactics.AAC ]
+
compare_weak_spec [in
AAC_tactics.Utils ]
+
D
+
decide_spec [in
AAC_tactics.Utils ]
+
I
+
Idempotent [in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit [in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit [in
AAC_tactics.AAC ]
+
Internal.discr [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_ind [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_ind [in
AAC_tactics.AAC ]
+
Internal.m [in
AAC_tactics.AAC ]
+
Internal.T [in
AAC_tactics.AAC ]
+
Internal.vT [in
AAC_tactics.AAC ]
+
N
+
nelist [in
AAC_tactics.Utils ]
+
+
Projection Index
+
A
+
aac_list_proper [in
AAC_tactics.AAC ]
+
aac_lift_equivalence [in
AAC_tactics.AAC ]
+
I
+
Internal.Bin.assoc [in
AAC_tactics.AAC ]
+
Internal.Bin.comm [in
AAC_tactics.AAC ]
+
Internal.Bin.compat [in
AAC_tactics.AAC ]
+
Internal.Bin.idem [in
AAC_tactics.AAC ]
+
Internal.Bin.value [in
AAC_tactics.AAC ]
+
Internal.Sym.ar [in
AAC_tactics.AAC ]
+
Internal.Sym.morph [in
AAC_tactics.AAC ]
+
Internal.Sym.value [in
AAC_tactics.AAC ]
+
Internal.uf_desc [in
AAC_tactics.AAC ]
+
Internal.uf_idx [in
AAC_tactics.AAC ]
+
Internal.u_desc [in
AAC_tactics.AAC ]
+
Internal.u_value [in
AAC_tactics.AAC ]
+
L
+
law_neutral_right [in
AAC_tactics.AAC ]
+
law_neutral_left [in
AAC_tactics.AAC ]
+
law_idem [in
AAC_tactics.AAC ]
+
law_comm [in
AAC_tactics.AAC ]
+
law_assoc [in
AAC_tactics.AAC ]
+
+
Section Index
+
A
+
AAC_normalise [in
AAC_tactics.Tutorial ]
+
B
+
base [in
AAC_tactics.Tutorial ]
+
base.both [in
AAC_tactics.Tutorial ]
+
base.dealing_with_units [in
AAC_tactics.Tutorial ]
+
base.morphisms [in
AAC_tactics.Tutorial ]
+
base.occurrence [in
AAC_tactics.Tutorial ]
+
base.reminder [in
AAC_tactics.Tutorial ]
+
base.subst [in
AAC_tactics.Tutorial ]
+
D
+
dep [in
AAC_tactics.Utils ]
+
E
+
evars [in
AAC_tactics.Caveats ]
+
Examples [in
AAC_tactics.Tutorial ]
+
I
+
ineq [in
AAC_tactics.Caveats ]
+
Internal.Bin.t [in
AAC_tactics.AAC ]
+
Internal.copy [in
AAC_tactics.AAC ]
+
Internal.s [in
AAC_tactics.AAC ]
+
Internal.Sym.t [in
AAC_tactics.AAC ]
+
Internal.s.prds [in
AAC_tactics.AAC ]
+
Internal.s.prd_correctness [in
AAC_tactics.AAC ]
+
Internal.s.sums [in
AAC_tactics.AAC ]
+
Internal.s.sum_correctness [in
AAC_tactics.AAC ]
+
introduction [in
AAC_tactics.Tutorial ]
+
L
+
lists [in
AAC_tactics.Utils ]
+
Lists [in
AAC_tactics.Tutorial ]
+
lists.c [in
AAC_tactics.Utils ]
+
lists.list_compare_weak_spec [in
AAC_tactics.Utils ]
+
lists.m [in
AAC_tactics.Utils ]
+
lists.mset_compare_weak_spec [in
AAC_tactics.Utils ]
+
M
+
morphism [in
AAC_tactics.Caveats ]
+
P
+
parameters [in
AAC_tactics.Caveats ]
+
Peano [in
AAC_tactics.Caveats ]
+
Peano [in
AAC_tactics.Tutorial ]
+
Props [in
AAC_tactics.Tutorial ]
+
R
+
Relations.defs [in
AAC_tactics.Instances ]
+
S
+
sigma [in
AAC_tactics.AAC ]
+
T
+
t [in
AAC_tactics.AAC ]
+
U
+
U [in
AAC_tactics.Caveats ]
+
V
+
V [in
AAC_tactics.Caveats ]
+
W
+
W [in
AAC_tactics.Caveats ]
+
Z
+
Z [in
AAC_tactics.Caveats ]
+
+
Instance Index
+
A
+
aac_lift_proper [in
AAC_tactics.AAC ]
+
aac_lift_subrelation [in
AAC_tactics.AAC ]
+
aac_le_eq_lift [in
AAC_tactics.Tutorial ]
+
aac_Nat_max_0_Unit [in
AAC_tactics.Tutorial ]
+
aac_Nat_max_Idem [in
AAC_tactics.Tutorial ]
+
aac_Nat_max_Assoc [in
AAC_tactics.Tutorial ]
+
aac_Nat_max_Comm [in
AAC_tactics.Tutorial ]
+
aac_Nat_add_0_Unit [in
AAC_tactics.Tutorial ]
+
aac_Nat_mul_1_Unit [in
AAC_tactics.Tutorial ]
+
aac_Nat_mul_Assoc [in
AAC_tactics.Tutorial ]
+
aac_Nat_mul_Comm [in
AAC_tactics.Tutorial ]
+
aac_Nat_add_Comm [in
AAC_tactics.Tutorial ]
+
aac_Nat_add_Assoc [in
AAC_tactics.Tutorial ]
+
B
+
Bool.aac_Bool_andb_true_Unit [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_false_Unit [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_Idem [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_Comm [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_andb_Assoc [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_Idem [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_Comm [in
AAC_tactics.Instances ]
+
Bool.aac_Bool_orb_Assoc [in
AAC_tactics.Instances ]
+
Bool.negb_compat [in
AAC_tactics.Instances ]
+
I
+
Internal.assoc [in
AAC_tactics.AAC ]
+
Internal.Binvalue_Proper [in
AAC_tactics.AAC ]
+
Internal.Binvalue_Associative [in
AAC_tactics.AAC ]
+
Internal.Binvalue_Idempotent [in
AAC_tactics.AAC ]
+
Internal.Binvalue_Commutative [in
AAC_tactics.AAC ]
+
Internal.compat_prd_Unit [in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_Unit [in
AAC_tactics.AAC ]
+
Internal.copy_compat [in
AAC_tactics.AAC ]
+
Internal.eval_aux_compat [in
AAC_tactics.AAC ]
+
Internal.proper [in
AAC_tactics.AAC ]
+
L
+
Lists.aac_List_app_nil_Permutation_Unit [in
AAC_tactics.Instances ]
+
Lists.aac_List_app_Permutation_Comm [in
AAC_tactics.Instances ]
+
Lists.aac_List_app_Permutation_Assoc [in
AAC_tactics.Instances ]
+
Lists.aac_List_app_nil_Unit [in
AAC_tactics.Instances ]
+
Lists.aac_List_app_Assoc [in
AAC_tactics.Instances ]
+
N
+
N.aac_N_le_eq_lift [in
AAC_tactics.Instances ]
+
N.aac_N_max_0_Unit [in
AAC_tactics.Instances ]
+
N.aac_N_add_0_Unit [in
AAC_tactics.Instances ]
+
N.aac_N_mul_1_Unit [in
AAC_tactics.Instances ]
+
N.aac_N_max_Idem [in
AAC_tactics.Instances ]
+
N.aac_N_max_Assoc [in
AAC_tactics.Instances ]
+
N.aac_N_max_Comm [in
AAC_tactics.Instances ]
+
N.aac_N_min_Idem [in
AAC_tactics.Instances ]
+
N.aac_N_min_Assoc [in
AAC_tactics.Instances ]
+
N.aac_N_min_Comm [in
AAC_tactics.Instances ]
+
N.aac_N_mul_Assoc [in
AAC_tactics.Instances ]
+
N.aac_N_mul_Comm [in
AAC_tactics.Instances ]
+
N.aac_N_add_Comm [in
AAC_tactics.Instances ]
+
N.aac_N_add_Assoc [in
AAC_tactics.Instances ]
+
N.N_le_PreOrder [in
AAC_tactics.Instances ]
+
P
+
Peano.aac_Nat_le_eq_lift [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_0_Unit [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_add_0_Unit [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_mul_1_Unit [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_Idem [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_Assoc [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_max_Comm [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_min_Idem [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_min_Assoc [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_min_Comm [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_mul_Assoc [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_mul_Comm [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_add_Comm [in
AAC_tactics.Instances ]
+
Peano.aac_Nat_add_Assoc [in
AAC_tactics.Instances ]
+
Peano.Nat_le_PreOrder [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_impl_iff_lift [in
AAC_tactics.Instances ]
+
Prop_ops.not_iff_compat [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_True_iff_Unit [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_False_iff_Unit [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_iff_Idem [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_iff_Comm [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_and_iff_Assoc [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_iff_Idem [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_iff_Comm [in
AAC_tactics.Instances ]
+
Prop_ops.aac_Prop_or_iff_Assoc [in
AAC_tactics.Instances ]
+
P.aac_Pos_le_eq_lift [in
AAC_tactics.Instances ]
+
P.aac_Pos_max_1_Unit [in
AAC_tactics.Instances ]
+
P.aac_Pos_mul_1_Unit [in
AAC_tactics.Instances ]
+
P.aac_Pos_max_Idem [in
AAC_tactics.Instances ]
+
P.aac_Pos_max_Assoc [in
AAC_tactics.Instances ]
+
P.aac_Pos_max_Comm [in
AAC_tactics.Instances ]
+
P.aac_Pos_min_Idem [in
AAC_tactics.Instances ]
+
P.aac_Pos_min_Assoc [in
AAC_tactics.Instances ]
+
P.aac_Pos_min_Comm [in
AAC_tactics.Instances ]
+
P.aac_Pos_mul_Assoc [in
AAC_tactics.Instances ]
+
P.aac_Pos_mul_Comm [in
AAC_tactics.Instances ]
+
P.aac_Pos_add_Comm [in
AAC_tactics.Instances ]
+
P.aac_Pos_add_Assoc [in
AAC_tactics.Instances ]
+
P.Pos_le_PreOrder [in
AAC_tactics.Instances ]
+
Q
+
Q.aac_Q_Qle_eq_lift [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qplus_0_Qeq_Unit [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmult_1_Qeq_Unit [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmax_Qeq_Idem [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmax_Qeq_Assoc [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmax_Qeq_Comm [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmin_Qeq_Idem [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmin_Qeq_Assoc [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmin_Qeq_Comm [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmult_Qeq_Assoc [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qmult_Qeq_Comm [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qplus_Qeq_Comm [in
AAC_tactics.Instances ]
+
Q.aac_Q_Qplus_Qeq_Assoc [in
AAC_tactics.Instances ]
+
Q.Q_Qle_PreOrder [in
AAC_tactics.Instances ]
+
R
+
Relations.aac_inclusion_same_relation_lift [in
AAC_tactics.Instances ]
+
Relations.aac_compo_eq_same_relation_Unit [in
AAC_tactics.Instances ]
+
Relations.aac_compo_same_relation_Assoc [in
AAC_tactics.Instances ]
+
Relations.aac_inter_top_same_relation_Unit [in
AAC_tactics.Instances ]
+
Relations.aac_inter_same_relation_Idem [in
AAC_tactics.Instances ]
+
Relations.aac_inter_same_relation_Assoc [in
AAC_tactics.Instances ]
+
Relations.aac_inter_same_relation_Comm [in
AAC_tactics.Instances ]
+
Relations.aac_bot_union_same_relation_Unit [in
AAC_tactics.Instances ]
+
Relations.aac_union_same_relation_Idem [in
AAC_tactics.Instances ]
+
Relations.aac_union_same_relation_Assoc [in
AAC_tactics.Instances ]
+
Relations.aac_union_same_relation_Comm [in
AAC_tactics.Instances ]
+
Relations.clos_refl_trans_same_relation_compat [in
AAC_tactics.Instances ]
+
Relations.clos_refl_trans_incr [in
AAC_tactics.Instances ]
+
Relations.clos_trans_same_relation_compat [in
AAC_tactics.Instances ]
+
Relations.clos_trans_incr [in
AAC_tactics.Instances ]
+
Relations.inclusion_PreOrder [in
AAC_tactics.Instances ]
+
Relations.negr_same_relation_compat [in
AAC_tactics.Instances ]
+
Relations.same_relation_Equivalence [in
AAC_tactics.Instances ]
+
Relations.transp_same_relation_compat [in
AAC_tactics.Instances ]
+
Z
+
Z_add_incr [in
AAC_tactics.Caveats ]
+
Z_add_le_compat [in
AAC_tactics.Tutorial ]
+
Z_opp_ge_le_compat [in
AAC_tactics.Tutorial ]
+
Z.aac_Z_le_eq_lift [in
AAC_tactics.Instances ]
+
Z.aac_Z_add_0_Unit [in
AAC_tactics.Instances ]
+
Z.aac_Z_mul_1_Unit [in
AAC_tactics.Instances ]
+
Z.aac_Z_max_Idem [in
AAC_tactics.Instances ]
+
Z.aac_Z_max_Assoc [in
AAC_tactics.Instances ]
+
Z.aac_Z_max_Comm [in
AAC_tactics.Instances ]
+
Z.aac_Z_min_Idem [in
AAC_tactics.Instances ]
+
Z.aac_Z_min_Assoc [in
AAC_tactics.Instances ]
+
Z.aac_Z_min_Comm [in
AAC_tactics.Instances ]
+
Z.aac_Z_mul_Assoc [in
AAC_tactics.Instances ]
+
Z.aac_Z_mul_Comm [in
AAC_tactics.Instances ]
+
Z.aac_Z_add_Comm [in
AAC_tactics.Instances ]
+
Z.aac_Z_add_Assoc [in
AAC_tactics.Instances ]
+
Z.Z_le_PreOrder [in
AAC_tactics.Instances ]
+
+
Abbreviation Index
+
C
+
cast [in
AAC_tactics.Utils ]
+
I
+
idx [in
AAC_tactics.Utils ]
+
L
+
lex [in
AAC_tactics.Utils ]
+
P
+
pos_compare [in
AAC_tactics.Utils ]
+
+
Definition Index
+
A
+
appne [in
AAC_tactics.Utils ]
+
C
+
compare_weak_spec_sind [in
AAC_tactics.Utils ]
+
compare_weak_spec_ind [in
AAC_tactics.Utils ]
+
D
+
decide_spec_sind [in
AAC_tactics.Utils ]
+
decide_spec_ind [in
AAC_tactics.Utils ]
+
E
+
eq_idx_bool [in
AAC_tactics.Utils ]
+
F
+
fold_map' [in
AAC_tactics.Utils ]
+
fold_map [in
AAC_tactics.Utils ]
+
I
+
idx_compare [in
AAC_tactics.Utils ]
+
insert [in
AAC_tactics.Utils ]
+
Internal.add_to_prd [in
AAC_tactics.AAC ]
+
Internal.add_to_sum [in
AAC_tactics.AAC ]
+
Internal.comp [in
AAC_tactics.AAC ]
+
Internal.compare [in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_sind [in
AAC_tactics.AAC ]
+
Internal.compat_prd_unit_ind [in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_sind [in
AAC_tactics.AAC ]
+
Internal.compat_sum_unit_ind [in
AAC_tactics.AAC ]
+
Internal.copy [in
AAC_tactics.AAC ]
+
Internal.copy_mset [in
AAC_tactics.AAC ]
+
Internal.copy' [in
AAC_tactics.AAC ]
+
Internal.discr_sind [in
AAC_tactics.AAC ]
+
Internal.discr_rec [in
AAC_tactics.AAC ]
+
Internal.discr_ind [in
AAC_tactics.AAC ]
+
Internal.discr_rect [in
AAC_tactics.AAC ]
+
Internal.eval [in
AAC_tactics.AAC ]
+
Internal.eval_norm_aux [in
AAC_tactics.AAC ]
+
Internal.eval_norm [in
AAC_tactics.AAC ]
+
Internal.eval_aux [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_ind_sind [in
AAC_tactics.AAC ]
+
Internal.is_prd_spec_ind_ind [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_ind_sind [in
AAC_tactics.AAC ]
+
Internal.is_sum_spec_ind_ind [in
AAC_tactics.AAC ]
+
Internal.is_prd [in
AAC_tactics.AAC ]
+
Internal.is_sum [in
AAC_tactics.AAC ]
+
Internal.is_idempotent [in
AAC_tactics.AAC ]
+
Internal.is_commutative [in
AAC_tactics.AAC ]
+
Internal.is_unit_of [in
AAC_tactics.AAC ]
+
Internal.m_sind [in
AAC_tactics.AAC ]
+
Internal.m_rec [in
AAC_tactics.AAC ]
+
Internal.m_ind [in
AAC_tactics.AAC ]
+
Internal.m_rect [in
AAC_tactics.AAC ]
+
Internal.norm [in
AAC_tactics.AAC ]
+
Internal.norm_msets [in
AAC_tactics.AAC ]
+
Internal.norm_lists [in
AAC_tactics.AAC ]
+
Internal.norm_lists_ [in
AAC_tactics.AAC ]
+
Internal.norm_msets_ [in
AAC_tactics.AAC ]
+
Internal.prd' [in
AAC_tactics.AAC ]
+
Internal.return_prd [in
AAC_tactics.AAC ]
+
Internal.return_sum [in
AAC_tactics.AAC ]
+
Internal.run_msets [in
AAC_tactics.AAC ]
+
Internal.run_list [in
AAC_tactics.AAC ]
+
Internal.sum' [in
AAC_tactics.AAC ]
+
Internal.Sym.null [in
AAC_tactics.AAC ]
+
Internal.Sym.rel_of [in
AAC_tactics.AAC ]
+
Internal.Sym.type_of [in
AAC_tactics.AAC ]
+
Internal.tcompare_weak_spec [in
AAC_tactics.AAC ]
+
Internal.T_sind [in
AAC_tactics.AAC ]
+
Internal.T_rec [in
AAC_tactics.AAC ]
+
Internal.T_ind [in
AAC_tactics.AAC ]
+
Internal.T_rect [in
AAC_tactics.AAC ]
+
Internal.vcompare [in
AAC_tactics.AAC ]
+
Internal.vcompare_reflect_eqdep [in
AAC_tactics.AAC ]
+
Internal.vnorm [in
AAC_tactics.AAC ]
+
Internal.vT_sind [in
AAC_tactics.AAC ]
+
Internal.vT_rec [in
AAC_tactics.AAC ]
+
Internal.vT_ind [in
AAC_tactics.AAC ]
+
Internal.vT_rect [in
AAC_tactics.AAC ]
+
L
+
list_compare [in
AAC_tactics.Utils ]
+
M
+
merge_map [in
AAC_tactics.Utils ]
+
merge_msets [in
AAC_tactics.Utils ]
+
mset [in
AAC_tactics.Utils ]
+
mset_compare [in
AAC_tactics.Utils ]
+
N
+
nelist_map [in
AAC_tactics.Utils ]
+
nelist_sind [in
AAC_tactics.Utils ]
+
nelist_rec [in
AAC_tactics.Utils ]
+
nelist_ind [in
AAC_tactics.Utils ]
+
nelist_rect [in
AAC_tactics.Utils ]
+
R
+
reduce_mset [in
AAC_tactics.Utils ]
+
reflect_eqdep [in
AAC_tactics.Utils ]
+
Relations.bot [in
AAC_tactics.Instances ]
+
Relations.compo [in
AAC_tactics.Instances ]
+
Relations.inter [in
AAC_tactics.Instances ]
+
Relations.negr [in
AAC_tactics.Instances ]
+
Relations.top [in
AAC_tactics.Instances ]
+
S
+
sigma [in
AAC_tactics.AAC ]
+
sigma_empty [in
AAC_tactics.AAC ]
+
sigma_add [in
AAC_tactics.AAC ]
+
sigma_get [in
AAC_tactics.AAC ]
+
U
+
Unnamed_thm5 [in
AAC_tactics.Caveats ]
+
Unnamed_thm5 [in
AAC_tactics.Caveats ]
+
Unnamed_thm5 [in
AAC_tactics.Caveats ]
+
Unnamed_thm5 [in
AAC_tactics.Caveats ]
+
Unnamed_thm4 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm3 [in
AAC_tactics.Caveats ]
+
Unnamed_thm2 [in
AAC_tactics.Caveats ]
+
Unnamed_thm1 [in
AAC_tactics.Caveats ]
+
Unnamed_thm1 [in
AAC_tactics.Caveats ]
+
Unnamed_thm0 [in
AAC_tactics.Caveats ]
+
Unnamed_thm [in
AAC_tactics.Caveats ]
+
Unnamed_thm26 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm25 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm24 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm23 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm22 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm21 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm20 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm20 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm20 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm19 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm18 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm17 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm16 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm15 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm14 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm13 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm12 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm11 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm11 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm10 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm9 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm8 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm7 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm6 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm5 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm4 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm3 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm2 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm1 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm0 [in
AAC_tactics.Tutorial ]
+
Unnamed_thm [in
AAC_tactics.Tutorial ]
+
+
Record Index
+
A
+
AAC_lift [in
AAC_tactics.AAC ]
+
Associative [in
AAC_tactics.AAC ]
+
C
+
Commutative [in
AAC_tactics.AAC ]
+
I
+
Idempotent [in
AAC_tactics.AAC ]
+
Internal.Bin.pack [in
AAC_tactics.AAC ]
+
Internal.Sym.pack [in
AAC_tactics.AAC ]
+
Internal.unit_pack [in
AAC_tactics.AAC ]
+
Internal.unit_of [in
AAC_tactics.AAC ]
+
U
+
Unit [in
AAC_tactics.AAC ]
+
+
+Global Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(663 entries)
+
+
+Notation Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(19 entries)
+
+
+Module Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(13 entries)
+
+
+Variable Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(176 entries)
+
+
+Library Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(6 entries)
+
+
+Lemma Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(54 entries)
+
+
+Constructor Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(31 entries)
+
+
+Inductive Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(14 entries)
+
+
+Projection Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(19 entries)
+
+
+Section Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(39 entries)
+
+
+Instance Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(141 entries)
+
+
+Abbreviation Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(4 entries)
+
+
+Definition Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(138 entries)
+
+
+Record Index
+A
+B
+C
+D
+E
+F
+G
+H
+I
+J
+K
+L
+M
+N
+O
+P
+Q
+R
+S
+T
+U
+V
+W
+X
+Y
+Z
+_
+other
+(9 entries)
+
+
+
+
+
+
+
+
diff --git a/docs/coqdoc/toc.html b/docs/coqdoc/toc.html
new file mode 100644
index 0000000..85db8c6
--- /dev/null
+++ b/docs/coqdoc/toc.html
@@ -0,0 +1,223 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/docs/ocamldoc/Aac_rewrite.html b/docs/ocamldoc/Aac_rewrite.html
new file mode 100644
index 0000000..b15c33f
--- /dev/null
+++ b/docs/ocamldoc/Aac_rewrite.html
@@ -0,0 +1,39 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Aac_rewrite
+
+
+
+
+
+module Aac_rewrite : sig
.. end
+
+
aac_rewrite -- rewriting modulo A or AC
+
+
+
+
+val aac_reflexivity : unit Proofview.tactic
+val aac_normalise : unit Proofview.tactic
+val aac_rewrite : args:(string * int) list -> ?abort:bool -> ?l2r:bool -> ?show:bool -> ?strict:bool -> ?extra:EConstr.t -> EConstr.constr -> unit Proofview.tactic
+val add : string -> 'a -> (string * 'a) list -> (string * 'a) list
+val pr_aac_args : 'a -> 'b -> 'c -> (string * int) list -> Pp.t
diff --git a/docs/ocamldoc/Coq.Classes.html b/docs/ocamldoc/Coq.Classes.html
new file mode 100644
index 0000000..7b9fe16
--- /dev/null
+++ b/docs/ocamldoc/Coq.Classes.html
@@ -0,0 +1,40 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Classes
+
+
+
+
+
+module Classes : sig
.. end
+
+
+val mk_morphism : EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
+val mk_equivalence : EConstr.constr -> EConstr.constr -> EConstr.constr
+val mk_reflexive : EConstr.constr -> EConstr.constr -> EConstr.constr
+val mk_transitive : EConstr.constr -> EConstr.constr -> EConstr.constr
diff --git a/docs/ocamldoc/Coq.Equivalence.html b/docs/ocamldoc/Coq.Equivalence.html
new file mode 100644
index 0000000..84900ce
--- /dev/null
+++ b/docs/ocamldoc/Coq.Equivalence.html
@@ -0,0 +1,62 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Equivalence
+
+
+
+
+
+module Equivalence : sig
.. end
+
+type
t = {
+
+
+
+
+carrier : EConstr.constr
;
+
+
+
+
+
+
+eq : EConstr.constr
;
+
+
+
+
+
+
+equivalence : EConstr.constr
;
+
+
+}
+
+
+
+val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t
+val infer : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> t * Evd.evar_map
+val from_relation : Environ.env -> Evd.evar_map -> Coq.Relation.t -> t * Evd.evar_map
+val to_relation : t -> Coq.Relation.t
+val split : t -> EConstr.constr * EConstr.constr * EConstr.constr
diff --git a/docs/ocamldoc/Coq.List.html b/docs/ocamldoc/Coq.List.html
new file mode 100644
index 0000000..ce6fab9
--- /dev/null
+++ b/docs/ocamldoc/Coq.List.html
@@ -0,0 +1,46 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.List
+
+
+
+
+
+module List : sig
.. end
+
+
+val of_list : EConstr.constr -> EConstr.constr list -> EConstr.constr
+
+val type_of_list : EConstr.constr -> EConstr.constr
+
diff --git a/docs/ocamldoc/Coq.Nat.html b/docs/ocamldoc/Coq.Nat.html
new file mode 100644
index 0000000..04b6ff9
--- /dev/null
+++ b/docs/ocamldoc/Coq.Nat.html
@@ -0,0 +1,38 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Nat
+
+
+
+
+
+module Nat : sig
.. end
+
+
Coq unary numbers (peano)
+
+
+
+
+val typ : Coq.lazy_ref
+val of_int : int -> Constr.constr
diff --git a/docs/ocamldoc/Coq.Option.html b/docs/ocamldoc/Coq.Option.html
new file mode 100644
index 0000000..293ec43
--- /dev/null
+++ b/docs/ocamldoc/Coq.Option.html
@@ -0,0 +1,35 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Option
+
+
+
+
+
+module Option : sig
.. end
+
+val typ : Coq.lazy_ref
+val some : EConstr.constr -> EConstr.constr -> EConstr.constr
+val none : EConstr.constr -> EConstr.constr
+val of_option : EConstr.constr -> EConstr.constr option -> EConstr.constr
diff --git a/docs/ocamldoc/Coq.Pair.html b/docs/ocamldoc/Coq.Pair.html
new file mode 100644
index 0000000..4c02a96
--- /dev/null
+++ b/docs/ocamldoc/Coq.Pair.html
@@ -0,0 +1,39 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Pair
+
+
+
+
+
+module Pair : sig
.. end
+
+
+val typ : Coq.lazy_ref
+val pair : Coq.lazy_ref
+val of_pair : EConstr.constr -> EConstr.constr -> EConstr.constr * EConstr.constr -> EConstr.constr
diff --git a/docs/ocamldoc/Coq.Pos.html b/docs/ocamldoc/Coq.Pos.html
new file mode 100644
index 0000000..635f0b1
--- /dev/null
+++ b/docs/ocamldoc/Coq.Pos.html
@@ -0,0 +1,38 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Pos
+
+
+
+
+
+module Pos : sig
.. end
+
+
Coq positive numbers (pos)
+
+
+
+
+val typ : Coq.lazy_ref
+val of_int : int -> EConstr.constr
diff --git a/docs/ocamldoc/Coq.Relation.html b/docs/ocamldoc/Coq.Relation.html
new file mode 100644
index 0000000..bd18049
--- /dev/null
+++ b/docs/ocamldoc/Coq.Relation.html
@@ -0,0 +1,52 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Relation
+
+
+
+
+
+module Relation : sig
.. end
+
+type
t = {
+
+
+
+
+carrier : EConstr.constr
;
+
+
+
+
+
+
+r : EConstr.constr
;
+
+
+}
+
+
+
+val make : EConstr.constr -> EConstr.constr -> t
+val split : t -> EConstr.constr * EConstr.constr
diff --git a/docs/ocamldoc/Coq.Rewrite.html b/docs/ocamldoc/Coq.Rewrite.html
new file mode 100644
index 0000000..b37d387
--- /dev/null
+++ b/docs/ocamldoc/Coq.Rewrite.html
@@ -0,0 +1,181 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Rewrite
+
+
+
+
+
+module Rewrite : sig
.. end
+The rewriting tactics used in aac_rewrite, build as handlers of the usual setoid_rewrite
+Datatypes
+type
hypinfo = {
+
+
+
+
+hyp : EConstr.constr
;
+
+
+
+
+
+
+hyptype : EConstr.constr
;
+
+
+
+
+
+
+context : EConstr.rel_context
;
+
+
+
+
+
+
+body : EConstr.constr
;
+
+
+
+
+
+
+rel : Coq.Relation.t
;
+
+
+
+
+
+
+left : EConstr.constr
;
+
+
+
+
+
+
+right : EConstr.constr
;
+
+
+
+
+
+
+l2r : bool
;
+
+
+}
+
+
+
+
We keep some informations about the hypothesis, with an (informal)
+ invariant:
+
+typeof hyp = typ
+typ = forall context, body
+body = rel left right
+
+
+
+
+
+val get_hypinfo : Environ.env -> Evd.evar_map -> ?check_type:(EConstr.types -> bool) -> EConstr.constr -> l2r:bool -> hypinfo
+
+
get_hypinfo ?check_type H l2r
analyse the hypothesis H, and
+ build the related hypinfo. Moreover, an optionnal
+ function can be provided to check the type of every free
+ variable of the body of the hypothesis.
+
+
+Rewriting with bindings
+The problem : Given a term to rewrite of type H :forall xn ... x1,
+ t
, we have to instanciate the subset of xi
of type
+ carrier
. subst : (int * constr)
is the mapping the De Bruijn
+ indices in t
to the constrs
. We need to handle the rest of the
+ indexes. Two ways :
+
+
+either using fresh evars and rewriting H tn ?1 tn-2 ?2
+either building a term like fun 1 2 => H tn 1 tn-2 2
+
+Both these terms have the same type.
+
+val build : hypinfo -> (int * EConstr.constr) list -> EConstr.constr
+
+
build the constr to rewrite, with lambda abstractions
+
+
+build the constr to rewrite, in CPS style, with evars
+
+val rewrite : ?abort:bool -> hypinfo -> (int * EConstr.constr) list -> unit Proofview.tactic
+
+
rewrite ?abort hypinfo subst
builds the rewriting tactic
+ associated with the given subst
and hypinfo
.
+If abort
is set to true
, we build
+ tclIDTAC
instead.
+
+
+
diff --git a/docs/ocamldoc/Coq.html b/docs/ocamldoc/Coq.html
new file mode 100644
index 0000000..7939c99
--- /dev/null
+++ b/docs/ocamldoc/Coq.html
@@ -0,0 +1,142 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq
+
+
+
+Module Coq
+
+module Coq : sig
.. end
+
+
Interface with Coq where we define some handlers for Coq's API,
+ and we import several definitions from Coq's standard library.
+
+
This general purpose library could be reused by other plugins.
+
+
Some salient points:
+
+we use Caml's module system to mimic Coq's one, and avoid cluttering
+ the namespace;
+we also provide several handlers for standard coq tactics, in
+ order to provide a unified setting (we replace functions that
+ modify the evar_map by functions that operate on the whole
+ goal, and repack the modified evar_map with it).
+
+
+
+
+
+type
tactic = unit Proofview.tactic
+
+
+type
lazy_ref = Names.GlobRef.t Stdlib.Lazy.t
+
+
+
Getting Coq terms from the environment
+
+
+
+val get_fresh : lazy_ref -> Constr.constr
+val get_efresh : lazy_ref -> EConstr.constr
+val find_global : string -> lazy_ref
General purpose functions
+val cps_resolve_one_typeclass : ?error:Pp.t -> EConstr.types -> (EConstr.constr -> tactic ) -> tactic
+val evar_binary : Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
+val evar_relation : Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
+val cps_mk_letin : string -> EConstr.constr -> (EConstr.constr -> tactic ) -> tactic
+
+
cps_mk_letin name v
binds the constr v
using a letin tactic
+
+
+
+val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic
+val retype : EConstr.constr -> tactic
+val tclRETYPE : EConstr.constr -> unit Proofview.tactic
+val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr, EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term
Bindings with Coq' Standard Library
+module List : sig
.. end
+
+module Pair : sig
.. end
+
+module Option : sig
.. end
+module Pos : sig
.. end
+
Coq positive numbers (pos)
+
+
+
+module Nat : sig
.. end
+
Coq unary numbers (peano)
+
+
+
+module Classes : sig
.. end
+
+module Relation : sig
.. end
+module Equivalence : sig
.. end
+val match_as_equation : ?context:EConstr.rel_context -> Environ.env -> Evd.evar_map -> EConstr.constr -> (EConstr.constr * EConstr.constr * Relation.t ) option
+
+
match_as_equation ?context env sigma c
try to decompose c as a
+ relation applied to two terms.
+
+
+
+val tclTIME : string -> tactic -> tactic
+
+
time the execution of a tactic
+
+
+
+val tclDEBUG : string -> unit Proofview.tactic
+
+
emit debug messages to see which tactics are failing
+
+
+
+val tclPRINT : unit Proofview.tactic
+
+
print the current goal
+
+
+
+val anomaly : string -> 'a
+val user_error : Pp.t -> 'a
+val warning : string -> unit
Helpers
+val show_proof : Declare.Proof.t -> unit
+
+
print the current proof term
+
+
+Rewriting tactics used in aac_rewrite
+module Rewrite : sig
.. end
diff --git a/docs/ocamldoc/Helper.CONTROL.html b/docs/ocamldoc/Helper.CONTROL.html
new file mode 100644
index 0000000..55fdf17
--- /dev/null
+++ b/docs/ocamldoc/Helper.CONTROL.html
@@ -0,0 +1,30 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Helper.CONTROL
+
+
+
+
+
+module type CONTROL = sig
.. end
+
+val debug : bool
+val time : bool
+val printing : bool
diff --git a/docs/ocamldoc/Helper.Debug.html b/docs/ocamldoc/Helper.Debug.html
new file mode 100644
index 0000000..921e9c5
--- /dev/null
+++ b/docs/ocamldoc/Helper.Debug.html
@@ -0,0 +1,62 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Helper.Debug
+
+
+
+
+
+module Debug :
+
+
+val debug : string -> unit
+
+
debug
prints the string and end it with a newline
+
+
+
+val debug_exception : string -> exn -> unit
+val time : ('a -> 'b) -> 'a -> (float -> unit, Stdlib.out_channel, unit) Stdlib.format -> 'b
+
+
time
computes the time spent in a function, and then
+ print it using the given format
+
+
+
+val pr_constr : Environ.env -> Evd.evar_map -> string -> EConstr.constr -> unit
+
+
pr_constr
print a Coq constructor, that can be labelled
+ by a string
+
+
+
diff --git a/docs/ocamldoc/Helper.html b/docs/ocamldoc/Helper.html
new file mode 100644
index 0000000..4c4ac84
--- /dev/null
+++ b/docs/ocamldoc/Helper.html
@@ -0,0 +1,38 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Helper
+
+
+
+
+
+module Helper : sig
.. end
+
+
Debugging functions, that can be triggered on a per-file base.
+
+
+
+
+module type CONTROL = sig
.. end
+module Debug :
diff --git a/docs/ocamldoc/Matcher.Subst.html b/docs/ocamldoc/Matcher.Subst.html
new file mode 100644
index 0000000..d780c1a
--- /dev/null
+++ b/docs/ocamldoc/Matcher.Subst.html
@@ -0,0 +1,47 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Matcher.Subst
+
+
+
+
+
+module Subst : sig
.. end
+
+
Substitutions (or environments)
+
+
The module Matcher.Subst
contains infrastructure to deal with
+ substitutions, i.e., functions from variables to terms. Only a
+ restricted subsets of these functions need to be exported.
+
+
As expected, a particular substitution can be used to
+ instantiate a pattern.
+
+
+
+
+type
t
+
+
+val sprint : t -> string
+val instantiate : t -> Matcher.Terms.t -> Matcher.Terms.t
+val to_list : t -> (Matcher.var * Matcher.Terms.t ) list
diff --git a/docs/ocamldoc/Matcher.Terms.html b/docs/ocamldoc/Matcher.Terms.html
new file mode 100644
index 0000000..d8d5943
--- /dev/null
+++ b/docs/ocamldoc/Matcher.Terms.html
@@ -0,0 +1,134 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Matcher.Terms
+
+
+
+
+
+module Terms : sig
.. end
+
+
Representations of expressions
+
+
The module Matcher.Terms
defines two different types for expressions.
+
+a public type Matcher.Terms.t
that represents abstract syntax trees
+ of expressions with binary associative and commutative operators
+a private type Matcher.Terms.nf_term
, corresponding to a canonical
+ representation for the above terms modulo AACU. The construction
+ functions on this type ensure that these terms are in normal form
+ (that is, no sum can appear as a subterm of the same sum, no
+ trailing units, lists corresponding to multisets are sorted,
+ etc...).
+
+
+
+
+Abstract syntax tree of terms and patterns
+We represent both terms and patterns using the following datatype.
+
+Values of type symbol
are used to index symbols. Typically,
+ given two associative operations (^)
and ( * )
, and two
+ morphisms f
and g
, the term f (a^b) (a*g b)
is represented
+ by the following value
+ Sym(0,[| Dot(1, Sym(2,[||]), Sym(3,[||]));
+ Dot(4, Sym(2,[||]), Sym(5,[|Sym(3,[||])|])) |])
+ where the implicit symbol environment associates
+ f
to 0
, (^)
to 1
, a
to 2
, b
to 3
, ( * )
to 4
, and g
to 5
,
+
+Accordingly, the following value, that contains "variables"
+ Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x,
+ Sym(5,[|Sym(3,[||])|])) |])
represents the pattern forall x, f
+ (x^1) (x*g b)
. The relationship between 1
and ( * )
is only
+ mentionned in the units table.
+
+type
t =
+
+
+
+val equal_aac : Matcher.units -> t -> t -> bool
+
+
Test for equality of terms modulo AACU (relies on the following
+ canonical representation of terms). Note than two different
+ units of a same operator are not considered equal.
+
+
+Normalised terms (canonical representation)
+A term in normal form is the canonical representative of the
+ equivalence class of all the terms that are equal modulo AACU.
+ This representation is only used internally; it is exported here
+ for the sake of completeness
+
+type
nf_term
+
+Comparisons
+val nf_term_compare : nf_term -> nf_term -> int
+val nf_equal : nf_term -> nf_term -> bool
Printing function
+val sprint_nf_term : nf_term -> string
Conversion functions
+val term_of_t : Matcher.units -> t -> nf_term
+
+
we have the following property: a
and b
are equal modulo AACU
+ iif nf_equal (term_of_t a) (term_of_t b) = true
+
+
+
+val t_of_term : nf_term -> t
diff --git a/docs/ocamldoc/Matcher.html b/docs/ocamldoc/Matcher.html
new file mode 100644
index 0000000..839af8d
--- /dev/null
+++ b/docs/ocamldoc/Matcher.html
@@ -0,0 +1,158 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Matcher
+
+
+
+
+
+module Matcher : sig
.. end
+
+
Standalone module containing the algorithm for matching modulo
+ associativity and associativity and commutativity
+ (AAC). Additionnaly, some A or AC operators can have units (U).
+
+
This module could be reused outside of the Coq plugin.
+
+
Matching a pattern p
against a term t
modulo AACU boils down
+ to finding a substitution env
such that the pattern p
+ instantiated with env
is equal to t
modulo AACU.
+
+
We proceed by structural decomposition of the pattern, trying all
+ possible non-deterministic splittings of the subject, when needed. The
+ function Matcher.matcher
is limited to top-level matching, that is, the
+ subject must make a perfect match against the pattern (x+x
does
+ not match a+a+b
).
+
+
We use a search monad Search_monad
to perform non-deterministic
+ choices in an almost transparent way.
+
+
We also provide a function Matcher.subterm
for finding a match that is
+ a subterm of the subject modulo AACU. In particular, this function
+ gives a solution to the aforementioned case (x+x
against
+ a+b+a
).
+
+
On a slightly more involved level :
+
+it must be noted that we allow several AC/A operators to share
+ the same units, but that a given AC/A operator can have at most
+ one unit.
+
+
+if the pattern does not contain "hard" symbols (like constants,
+ function symbols, AC or A symbols without units), there can be
+ infinitely many subterms such that the pattern matches: it is
+ possible to build "subterms" modulo AAC and U that make the size
+ of the term increase (by making neutral elements appear in a
+ layered fashion). Hence, in this case, a warning is issued, and
+ some solutions are omitted.
+
+
+
+
+Utility functions
+type
symbol = int
+
+
+type
var = int
+
+Relationship between units and operators. This is a sparse
+ representation of a matrix of couples (op,unit)
where op
is
+ the index of the operation, and unit
the index of the relevant
+ unit. We make the assumption that any operation has 0 or 1 unit,
+ and that operations can share a unit).
+
+type
units = (symbol * symbol ) list
+
+
+type
ext_units = {
+
+
+
+
+unit_for : units
;
+
+
+
+
+
+
+is_ac : (symbol * bool) list
;
+
+
+}
+
+
+
+type 'a
mset = ('a * int) list
+
+
+
The arguments of sums (or AC operators) are represented using finite multisets.
+ (Typically, a+b+a
corresponds to 2.a+b
, i.e. Sum[a,2;b,1]
)
+
+
+
+
+val linear : 'a mset -> 'a list
+
+
linear
expands a multiset into a simple list
+
+
+
+module Terms : sig
.. end
+
Representations of expressions
+
+
+
+module Subst : sig
.. end
+
Substitutions (or environments)
+
+
+Main functions exported by this module
+val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t Search_monad.m
+
+
matcher p t
computes the set of solutions to the given top-level
+ matching problem (p
is the pattern, t
is the term). If the
+ strict
flag is set, solutions where units are used to
+ instantiate some variables are excluded, unless this unit appears
+ directly under a function symbol (e.g., f(x) still matches f(1),
+ while x+x+y does not match a+b+c, since this would require to
+ assign 1 to x).
+
+
+
+val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t Search_monad.m ) Search_monad.m
+
+
subterm p t
computes a set of solutions to the given
+ subterm-matching problem.
+
+
Return a collection of possible solutions (each with the
+ associated depth, the context, and the solutions of the matching
+ problem). The context is actually a Matcher.Terms.t
where the variables
+ are yet to be instantiated by one of the associated substitutions
+
+
+
diff --git a/docs/ocamldoc/Print.html b/docs/ocamldoc/Print.html
new file mode 100644
index 0000000..407263a
--- /dev/null
+++ b/docs/ocamldoc/Print.html
@@ -0,0 +1,46 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Print
+
+
+
+
+
+module Print : sig
.. end
+
+
Pretty printing functions we use for the aac_instances
+ tactic.
+
+
+
+
+val print : Coq.Relation.t -> Theory.Trans.ir -> (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m ) Search_monad.m -> EConstr.rel_context -> unit Proofview.tactic
+
+
The main printing function. Print.print
uses the rel-context
+ to rename the variables, and rebuilds raw Coq terms (for the given
+ context, and the terms in the environment). In order to do so, it
+ requires the information gathered by the Theory.Trans
module.
+
+
+
diff --git a/docs/ocamldoc/Search_monad.html b/docs/ocamldoc/Search_monad.html
new file mode 100644
index 0000000..501938f
--- /dev/null
+++ b/docs/ocamldoc/Search_monad.html
@@ -0,0 +1,83 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Search_monad
+
+
+
+
+
+module Search_monad : sig
.. end
+
+
Search monad that allows to express non-deterministic algorithms
+ in a legible maner, or programs that solve combinatorial problems.
+
+
+
+
+
+type 'a
m
+
+
+
A data type that represent a collection of 'a
+
+
+
+Monadic operations
+val (>>) : 'a m -> ('a -> 'b m ) -> 'b m
+
+val return : 'a -> 'a m
+val (>>|) : 'a m -> 'a m -> 'a m
+
+
non-deterministic choice
+
+
+
+val fail : unit -> 'a m
+
+val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b
+
+
folding through the collection
+
+
+Derived facilities
+val sprint : ('a -> string) -> 'a m -> string
+val count : 'a m -> int
+val choose : 'a m -> 'a option
+val to_list : 'a m -> 'a list
+val sort : ('a -> 'a -> int) -> 'a m -> 'a m
+val is_empty : 'a m -> bool
+val filter : ('a -> bool) -> 'a m -> 'a m
diff --git a/docs/ocamldoc/Theory.Sigma.html b/docs/ocamldoc/Theory.Sigma.html
new file mode 100644
index 0000000..713b0e4
--- /dev/null
+++ b/docs/ocamldoc/Theory.Sigma.html
@@ -0,0 +1,58 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Sigma
+
+
+
+
+
+module Sigma : sig
.. end
+
+
+val add : EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
+
+
add ty n x map
adds the value x
of type ty
with key n
in map
+
+
+
+val empty : EConstr.constr -> EConstr.constr
+
+
empty ty
create an empty map of type ty
+
+
+
+val of_list : EConstr.constr -> EConstr.constr -> (int * EConstr.constr) list -> EConstr.constr
+
+
of_list ty null l
translates an OCaml association list into a Coq one
+
+
+
+val to_fun : EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
+
+
to_fun ty null map
converts a Coq association list into a Coq function (with default value null
)
+
+
+
diff --git a/docs/ocamldoc/Theory.Stubs.html b/docs/ocamldoc/Theory.Stubs.html
new file mode 100644
index 0000000..b716d16
--- /dev/null
+++ b/docs/ocamldoc/Theory.Stubs.html
@@ -0,0 +1,57 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Stubs
+
+
+
+
+
+module Stubs : sig
.. end
+
+
We need to export some Coq stubs out of this module. They are used
+ by the main tactic, see Rewrite
+
+
+
+
+val lift : Coq.lazy_ref
+val lift_proj_equivalence : Coq.lazy_ref
+val lift_transitivity_left : Coq.lazy_ref
+val lift_transitivity_right : Coq.lazy_ref
+val lift_reflexivity : Coq.lazy_ref
+val eval : Coq.lazy_ref
+
+
The evaluation fonction, used to convert a reified coq term to a
+ raw coq term
+
+
+
+val decide_thm : Coq.lazy_ref
+
+
The main lemma of our theory, that is
+ compare (norm u) (norm v) = Eq -> eval u == eval v
+
+
+
+val lift_normalise_thm : Coq.lazy_ref
diff --git a/docs/ocamldoc/Theory.Sym.html b/docs/ocamldoc/Theory.Sym.html
new file mode 100644
index 0000000..eb2f541
--- /dev/null
+++ b/docs/ocamldoc/Theory.Sym.html
@@ -0,0 +1,80 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Sym
+
+
+
+
+
+module Sym : sig
.. end
+
+
Dynamically typed morphisms
+
+
+
+
+type
pack = {
+
+
+
+
+ar : Constr.t
;
+
+
+
+
+
+
+value : Constr.t
;
+
+
+
+
+
+
+morph : Constr.t
;
+
+
+}
+
+
+
+
mimics the Coq record Sym.pack
+
+
+
+
+val typ : Coq.lazy_ref
+val mk_pack : Coq.Relation.t -> pack -> EConstr.constr
+
+
mk_pack rlt (ar,value,morph)
+
+
+
+val null : Coq.Relation.t -> EConstr.constr
+
diff --git a/docs/ocamldoc/Theory.Trans.html b/docs/ocamldoc/Theory.Trans.html
new file mode 100644
index 0000000..165a5ec
--- /dev/null
+++ b/docs/ocamldoc/Theory.Trans.html
@@ -0,0 +1,157 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Trans
+
+
+
+
+
+module Trans : sig
.. end
+
+
Tranlations between Coq and OCaml
+
+
+
+This module provides facilities to interpret a term with
+ arbitrary operators as an instance of an abstract syntax tree
+ Matcher.Terms.t
.
+
+For each Coq application f x_1 ... x_n
, this amounts to
+ deciding whether one of the partial applications f x_1
+ ... x_i
, i<=n
is a proper morphism, whether the partial
+ application with i=n-2
yields an A or AC binary operator, and
+ whether the whole term is the unit for some A or AC operator. We
+ use typeclass resolution to test each of these possibilities.
+
+Note that there are ambiguous terms:
+
+a term like f x y
might yield a unary morphism (f x
) and a
+ binary one (f
); we select the latter one (unless f
is A or
+ AC, in which case we declare it accordingly);
+a term like S O
can be considered as a morphism (S
)
+ applied to a unit for (+)
, or as a unit for ( * )
; we
+ chose to give priority to units, so that the latter
+ interpretation is selected in this case;
+an element might be the unit for several operations
+
+To achieve this reification, one need to record informations
+ about the collected operators (symbols, binary operators,
+ units). We use the following imperative internal data-structure to
+ this end.
+
+type
envs
+
+
+val empty_envs : unit -> envs
Reification: from Coq terms to AST Matcher.Terms.t
t_of_constr goal rlt envs (left,right)
builds the abstract
+ syntax tree of the terms left
and right
. We rely on the goal
+ to perform typeclasses resolutions to find morphisms compatible
+ with the relation rlt
. Doing so, it modifies the reification
+ environment envs
. Moreover, we need to create fresh
+ evars; this is why we give back the goal
, accordingly
+ updated.
+
+val t_of_constr : Environ.env -> Evd.evar_map -> Coq.Relation.t -> envs -> EConstr.constr * EConstr.constr -> Matcher.Terms.t * Matcher.Terms.t * Evd.evar_map
+val add_symbol : Environ.env -> Evd.evar_map -> Coq.Relation.t -> envs -> Constr.t -> Evd.evar_map
+
+
add_symbol
adds a given binary symbol to the environment of
+ known stuff.
+
+
+Reconstruction: from AST back to Coq terms
+The next functions allow one to map OCaml abstract syntax trees
+ to Coq terms. We need two functions to rebuild different kind of
+ terms: first, raw terms, like the one encountered by
+ Theory.Trans.t_of_constr
; second, reified Coq terms, that are required for
+ the reflexive decision procedure.
+
+type
ir
+
+
+val ir_of_envs : Environ.env -> Evd.evar_map -> Coq.Relation.t -> envs -> Evd.evar_map * ir
+val ir_to_units : ir -> Matcher.ext_units
Building raw, natural, terms
+val raw_constr_of_t : ir -> Coq.Relation.t -> EConstr.rel_context -> Matcher.Terms.t -> EConstr.constr
+
+
raw_constr_of_t
rebuilds a term in the raw representation, and
+ reconstruct the named products on top of it. In particular, this
+ allow us to print the context put around the left (or right)
+ hand side of a pattern.
+
+
+Building reified terms The reification environments, as Coq constrs
+
+type
sigmas = {
+
+
+
+
+env_sym : EConstr.constr
;
+
+
+
+
+
+
+env_bin : EConstr.constr
;
+
+
+
+
+
+
+env_units : EConstr.constr
;
+
+
+}
+
+
+
+type
reifier
+
+
+
We need to reify two terms (left and right members of a goal)
+ that share the same reification envirnoment. Therefore, we need
+ to add letins to the proof context in order to ensure some
+ sharing in the proof terms we produce.
+
+
Moreover, in order to have as much sharing as possible, we also
+ add letins for various partial applications that are used
+ throughout the terms.
+
+
To achieve this, we decompose the reconstruction function into
+ two steps: first, we build the reification environment and then
+ reify each term successively.
+
+
+
+
+val mk_reifier : Coq.Relation.t -> EConstr.constr -> ir -> (sigmas * reifier ) Proofview.tactic
+val reif_constr_of_t : reifier -> Matcher.Terms.t -> EConstr.constr
+
+
reif_constr_of_t reifier t
rebuilds the term t
in the
+ reified form.
+
+
+
diff --git a/docs/ocamldoc/Theory.html b/docs/ocamldoc/Theory.html
new file mode 100644
index 0000000..3f3761c
--- /dev/null
+++ b/docs/ocamldoc/Theory.html
@@ -0,0 +1,78 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory
+
+
+
+
+
+module Theory : sig
.. end
+
+
Bindings for Coq constants that are specific to the plugin;
+ reification and translation functions.
+
+
Note: this module is highly correlated with the definitions of AAC_rewrite.v .
+
+
This module interfaces with the above Coq module; it provides
+ facilities to interpret a term with arbitrary operators as an
+ abstract syntax tree, and to convert an AST into a Coq term
+ (either using the Coq "raw" terms, as written in the starting
+ goal, or using the reified Coq datatypes we define in AAC_rewrite.v ).
+
+
+
+Both in OCaml and Coq, we represent finite multisets using
+ weighted lists (('a*int) list
), see Matcher.mset
.
+
+mk_mset ty l
constructs a Coq multiset from an OCaml multiset
+ l
of Coq terms of type ty
+
+val mk_mset : EConstr.constr -> (EConstr.constr * int) list -> EConstr.constr
Packaging modules
+module Sigma : sig
.. end
+
+module Sym : sig
.. end
+
Dynamically typed morphisms
+
+
+
+module Stubs : sig
.. end
+
We need to export some Coq stubs out of this module.
+
+
+Building reified terms
+We define a bundle of functions to build reified versions of the
+ terms (those that will be given to the reflexive decision
+ procedure). In particular, each field takes as first argument the
+ index of the symbol rather than the symbol itself.
+
+module Trans : sig
.. end
+
Tranlations between Coq and OCaml
+
+
+
diff --git a/docs/ocamldoc/index.html b/docs/ocamldoc/index.html
new file mode 100644
index 0000000..50d4567
--- /dev/null
+++ b/docs/ocamldoc/index.html
@@ -0,0 +1,74 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq
+
Interface with Coq where we define some handlers for Coq's API,
+ and we import several definitions from Coq's standard library.
+
+
+
+Helper
+
Debugging functions, that can be triggered on a per-file base.
+
+
+
+Search_monad
+
Search monad that allows to express non-deterministic algorithms
+ in a legible maner, or programs that solve combinatorial problems.
+
+
+
+Matcher
+
Standalone module containing the algorithm for matching modulo
+ associativity and associativity and commutativity
+ (AAC).
+
+
+
+Theory
+
Bindings for Coq constants that are specific to the plugin;
+ reification and translation functions.
+
+
+
+Print
+
Pretty printing functions we use for the aac_instances
+ tactic.
+
+
+
+Aac_rewrite
+
aac_rewrite -- rewriting modulo A or AC
+
+
+
+
+
+
diff --git a/docs/ocamldoc/index_attributes.html b/docs/ocamldoc/index_attributes.html
new file mode 100644
index 0000000..4923044
--- /dev/null
+++ b/docs/ocamldoc/index_attributes.html
@@ -0,0 +1,26 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of class attributes
+
+
+
+Index of class attributes
+
+
+
diff --git a/docs/ocamldoc/index_class_types.html b/docs/ocamldoc/index_class_types.html
new file mode 100644
index 0000000..b6c33cb
--- /dev/null
+++ b/docs/ocamldoc/index_class_types.html
@@ -0,0 +1,26 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of class types
+
+
+
+Index of class types
+
+
+
diff --git a/docs/ocamldoc/index_classes.html b/docs/ocamldoc/index_classes.html
new file mode 100644
index 0000000..8666e16
--- /dev/null
+++ b/docs/ocamldoc/index_classes.html
@@ -0,0 +1,26 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of classes
+
+
+
+Index of classes
+
+
+
diff --git a/docs/ocamldoc/index_exceptions.html b/docs/ocamldoc/index_exceptions.html
new file mode 100644
index 0000000..3852218
--- /dev/null
+++ b/docs/ocamldoc/index_exceptions.html
@@ -0,0 +1,26 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of exceptions
+
+
+
+Index of exceptions
+
+
+
diff --git a/docs/ocamldoc/index_extensions.html b/docs/ocamldoc/index_extensions.html
new file mode 100644
index 0000000..03ada85
--- /dev/null
+++ b/docs/ocamldoc/index_extensions.html
@@ -0,0 +1,26 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of extensions
+
+
+
+Index of extensions
+
+
+
diff --git a/docs/ocamldoc/index_methods.html b/docs/ocamldoc/index_methods.html
new file mode 100644
index 0000000..21014d9
--- /dev/null
+++ b/docs/ocamldoc/index_methods.html
@@ -0,0 +1,26 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of class methods
+
+
+
+Index of class methods
+
+
+
diff --git a/docs/ocamldoc/index_module_types.html b/docs/ocamldoc/index_module_types.html
new file mode 100644
index 0000000..f62a16b
--- /dev/null
+++ b/docs/ocamldoc/index_module_types.html
@@ -0,0 +1,29 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of module types
+
+
+
+Index of module types
+
+
+
diff --git a/docs/ocamldoc/index_modules.html b/docs/ocamldoc/index_modules.html
new file mode 100644
index 0000000..4c3f3e5
--- /dev/null
+++ b/docs/ocamldoc/index_modules.html
@@ -0,0 +1,163 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of modules
+
+
+
+Index of modules
+
+A
+Aac_rewrite
+
+
aac_rewrite -- rewriting modulo A or AC
+
+
+
+C
+Classes [Coq ]
+
+
+Coq
+
+
Interface with Coq where we define some handlers for Coq's API,
+ and we import several definitions from Coq's standard library.
+
+
+
+D
+Debug [Helper ]
+
+E
+Equivalence [Coq ]
+
+H
+Helper
+
+
Debugging functions, that can be triggered on a per-file base.
+
+
+
+L
+List [Coq ]
+
+
+M
+Matcher
+
+
Standalone module containing the algorithm for matching modulo
+ associativity and associativity and commutativity
+ (AAC).
+
+
+
+N
+Nat [Coq ]
+
+
Coq unary numbers (peano)
+
+
+
+O
+Option [Coq ]
+
+P
+Pair [Coq ]
+
+
+Pos [Coq ]
+
+
Coq positive numbers (pos)
+
+
+
+Print
+
+
Pretty printing functions we use for the aac_instances
+ tactic.
+
+
+
+R
+Relation [Coq ]
+
+Rewrite [Coq ]
+
+S
+Search_monad
+
+
Search monad that allows to express non-deterministic algorithms
+ in a legible maner, or programs that solve combinatorial problems.
+
+
+
+Sigma [Theory ]
+
+
+Stubs [Theory ]
+
+
We need to export some Coq stubs out of this module.
+
+
+
+Subst [Matcher ]
+
+
Substitutions (or environments)
+
+
+
+Sym [Theory ]
+
+
Dynamically typed morphisms
+
+
+
+T
+Terms [Matcher ]
+
+
Representations of expressions
+
+
+
+Theory
+
+
Bindings for Coq constants that are specific to the plugin;
+ reification and translation functions.
+
+
+
+Trans [Theory ]
+
+
Tranlations between Coq and OCaml
+
+
+
+
+
+
diff --git a/docs/ocamldoc/index_types.html b/docs/ocamldoc/index_types.html
new file mode 100644
index 0000000..e994c1b
--- /dev/null
+++ b/docs/ocamldoc/index_types.html
@@ -0,0 +1,102 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of types
+
+
+
+Index of types
+
+
+
diff --git a/docs/ocamldoc/index_values.html b/docs/ocamldoc/index_values.html
new file mode 100644
index 0000000..0403935
--- /dev/null
+++ b/docs/ocamldoc/index_values.html
@@ -0,0 +1,413 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Index of values
+
+
+
+Index of values
+
+
+(>>) [Search_monad ]
+
+
+(>>|) [Search_monad ]
+
+
non-deterministic choice
+
+
+
+A
+aac_normalise [Aac_rewrite ]
+
+aac_reflexivity [Aac_rewrite ]
+
+aac_rewrite [Aac_rewrite ]
+
+add [Aac_rewrite ]
+
+add [Theory.Sigma ]
+
+
add ty n x map
adds the value x
of type ty
with key n
in map
+
+
+
+add_symbol [Theory.Trans ]
+
+
add_symbol
adds a given binary symbol to the environment of
+ known stuff.
+
+
+
+anomaly [Coq ]
+
+B
+build [Coq.Rewrite ]
+
+
build the constr to rewrite, with lambda abstractions
+
+
+
+C
+choose [Search_monad ]
+
+count [Search_monad ]
+
+cps_mk_letin [Coq ]
+
+
cps_mk_letin name v
binds the constr v
using a letin tactic
+
+
+
+cps_resolve_one_typeclass [Coq ]
+
+D
+debug [Helper.CONTROL ]
+
+debug [Helper.Debug ]
+
+
debug
prints the string and end it with a newline
+
+
+
+debug_exception [Helper.Debug ]
+
+decide_thm [Theory.Stubs ]
+
+
The main lemma of our theory, that is
+ compare (norm u) (norm v) = Eq -> eval u == eval v
+
+
+
+decomp_term [Coq ]
+
+E
+empty [Theory.Sigma ]
+
+
empty ty
create an empty map of type ty
+
+
+
+empty_envs [Theory.Trans ]
+
+equal_aac [Matcher.Terms ]
+
+
Test for equality of terms modulo AACU (relies on the following
+ canonical representation of terms).
+
+
+
+eval [Theory.Stubs ]
+
+
The evaluation fonction, used to convert a reified coq term to a
+ raw coq term
+
+
+
+evar_binary [Coq ]
+
+evar_relation [Coq ]
+
+F
+fail [Search_monad ]
+
+
+filter [Search_monad ]
+
+find_global [Coq ]
+
+fold [Search_monad ]
+
+
folding through the collection
+
+
+
+from_relation [Coq.Equivalence ]
+
+G
+get_efresh [Coq ]
+
+get_fresh [Coq ]
+
+get_hypinfo [Coq.Rewrite ]
+
+
get_hypinfo ?check_type H l2r
analyse the hypothesis H, and
+ build the related hypinfo.
+
+
+
+I
+infer [Coq.Equivalence ]
+
+instantiate [Matcher.Subst ]
+
+ir_of_envs [Theory.Trans ]
+
+ir_to_units [Theory.Trans ]
+
+is_empty [Search_monad ]
+
+L
+lift [Theory.Stubs ]
+
+lift_normalise_thm [Theory.Stubs ]
+
+lift_proj_equivalence [Theory.Stubs ]
+
+lift_reflexivity [Theory.Stubs ]
+
+lift_transitivity_left [Theory.Stubs ]
+
+lift_transitivity_right [Theory.Stubs ]
+
+linear [Matcher ]
+
+
linear
expands a multiset into a simple list
+
+
+
+M
+make [Coq.Equivalence ]
+
+make [Coq.Relation ]
+
+match_as_equation [Coq ]
+
+
match_as_equation ?context env sigma c
try to decompose c as a
+ relation applied to two terms.
+
+
+
+matcher [Matcher ]
+
+
matcher p t
computes the set of solutions to the given top-level
+ matching problem (p
is the pattern, t
is the term).
+
+
+
+mk_equivalence [Coq.Classes ]
+
+mk_letin [Coq ]
+
+mk_morphism [Coq.Classes ]
+
+mk_mset [Theory ]
+
+mk_pack [Theory.Sym ]
+
+
mk_pack rlt (ar,value,morph)
+
+
+
+mk_reflexive [Coq.Classes ]
+
+mk_reifier [Theory.Trans ]
+
+mk_transitive [Coq.Classes ]
+
+N
+nf_equal [Matcher.Terms ]
+
+nf_term_compare [Matcher.Terms ]
+
+none [Coq.Option ]
+
+null [Theory.Sym ]
+
+
+O
+of_int [Coq.Nat ]
+
+of_int [Coq.Pos ]
+
+of_list [Theory.Sigma ]
+
+
of_list ty null l
translates an OCaml association list into a Coq one
+
+
+
+of_list [Coq.List ]
+
+
+of_option [Coq.Option ]
+
+of_pair [Coq.Pair ]
+
+P
+pair [Coq.Pair ]
+
+pr_aac_args [Aac_rewrite ]
+
+pr_constr [Helper.Debug ]
+
+
pr_constr
print a Coq constructor, that can be labelled
+ by a string
+
+
+
+print [Print ]
+
+
The main printing function.
+
+
+
+printing [Helper.CONTROL ]
+
+R
+raw_constr_of_t [Theory.Trans ]
+
+
raw_constr_of_t
rebuilds a term in the raw representation, and
+ reconstruct the named products on top of it.
+
+
+
+reif_constr_of_t [Theory.Trans ]
+
+
reif_constr_of_t reifier t
rebuilds the term t
in the
+ reified form.
+
+
+
+return [Search_monad ]
+
+retype [Coq ]
+
+rewrite [Coq.Rewrite ]
+
+
rewrite ?abort hypinfo subst
builds the rewriting tactic
+ associated with the given subst
and hypinfo
.
+
+
+
+S
+show_proof [Coq ]
+
+
print the current proof term
+
+
+
+some [Coq.Option ]
+
+sort [Search_monad ]
+
+split [Coq.Equivalence ]
+
+split [Coq.Relation ]
+
+sprint [Matcher.Subst ]
+
+sprint [Search_monad ]
+
+sprint_nf_term [Matcher.Terms ]
+
+subterm [Matcher ]
+
+
subterm p t
computes a set of solutions to the given
+ subterm-matching problem.
+
+
+
+T
+t_of_constr [Theory.Trans ]
+
+t_of_term [Matcher.Terms ]
+
+tclDEBUG [Coq ]
+
+
emit debug messages to see which tactics are failing
+
+
+
+tclPRINT [Coq ]
+
+
print the current goal
+
+
+
+tclRETYPE [Coq ]
+
+tclTIME [Coq ]
+
+
time the execution of a tactic
+
+
+
+term_of_t [Matcher.Terms ]
+
+
we have the following property: a
and b
are equal modulo AACU
+ iif nf_equal (term_of_t a) (term_of_t b) = true
+
+
+
+time [Helper.CONTROL ]
+
+time [Helper.Debug ]
+
+
time
computes the time spent in a function, and then
+ print it using the given format
+
+
+
+to_fun [Theory.Sigma ]
+
+
to_fun ty null map
converts a Coq association list into a Coq function (with default value null
)
+
+
+
+to_list [Matcher.Subst ]
+
+to_list [Search_monad ]
+
+to_relation [Coq.Equivalence ]
+
+typ [Theory.Sym ]
+
+typ [Coq.Nat ]
+
+typ [Coq.Pos ]
+
+typ [Coq.Option ]
+
+typ [Coq.Pair ]
+
+type_of_list [Coq.List ]
+
+
+U
+user_error [Coq ]
+
+W
+warning [Coq ]
+
+
+
+
diff --git a/docs/ocamldoc/style.css b/docs/ocamldoc/style.css
new file mode 100644
index 0000000..259bd49
--- /dev/null
+++ b/docs/ocamldoc/style.css
@@ -0,0 +1,43 @@
+.keyword { font-weight : bold ; color : Red }
+.keywordsign { color : #C04600 }
+.comment { color : Green }
+.constructor { color : Blue }
+.type { color : #5C6585 }
+.string { color : Maroon }
+.warning { color : Red ; font-weight : bold }
+.info { margin-left : 3em; margin-right: 3em }
+.param_info { margin-top: 4px; margin-left : 3em; margin-right : 3em }
+.code { color : #465F91 ; }
+.typetable { border-style : hidden }
+.paramstable { border-style : hidden ; padding: 5pt 5pt}
+tr { background-color : White }
+td.typefieldcomment { background-color : #FFFFFF ; font-size: smaller ;}
+div.sig_block {margin-left: 2em}
+*:target { background: yellow; }
+body {font: 13px sans-serif; color: black; text-align: left; padding: 5px; margin: 0}
+h1 { font-size : 20pt ; text-align: center; }
+h2 { font-size : 20pt ; text-align: center; }
+h3 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ;padding: 2px; }
+h4 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ;padding: 2px; }
+h5 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90EDFF ;padding: 2px; }
+h6 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90FDFF ;padding: 2px; }
+div.h7 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ; padding: 2px; }
+div.h8 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #E0FFFF ; padding: 2px; }
+div.h9 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #F0FFFF ; padding: 2px; }
+div.h10 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #FFFFFF ; padding: 2px; }
+a {color: #416DFF; text-decoration: none}
+a:hover {background-color: #ddd; text-decoration: underline}
+pre { margin-bottom: 4px; font-family: monospace; }
+pre.verbatim, pre.codepre { }
+.indextable {border: 1px #ddd solid; border-collapse: collapse}
+.indextable td, .indextable th {border: 1px #ddd solid; min-width: 80px}
+.indextable td.module {background-color: #eee ; padding-left: 2px; padding-right: 2px}
+.indextable td.module a {color: #4E6272; text-decoration: none; display: block; width: 100%}
+.indextable td.module a:hover {text-decoration: underline; background-color: transparent}
+.deprecated {color: #888; font-style: italic}
+.indextable tr td div.info { margin-left: 2px; margin-right: 2px }
+ul.indexlist { margin-left: 0; padding-left: 0;}
+ul.indexlist li { list-style-type: none ; margin-left: 0; padding-left: 0; }
+ul.info-attributes {list-style: none; margin: 0; padding: 0; }
+div.info > p:first-child { margin-top:0; }
+div.info-desc > p:first-child { margin-top:0; margin-bottom:0; }
\ No newline at end of file
diff --git a/docs/ocamldoc/type_Aac_rewrite.html b/docs/ocamldoc/type_Aac_rewrite.html
new file mode 100644
index 0000000..8f159a5
--- /dev/null
+++ b/docs/ocamldoc/type_Aac_rewrite.html
@@ -0,0 +1,31 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Aac_rewrite
+
+
+sig
+ val aac_reflexivity : unit Proofview .tactic
+ val aac_normalise : unit Proofview .tactic
+ val aac_rewrite :
+ args:(string * int) list ->
+ ?abort:bool ->
+ ?l2r:bool ->
+ ?show:bool ->
+ ?strict:bool ->
+ ?extra:EConstr .t -> EConstr .constr -> unit Proofview .tactic
+ val add : string -> ' a -> (string * ' a) list -> (string * ' a) list
+ val pr_aac_args : ' a -> ' b -> ' c -> (string * int) list -> Pp .t
+end
diff --git a/docs/ocamldoc/type_Coq.Classes.html b/docs/ocamldoc/type_Coq.Classes.html
new file mode 100644
index 0000000..b2c6c05
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Classes.html
@@ -0,0 +1,25 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Classes
+
+
+sig
+ val mk_morphism :
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> EConstr .constr
+ val mk_equivalence : EConstr .constr -> EConstr .constr -> EConstr .constr
+ val mk_reflexive : EConstr .constr -> EConstr .constr -> EConstr .constr
+ val mk_transitive : EConstr .constr -> EConstr .constr -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Coq.Equivalence.html b/docs/ocamldoc/type_Coq.Equivalence.html
new file mode 100644
index 0000000..1bcdda9
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Equivalence.html
@@ -0,0 +1,37 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Equivalence
+
+
+sig
+ type t = {
+ carrier : EConstr .constr;
+ eq : EConstr .constr;
+ equivalence : EConstr .constr;
+ }
+ val make :
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> Coq .Equivalence .t
+ val infer :
+ Environ .env ->
+ Evd .evar_map ->
+ EConstr .constr -> EConstr .constr -> Coq .Equivalence .t * Evd .evar_map
+ val from_relation :
+ Environ .env ->
+ Evd .evar_map -> Coq .Relation .t -> Coq .Equivalence .t * Evd .evar_map
+ val to_relation : Coq .Equivalence .t -> Coq .Relation .t
+ val split :
+ Coq .Equivalence .t -> EConstr .constr * EConstr .constr * EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Coq.List.html b/docs/ocamldoc/type_Coq.List.html
new file mode 100644
index 0000000..2e913af
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.List.html
@@ -0,0 +1,22 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.List
+
+
+sig
+ val of_list : EConstr .constr -> EConstr .constr list -> EConstr .constr
+ val type_of_list : EConstr .constr -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Coq.Nat.html b/docs/ocamldoc/type_Coq.Nat.html
new file mode 100644
index 0000000..243ed36
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Nat.html
@@ -0,0 +1,19 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Nat
+
+
+sig val typ : Coq .lazy_ref val of_int : int -> Constr .constr end
diff --git a/docs/ocamldoc/type_Coq.Option.html b/docs/ocamldoc/type_Coq.Option.html
new file mode 100644
index 0000000..ca10254
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Option.html
@@ -0,0 +1,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Option
+
+
+sig
+ val typ : Coq .lazy_ref
+ val some : EConstr .constr -> EConstr .constr -> EConstr .constr
+ val none : EConstr .constr -> EConstr .constr
+ val of_option : EConstr .constr -> EConstr .constr option -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Coq.Pair.html b/docs/ocamldoc/type_Coq.Pair.html
new file mode 100644
index 0000000..c2f8f74
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Pair.html
@@ -0,0 +1,25 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Pair
+
+
+sig
+ val typ : Coq .lazy_ref
+ val pair : Coq .lazy_ref
+ val of_pair :
+ EConstr .constr ->
+ EConstr .constr -> EConstr .constr * EConstr .constr -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Coq.Pos.html b/docs/ocamldoc/type_Coq.Pos.html
new file mode 100644
index 0000000..ea67180
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Pos.html
@@ -0,0 +1,19 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Pos
+
+
+sig val typ : Coq .lazy_ref val of_int : int -> EConstr .constr end
diff --git a/docs/ocamldoc/type_Coq.Relation.html b/docs/ocamldoc/type_Coq.Relation.html
new file mode 100644
index 0000000..dd2db05
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Relation.html
@@ -0,0 +1,23 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Relation
+
+
+sig
+ type t = { carrier : EConstr .constr; r : EConstr .constr; }
+ val make : EConstr .constr -> EConstr .constr -> Coq .Relation .t
+ val split : Coq .Relation .t -> EConstr .constr * EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Coq.Rewrite.html b/docs/ocamldoc/type_Coq.Rewrite.html
new file mode 100644
index 0000000..a414198
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.Rewrite.html
@@ -0,0 +1,41 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq.Rewrite
+
+
+sig
+ type hypinfo = {
+ hyp : EConstr .constr;
+ hyptype : EConstr .constr;
+ context : EConstr .rel_context;
+ body : EConstr .constr;
+ rel : Coq .Relation .t;
+ left : EConstr .constr;
+ right : EConstr .constr;
+ l2r : bool;
+ }
+ val get_hypinfo :
+ Environ .env ->
+ Evd .evar_map ->
+ ?check_type:(EConstr .types -> bool) ->
+ EConstr .constr -> l2r:bool -> Coq .Rewrite .hypinfo
+ val build :
+ Coq .Rewrite .hypinfo -> (int * EConstr .constr) list -> EConstr .constr
+ val rewrite :
+ ?abort:bool ->
+ Coq .Rewrite .hypinfo ->
+ (int * EConstr .constr) list -> unit Proofview .tactic
+end
diff --git a/docs/ocamldoc/type_Coq.html b/docs/ocamldoc/type_Coq.html
new file mode 100644
index 0000000..0837aea
--- /dev/null
+++ b/docs/ocamldoc/type_Coq.html
@@ -0,0 +1,141 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Coq
+
+
+sig
+ type tactic = unit Proofview .tactic
+ type lazy_ref = Names .GlobRef .t Stdlib .Lazy .t
+ val get_fresh : Coq .lazy_ref -> Constr .constr
+ val get_efresh : Coq .lazy_ref -> EConstr .constr
+ val find_global : string -> Coq .lazy_ref
+ val cps_resolve_one_typeclass :
+ ?error:Pp .t ->
+ EConstr .types -> (EConstr .constr -> Coq .tactic) -> Coq .tactic
+ val evar_binary :
+ Environ .env ->
+ Evd .evar_map -> EConstr .constr -> Evd .evar_map * EConstr .constr
+ val evar_relation :
+ Environ .env ->
+ Evd .evar_map -> EConstr .constr -> Evd .evar_map * EConstr .constr
+ val cps_mk_letin :
+ string -> EConstr .constr -> (EConstr .constr -> Coq .tactic) -> Coq .tactic
+ val mk_letin : string -> EConstr .constr -> EConstr .constr Proofview .tactic
+ val retype : EConstr .constr -> Coq .tactic
+ val tclRETYPE : EConstr .constr -> unit Proofview .tactic
+ val decomp_term :
+ Evd .evar_map ->
+ EConstr .constr ->
+ (EConstr .constr, EConstr .types, EConstr .ESorts .t, EConstr .EInstance .t)
+ Constr .kind_of_term
+ module List :
+ sig
+ val of_list : EConstr .constr -> EConstr .constr list -> EConstr .constr
+ val type_of_list : EConstr .constr -> EConstr .constr
+ end
+ module Pair :
+ sig
+ val typ : Coq .lazy_ref
+ val pair : Coq .lazy_ref
+ val of_pair :
+ EConstr .constr ->
+ EConstr .constr -> EConstr .constr * EConstr .constr -> EConstr .constr
+ end
+ module Option :
+ sig
+ val typ : Coq .lazy_ref
+ val some : EConstr .constr -> EConstr .constr -> EConstr .constr
+ val none : EConstr .constr -> EConstr .constr
+ val of_option :
+ EConstr .constr -> EConstr .constr option -> EConstr .constr
+ end
+ module Pos :
+ sig val typ : Coq .lazy_ref val of_int : int -> EConstr .constr end
+ module Nat :
+ sig val typ : Coq .lazy_ref val of_int : int -> Constr .constr end
+ module Classes :
+ sig
+ val mk_morphism :
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> EConstr .constr
+ val mk_equivalence : EConstr .constr -> EConstr .constr -> EConstr .constr
+ val mk_reflexive : EConstr .constr -> EConstr .constr -> EConstr .constr
+ val mk_transitive : EConstr .constr -> EConstr .constr -> EConstr .constr
+ end
+ module Relation :
+ sig
+ type t = { carrier : EConstr .constr; r : EConstr .constr; }
+ val make : EConstr .constr -> EConstr .constr -> Coq .Relation .t
+ val split : Coq .Relation .t -> EConstr .constr * EConstr .constr
+ end
+ module Equivalence :
+ sig
+ type t = {
+ carrier : EConstr .constr;
+ eq : EConstr .constr;
+ equivalence : EConstr .constr;
+ }
+ val make :
+ EConstr .constr ->
+ EConstr .constr -> EConstr .constr -> Coq .Equivalence .t
+ val infer :
+ Environ .env ->
+ Evd .evar_map ->
+ EConstr .constr -> EConstr .constr -> Coq .Equivalence .t * Evd .evar_map
+ val from_relation :
+ Environ .env ->
+ Evd .evar_map -> Coq .Relation .t -> Coq .Equivalence .t * Evd .evar_map
+ val to_relation : Coq .Equivalence .t -> Coq .Relation .t
+ val split :
+ Coq .Equivalence .t -> EConstr .constr * EConstr .constr * EConstr .constr
+ end
+ val match_as_equation :
+ ?context:EConstr .rel_context ->
+ Environ .env ->
+ Evd .evar_map ->
+ EConstr .constr ->
+ (EConstr .constr * EConstr .constr * Coq .Relation .t) option
+ val tclTIME : string -> Coq .tactic -> Coq .tactic
+ val tclDEBUG : string -> unit Proofview .tactic
+ val tclPRINT : unit Proofview .tactic
+ val anomaly : string -> ' a
+ val user_error : Pp .t -> ' a
+ val warning : string -> unit
+ val show_proof : Declare .Proof .t -> unit
+ module Rewrite :
+ sig
+ type hypinfo = {
+ hyp : EConstr .constr;
+ hyptype : EConstr .constr;
+ context : EConstr .rel_context;
+ body : EConstr .constr;
+ rel : Coq .Relation .t;
+ left : EConstr .constr;
+ right : EConstr .constr;
+ l2r : bool;
+ }
+ val get_hypinfo :
+ Environ .env ->
+ Evd .evar_map ->
+ ?check_type:(EConstr .types -> bool) ->
+ EConstr .constr -> l2r:bool -> Coq .Rewrite .hypinfo
+ val build :
+ Coq .Rewrite .hypinfo -> (int * EConstr .constr) list -> EConstr .constr
+ val rewrite :
+ ?abort:bool ->
+ Coq .Rewrite .hypinfo ->
+ (int * EConstr .constr) list -> unit Proofview .tactic
+ end
+end
diff --git a/docs/ocamldoc/type_Helper.CONTROL.html b/docs/ocamldoc/type_Helper.CONTROL.html
new file mode 100644
index 0000000..0bf847c
--- /dev/null
+++ b/docs/ocamldoc/type_Helper.CONTROL.html
@@ -0,0 +1,19 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Helper.CONTROL
+
+
+sig val debug : bool val time : bool val printing : bool end
diff --git a/docs/ocamldoc/type_Helper.Debug.html b/docs/ocamldoc/type_Helper.Debug.html
new file mode 100644
index 0000000..2520d76
--- /dev/null
+++ b/docs/ocamldoc/type_Helper.Debug.html
@@ -0,0 +1,28 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Helper.Debug
+
+
+functor (X : CONTROL ) ->
+ sig
+ val debug : string -> unit
+ val debug_exception : string -> exn -> unit
+ val time :
+ (' a -> ' b) ->
+ ' a -> (float -> unit, Stdlib .out_channel, unit) Stdlib .format -> ' b
+ val pr_constr :
+ Environ .env -> Evd .evar_map -> string -> EConstr .constr -> unit
+ end
diff --git a/docs/ocamldoc/type_Helper.html b/docs/ocamldoc/type_Helper.html
new file mode 100644
index 0000000..c9485f3
--- /dev/null
+++ b/docs/ocamldoc/type_Helper.html
@@ -0,0 +1,33 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Helper
+
+
+sig
+ module type CONTROL =
+ sig val debug : bool val time : bool val printing : bool end
+ module Debug :
+ functor (X : CONTROL ) ->
+ sig
+ val debug : string -> unit
+ val debug_exception : string -> exn -> unit
+ val time :
+ (' a -> ' b) ->
+ ' a -> (float -> unit, Stdlib .out_channel, unit) Stdlib .format -> ' b
+ val pr_constr :
+ Environ .env -> Evd .evar_map -> string -> EConstr .constr -> unit
+ end
+end
diff --git a/docs/ocamldoc/type_Matcher.Subst.html b/docs/ocamldoc/type_Matcher.Subst.html
new file mode 100644
index 0000000..afbf434
--- /dev/null
+++ b/docs/ocamldoc/type_Matcher.Subst.html
@@ -0,0 +1,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Matcher.Subst
+
+
+sig
+ type t
+ val sprint : Matcher .Subst .t -> string
+ val instantiate : Matcher .Subst .t -> Matcher .Terms .t -> Matcher .Terms .t
+ val to_list : Matcher .Subst .t -> (Matcher .var * Matcher .Terms .t) list
+end
diff --git a/docs/ocamldoc/type_Matcher.Terms.html b/docs/ocamldoc/type_Matcher.Terms.html
new file mode 100644
index 0000000..21628c1
--- /dev/null
+++ b/docs/ocamldoc/type_Matcher.Terms.html
@@ -0,0 +1,33 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Matcher.Terms
+
+
+sig
+ type t =
+ Dot of (Matcher .symbol * Matcher .Terms .t * Matcher .Terms .t)
+ | Plus of (Matcher .symbol * Matcher .Terms .t * Matcher .Terms .t)
+ | Sym of (Matcher .symbol * Matcher .Terms .t array)
+ | Var of Matcher .var
+ | Unit of Matcher .symbol
+ val equal_aac : Matcher .units -> Matcher .Terms .t -> Matcher .Terms .t -> bool
+ type nf_term
+ val nf_term_compare : Matcher .Terms .nf_term -> Matcher .Terms .nf_term -> int
+ val nf_equal : Matcher .Terms .nf_term -> Matcher .Terms .nf_term -> bool
+ val sprint_nf_term : Matcher .Terms .nf_term -> string
+ val term_of_t : Matcher .units -> Matcher .Terms .t -> Matcher .Terms .nf_term
+ val t_of_term : Matcher .Terms .nf_term -> Matcher .Terms .t
+end
diff --git a/docs/ocamldoc/type_Matcher.html b/docs/ocamldoc/type_Matcher.html
new file mode 100644
index 0000000..22bcc7b
--- /dev/null
+++ b/docs/ocamldoc/type_Matcher.html
@@ -0,0 +1,65 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Matcher
+
+
+sig
+ type symbol = int
+ type var = int
+ type units = (Matcher .symbol * Matcher .symbol) list
+ type ext_units = {
+ unit_for : Matcher .units;
+ is_ac : (Matcher .symbol * bool) list;
+ }
+ type ' a mset = (' a * int) list
+ val linear : ' a Matcher .mset -> ' a list
+ module Terms :
+ sig
+ type t =
+ Dot of (Matcher .symbol * Matcher .Terms .t * Matcher .Terms .t)
+ | Plus of (Matcher .symbol * Matcher .Terms .t * Matcher .Terms .t)
+ | Sym of (Matcher .symbol * Matcher .Terms .t array)
+ | Var of Matcher .var
+ | Unit of Matcher .symbol
+ val equal_aac :
+ Matcher .units -> Matcher .Terms .t -> Matcher .Terms .t -> bool
+ type nf_term
+ val nf_term_compare :
+ Matcher .Terms .nf_term -> Matcher .Terms .nf_term -> int
+ val nf_equal : Matcher .Terms .nf_term -> Matcher .Terms .nf_term -> bool
+ val sprint_nf_term : Matcher .Terms .nf_term -> string
+ val term_of_t :
+ Matcher .units -> Matcher .Terms .t -> Matcher .Terms .nf_term
+ val t_of_term : Matcher .Terms .nf_term -> Matcher .Terms .t
+ end
+ module Subst :
+ sig
+ type t
+ val sprint : Matcher .Subst .t -> string
+ val instantiate : Matcher .Subst .t -> Matcher .Terms .t -> Matcher .Terms .t
+ val to_list : Matcher .Subst .t -> (Matcher .var * Matcher .Terms .t) list
+ end
+ val matcher :
+ ?strict:bool ->
+ Matcher .ext_units ->
+ Matcher .Terms .t -> Matcher .Terms .t -> Matcher .Subst .t Search_monad .m
+ val subterm :
+ ?strict:bool ->
+ Matcher .ext_units ->
+ Matcher .Terms .t ->
+ Matcher .Terms .t ->
+ (int * Matcher .Terms .t * Matcher .Subst .t Search_monad .m) Search_monad .m
+end
diff --git a/docs/ocamldoc/type_Print.html b/docs/ocamldoc/type_Print.html
new file mode 100644
index 0000000..263e5e7
--- /dev/null
+++ b/docs/ocamldoc/type_Print.html
@@ -0,0 +1,25 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Print
+
+
+sig
+ val print :
+ Coq .Relation .t ->
+ Theory .Trans .ir ->
+ (int * Matcher .Terms .t * Matcher .Subst .t Search_monad .m) Search_monad .m ->
+ EConstr .rel_context -> unit Proofview .tactic
+end
diff --git a/docs/ocamldoc/type_Search_monad.html b/docs/ocamldoc/type_Search_monad.html
new file mode 100644
index 0000000..ea09c0e
--- /dev/null
+++ b/docs/ocamldoc/type_Search_monad.html
@@ -0,0 +1,34 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Search_monad
+
+
+sig
+ type ' a m
+ val ( >> ) :
+ ' a Search_monad .m -> (' a -> ' b Search_monad .m) -> ' b Search_monad .m
+ val return : ' a -> ' a Search_monad .m
+ val ( >>| ) : ' a Search_monad .m -> ' a Search_monad .m -> ' a Search_monad .m
+ val fail : unit -> ' a Search_monad .m
+ val fold : (' a -> ' b -> ' b) -> ' a Search_monad .m -> ' b -> ' b
+ val sprint : (' a -> string) -> ' a Search_monad .m -> string
+ val count : ' a Search_monad .m -> int
+ val choose : ' a Search_monad .m -> ' a option
+ val to_list : ' a Search_monad .m -> ' a list
+ val sort : (' a -> ' a -> int) -> ' a Search_monad .m -> ' a Search_monad .m
+ val is_empty : ' a Search_monad .m -> bool
+ val filter : (' a -> bool) -> ' a Search_monad .m -> ' a Search_monad .m
+end
diff --git a/docs/ocamldoc/type_Theory.Sigma.html b/docs/ocamldoc/type_Theory.Sigma.html
new file mode 100644
index 0000000..f30c143
--- /dev/null
+++ b/docs/ocamldoc/type_Theory.Sigma.html
@@ -0,0 +1,29 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Sigma
+
+
+sig
+ val add :
+ EConstr .constr ->
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> EConstr .constr
+ val empty : EConstr .constr -> EConstr .constr
+ val of_list :
+ EConstr .constr ->
+ EConstr .constr -> (int * EConstr .constr) list -> EConstr .constr
+ val to_fun :
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Theory.Stubs.html b/docs/ocamldoc/type_Theory.Stubs.html
new file mode 100644
index 0000000..0fbf9c5
--- /dev/null
+++ b/docs/ocamldoc/type_Theory.Stubs.html
@@ -0,0 +1,28 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Stubs
+
+
+sig
+ val lift : Coq .lazy_ref
+ val lift_proj_equivalence : Coq .lazy_ref
+ val lift_transitivity_left : Coq .lazy_ref
+ val lift_transitivity_right : Coq .lazy_ref
+ val lift_reflexivity : Coq .lazy_ref
+ val eval : Coq .lazy_ref
+ val decide_thm : Coq .lazy_ref
+ val lift_normalise_thm : Coq .lazy_ref
+end
diff --git a/docs/ocamldoc/type_Theory.Sym.html b/docs/ocamldoc/type_Theory.Sym.html
new file mode 100644
index 0000000..e20ca16
--- /dev/null
+++ b/docs/ocamldoc/type_Theory.Sym.html
@@ -0,0 +1,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Sym
+
+
+sig
+ type pack = { ar : Constr .t; value : Constr .t; morph : Constr .t; }
+ val typ : Coq .lazy_ref
+ val mk_pack : Coq .Relation .t -> Theory .Sym .pack -> EConstr .constr
+ val null : Coq .Relation .t -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Theory.Trans.html b/docs/ocamldoc/type_Theory.Trans.html
new file mode 100644
index 0000000..cd10c81
--- /dev/null
+++ b/docs/ocamldoc/type_Theory.Trans.html
@@ -0,0 +1,56 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory.Trans
+
+
+sig
+ type envs
+ val empty_envs : unit -> Theory .Trans .envs
+ val t_of_constr :
+ Environ .env ->
+ Evd .evar_map ->
+ Coq .Relation .t ->
+ Theory .Trans .envs ->
+ EConstr .constr * EConstr .constr ->
+ Matcher .Terms .t * Matcher .Terms .t * Evd .evar_map
+ val add_symbol :
+ Environ .env ->
+ Evd .evar_map ->
+ Coq .Relation .t -> Theory .Trans .envs -> Constr .t -> Evd .evar_map
+ type ir
+ val ir_of_envs :
+ Environ .env ->
+ Evd .evar_map ->
+ Coq .Relation .t -> Theory .Trans .envs -> Evd .evar_map * Theory .Trans .ir
+ val ir_to_units : Theory .Trans .ir -> Matcher .ext_units
+ val raw_constr_of_t :
+ Theory .Trans .ir ->
+ Coq .Relation .t ->
+ EConstr .rel_context -> Matcher .Terms .t -> EConstr .constr
+ type sigmas = {
+ env_sym : EConstr .constr;
+ env_bin : EConstr .constr;
+ env_units : EConstr .constr;
+ }
+ type reifier
+ val mk_reifier :
+ Coq .Relation .t ->
+ EConstr .constr ->
+ Theory .Trans .ir ->
+ (Theory .Trans .sigmas * Theory .Trans .reifier) Proofview .tactic
+ val reif_constr_of_t :
+ Theory .Trans .reifier -> Matcher .Terms .t -> EConstr .constr
+end
diff --git a/docs/ocamldoc/type_Theory.html b/docs/ocamldoc/type_Theory.html
new file mode 100644
index 0000000..7bf9ff1
--- /dev/null
+++ b/docs/ocamldoc/type_Theory.html
@@ -0,0 +1,91 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Theory
+
+
+sig
+ val mk_mset :
+ EConstr .constr -> (EConstr .constr * int) list -> EConstr .constr
+ module Sigma :
+ sig
+ val add :
+ EConstr .constr ->
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> EConstr .constr
+ val empty : EConstr .constr -> EConstr .constr
+ val of_list :
+ EConstr .constr ->
+ EConstr .constr -> (int * EConstr .constr) list -> EConstr .constr
+ val to_fun :
+ EConstr .constr -> EConstr .constr -> EConstr .constr -> EConstr .constr
+ end
+ module Sym :
+ sig
+ type pack = { ar : Constr .t; value : Constr .t; morph : Constr .t; }
+ val typ : Coq .lazy_ref
+ val mk_pack : Coq .Relation .t -> Theory .Sym .pack -> EConstr .constr
+ val null : Coq .Relation .t -> EConstr .constr
+ end
+ module Stubs :
+ sig
+ val lift : Coq .lazy_ref
+ val lift_proj_equivalence : Coq .lazy_ref
+ val lift_transitivity_left : Coq .lazy_ref
+ val lift_transitivity_right : Coq .lazy_ref
+ val lift_reflexivity : Coq .lazy_ref
+ val eval : Coq .lazy_ref
+ val decide_thm : Coq .lazy_ref
+ val lift_normalise_thm : Coq .lazy_ref
+ end
+ module Trans :
+ sig
+ type envs
+ val empty_envs : unit -> Theory .Trans .envs
+ val t_of_constr :
+ Environ .env ->
+ Evd .evar_map ->
+ Coq .Relation .t ->
+ Theory .Trans .envs ->
+ EConstr .constr * EConstr .constr ->
+ Matcher .Terms .t * Matcher .Terms .t * Evd .evar_map
+ val add_symbol :
+ Environ .env ->
+ Evd .evar_map ->
+ Coq .Relation .t -> Theory .Trans .envs -> Constr .t -> Evd .evar_map
+ type ir
+ val ir_of_envs :
+ Environ .env ->
+ Evd .evar_map ->
+ Coq .Relation .t -> Theory .Trans .envs -> Evd .evar_map * Theory .Trans .ir
+ val ir_to_units : Theory .Trans .ir -> Matcher .ext_units
+ val raw_constr_of_t :
+ Theory .Trans .ir ->
+ Coq .Relation .t ->
+ EConstr .rel_context -> Matcher .Terms .t -> EConstr .constr
+ type sigmas = {
+ env_sym : EConstr .constr;
+ env_bin : EConstr .constr;
+ env_units : EConstr .constr;
+ }
+ type reifier
+ val mk_reifier :
+ Coq .Relation .t ->
+ EConstr .constr ->
+ Theory .Trans .ir ->
+ (Theory .Trans .sigmas * Theory .Trans .reifier) Proofview .tactic
+ val reif_constr_of_t :
+ Theory .Trans .reifier -> Matcher .Terms .t -> EConstr .constr
+ end
+end
diff --git a/index.html b/index.html
new file mode 100644
index 0000000..82ba2e8
--- /dev/null
+++ b/index.html
@@ -0,0 +1,54 @@
+
+
+
+
+
+
+ AAC Tactics
+
+
+
+
+
+
+
+
+
+
+About
+Welcome to the AAC Tactics project website! This project is part of coq-community .
+This Coq plugin provides tactics for rewriting and proving universally quantified equations modulo associativity and commutativity of some operator, with idempotent commutative operators enabling additional simplifications. The tactics can be applied for custom operators by registering the operators and their properties as type class instances. Instances for many commonly used operators, such as for binary integer arithmetic and booleans, are provided with the plugin.
+This is an open source project, licensed under the GNU Lesser General Public License v3.0 or later.
+Get the code
+The current stable release of AAC Tactics can be downloaded from GitHub .
+Documentation
+
+
+
+Authors
+
+Thomas Braibant
+Damien Pous
+Fabian Kunze
+
+
+