Four Approaches to Automated Reasoning with Differential Algebraic Structures - Artificial Intelligence and Symbolic Computation - page 231

Example 2. assumes p, D, D ◦ h, D, D = h, D, D

shows id − p, D, ker p ◦ h, D, D = 0 ,D, ker p

proof -
have id − p, D, D ◦ h, D, D =( id D, D − p, D, D ) ◦ h, D, D

(...)
also have ··· = 0 ,D,D

finally have one: id − p, D, D ◦ h, D, D = 0 ,D,D

from prems have two: im(id − p ) ⊆ ker p

from one and two
have (

id − p, D, D ◦ h, D, D = 0 ,D,D ) ≡ ( id − p, D, ker p ◦ h, D, D =

0 ,D, ker p )

In order to obtain this degree of expressiveness, two major modifications must
be made. The first one is related to the implementation of homomorphisms. The
information about their domain and codomain must be explicit, otherwise it
is not possible to convert them from

then show id − p, D, ker p ◦ h, D, D = 0 ,D, ker p qed

. Secondly, some
lemmas allowing to modify these triples must be introduced (and proved) in
Isabelle. These lemmas permit to change the domain and codomain of homo-
morphism provided that certain conditions are satisfied; when the composition
of two homomorphisms is equal to a third one, the domain and codomain of
the three homomorphisms can be changed and the equality holds. This collec-
tion of lemmas can be summarized in the following one, a generic version of
all of them where all the algebraic structures (domains and codomains of the
homomorphisms) can be changed:
Lemma 7. Laureano's Lemma -Let

f, D, D to f, D, ker p

g, C, D and f, A, B be two homomor-

phisms between chain complexes satisfying and let

A be a chain subcomplex from A , B a chain subcomplex from C , im f contained
on B ,and im h contained on D .Then

g, C, D ◦ f, A, B = h, A, D

g, C ,D ◦ f, A ,B h, A ,D .

With this lemma and the new proposed representation for homomorphisms a
framework with the following advantages is built. From the point of view of ca-
pability, it is possible to implement all the properties needed for Lemma 2. It
should be also emphasized that the size of the proofs is manageable and some-
times the proofs require some human guidance in order to finish. Moreover, the
framework can be transferred to other problems dealing with homomorphisms
and particular reasoning about them. Embedding homomorphisms (even be-
tween different algebraic structures) in only one algebraic structure can help to
easily implement proofs of properties about these homomorphisms (and avoids
the implementation of more elaborated algebraic structures); moreover, Lemma 7
can be easily generalized for compositions of n homomorphisms. From the formal
point of view, all the computations are carried out in this algebraic structure
and all the operations needed can be identified as simplifications inside the ring,
or applications of Lemma 7; the abstraction process from the implemented proof
to the mathematical proof can be accurately defined.
On the other hand, the amount of concepts that need to be mechanized is
rather large. In addition to this, we have observed that the implementation of

=