[Agda] Termination checker on commutative functions

[Jesper Cockx]

Hi Jacek,

The best way I know to deal with these kind of situations is to define a
'view' type that makes the cases you want to consider explicit.

```
case_of_ : {A B : Set} → A → (A → B) → B
case x of f = f x

data Case-f : Set where
  A-A : X → X → Case-f
  A-B : X → Y → Case-f
  A-C : X → Z → Case-f
  -- etc

view-f : T → T → Case-f
view-f (A x₁) (A x₂) = A-A x₁ x₂
view-f (A x)  (B y ) = A-B x y
view-f (A x)  (C z ) = A-C x z
view-f (B y)  (A x ) = A-B x y
view-f (C z)  (A x ) = A-C x z
view-f (C z)  (B y ) = {!etc!}

f : T → T → T'
f x y = case (view-f x y) of λ where
  (A-A x₁ x₂) → {!complicated stuff!}
  (A-B x  y ) → {!more complicated stuff!}
  (A-C x  z ) → {!even more complicated stuff!}
```

This is a bit more verbose to begin with, but it usually pays off to have a
view type when you want to prove stuff about the function f, since you are
now better equipped to talk about the symmetric cases without repeating
yourself.

-- Jesper

On Thu, Nov 7, 2019 at 9:18 AM Jacek Karwowski <jac.karwowski at gmail.com>
wrote:

> Hi Jesper,
>
> Thanks for your response and your time. This indeed solves the example toy
> problem, but it does that by exploiting some structure in this code (this
> obviously means it wasn't a good example to begin with, sorry about that).
> What I'm looking for, In general, is a fully general solution that treats
> the constructors as more-or-less black boxes (in particular, under
> assumption that there's no easy way of defining functions over subsets of
> them, like you did with substraction).
>
> Let's say there are three constructors:
> ```
> postulate
>   X : Set
>   Y : Set
>   Z : Set
>   T' : Set
>
> data T : Set where
>   A : X -> T
>   B : Y -> T
>   C : Z -> T
> ```
>
> and I'd now like to define a commutative function over them.
>
> ```
> f : T -> T -> T'
> f (A x) (A x) = (some complicated definition using the specifics of x's)
> f (A x) (B y) = (some complicated definition using the specifics of x's
> and y's)
> f (A x) (C z) = (some complicated definition using the specifics of x's
> and z's)
> -- etc for all other required cases
> -- and now I don't want to repeat code from above, but I want to be able
> to define
> f (B y) (A x) = f (A x) (B y)
> f (C z) (A x) = f (A x) (C z)
> f (C z) (B y) = f (B y) (C z)
> ```
>
> There's no easy way of refactoring out these particular cases, and then
> just using this refactored-out function with changed order of arguments.
> So, is there any "idiomatic" way of dealing with these kinds of situations?
>
> Best
> Jacek
>
> On Thu, Oct 31, 2019 at 5:03 AM Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> Hi Jacek,
>>
>> The easiest solution here would be to first define a helper function for
>> subtraction on `Nat`, and then use it to deal with the two symmetric cases:
>>
>> ```
>> module _ where
>>
>> open import Agda.Builtin.Nat
>>
>> data Int : Set where
>>   Pos : (x : Nat) → Int
>>   Neg : (x : Nat) → Int
>>
>> _⊝Nat_ : Nat → Nat → Int
>> x       ⊝Nat zero    = Pos x
>> zero    ⊝Nat y       = Neg y
>> (suc x) ⊝Nat (suc y) = x ⊝Nat y
>>
>> _⊕_ : Int → Int → Int
>> Pos x ⊕ Pos y = Pos (x + y)
>> Neg x ⊕ Neg y = Neg (x + y)
>> Pos x ⊕ Neg y = x ⊝Nat y
>> Neg x ⊕ Pos y = y ⊝Nat x
>> ```
>>
>> -- Jesper
>>
>> On Thu, Oct 31, 2019 at 2:00 AM Jacek Karwowski <jac.karwowski at gmail.com>
>> wrote:
>>
>>> Hi,
>>>
>>> I'm trying to write a commutative function over some type, and not
>>> repeat the code in the process.
>>>
>>> The toy example is as follows:
>>> ```
>>> module _ where
>>>
>>> open import Data.Nat
>>>
>>> data Int : {i : Size} -> Set where
>>>   Pos : (x : ℕ) -> Int
>>>   Neg : (x : ℕ) -> Int
>>>
>>> _⊕_ : Int -> Int -> Int
>>> Pos x ⊕ Pos y = Pos (x + y)
>>> Neg x ⊕ Neg y = Neg (x + y)
>>> Pos x ⊕ Neg zero = Pos x
>>> Pos zero ⊕ Neg y = Neg y
>>> Pos (suc x) ⊕ Neg (suc y) = (Pos x) ⊕ (Neg y)
>>> --- problematic call
>>> Neg x ⊕ Pos y = (Pos y) ⊕ (Neg x)
>>> ```
>>> In the example above, termination checker complains about the last call,
>>> since it is not a structural recursion.
>>>
>>> (Of course, real types can (and do) have more than two constructors, the
>>> constructors are recursive, etc.)
>>>
>>> The naive, manual way I see would be to introduce an explicit order on
>>> the constructors by some external function, and then call ⊕ passing this
>>> parameter over:
>>>
>>> ```
>>> ord : Int -> ℕ
>>> ord (Pos _) = 0
>>> ord (Neg _) = 1
>>>
>>> _⊕_ : {s : ℕ} -> (x : Int) -> {s ≡ ord x} -> Int -> Int
>>> Pos x ⊕ Pos y = Pos (x + y)
>>> Neg x ⊕ Neg y = Neg (x + y)
>>> Pos x ⊕ Neg zero = Pos x
>>> Pos zero ⊕ Neg y = Neg y
>>> Pos (suc x) ⊕ Neg (suc y) = _⊕_ {zero} (Pos x) {refl} (Neg y)
>>> --- problematic call
>>> _⊕_ {suc zero} (Neg x) (Pos y) = _⊕_ {zero} (Pos y) {refl} (Neg x)
>>> ```
>>> but this ends up being very ugly and hard to read.
>>>
>>> What is the idiomatic way of handling these types of situations,
>>> introducing as little code overhead as possible?
>>>
>>> Thanks,
>>> Jacek
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>
> --
> Best regards
> Jacek Karwowski
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191107/e182dd3e/attachment.html>