spitters/new-alg-hierarchy forked from math-classes/math-classes

Merge branch 'master' of git://github.com/Eelis/math-classes

2 parents 5ecc59d + ec2390b commit 253dbf3ae5fa00a5ad37e58ca043dbb3d2ed3900 robbertkrebbers committed with Eelis Dec 7, 2010
1 .gitignore
 @@ -2,6 +2,7 @@ *.glob *.pdf *.crashcoqide +*.pyc tmp.* src/deps src/.sconsign.dblite
37 papers/mscs/mscs.tex
 @@ -177,11 +177,12 @@ \section{Bundling is bad}\label{bundling} \end{lstlisting} The curly brackets used for \lstinline|A| mark it as an implicit argument. -More elaborate structures, too, can be expressed as predicates (expressing laws) over a number of carriers, relations, and operations. While optimally flexible in principle, in practice \emph{na\"ive} adoption of this approach (that is, without using type classes) leads to substantial inconveniences in actual use: when \emph{stating} theorems about abstract instances of such structures, one must enumerate all components along with the structure (predicate) of interest. And when \emph{applying} such theorems, one must either enumerate any non-inferrable components, or let the system spawn awkward metavariables to be resolved at a later time. Importantly, this also hinders proof search for proofs of the structure predicates, making any nontrivial use of theorems a laborious experience. Finally, the lack of \emph{canonical names} for particular components of abstract structures makes it impossible to associate idiomatic notations with them. +More elaborate structures, too, can be expressed as predicates (expressing laws) over a number of carriers, relations, and operations. While optimally flexible in principle, in practice \emph{naive} adoption of this approach (that is, without using type classes) leads to substantial inconveniences in actual use: when \emph{stating} theorems about abstract instances of such structures, one must enumerate all components along with the structure (predicate) of interest. And when \emph{applying} such theorems, one must either enumerate any non-inferrable components, or let the system spawn awkward metavariables to be resolved at a later time. Importantly, this also hinders proof search for proofs of the structure predicates, making any nontrivial use of theorems a laborious experience. Finally, the lack of \emph{canonical names} for particular components of abstract structures makes it impossible to associate idiomatic notations with them. % hm, i used to have paragraphs here about how it would be unclear how this approach could support structure inference and structure inheritance, but those are actually pretty straightforward using ordinary proof search. In the absence of type classes, these are all very real problems, and for this reason the two largest formalizations of abstract algebraic structures in Coq today, CoRN~\cite{C-corn} and \textsc{Ssreflect}~\cite{Packed}, both use \emph{bundled} representation schemes, using records with one or more of the components as fields instead of parameters. For reflexive relations, the following is a fully bundled representation---the other end of the spectrum: +\newpage \begin{lstlisting} Record ReflexiveRelation: Type := { rr_carrier: Type @@ -277,7 +278,7 @@ \section{Bundling is bad}\label{bundling} \section{Predicate classes and operational classes}\label{predicateclasses} -We will tackle the problems associated with the use of structure predicates one by one, starting with those encountered during theorem \emph{application}. Suppose we have defined \lstinline|SemiGroup| as a structure predicate as follows\footnote{Note that defining \lstinline|SemiGroup| as a record instead of a straight conjunction does not make it any less of a predicate. The record form is simply more convenient in that it immediately gives us named projections for laws and substructures.}: +To show that the fully unbundled approach with structures represented by predicates can be made feasible using type classes, we will tackle one by one the problems traditionally associated with their use, starting with those encountered during theorem \emph{application}. Suppose we have defined \lstinline|SemiGroup| as a structure predicate as follows\footnote{Note that defining \lstinline|SemiGroup| as a record instead of a straight conjunction does not make it any less of a predicate. The record form is simply more convenient in that it immediately gives us named projections for laws and substructures.}: \begin{lstlisting} Record SemiGroup (G: Type) (e: relation G) (op: G → G → G): Prop := { sg_setoid: Equivalence e @@ -415,17 +416,17 @@ \section{The algebraic hierarchy}\label{classes} The declarations of the two inherited \lstinline|CommutativeMonoid| structures in \lstinline|SemiRing| nicely illustrate how predicate classes naturally support not just multiple inheritance, but \emph{overlapping} multiple inheritance, where the inherited structures may share components (in this case carrier and equivalence relation). The carrier \lstinline|A|, being an explicit argument, is specified as normal. The equivalence relation, being an implicit argument of class type, is resolved automatically to \lstinline|e|. The binary operation and constant would normally be automatically resolved as well, but we override the inference mechanism locally using Coq's existing named argument facility (which is only syntactic sugar of the most superficial kind) in order to explicitly pair multiplication with 1 for the first \lstinline|CommutativeMonoid| substructure, and addition with 0 for the second \lstinline|CommutativeMonoid| substructure. Again, contrast this with type system extensions such as Matita's manifest records, which are required to make this work when the records bundle components such as \lstinline|op| and \lstinline{unit} as \emph{fields} instead of parameters. -Since \lstinline|CommutativeMonoid| indirectly includes a \lstinline|SemiGroup| field, which in turn includes a \lstinline|Equivalence| field, having a \lstinline|SemiRing| proof means having two distinct proofs that the equality relation is an equivalence. This kind of redundant knowledge ()which arises naturally) is never a problem in our setup, because the use of operational type classes ensures that terms composed of algebraic operations and relations never refer to structure proofs. We find that this is a tremendous relief compared to approaches that \emph{do} intermix the two and where one must be careful to ensure that such terms refer to the \emph{right} proofs of properties. There, even \emph{strong} proof irrelevance (which would make terms convertible that differ only in what proofs they refer to) would not make these difficulties go away entirely, because high-level tactics that rely on quotation of terms require syntactic identity (rather than mere' convertibility) to recognize identical subterms. +Since \lstinline|CommutativeMonoid| indirectly includes a \lstinline|SemiGroup| field, which in turn includes a \lstinline|Equivalence| field, having a \lstinline|SemiRing| proof means having two distinct proofs that the equality relation is an equivalence. This kind of redundant knowledge (which arises naturally) is never a problem in our setup, because the use of operational type classes ensures that terms composed of algebraic operations and relations never refer to structure proofs. We find that this is a tremendous relief compared to approaches that \emph{do} intermix the two and where one must be careful to ensure that such terms refer to the \emph{right} proofs of properties. There, even \emph{strong} proof irrelevance (which would make terms convertible that differ only in what proofs they refer to) would not make these difficulties go away entirely, because high-level tactics that rely on quotation of terms require syntactic identity (rather than mere' convertibility) to recognize identical subterms. -Because predicate classes only provide contextual information and are insulated from the actual algebraic expressions, their instances can always be kept entirely opaque---only their existence matters. Together, these properties largely defuse an argument occasionally voiced against type classes concerning perceived unpredictability of instance resolution. While it is certainly true that in contexts with redundant information it can become hard to predict which instance of a predicate class will be found by proof search, it simply \emph{does not matter} which one is found. Moreover, for operational type classes the issue rarely arises because their instances are not nearly as abundant. +Because predicate classes only provide contextual information and are insulated from the actual algebraic expressions, their instances can always be kept entirely opaque---only their existence matters. Together, these properties largely defuse an argument occasionally voiced against type classes concerning perceived unpredictability of instance resolution. While it is certainly true that in contexts with redundant information it can become hard to predict which instance of a predicate class will be found by proof search, it simply \emph{does not matter} which one is found. Moreover, for operational type classes the issue rarely arises because their instances are not nearly as abundant, and are systematically shared. % rather strict separation of operations and proofs of properties about them (resolved by instance resolution) provides a very pleasing environment to work in, without any need for hacks. % terms composed of algebraic operations and relations % separation of , this kind of redundance is never a problem for us. % it is /never/ a problem to know a fact twice. % multiple proofs of equality, and even of semigroup-ness (since both Monoid), but that's simply not a problem, since none of our terms ever refers to such proofs. We have found that this rather strict separation of operations and proofs of properties about them (resolved by instance resolution) provides a very pleasing environment to work in, without any need for hacks. -We use names for properties like distributivity and absorption, because these are type classes as well (which is why we declare them with \lstinline|:>|). It has been our experience that almost any generic predicate worth naming is worth representing as a predicate type class, so that its proofs will be resolved as instances behind the scenes whenever possible. Doing this consistently minimizes administrative noise in the code, bringing us closer to ordinary mathematical vernacular. Indeed, we believe that type classes are an elegant and apt formalization of the seemingly casual manner in which ordinary mathematical presentation assumes implicit administration and use of a database' of properties previously proved. Much more so than the existing canonical structures facility, because canonical structures can only be used with bundled representations, which we argued against in section~\ref{bundling}. +We use names for properties like distributivity and absorption, because these are type classes as well (which is why we declare their instances with \lstinline|:>|). It has been our experience that almost any generic predicate worth naming is worth representing as a predicate type class, so that its proofs will be resolved as instances behind the scenes whenever possible. Doing this consistently minimizes administrative noise in the code, bringing us closer to ordinary mathematical vernacular. Indeed, we believe that type classes provide an elegant and apt formalization of the seemingly casual manner in which ordinary mathematical presentation assumes implicit administration and use of a database' of properties previously proved. The operational type classes used in \lstinline|SemiRing| for zero, one, multiplication and addition, are the same ones used by \lstinline|Ring| and \lstinline|Field| (not shown). Thus, the realization that a particular semiring is in fact a ring or field has no bearing on how one refers to the operations in question, which is as it should be. The realization that a particular semigroup is part of a semiring \emph{does} call for a new (canonical) name, simply because of the need for disambiguation. The introduction of these additional names for the same operation is quite harmless in practice, because canonical names established by operational type class fields are identity functions, so that in most contexts the distinction reduces away instantly. @@ -444,7 +445,7 @@ \section{The algebraic hierarchy}\label{classes} Notice that \lstinline|f| is \emph{not} made into an operational type class. The reason for this is that the role of \lstinline|f| is analogous to the carrier type in the previous predicate class definitions, in that it serves as the primary identification for the structure, and should therefore not be inferred. -The \lstinline|monmor_to| and \lstinline|monmor_from| fields are not an absolute necessity, but eliminate the need for theorems to declare \lstinline|Monoid| parameters when they already declare \lstinline|Monoid_Morphism| parameters. This is an instance where we can freely posit structural properties without worrying about potential problems when such information turns out to be redundant in contexts where the source and target of the morphism are already known to be \lstinline|Monoid|s. +We include the \lstinline|monmor_to| and \lstinline|monmor_from| fields because it does not make much sense to talk about monoid morphisms between non-monoids, and having these fields removes the need for \lstinline|Monoid| class constraints when we are already parameterizing definitions or theory on a \lstinline|Monoid_Morphism|. On the other hand, we will also wish to talk about monoid morphisms between \emph{known} monoids, and in these cases the fields will be strictly redundant. As mentioned before, it is a strength of our approach that such redundant knowledge is entirely harmless, so that we may freely posit these structural properties whenever they make sense and provide convenience, without risking rebundling tar-pits or projection path ambiguities down the line. Unfortunately, there is actually one annoying wrinkle here, which will also explain why we do not register these two fields as instance resolution hints (by declaring them with \lstinline|:>|). What we really want these fields to express is \emph{if} in a certain context we know something to be a \lstinline|Monoid_Morphism|, \emph{then} realize that the source and target are \lstinline|Monoid|s''. However, the current instance resolution implementation has little support for this style of \emph{forward} reasoning, and is really primarily oriented on \emph{backward} reasoning: had we registered \lstinline|monmor_to| and \lstinline|monmor_from| as instance resolution hints, we would in fact be saying \emph{if} trying to establish that something is a \lstinline|Monoid|, \emph{then} try finding a \lstinline|Monoid_Morphism| to or from it'', which quickly degenerates into a wild goose chase. We will return to this point in section~\ref{conclusions}. @@ -618,29 +619,27 @@ \subsection{Signatures and algebras} ; operation:> Set ; operation_type:> operation → ne_list sorts }. \end{lstlisting} -Given an interpretation of the sorts (mapping each symbolic sort to a carrier), an interpretation for the operations is easily written as an operational type class: +Given an interpretation of the sorts (mapping each symbolic sort to a carrier type), interpretations of the operations are easily represented by an operational type class: \begin{lstlisting} - Variables (σ: Signature) (carriers: sorts σ → Type). + Variables (σ: Signature) (carriers: sorts σ$$→ Type). - Definition op_type: ne_list (sorts σ) → Type := fold (→) ∘ map carrier. - - Class AlgebraOps (σ: Signature) (carriers: sorts σ$$ → Type) - := algebra_op: ∀ o: operation σ, op_type carriers (σ o). + Class AlgebraOps := + algebra_op: ∀ o: operation σ, fold (→$\hspace{-1mm}$) (map carriers (operation_type σ$$o)). \end{lstlisting} Because our carriers will normally be equipped with a setoid equality, we further define the predicate class \lstinline|Algebra|, stating that each of the operations respects the setoid equality on the carriers: \begin{lstlisting} - Class Algebra {∀$$a, Equiv (carriers a)} {AlgebraOps σ$$carriers}: Prop := + Class Algebra {∀$$a, Equiv (carriers a)} {AlgebraOps}: Prop := { algebra_setoids:> ∀ a, Setoid (carriers a) ; algebra_propers:> ∀ o: σ, Proper (=) (algebra_op o) }. \end{lstlisting} -The \lstinline|(=)| referred to in \lstinline|algebra_propers| is an \lstinline|Equiv| instance expressing setoid-respecting extensionality for the function types generated by \lstinline|op_type|. +The \lstinline|(=)| referred to in \lstinline|algebra_propers| is an automatically derived \lstinline|Equiv| instance expressing setoid-respecting extensionality for the function types produced by the \lstinline|fold| in \lstinline|AlgebraOps|. We do not unbundle \lstinline|Signature| because it represents a triple that will always be specifically constructed for subsequent use with the universal algebra facilities. We have no ambition to recognize signature triples in the wild'', nor will we ever talk about multiple signatures sharing sort- or operation enumerations. \subsection{Equational theories and varieties} \label{varieties} -To characterize structures such as semirings and rings, we need equational theories, consisting of a signature together with laws (represented by a predicate over equality entailments): +To adequately characterize structures such as semirings and rings, we need not just a signature that enumerates and gives the types of their operations, but also a specification of the axioms (laws) that these operations must satisfy. For this, we define \lstinline|EquationalTheory| as a signature together with a set of laws, the latter represented by a predicate over equality entailments: \begin{lstlisting} Record EquationalTheory := { eqt_sig:> Signature @@ -685,7 +684,7 @@ \subsection{The first homomorphism theorem} To give a further taste of what universal algebra in our development looks like, we consider the definitions involved in the first homomorphism theorem~\cite{meinke1993universal} in more detail: \begin{theorem}[First homomorphism theorem] -If $A$ and $B$ are algebras, and $f$ is a homomorphism from $A$ to $B$, then the equivalence relation defined by $a\sim b$ if and only if $f(a)=f(b)$ is a congruence on $A$, and the algebra $A/\hspace{-1mm}\sim$ is isomorphic to the image of $f$, which is a subalgebra of B. +If $A$ and $B$ are algebras, and $f$ is a homomorphism from $A$ to $B$, then the equivalence relation $\sim$ defined by $a\sim b \leftrightarrow f(a)=f(b)$'' is a congruence on $A$, and the quotient algebra $A/\hspace{-1mm}\sim$ is isomorphic to the image of $f$, which is a subalgebra of B. \end{theorem} A set of relations \lstinline|e| (one for each sort) is a congruence for an existing algebra if (1) \lstinline|e| respects that algebra's existing setoid equality, and (2) the operations with \lstinline|e| again form an algebra (namely the quotient algebra): @@ -699,9 +698,9 @@ \subsection{The first homomorphism theorem} For the homomorphism theorem, we begin by declaring our dramatis personae: \begin{lstlisting} - Context {Algebra σ$$A} {Algebra σ$$ B} {HomoMorphism σ$$A B f}. + Context {HomoMorphism σ$$ A B f}. \end{lstlisting} -With \lstinline|~| defined as described, the first part of the proof is simply the definition of the following instance: +With \lstinline|~| defined as indicated, the first part of the proof is simply the definition of the following instance: \begin{lstlisting} Instance co: Congruence σ (~). \end{lstlisting} @@ -723,7 +722,7 @@ \subsection{The first homomorphism theorem} The reason we define \lstinline|image| and \lstinline|ClosedSubset| in \lstinline|Type| rather than in \lstinline|Prop| is that since the final goal of the proof is to establish an isomorphism in the category of σ-algebras (where arrows are algebra homomorphisms), we will eventually need to map elements in the subalgebra defined by \lstinline|image| back to their pre-image in \lstinline|A|. -However, there are contexts (in other proofs) where \lstinline|Prop|-sorted construction of subalgebras really \emph{is} appropriate. Unfortunately, Coq's universe polymorphism is not yet up to the task of letting us use a single set of definitions to handle both cases. In particular, there is no universe polymorphism for definitions (as opposed to inductive definitions) yet. We will return to this point later. In our development, we have two sets of definitions, one for \lstinline|Prop| and one for \lstinline|Type|, resulting in duplication of about a hundred lines of code. +However, there are contexts (in other proofs) where \lstinline|Prop|-sorted construction of subalgebras really \emph{is} appropriate. Unfortunately, Coq's universe polymorphism is not yet up to the task of letting us use a single set of definitions to handle both cases. In particular, there is no universe polymorphism for ordinary definitions (as opposed to inductive definitions) yet. We will return to this point later. In our development, we have two sets of definitions, one for \lstinline|Prop| and one for \lstinline|Type|, resulting in duplication of about a hundred lines of code. For the main theorem, we now bundle the quotient algebra and the subalgebra into records akin to \lstinline|ObjectInVariety| from section~\ref{varieties}: \begin{lstlisting}
25 src/SConscript
 @@ -0,0 +1,25 @@ + +import os, glob, string + +nodes = ['.'] +dirs = [] +vs = [] + +while nodes: + node = nodes.pop() + b = os.path.basename(node) + if node.endswith('.v') and not b.endswith('_nobuild.v'): + vs += [File(node)] + if os.path.isdir(node) and b != 'broken': + dirs += [node] + nodes += glob.glob(node + '/*') + +env = DefaultEnvironment() + +vos = globs = [] +for node in vs: + vo, glob = env.Coq(node) + vos += [vo] + globs += [glob] + +Return('vs vos globs')
54 src/SConstruct
 @@ -1,54 +1,20 @@ +import os -import os, glob, string +env = DefaultEnvironment(ENV = os.environ, tools=['default', 'Coq']) +(vs, vos, globs) = env.SConscript(dirs='.') -nodes = ['.'] -dirs = [] -vs = [] +env['COQFLAGS'] = Rs = ' -R . "" ' -while nodes: - node = nodes.pop() - b = os.path.basename(node) - if node.endswith('.v') and node != "./misc/benchmarks.v": - vs += [node] - if os.path.isdir(node) and node != "./broken": - dirs += [node] - nodes += glob.glob(node + '/*') - -Rs = ' -R . "" ' - -coqc = 'coqc -q ' + Rs + ' $SOURCE' - -env = DefaultEnvironment(ENV = os.environ) - -def add_glob(target, source, env): - base, _ = os.path.splitext(str(target[0])) - target.append(base + ".glob") - return target, source - -env.Append(BUILDERS = - {'Coq' : Builder( - action = coqc, - suffix = '.vo', - src_suffix = '.v', - emitter = add_glob)}) +Default('implementations', 'theory', 'categories', 'orders', 'varieties', 'misc') -vos = globs = [] -for node in vs: - vo, glob = env.Coq(node) - vos += [vo] - globs += [glob] +env.CoqDoc(env.Dir('coqdoc'), vs, COQDOCFLAGS='-utf8 --toc -g --no-lib-name') + # Todo: Do "patch --backup$TARGET/coqdoc.css ../tools/coqdoc.css.diff", including the dependency on the .diff file. + # Note: The generated documentation is no good, because of Coq bug #2423. -env.Command(env.Dir('coqdoc'), vs + vos + globs + [File('../tools/coqdoc.css.diff')], - [ Delete('coqdoc') - , Mkdir('coqdoc') - , 'coqdoc -utf8 --toc -g --no-lib-name -d $TARGET' + Rs + ' '.join(vs) - , 'patch --backup$TARGET/coqdoc.css ../tools/coqdoc.css.diff']) +vs_string = ' '.join(map(str, vs)) -os.system('coqdep ' + Rs + ' '.join(vs) + ' > deps') +os.system('coqdep ' + Rs + vs_string + ' > deps') ParseDepends('deps') -Default('implementations', 'theory', 'categories', 'orders', 'varieties', 'misc') - open('coqidescript', 'w').write('#!/bin/sh\ncoqide ' + Rs.replace('"', '\\"') + ' $@ \n') os.chmod('coqidescript', 0755) - 2 src/categories/functor.v  @@ -1,6 +1,6 @@ Require Import Morphisms RelationClasses Equivalence Setoid - abstract_algebra functors categories. + abstract_algebra interfaces.functors categories. Section natural_transformations_id_comp. 2 src/implementations/QType_rationals.v  @@ -89,7 +89,7 @@ Qed. Instance: Inverse to_Q := of_Q. Instance: Surjective to_Q. -Proof. constructor. exact spec_of_Q. apply _. Qed. +Proof. constructor. intros x y E. rewrite <- E. apply spec_of_Q. apply _. Qed. Instance: Injective to_Q. Proof. constructor. auto. apply _. Qed. 2 src/implementations/ZType_integers.v  @@ -92,7 +92,7 @@ Qed. Instance: Inverse to_Z := of_Z. Instance: Surjective to_Z. -Proof. constructor. exact spec_of_Z. apply _. Qed. +Proof. constructor. intros x y E. rewrite <- E. apply spec_of_Z. apply _. Qed. Instance: Injective to_Z. Proof. constructor. unfold_equiv. intuition. apply _. Qed. 4 src/implementations/fast_rationals.v  @@ -42,8 +42,8 @@ Qed. Instance: Surjective (λ p, fastZ_to_fastQ (fst p) * / fastZ_to_fastQ (snd p)). Proof. split. - - intros x. unfold id, compose, inverse, fastZ_to_fastQ. + + intros x y E. rewrite <- E. clear E y. unfold id, compose, inverse, fastZ_to_fastQ. destruct x as [x | x y]; simpl. rewrite rings.preserves_1. field. apply (ne_zero 1). 3 src/implementations/field_of_fractions.v  @@ -152,7 +152,8 @@ Global Instance: Inverse inject_frac := λ x, (num x, den x). Global Instance: Surjective inject_frac. Proof. constructor. - intros [n d P]. + intros [n d P] y E. + rewrite <- E. unfold Basics.compose, inject_frac, equiv, frac_equiv. simpl. ring_simplify. 11 src/implementations/natpair_integers.v  @@ -211,15 +211,18 @@ Section for_another_ring. Instance: SemiRing_Morphism inject'_N. Lemma agree_on_nat: inject'_N = n_to_sr. - Proof. intro x. apply (naturals.to_semiring_unique inject'_N). Qed. + Proof. + intros x y E. rewrite E. + apply (naturals.to_semiring_unique inject'_N). + Qed. Lemma same_morphism: integers_to_ring Z R = inject'. - Proof. - intros [pos0 neg0]. + Proof with intuition. + intros [pos0 neg0] z' E. rewrite <- E. clear E z'. rewrite split_into_nats. preservation. rewrite preserves_inv, abstract_algebra.preserves_inv. - rewrite (agree_on_nat pos0), (agree_on_nat neg0). + rewrite (agree_on_nat pos0 pos0), (agree_on_nat neg0 neg0)... unfold integers_to_ring, inject. simpl. rewrite theory.rings.preserves_0. ring. Qed. 112 src/implementations/ne_list.v  @@ -1,11 +1,16 @@ -Set Implicit Arguments. +(** This module should be [Require]d but not [Import]ed (except for the notations submodule). *) Require Import - Unicode.Utf8 canonical_names Setoid. + Unicode.Utf8 Setoid Coq.Lists.List Setoid Morphisms Permutation. + +Instance: forall A, Proper (@Permutation A ==> eq) (@length A). +Proof Permutation_length. + +Existing Instance Permutation_map_aux_Proper. Section contents. - Variable T: Type. + Context {T: Type}. Inductive L: Type := one: T → L | cons: T → L → L. @@ -29,18 +34,115 @@ Section contents. Definition head (l: L): T := match l with one x => x | cons x _ => x end. - Definition last: L → T := foldr1 (λ x y, y). + Fixpoint to_list (l: L): list T := + match l with + | one x => x :: nil + | cons x xs => x :: to_list xs + end. + + Global Coercion to_list: L >-> list. + + Definition tail (l: L): list T := match l with one _ => nil | cons _ x => to_list x end. + + Definition last: L → T := foldr1 (fun x y => y). Fixpoint replicate_Sn (x: T) (n: nat): L := match n with | 0 => one x | S n' => cons x (replicate_Sn x n') end. + Fixpoint take (n: nat) (l: L): L := + match l, n with + | cons x xs, S n' => take n' xs + | _, _ => one (head l) + end. + + Lemma two_level_rect (P: L → Type) + (Pone: ∀ x, P (one x)) + (Ptwo: ∀ x y, P (cons x (one y))) + (Pmore: ∀ x y z, P z → (∀ y', P (cons y' z)) → P (cons x (cons y z))): + ∀ l, P l. + Proof with auto. + cut (∀ l, P l * ∀ x, P (cons x l)). + intros. apply X. + destruct l... + revert t. + induction l... + intros. + split. apply IHl. + intro. + apply Pmore; intros; apply IHl. + Qed. + + Lemma tl_length (l: L): S (length (tl l)) = length l. + Proof. destruct l; reflexivity. Qed. + + Notation ListPermutation := (@Permutation.Permutation _). + + Definition Permutation (x y: L): Prop := ListPermutation x y. + + Global Instance: Equivalence Permutation. + Proof with intuition. + unfold Permutation. + split; repeat intro... + transitivity y... + Qed. + + Global Instance: Proper (Permutation ==> ListPermutation) to_list. + Proof. firstorder. Qed. + + Lemma Permutation_ne_tl_length (x y: L): + Permutation x y → length (tl x) = length (tl y). + Proof. + intro H. + apply eq_add_S. + do 2 rewrite tl_length. + rewrite H. + reflexivity. + Qed. + End contents. -Fixpoint map (f: A → B) (l: L A): L B := +Implicit Arguments L []. + +Fixpoint tails {A} (l: L A): L (L A) := + match l with + | one x => one (one x) + | cons x y => cons l (tails y) + end. + +Lemma tails_are_shorter {A} (y x: L A): + In x (tails y) → + length x <= length y. +Proof with auto. + induction y; simpl. + intros [[] | ?]; intuition. + intros [[] | C]... +Qed. + +Fixpoint map {A B} (f: A → B) (l: L A): L B := match l with | one x => one (f x) | cons h t => cons (f h) (map f t) end. + +Lemma list_map {A B} (f: A → B) (l: L A): to_list (map f l) = List.map f (to_list l). +Proof. induction l. reflexivity. simpl. congruence. Qed. + +Global Instance: forall {A B} (f: A → B), Proper (Permutation ==> Permutation) (map f). +Proof with auto. + intros ????? E. + unfold Permutation. + do 2 rewrite list_map. + rewrite E. + reflexivity. +Qed. + +Module notations. + + Global Notation ne_list := L. + Global Infix ":::" := cons (at level 60, right associativity). + (* Todo: Try to get that "[ x ; .. ; y ]" notation working. *) + +End notations. 2 src/implementations/peano_naturals.v  @@ -99,7 +99,7 @@ Proof. reflexivity. Qed. Instance: Initial (semiring.object nat). Proof. intros. apply natural_initial. intros. - intro x. induction x. + intros x y E. unfold equiv, nat_equiv in E. subst y. induction x. replace 0%nat with (ring_zero:nat) by reflexivity. do 2 rewrite preserves_0. reflexivity. rewrite S_nat_1_plus. 5 src/implementations/positive_integers_naturals.v  @@ -126,8 +126,8 @@ Qed. Instance: Surjective of_nat. Proof. split. 2: apply _. - intros [x Ex]. - unfold to_nat, of_nat. unfold_equivs. + intros [x Ex] y E. rewrite <- E. + unfold to_nat, of_nat. unfold_equivs. apply integers.abs_nonneg. assumption. Qed. @@ -162,6 +162,7 @@ Lemma ZPos_to_nat_int_abs x p : naturals_to_semiring ZPos nat (exist _ x p) = in Proof. replace (int_abs Z nat x) with (to_nat (exist _ x p)) by reflexivity. apply naturals.to_semiring_unique'. apply _. apply ZPos_to_nat_sr_morphism. + reflexivity. Qed. Lemma ZPos_int_nat_precedes (x y : ZPos) : x ≤ y → x ≤ y. 3 src/implementations/signed_binary_positive_integers.v  @@ -153,8 +153,11 @@ Section for_another_ring. Lemma same_morphism: integers_to_ring Z R = map_Z'. Proof. intros []. + intros y E. rewrite <- E. apply agree_on_0. + intros p y E. rewrite <- E. apply agree_on_positive. + intros p y E. rewrite <- E. apply agree_on_negative. Qed. 4 src/implementations/stdlib_rationals.v  @@ -80,7 +80,7 @@ Instance: Inverse inject := λ x, (Qnum x, Zpos (Qden x)). Instance: Surjective (λ p, inject_Z (fst p) * / inject_Z (snd p)). Proof. constructor. 2: apply _. - intros [num den]. unfold Basics.compose, id. + intros [num den] q E. rewrite <- E. unfold Basics.compose, id. simpl. rewrite Qmake_Qdiv. reflexivity. Qed. @@ -94,4 +94,4 @@ Proof. case (decide (q = 0)); intros E. rewrite E. reflexivity. reflexivity. -Qed. +Qed. 9 src/interfaces/canonical_names.v  @@ -22,8 +22,13 @@ Notation "x ≠ y":= (~ equiv x y): type_scope. Infix "≡" := eq (at level 70, no associativity). (* Hm, we could define a very low priority Equiv instance for Leibniz equality.. *) -Instance ext_eq (A B: Type) (Equiv B): Equiv (A → B) - := λ f g: A → B, ∀ x, f x = g x. +Instance ext_eq {Equiv A} {Equiv B}: Equiv (A → B) + := ((=) ==> (=))%signature. + +(** Interestingly, most of the development works fine if this is defined as + ∀ x, f x = g x. +However, in the end that version was just not strong enough for comfortable rewriting +in setoid-pervasive contexts. *) (* Other canonically named relations/operations/constants: *) Class Decision P := decide: sumbool P (~ P). 38 src/interfaces/functors.v  @@ -1,6 +1,6 @@ Global Set Automatic Introduction. (* todo: do this in a more sensible place *) -Require Import abstract_algebra canonical_names Program. +Require Import abstract_algebra canonical_names Program Morphisms. Require setoids. Section functor_class. @@ -102,3 +102,39 @@ Section compose_functors. Qed. End compose_functors. + +(** The Functor class is nice and abstract and theory-friendly, but not as convenient + to use for regular programming as Haskell's Functor class. The reason for this is that + our Functor is parameterized on two Categories, which by necessity bundle setoid- + ness and setoid-morphism-ness into objects and arrows, respectively. + The Haskell Functor class, by contrast, is essentially specialized for endofunctors on + the category of Haskell types and functions between them. The latter corresponds to our + setoid.Object category. + + To recover convenience, we introduce a second functor type class tailored specifically to + functors of this kind. The specialization allows us to forgo bundling, and lets us recover + the down-to-earth Type→Type type for the type constructor, and the (a→b)→(F a→F b) + type for the function map, with all setoid/morphism proofs hidden in the structure class + in Prop. + + To justify this definition, in theory/functors we show that instances of this new functor + class do indeed give rise to instances of the original nice abstract Functor class. *) + +Section setoid_functor. + + Context (map_obj: Type → Type) {map_eq: ∀ {Equiv A}, Equiv (map_obj A)}. + + Class SFmap: Type := sfmap: ∀ (v → w), (map_obj v → map_obj w). + + Class SFunctor {SFmap}: Prop := + { sfunctor_makes_setoids {Setoid A}: Setoid (map_obj A) + ; sfunctor_makes_morphisms {Equiv v} {Equiv w} (f: v → w):> + Setoid_Morphism f → Setoid_Morphism (sfmap f) + ; sfunctor_morphism {Setoid v} {Setoid w}:> + Proper ((equiv ==> equiv) ==> (equiv ==> equiv)) (@sfmap _ v w) + ; sfunctor_id {Setoid v}: sfmap id = id + ; sfunctor_comp {Equiv a} {Equiv b} {Equiv c} (f: b → c) (g: a → b): + Setoid_Morphism f → Setoid_Morphism g → + sfmap (f ∘ g) = sfmap f ∘ sfmap g }. + +End setoid_functor. 7 src/interfaces/integers.v  @@ -25,10 +25,11 @@ Section initial_maps. Lemma integer_initial (same_morphism : ∀ {Ring B} {h : Int → B} {!Ring_Morphism h}, integers_to_ring B = h) : Initial (ring.object Int). Proof. - intros y [x h] []. simpl in *. + intros y [x h] [] ?. simpl in *. apply same_morphism. - apply ring.decode_variety_and_ops. - apply (@ring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h). + apply ring.decode_variety_and_ops. + apply (@ring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h). + reflexivity. Qed. End initial_maps. 44 src/interfaces/monads.v  @@ -3,29 +3,39 @@ Require categories.setoid. Require Import Setoid Morphisms. Require Import abstract_algebra canonical_names theory.categories. -Section contents. +Section ops. -Context (M: Type → Type). + Context (M: Type → Type). -Class MonadReturn := ret: ∀ {A}, A → M A. -Class MonadBind := bind: ∀ {A B}, M A → (A → M B) → M B. + Class MonadReturn := ret: ∀ {A}, A → M A. + Class MonadBind := bind: ∀ {A B}, M A → (A → M B) → M B. + +End ops. + +Implicit Arguments ret [[M] [MonadReturn] [A]]. +Implicit Arguments bind [[M] [MonadBind] [A] [B]]. Infix ">>=" := bind (at level 50, no associativity). +Notation "x ← y ; z" := (y >>= (λ x : _, z)) (at level 30, right associativity). +Notation "x >> y" := (_ ← x ; y) (at level 30, right associativity). + +Section structure. + + Context (M: Type → Type). -Class Monad {Me: ∀ A, Equiv A → Equiv (M A)} {MonadReturn} {MonadBind}: Prop := + Class Monad {Me: ∀ A, Equiv A → Equiv (M A)} {MonadReturn M} {MonadBind M}: Prop := (* Propers: *) - { ret_proper:> ∀ {Equiv A}, Proper (equiv ==> equiv) (@ret _ A) - ; bind_proper:> ∀ {Equiv A} {Equiv B}, - Proper (equiv ==> (equiv ==> equiv) ==> equiv) (@bind _ A B) + { ret_proper:> ∀ {Equiv A}, Proper (equiv ==> equiv) (@ret _ _ A) + ; bind_proper:> ∀ {Equiv A} {Equiv B}, + Proper (equiv ==> (equiv ==> equiv) ==> equiv) (@bind _ _ A B) - ; equivalence: ∀ {Setoid A}, Setoid (M A) + ; mon_setoid: ∀ {Setoid A}, Setoid (M A) - (* Laws: *) - ; mon_lunit: ∀ {Setoid A} {Setoid B} (x: A) (f: A → M B), ret x >>= f = f x - ; mon_runit: ∀ {Setoid A} (m: M A), m >>= ret = m - ; mon_assoc: ∀ {Setoid A} {Setoid B} {Setoid C} (n: M A) (f: A → M B) (g: B → M C), - (n >>= f) >>= g = n >>= (λ x, f x >>= g) - (* todo: write using Setoid type class (rather than categories.setoid.Object) *) - }. + (* Laws: *) + ; mon_lunit: ∀ {Setoid A} {Setoid B} (x: A) (f: A → M B), ret x >>= f = f x + ; mon_runit: ∀ {Setoid A} (m: M A), m >>= ret = m + ; mon_assoc: ∀ {Setoid A} {Setoid B} {Setoid C} (n: M A) (f: A → M B) (g: B → M C), + (n >>= f) >>= g = n >>= (λ x, f x >>= g) + }. -End contents. +End structure. 8 src/interfaces/naturals.v  @@ -34,11 +34,13 @@ Section initial_maps. Lemma natural_initial (same_morphism : ∀ {SemiRing B} {h : A → B} {!SemiRing_Morphism h}, naturals_to_semiring B = h) : Initial (semiring.object A). Proof. - intros y [x h] []. simpl in *. + intros y [x h] [] ?. simpl in *. apply same_morphism. - apply semiring.decode_variety_and_ops. - apply (@semiring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h). + apply semiring.decode_variety_and_ops. + apply (@semiring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h). + reflexivity. Qed. + End initial_maps. Instance: Params (@naturals_to_semiring) 7. 22 src/interfaces/sequences.v  @@ -3,26 +3,16 @@ Set Automatic Coercions Import. Require Import Morphisms List Program - abstract_algebra theory.categories forget_algebra forget_variety theory.rings interfaces.functors. + abstract_algebra theory.categories forget_algebra forget_variety theory.rings interfaces.functors + canonical_names. Require categories.setoid categories.product varieties.monoid categories.algebra. Require categories.cat theory.setoids. Module ua := universal_algebra. -Instance oh: ∀ {A} {Equiv B} {Equiv C} (f: B → C) {!Setoid_Morphism f}, - Proper ((=) ==> (=)) (@compose A B C f). -Proof. firstorder. Qed. - -Instance: ∀ {A} {Equiv B} {Equiv C}, Proper ((=) ==> eq ==> (=)) (@compose A B C). -Proof. repeat intro. subst. firstorder. Qed. - -Lemma eta {A} {Setoid B} (f: A → B): (λ x, f x) = f. -Proof. intro. reflexivity. Qed. - Instance: Arrows Type := λ X Y, X → Y. - -(* todo: move last four elsewhere *) + (* todo: move elsewhere *) (* First, the nice clean high level encapsulated version: *) @@ -103,9 +93,11 @@ Section practical. repeat intro. simpl. apply sequence_fmap_id. + reflexivity. repeat intro. simpl. apply sequence_fmap_comp. + reflexivity. Qed. Program Definition posh_inject: id ⇛ monoid.forget ∘ posh_free := λ a, inject a. @@ -135,6 +127,7 @@ Section practical. rewrite E. apply sequence_inject_natural. apply _. + reflexivity. Qed. Goal @PoshSequence posh_free posh_fmap posh_inject posh_extend. @@ -155,13 +148,14 @@ Section practical. rewrite H4. symmetry. apply (@sequence_extend_commutes PS x _ _ _ _ _ _ H2 f fM). + reflexivity. unfold compose. intros [x0 h] H4 [] a. unfold equiv, setoid.Equiv_instance_0 in H4. simpl in *. apply (@sequence_only_extend_commutes PS x _ _ _ _ _ _ H2 f _ (x0 tt)). apply (@monoid.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h). - intro. symmetry. apply H4. reflexivity. + intros. symmetry. apply H4. reflexivity. unfold posh_extend. intros [x ??] [y ?? yV]. constructor; try apply _. 0 src/misc/benchmarks.v → src/misc/benchmarks_nobuild.v File renamed without changes. 30 src/site_scons/site_tools/Coq.py  @@ -0,0 +1,30 @@ +# -*- coding: utf-8 -*- + +import SCons.Defaults, SCons.Tool, SCons.Util, os + +def add_glob(target, source, env): + base, _ = os.path.splitext(str(target[0])) + target.append(base + ".glob") + return target, source + +Coq = SCons.Builder.Builder( + action = '$COQCMD', + suffix = '.vo', + src_suffix = '.v', + emitter = add_glob) + +def coqdoc_gen(source, target, env, for_signature): + for s in source: + base, _ = os.path.splitext(str(s)) + env.Depends(target, env.File(base + '.glob')) + return [SCons.Defaults.Mkdir(target), 'coqdoc $COQDOCFLAGS -d$TARGET $COQFLAGS$SOURCES'] + +CoqDoc = SCons.Builder.Builder(generator = coqdoc_gen) + +def generate(env): + env['COQC'] = 'coqc' + env['COQCMD'] = '$COQC$COQFLAGS -q \$SOURCE' + env.Append(BUILDERS = {'Coq': Coq, 'CoqDoc': CoqDoc}) + +def exists(env): + return env.Detect('coqc')
 @@ -4,7 +4,7 @@ Set Automatic Introduction. Require Import Relation_Definitions Morphisms Setoid Program - abstract_algebra setoids functors categories + abstract_algebra setoids interfaces.functors categories workaround_tactics theory.jections. Require dual. @@ -151,7 +151,8 @@ Section for_ηAdjunction. unfold φ. repeat intro. constructor. - intro. symmetry. + intros x0 y E. symmetry. + rewrite <- E. apply (η_adjunction_universal F G x). constructor... intros ?? E. rewrite E. reflexivity.
6 src/theory/categories.v
 @@ -1,7 +1,7 @@ Set Automatic Introduction. Require Import - Relation_Definitions Morphisms Setoid Program abstract_algebra setoids functors theory.jections. + Relation_Definitions Morphisms Setoid Program abstract_algebra setoids interfaces.functors theory.jections. Notation "x ⇛ y" := (∀ a, x a ⟶ y a) (at level 90, right associativity). (* Transformations (polymorphic arrows). Couldn't find an "arrow with dot over it" unicode character. *) @@ -60,8 +60,8 @@ Section adjunction. ; ηε_adjunction_right_functor: Functor G _ ; ηε_adjunction_η_natural: NaturalTransformation η ; ηε_adjunction_ε_natural: NaturalTransformation ε - ; ηε_adjunction_identity_at_G: (λ a, fmap G (ε a) ◎ η (G a)) = id_nat_trans G - ; ηε_adjunction_identity_at_F: (λ a, ε (F a) ◎ fmap F (η a)) = id_nat_trans F }. + ; ηε_adjunction_identity_at_G: ∀ a, fmap G (ε a) ◎ η (G a) = id_nat_trans G a + ; ηε_adjunction_identity_at_F: ∀ a, ε (F a) ◎ fmap F (η a) = id_nat_trans F a }. (* We currently don't define adjunctions as characterized in MacLane p81 Theorem 2 (ii) and (iv). *)
53 src/theory/functors.v
 @@ -0,0 +1,53 @@ + +Require Import + Program + canonical_names abstract_algebra + interfaces.functors. +Require + categories.setoid. + +Section setoid_functor_as_posh_functor. + + Context {SFunctor F}. + + Program Definition map_setoid: setoid.Object → setoid.Object := + λ o, @setoid.object (F (setoid.T o)) (map_eq (setoid.T o) (setoid.e o)) _. + + Next Obligation. Proof. + destruct o. + apply (@sfunctor_makes_setoids F _ _ _). + assumption. + Qed. + + Program Instance: Fmap map_setoid := λ v w X, @sfmap F H _ _ (proj1_sig X). + + Next Obligation. Proof. + destruct v, w, X. simpl in *. + apply sfunctor_makes_morphisms; apply _. + Qed. + + Instance: Functor map_setoid _. + Proof with auto; intuition. + pose proof (@sfunctor_makes_setoids F _ _ _). + constructor; try apply _. + intros [???] [???]. + constructor; try apply _. + intros [x ?] [y ?] U ?? E. simpl in *. + rewrite E. + cut (sfmap F x = sfmap F y)... + assert (x = y) as E'. intro... + rewrite E'... + apply (sfunctor_makes_morphisms F)... + intros [???] x ??. simpl in *. + rewrite (sfunctor_id F x x)... + intros [???] [???] [??] [???] [??] ?? E. simpl in *. + unfold compose at 2. + rewrite <- E. + apply (sfunctor_comp F)... + Qed. + +End setoid_functor_as_posh_functor. + +(** Note that we cannot prove the reverse (i.e. that an endo-Functor on + setoid.Object gives rise to an SFunctor, because an SFunctor requires a + Type→Type map, which we cannot get from a setoid.Object→setoid.Object map. *)
2 src/theory/hom_functor.v
 @@ -2,7 +2,7 @@ Set Automatic Introduction. Require Import Relation_Definitions Morphisms Setoid Program - abstract_algebra setoids functors categories. + abstract_algebra setoids interfaces.functors categories. Require categories.setoid.
17 src/theory/integers.v
 @@ -32,20 +32,21 @@ Qed. Lemma to_ring_unique' {Integers Int} {Ring R} (f g: Int → R) {!Ring_Morphism f} {!Ring_Morphism g}: f = g. Proof. - intro. + intros x y E. rewrite (to_ring_unique f), (to_ring_unique g). + rewrite E. reflexivity. Qed. (* A ring morphism from integers to another ring is injective if there's an injection in the other direction: *) Lemma to_ring_injective {Integers Int} {Ring R} (f: R → Int) (g: Int → R) {!Ring_Morphism f} {!Ring_Morphism g}: Injective g. -Proof. +Proof with intuition. constructor. 2: constructor; apply _. intros x y E. - rewrite <- (to_ring_unique' (f ∘ g) id x). - rewrite <- (to_ring_unique' (f ∘ g) id y). - unfold compose. rewrite E. reflexivity. + rewrite <- (to_ring_unique' (f ∘ g) id x x)... + rewrite <- (to_ring_unique' (f ∘ g) id y y)... + unfold compose. rewrite E... Qed. Instance integers_to_integers_injective {Integers Int} {Integers Int2} (f: Int → Int2) {!Ring_Morphism f}: @@ -80,11 +81,11 @@ Section retract_is_int. Lemma same_morphism: integers_to_ring Int R ∘ inverse f = h. Proof with auto. - intro x. + intros x y U. pose proof (to_ring_unique (h ∘ f)) as E. unfold compose in *. - rewrite <-E. apply sm_proper. - apply jections.surjective_applied. + rewrite <- E. apply sm_proper. + rewrite <- U. apply jections.surjective_applied. Qed. End for_another_ring.
61 src/theory/jections.v
 @@ -18,22 +18,32 @@ Section compositions. Proof. firstorder. Qed. Global Instance: Surjective f → Surjective g → Surjective (f ∘ g). - Proof with try apply _. + Proof with try apply _; intuition. constructor... - change (f ∘ (g ∘ gi ∘ fi) = id). - intro. unfold compose. pose proof (setoidmor_b f). - posed_rewrite (surjective g (fi x)). - posed_rewrite (surjective f x). - reflexivity. + pose proof (setoidmor_a f). + intros x y E. unfold compose. + posed_rewrite (surjective g (fi x) (fi x))... + posed_rewrite (surjective f x x)... Qed. Global Instance: Bijective f → Bijective g → Bijective (f ∘ g). End compositions. Lemma back {Bijective A B f}: f ⁻¹ ∘ f = id. (* a.k.a. "split-mono" *) -Proof. firstorder. Qed. +Proof. + intros x y E. + unfold compose. + destruct H. + unfold id, inverse. + apply bijective_injective. + destruct (bijective_surjective). + apply surjective. + destruct surjective_mor. + apply sm_proper. + assumption. +Qed. (* recall that "f ∘ f ⁻¹ = id" is just surjective. *) Lemma surjective_applied {Surjective A B f} x : f (f⁻¹ x) = x. @@ -50,28 +60,29 @@ Lemma alt_injective {Equiv A} {Equiv B} {f: A → B} {!Inverse f}: Setoid_Morphism f → Setoid_Morphism (f ⁻¹: B → A) → f ⁻¹ ∘ f = id → Injective f. -Proof with try tauto. +Proof with try tauto; intuition. intros ?? E. pose proof (setoidmor_a f). pose proof (setoidmor_b f). - constructor... - intros ?? E'. - rewrite <- (E x), <- (E y). - unfold compose. - rewrite E'... - intuition. + constructor. + intros ?? F. + rewrite <- (E x x), <- (E y y)... + unfold compose. + rewrite F... + tauto. Qed. Instance: ∀ {Bijective A B f}, Setoid_Morphism (f⁻¹). -Proof with try tauto. +Proof with try tauto; intuition. intros. pose proof (setoidmor_a f). pose proof (setoidmor_b f). constructor... repeat intro. apply (injective f). change ((f ∘ f ⁻¹) x = (f ∘ f ⁻¹) y). - do 2 rewrite (surjective f _)... + rewrite (surjective f x x)... + rewrite (surjective f y y)... Qed. Instance: ∀ {Inverse A B f}, Inverse (f ⁻¹) := λ _ _ f _, f. @@ -83,10 +94,11 @@ Proof with intuition. pose proof (setoidmor_b f). repeat (constructor; try apply _). intros x y E. - rewrite <- (surjective f x), <- (surjective f y). + rewrite <- (surjective f x x), <- (surjective f y y)... unfold compose. (* f_equal ?*) rewrite E... - intro. apply (injective f), (surjective f). + intros x y E. rewrite <- E. + apply bijective_applied. Qed. Hint Extern 4 (Bijective (inverse _)) => apply flip_bijection_pseudoinstance: typeclass_instances. @@ -104,8 +116,9 @@ Proof. pose proof (setoidmor_a f). pose proof (setoidmor_b f). intros. apply (injective f). - posed_rewrite (surjective f y). + posed_rewrite (surjective f y y). assumption. + reflexivity. Qed. Lemma cancel_left' {Bijective A B f} x y: f ⁻¹ x = y → x = f y. @@ -123,15 +136,17 @@ Proof with intuition. constructor. intros x y ?. apply (injective f). - rewrite (P x), (P y)... + rewrite (P x x), (P y y)... rewrite <-P... Qed. Instance Surjective_proper {Equiv A} {Equiv B} (f g: A → B) {finv: Inverse f}: f = g → Surjective g (inv:=finv) → Surjective f. -Proof with try apply _; try assumption. +Proof with try apply _; intuition. intros E [P [Q U Z]]. repeat constructor... - intro. unfold compose. rewrite (E (inverse f x)). apply P. - repeat intro. rewrite (E x), (E y). apply Z... + intros x y F. unfold compose. + rewrite <- F. + rewrite (E (inverse f x) (inverse f x))... apply P... + repeat intro. rewrite (E x x), (E y y)... Qed.
 @@ -0,0 +1,50 @@ + +Require Import + Program Morphisms + canonical_names + abstract_algebra + interfaces.monads + interfaces.functors. + +Section contents. + + Context {Monad M}. + + Instance liftM: SFmap M := λ {A B} (f: A → B) (ma: M A), ma >>= ret ∘ f. + + Instance: SFunctor M. + Proof with intuition. + pose proof (@mon_setoid M _ _ _ _). + constructor; intros; try apply _; unfold sfmap, liftM. + pose proof (setoidmor_a f). + pose proof (setoidmor_b f). + constructor; try apply _. + intros ?? E. rewrite E... + intros ?? E. repeat intro. + apply (@bind_proper M _ _ _ _ v _ w _)... + intros c d. intros. + unfold compose. + rewrite (E c d)... + intros x y E. + unfold id at 2. + rewrite <- E. + rewrite compose_id_right. + apply mon_runit; apply _. + intros x y E. + unfold compose at 3. + pose proof (setoidmor_a g). + pose proof (setoidmor_b g). + pose proof (setoidmor_b f). + rewrite mon_assoc; try apply _. + apply (bind_proper M x y E). + intros v w U. + unfold compose. + rewrite mon_lunit; try apply _. + rewrite U. + reflexivity. + Qed. + + Definition liftM2 {A B C} (f: A → B → C) (x: M A) (y: M B): M C := + xv ← x; yv ← y; ret (f xv yv). + +End contents.
18 src/theory/naturals.v
 @@ -29,9 +29,10 @@ Qed. Lemma to_semiring_unique' {Naturals N} {SemiRing SR} (f g: N → SR) {!SemiRing_Morphism f} {!SemiRing_Morphism g} : f = g. Proof. - intro. + intros x y E. rewrite (to_semiring_unique f). rewrite (to_semiring_unique g). + rewrite E. reflexivity. Qed. @@ -60,11 +61,11 @@ Qed. Lemma to_semiring_injective {Naturals N} {SemiRing A} (f: A → N) (g: N → A) {!SemiRing_Morphism f} {!SemiRing_Morphism g}: Injective g. -Proof. +Proof with intuition. constructor. 2: constructor; apply _. intros x y E. - rewrite <- (to_semiring_unique' (f ∘ g) id x). - rewrite <- (to_semiring_unique' (f ∘ g) id y). + rewrite <- (to_semiring_unique' (f ∘ g) id x x)... + rewrite <- (to_semiring_unique' (f ∘ g) id y y)... unfold compose. rewrite E. reflexivity. Qed. @@ -90,10 +91,11 @@ Section retract_is_nat. Lemma same_morphism: naturals_to_semiring N R ∘ inverse f = h. Proof with auto. - intro x. + intros x y F. pose proof (to_semiring_unique (h ∘ f)) as E. unfold compose in *. - rewrite <-E. apply sm_proper. + rewrite <- E. apply sm_proper. + rewrite <- F. apply jections.surjective_applied. Qed. End for_another_semiring. @@ -260,8 +262,8 @@ Section contents. rewrite A, E, F, B... Qed. - Lemma nat_distance_unique {a b: NatDistance N} x: a x = b x. - Proof. intro. apply nat_distance_unique_respectful; reflexivity. Qed. +(* Lemma nat_distance_unique {a b: NatDistance N} x: a x = b x. + Proof. intro. apply nat_distance_unique_respectful; reflexivity. Qed.*) Global Instance nat_distance_proper {!NatDistance N}: Proper ((=) ==> (=) ==> (=)) (λ x y: N,  (nat_distance x y)). (* Program *should* allow us to write plain nat_distance instead of the
8 src/theory/rationals.v
 @@ -21,11 +21,11 @@ Section alt_Build_Rationals. intro x. unfold Basics.compose, id in *. transitivity (inject (fst (inverse _ x)) * / inject (snd (inverse _ x))). - 2: apply sur. + 2: apply sur... pose proof (integers.to_ring_unique' (integers_to_ring (Z nat) A ∘ integers_to_ring Int (Z nat)) inject) as B. - pose proof (B (fst (inverse _ x))) as P1. simpl in P1. rewrite P1. - pose proof (B (snd (inverse _ x))) as P2. simpl in P2. rewrite P2. + pose proof (B (fst (inverse _ x)) (fst (inverse _ x)) (reflexivity _)) as P1. simpl in P1. rewrite P1. + pose proof (B (snd (inverse _ x)) (snd (inverse _ x)) (reflexivity _)) as P2. simpl in P2. rewrite P2. reflexivity. constructor; try apply _. intros x y E. @@ -80,7 +80,7 @@ Section isomorphism_is_rationals. Lemma isomorphism_is_rationals: Rationals F (inj_inv:=isomorphism_is_inj_inv). Proof. repeat (split; try apply _). - intros x. unfold id, compose, inverse, isomorphism_is_inj_inv, compose. + intros x y U. rewrite <- U. unfold id, compose, inverse, isomorphism_is_inj_inv, compose. apply (injective (inverse f)). rewrite <-(@surjective_applied _ _ _ _ _ inj_inv rationals_frac (inverse f x)) at 3. rewrite rings.preserves_mult, preserves_dec_mult_inv.
18 src/theory/sequences.v
 @@ -3,7 +3,7 @@ Set Automatic Introduction. Require Import Program theory.categories - functors + interfaces.functors abstract_algebra interfaces.sequences canonical_names. @@ -22,7 +22,11 @@ Section contents. pose proof (@setoidmor_a _ _ _ _ f _). pose proof (@monmor_b _ _ _ _ _ _ _ _ g _). pose proof (sequence_only_extend_commutes sq (f ∘ inject A) _) as E. + pose proof (_: Setoid_Morphism (f ∘ inject A)) as cm. rewrite (E f), (E g)... + apply (sequence_extend_morphism sq)... + apply cm. + apply cm. Qed. Lemma extend_comp @@ -40,17 +44,17 @@ Section contents. apply (sequence_only_extend_commutes sq (f ∘ g))... symmetry. rewrite <- (sequence_extend_commutes sq g _) at 1. - reflexivity. + apply sm_proper. Qed. - Lemma extend_inject A {Setoid A}: extend (inject A) = id. + Lemma extend_inject {Setoid A}: extend (inject A) = @id (sq A). Proof with try apply _. symmetry. apply (sequence_only_extend_commutes sq)... - intro. reflexivity. + apply sm_proper. Qed. Lemma fmap_alt {Equiv A} {Equiv B} (f: A → B): - Setoid_Morphism f → extend (inject B ∘ f) = fmap sq f. + Setoid_Morphism f → extend (inject B ∘ f) = (fmap sq f: sq A → sq B). Proof with try apply _. intros. pose proof (@setoidmor_a _ _ _ _ f _). @@ -76,7 +80,7 @@ Section contents. change (f = fold sq ∘ inject B ∘ f). rewrite fold_inject. rewrite compose_id_left. - reflexivity. + apply sm_proper. Qed. End contents. @@ -98,7 +102,7 @@ Section semiring_folds. rewrite <- extend_comp... rewrite compose_id_right. rewrite fold_map... - reflexivity. + apply sm_proper. Qed. End semiring_folds.
15 src/theory/setoids.v
 @@ -5,11 +5,15 @@ Set Automatic Introduction. Require Import Morphisms Setoid abstract_algebra Program. +Instance ext_eq_trans {Setoid A} {Setoid B}: Transitive (equiv: relation (A → B)). +Proof. intros ? y ???? w ?. transitivity (y w); firstorder. Qed. + +Instance ext_eq_sym {Setoid A} {Setoid B}: Symmetric (equiv: relation (A → B)). +Proof. firstorder. Qed. + Instance: Equiv Prop := iff. Instance: Setoid Prop. -Instance: ∀ A {Setoid B}, Setoid (A → B). - Instance sig_Setoid {Setoid A} (P: A → Prop): Setoid (sig P). Instance sigT_Setoid {Setoid A} (P: A → Type): Setoid (sigT P). @@ -39,7 +43,7 @@ Section product. Let product: Type := ∀ i, c i. - Global Instance: Equiv product := (∀ i, x i = y i). + Instance product_eq: Equiv product := (∀ i, x i = y i). Global Instance: Setoid product. Proof. @@ -69,7 +73,8 @@ Proof. constructor; try apply _. repeat intro. apply (injective f). pose proof (surjective f) as E. - rewrite (E x), (E y). assumption. + unfold compose in E. + rewrite (E x x), (E y y); intuition. Qed. Instance morphism_proper {ea: Equiv A} {eb: Equiv B}: Proper ((=) ==> (=)) (@Setoid_Morphism A B _ _). @@ -78,7 +83,7 @@ Proof. firstorder. intros x y E [AS BS P]. constructor; try apply _. intros v w E'. - rewrite <- (E v), <- (E w), E'. reflexivity. + rewrite <- (E v), <- (E w), E'; reflexivity. Qed. Lemma projected_equivalence {Setoid B} {f: A → B}: Equivalence (λ x y, f x = f y).
3 src/theory/ua_congruence.v
 @@ -19,6 +19,9 @@ Section contents. (* Given an equivalence on the algebra's carrier that respects its setoid equality... *) + Let hint' (a: sorts σ): Equiv (ua_products.carrier σ bool (fun _: bool => v) a). + Proof. apply setoids.product_eq. intro. apply _. Defined. + Context (e: ∀ s, relation (v s)). Section for_nice_e.
7 src/theory/ua_homomorphisms.v
 @@ -155,15 +155,16 @@ Implicit Arguments inverse [[A] [B] [Inverse]]. induction (σ o); simpl. intros. apply (injective (f t)). - pose proof (surjective (f t) o1). + pose proof (surjective (f t) o1 o1 (reflexivity o1)). transitivity o1... symmetry... intros P Q R S T x. apply IHo0. specialize (R (inv t x)). - pose proof (surjective (f t) x) as E. + pose proof (surjective (f t) x x) as E. rewrite E in R. - assumption. + assumption. + reflexivity. apply S. reflexivity. apply T. reflexivity. Qed.
14 src/theory/ua_products.v
 @@ -22,7 +22,13 @@ Section algebras. | ne_list.cons _ g => λ X X0, rec_impl g (λ i, X i (X0 i)) end. - Instance rec_impl_proper: ∀ o, Proper (equiv ==> equiv) (rec_impl o). + Let u (s: sorts sig): Equiv (forall i : I, carriers i s). + apply setoids.product_eq. + intro. apply _. + Defined. + + Instance rec_impl_proper: ∀ o, + Proper (@setoids.product_eq I _ (fun _ => op_type_equiv _ _ _) ==> equiv) (rec_impl o). Proof with auto. induction o; simpl. repeat intro... intros ? ? Y x0 y0 ?. apply IHo. @@ -103,7 +109,11 @@ Section varieties. (eval et vars term1 (eval et vars term2))). apply sig_type_refl. intro. apply _. - apply _. + apply eval_proper; try apply _. + apply product_algebra. + intro. apply _. + reflexivity. + reflexivity. apply (nqe_proper t (eval et vars term1 (eval et vars term2)) (eval et vars term1 (eval et vars term2)) H2 k p). subst p k. simpl.
 @@ -1,6 +1,6 @@ Require Import Morphisms Setoid - abstract_algebra universal_algebra monads canonical_names. + abstract_algebra universal_algebra interfaces.monads canonical_names. Section contents. @@ -100,7 +100,7 @@ Section contents. Instance: MonadReturn M := λ _ x, Var sign _ x tt. - Instance: ∀ {Equiv A}, Proper (equiv ==> equiv) (ret M). + Instance: ∀ {Equiv A}, Proper (equiv ==> equiv) (@ret M _ A). Proof. repeat intro. assumption. Qed. (* What remains are the laws: *)