Something in Cslib.Automata is interfering with Sum

Stream: CSLib

[Ching-Tsun Chou]

I think something in Cslib.Automata is interfering with Sum. For example, if a file contains only the following code:

open Sum
#check inl
#check inr

then everything works fine. However, if I put the above code in the Cslib.Automata namespace as follows:

import Cslib.Computability.Automata.NA
namespace Cslib.Automata

open Sum
#check inl
#check inr

end Cslib.Automata

then Lean claims that inl and inr are "unknown identifiers" and I have to use Sum.inl and Sum.inr to get them. I think something imported by Cslib.Computability.Automata.NA is interfering with Sum. (The problem disappears if the import is removed.) I see that there are LTS.inl and LTS.inr in Cslib.Foundations.Semantics.LTS.Basic. But the code above did not open LTS. Any idea what's going on?

[Chris Henson]

Hmm, I don't immediately understand why, but if you move open Sum to be first you no longer get an error.

[Ching-Tsun Chou]

Thanks for the idea! I encountered the problem while working on this branch:
https://github.com/ctchou/cslib/tree/na-sum-work
In the file Cslib/Computability/Automata/Sum.lean, if you move the open Sum to inside namespace Cslib.Automata, then the definition of sum fails (because Lean says inl and inr are undefined) but the theorem statement of sum_run_iff works. However, while working on its proof, I found that the inl and inr in the theorem statement seem to be resolved into something different from Sum.inl and Sum.inr.

[Ching-Tsun Chou]

In the branch, I'm working inside the namespace Cslib.Automata.NA, which extends LTS, which has methods LTS.inl and LTS.inr. Perhaps this has something to do with the problem? But the code example I gave above does not open NA, so presumably the methods of LTS are not exposed and should not cause any problem.

[Fabrizio Montesi]

Mmmh that's the only possible reason I can think of, yes..

Note that, as I noted in the docstring, the 'union' section for LTS is still under active development. If it causes trouble, we can just put it in a separate file for now. I guess it might be convenient to have union/product/intersection operations for (F)LTSs for automata theory though, but we don't need to do that now.

[Chris Henson]

I think this is a red herring. Just the Cslib namespace like

import Cslib
namespace Cslib
open Sum
#check inl
#check inr

also fails, even if I completely remove LTS.{inl,inr}.

[Eric Wieser]

I would guess that somewhere there is a Cslib.Sum namespace

[Chris Henson]

Eric Wieser said:

I would guess that somewhere there is a Cslib.Sum namespace

Ahh that's it, thanks! There are functions that should be in the Sum namespace, but were accidentally declared as Sum.{...} at the root of the Cslib namespace. I'll PR a fix.

[Fabrizio Montesi]

Ah yes, I can imagine which they are now. Thanks for digging. :slight_smile:

(Maybe the names of some of these functions need updating as well, iirc.)

[Chris Henson]

Actually they can be removed completely, as they are the same as docs#Sum.isLeft_inl and docs#Sum.isRight_inr.

[Fabrizio Montesi]

Even better!

[Chris Henson]

cslib#162