Verify that all derivations have correct source and range

[zickgraf]

using the code in zickgraf@e0b9edf.

Currently, there are many false positives because of missing output_source/range_getter_strings (which means CompilerForCAP cannot determine the source/range of an operation) and because of missing WithGiven versions of operations (which means the given source or range cannot be passed through to the result).

[TKuh]

using the code in zickgraf@e0b9edf.

I'm currently working through the list your code generates and several derivations are from MonoidalCategories. Typically, both the closed and coclosed cases of a derivation are affected. In theory, I should now be able to use your code from #1468 to generate the coclosed derivations, right? :)
I just want to be sure I can (for now) safely skip the coclosed cases.

[zickgraf]

I'm currently working through the list your code generates and several derivations are from MonoidalCategories.

Nice :-)

Typically, both the closed and coclosed cases of a derivation are affected. In theory, I should now be able to use your code from #1468 to generate the coclosed derivations, right? :)

In theory, yes. In practice I'm not working on this right now and there are still some engineering problems to be solved, so there is no timeline for this from my side.

I just want to be sure I can (for now) safely skip the coclosed cases.

"Skip" in the sense of "not look at" or in the sense of "not fix"? If you find an error in the closed case, it would be very nice if you could also fix the coclosed case.

When applying #1468 for the first time, one should compare the autogenerated derivations to the existing ones to catch errors like #1465. So any error/inconsistency fixed beforehand makes this comparison easier.

[TKuh]

I just want to be sure I can (for now) safely skip the coclosed cases.

"Skip" in the sense of "not look at" or in the sense of "not fix"? If you find an error in the closed case, it would be very nice if you could also fix the coclosed case.

I'll give you an example of what I mean: the following derivation is missing a lot of WithGiven's

CAP_project/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi

Lines 728 to 757 in d726b24

	hom_a_b := InternalHomOnObjects( cat, a, b );
	hom_b_c := InternalHomOnObjects( cat, b, c );
	morphism := PreComposeList( cat,
	TensorProductOnObjects( cat,
	source,
	a ),
	[ AssociatorLeftToRight( cat, hom_a_b, hom_b_c, a ),
	TensorProductOnMorphisms( cat,
	IdentityMorphism( cat, hom_a_b ),
	Braiding( cat, hom_b_c, a ) ),
	AssociatorRightToLeft( cat, hom_a_b, a, hom_b_c ),
	TensorProductOnMorphisms( cat,
	EvaluationMorphism( cat, a, b ),
	IdentityMorphism( cat, hom_b_c ) ),
	Braiding( cat, b, hom_b_c ),
	EvaluationMorphism( cat, b, c ) ],
	c );
	return TensorProductToInternalHomAdjunctionMapWithGivenInternalHom( cat,
	source,
	a,
	morphism,
	range );

It's dual derivation has the same issue:

CAP_project/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi

Lines 740 to 771 in d726b24

	cohom_a_b := InternalCoHomOnObjects( cat, a, b );
	cohom_b_c := InternalCoHomOnObjects( cat, b, c );
	morphism := PreComposeList( cat,
	a,
	[ CoclosedEvaluationMorphism( cat, a, b ),
	Braiding( cat, cohom_a_b, b ),
	TensorProductOnMorphisms( cat,
	CoclosedEvaluationMorphism( cat, b, c ),
	IdentityMorphism( cat, cohom_a_b ) ),
	AssociatorLeftToRight( cat, cohom_b_c, c, cohom_a_b ),
	TensorProductOnMorphisms( cat,
	IdentityMorphism( cat, cohom_b_c ),
	Braiding( cat, c, cohom_a_b ) ),
	AssociatorRightToLeft( cat, cohom_b_c, cohom_a_b, c ) ],
	TensorProductOnObjects( cat,
	range,
	c ) );
	return TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( cat,
	range,
	c,
	morphism,
	source );
	end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );

This dual derivation works fine and has no bug (I think). So I hoped, if I add these WithGiven's in the closed case, I could for now skip adding them in the coclosed case and later just generate the coclosed case, and get the WithGiven's there too.

All of what I encountered until now in MonoidalCategories is of the above type.
If I encounter something that really doesn't work and requires a fix, then I'll fix it.

In theory, yes. In practice I'm not working on this right now and there are still some engineering problems to be solved, so there is no timeline for this from my side.

