[Agda] Help with With-permutations.

[Apostolis Xekoukoulotakis]

Ok, so one needs to look whether a with abstraction changes the type of a
variable and then if that variable is used by a function that can not be
abstracted. In this case, 'dun' requires a non-abstracted version of 'c'.

If we really wanted to abstract over 'fun' first, it is impossible to do
with 'with'-abstractions. It would require a notion of best-effort or
partial with-abstraction.

Here is qun with auxiliary functions and partial abstraction. :

```
cun-aux : A → A → A
cun-aux a a1 = a1
cun-aux a a2 = a1

cun' : A → A
cun' a = cun-aux a (fun a)

gun-aux2 : (a : A) → cun-aux a a1 ≡ a1 → A → A
gun-aux2 a c a1 = a1
gun-aux2 a c a2 = a1

gun-aux1 : (a : A) → (w : A) → cun-aux a w ≡ a1 → A
gun-aux1 a a1 c = gun-aux2 a c (bun a)
gun-aux1 a a2 c = a1

gun' : (a : A) → cun' a ≡ a1 → A
gun' a c = gun-aux1 a (fun a) c


dun-aux2 : (a : A) → (w : A) → cun-aux a w ≡ a1 → A
dun-aux2 a a1 c = a1
dun-aux2 a a2 c = a1

dun-aux1 : (a : A) → cun' a ≡ a1 → A → A
dun-aux1 a c a1 = dun-aux2 a (fun a) c
dun-aux1 a c a2 = a1

dun' : (a : A) → cun' a ≡ a1 → A
dun' a c = dun-aux1 a c (bun a)


qun-aux31 : (a : A) → (w : A) → (a1 ≡ w) → (cp : cun-aux a w ≡ a1) → a1 ≡
dun-aux2 a w cp
qun-aux31 a .a1 refl cp = refl


qun-aux32 : (a : A) → (w : A) → (a2 ≡ w) → (cp : cun-aux a w ≡ a1) → a1 ≡
dun-aux2 a w cp
qun-aux32 a .a2 refl cp = refl

qun-aux21 : (a : A) → (c : cun-aux a a1 ≡ a1) → (a1 ≡ fun a) → (cp : cun' a
≡ a1) → (w : A) → gun-aux2 a c w ≡ dun-aux1 a cp w
qun-aux21 a c eq cp a1 = qun-aux31 a (fun a) eq cp
qun-aux21 a c eq cp a2 = refl

qun-aux22 : (a : A) → (c : cun-aux a a2 ≡ a1) → (a2 ≡ fun a) → (cp : cun' a
≡ a1) → (w : A) → a1 ≡ dun-aux1 a cp w
qun-aux22 a c eq cp a1 = qun-aux32 a (fun a) eq cp
qun-aux22 a c eq cp a2 = refl

qun-aux1 : (a : A) → (w : A) → (c : cun-aux a w ≡ a1) → (w ≡ fun a) → (cp :
cun' a ≡ a1) → gun-aux1 a w c ≡ dun' a cp
qun-aux1 a a1 c eq cp = qun-aux21 a c eq cp (bun a)
qun-aux1 a a2 c eq cp = qun-aux22 a c eq cp (bun a)

qun' : (a : A) → (c : cun' a ≡ a1) → gun' a c ≡ dun' a c
qun' a c = qun-aux1 a (fun a) c refl c

```


*~~~~*
Given that 'with' auxiliary functions are not available and that there is
no notion of partial with abstraction, it seems possible to me to end up in
an order of required 'with'-abstractions that blocks us from going forward.
~~~~

I am thinking of reverting to using auxiliary functions to perform
abstractions. The downside is that it requires more lines of code and good
name conventions.

On Thu, Oct 12, 2017 at 7:25 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> Hello, I have something similar to the below :
>
> ```
> open import Relation.Binary.PropositionalEquality
>
> data A : Set where
>   a1 : A
>   a2 : A
>
>
>
> fun : A → A
> fun a1 = a2
> fun a2 = a1
>
> bun : A → A
> bun a1 = a2
> bun a2 = a1
>
> cun : A → A
> cun a with fun a
> cun a | a1 = a1
> cun a | a2 = a1
>
> gun : (a : A) → cun a ≡ a1 → A
> gun a c with fun a
> gun a c | a1 with bun a
> gun a c | a1 | a1 = a1
> gun a c | a1 | a2 = a1
> gun a c | a2 = a1
>
> dun : (a : A) → cun a ≡ a1 → A
> dun a c with bun a
> dun a c | a1 with fun a
> dun a c | a1 | a1 = a1
> dun a c | a1 | a2 = a1
> dun a c | a2 = a1
>
> --qun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c
> --qun a c with fun a
> --... | z = ?
>
>
> pun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c
> pun a c with bun a
> pun a c | a1 with fun a
> pun a c | a1 | a1 with bun a
> pun a c | a1 | a1 | a1 = refl
> pun a c | a1 | a1 | a2 = refl
> pun a c | a1 | a2 = refl
> pun a c | a2 with fun a
> pun a c | a2 | a1 with bun a
> pun a c | a2 | a1 | a1 = refl
> pun a c | a2 | a1 | a2 = refl
> pun a c | a2 | a2 = refl
>
> ```
>
> Could someone explain to me why qun returns an error?
>
> In my code, I have pun in the type of the function I am working on and I
> also have problems with with abstraction there.
> Given gun and dun, is there a way to simplify pun, possibly removing the
> second bun abstraction?
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171013/03a15087/attachment.html>