Right- vs left-pointing vectors and addition

[conal]

This PR adds left-pointing vectors Vˡ and renames V to “Vʳ”. It also changes Examples.Add to use Vˡ as mentioned in a comment there:

Note for a ⇨ᶜ b that the carry-in denotes 0 or 1, while the carry-out denotes (in these examples) 0 or 2^n. Positioning carry-in on the one side and carry-out on the other helps definitions below come out more simply. Left-in and right-out reflect the little-endian interpretation and use of left-pointing vectors, Vˡ. Choosing Vˡ rather than the more common Vʳ reflects the practice of writing least significant bit on the right and most significant on the left.

A syntactic convenience of using right-pointing vectors instead is that _,_ is right-associative, so right-pointing vectors print as “a , b , c , d , tt”, while left-pointing vectors print as “(((tt , a) , b) , c) , d”. To eliminate this syntactic burden, I defined the following pattern:

-- *Left*-associative pairing. Handy for notating left-pointing vectors
infixl 4 _،_
pattern _،_ a b = a , b

so that one can write “tt ، a ، b ، c ، d” instead as an expression or a pattern. This trick worked, but then Agda wants to change all uses of _,_ patterns into _،_ when doing automatic proof search and case splitting.

Sigh.

I’m inclined to abandon this whole experiment and accept MSB on the right instead of the left.

Thoughts?

[bolt12]

Is it maybe a naming issue? what if you chose maybe name for the pattern?

[conal]

Is it maybe a naming issue? what if you chose maybe name for the pattern?

I'm afraid I don't understand the queston/suggestion.

[bolt12]

Nevermind I understood it the other way around. What if you define 2 patterns with different names for left and right associative , ?

[conal]

Nevermind I understood it the other way around. What if you define 2 patterns with different names for left and right associative _,_?

Thanks for the suggestion. Here’s an experiment:

open import Data.Product
open import Data.Bool

infixr 4 _،_
pattern _،_ a b = a , b

infixl 4 _、_
pattern _、_ a b = a , b

right : Bool × (Bool × Bool) → Bool
right (x ، y ، z) = {! y !}

left : (Bool × Bool) × Bool → Bool
left (x 、 y 、 z) = {! y !}

If I do C-c C-c (agda2-make-case) in the right hole, I get

right : Bool × (Bool × Bool) → Bool
right (x ، false ، z) = {!!}
right (x ، true ، z) = {!!}

The same operation in the left hole gives

left : (Bool × Bool) × Bool → Bool
left ((x ، false) ، z) = {!!}
left ((x ، true) ، z) = {!!}

I think Agda has no way to know which synonym I want here and is aggressively helpful in introducing pattern synonyms. Usually I appreciate that help, but not this time.