I'm fine with doing both cases by hand if you advise this; it's just quite time consuming and error prone, so I hoped to be more efficient. :)

[zickgraf]

So I hoped, if I add these WithGiven's in the closed case, I could for now skip adding them in the coclosed case and later just generate the coclosed case, and get the WithGiven's there too.

Ah, now I understand. I think modifying only the closed case but not the coclosed case is not a good idea: This introduces unexpected asymmetries which in turn can lead to weird issues like #917.

I'm fine with doing both cases by hand if you advise this; it's just quite time consuming and error prone, so I hoped to be more efficient. :)

I see the following options:

1. Ignore these cases manually for now.
2. Extend the checks in the following way: For WithGiven operations additionally look at the source/range of the non-WithGiven operation and only display an error if this does not match either.
3. Modify both the closed and the coclosed cases manually.
4. Make the automatic dualization work for MonoidalCategories before continuing here.

I'll give you an example of what I mean: the following derivation is missing a lot of WithGiven's

CAP_project/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi

Lines 728 to 757 in d726b24

	hom_a_b := InternalHomOnObjects( cat, a, b );
	hom_b_c := InternalHomOnObjects( cat, b, c );
	morphism := PreComposeList( cat,
	TensorProductOnObjects( cat,
	source,
	a ),
	[ AssociatorLeftToRight( cat, hom_a_b, hom_b_c, a ),
	TensorProductOnMorphisms( cat,
	IdentityMorphism( cat, hom_a_b ),
	Braiding( cat, hom_b_c, a ) ),
	AssociatorRightToLeft( cat, hom_a_b, a, hom_b_c ),
	TensorProductOnMorphisms( cat,
	EvaluationMorphism( cat, a, b ),
	IdentityMorphism( cat, hom_b_c ) ),
	Braiding( cat, b, hom_b_c ),
	EvaluationMorphism( cat, b, c ) ],
	c );
	return TensorProductToInternalHomAdjunctionMapWithGivenInternalHom( cat,
	source,
	a,
	morphism,
	range );

Does this derivation show up as having the wrong source or range? Since the last function call is a WithGiven operation, I expect no problem here.

[TKuh]

1. Ignore these cases manually for now.

2. Extend the checks in the following way: For WithGiven operations additionally look at the source/range of the non-WithGiven operation and only display an error if this does not match either.

3. Modify both the closed and the coclosed cases manually.

4. Make the automatic dualization work for MonoidalCategories before continuing here.

Then I'll also make the corresponding coclosed changes (for everything I changed until now) to avoid asymmetries and then give the automatic dualization a try. If I can't get it to work, I'll continue doing it manually.

Does this derivation show up as having the wrong source or range? Since the last function call is a WithGiven operation, I expect no problem here.

At least its range is fine, I haven't checked sources, yet (but I guess here the source should be fine, too). What triggered an error is the comparison of compiled code at the end of your code (in the range case). I think because not all operations could be resolved, because of missing WithGiven's. After adding WithGiven's, compiling gave equal code.

[TKuh]

Something else I just noticed: many (all?) operations which return an isomorphism (e.g. IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram) do not have source/range getters. Is this on purpose (maybe related to your explanation here?) or are they just missing? This seems to be another big source for errors your code generates.

[zickgraf]

What triggered an error is the comparison of compiled code at the end of your code (in the range case). I think because not all operations could be resolved, because of missing WithGiven's. After adding WithGiven's, compiling gave equal code.

I think I have found the culprit: You are probably using zickgraf@e0b9edf as-is, right? That's a very old commit. @mohamed-barakat has recently added many WithGivens in b6e2ea5. You can find a rebased version of my commit by looking for Add CheckDerivationSourceAndRange on my math_output branch. Probably you can just check out that branch, although it contains many things not related to CheckDerivationSourceAndRange at all.

Something else I just noticed: many (all?) operations which return an isomorphism (e.g. IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram) do not have source/range getters. Is this on purpose (maybe related to your explanation here?)

Yes, those isomorphisms are mainly used for deriving one concept from another, including objects, e.g. DirectProduct from DirectSum. In this context, WithGiven versions do not make sense, because you obviously cannot derive DirectProduct from ...WithGivenDirectProduct.

[TKuh]

Thanks!

[zickgraf]

@TKuh FYI: I have removed the commit containing CheckDerivationSourceAndRange from my branch math_output and have instead created a new branch CheckDerivationSourceAndRange with only that commit.