<div dir="ltr"><div><div><div>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'.<br><br></div>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.</div><div><br></div><div>Here is qun with auxiliary functions and partial abstraction. :</div><div><br></div><div>```</div><div>cun-aux : A → A → A<br>cun-aux a a1 = a1<br>cun-aux a a2 = a1<br><br>cun' : A → A<br>cun' a = cun-aux a (fun a)<br><br>gun-aux2 : (a : A) → cun-aux a a1 ≡ a1 → A → A<br>gun-aux2 a c a1 = a1<br>gun-aux2 a c a2 = a1<br><br>gun-aux1 : (a : A) → (w : A) → cun-aux a w ≡ a1 → A<br>gun-aux1 a a1 c = gun-aux2 a c (bun a)<br>gun-aux1 a a2 c = a1<br><br>gun' : (a : A) → cun' a ≡ a1 → A<br>gun' a c = gun-aux1 a (fun a) c<br><br><br>dun-aux2 : (a : A) → (w : A) → cun-aux a w ≡ a1 → A<br>dun-aux2 a a1 c = a1<br>dun-aux2 a a2 c = a1<br><br>dun-aux1 : (a : A) → cun' a ≡ a1 → A → A<br>dun-aux1 a c a1 = dun-aux2 a (fun a) c<br>dun-aux1 a c a2 = a1<br><br>dun' : (a : A) → cun' a ≡ a1 → A<br>dun' a c = dun-aux1 a c (bun a)<br><br><br>qun-aux31 : (a : A) → (w : A) → (a1 ≡ w) → (cp : cun-aux a w ≡ a1) → a1 ≡ dun-aux2 a w cp<br>qun-aux31 a .a1 refl cp = refl<br><br><br>qun-aux32 : (a : A) → (w : A) → (a2 ≡ w) → (cp : cun-aux a w ≡ a1) → a1 ≡ dun-aux2 a w cp<br>qun-aux32 a .a2 refl cp = refl<br><br>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<br>qun-aux21 a c eq cp a1 = qun-aux31 a (fun a) eq cp<br>qun-aux21 a c eq cp a2 = refl<br><br>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<br>qun-aux22 a c eq cp a1 = qun-aux32 a (fun a) eq cp<br>qun-aux22 a c eq cp a2 = refl<br><br>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<br>qun-aux1 a a1 c eq cp = qun-aux21 a c eq cp (bun a)<br>qun-aux1 a a2 c eq cp = qun-aux22 a c eq cp (bun a)<br><br>qun' : (a : A) → (c : cun' a ≡ a1) → gun' a c ≡ dun' a c<br>qun' a c = qun-aux1 a (fun a) c refl c<br><br></div><div>```<br></div><div><b><br></b></div><div><b>~~~~<br></b></div>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.<br>~~~~<br><br></div>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. <br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 12, 2017 at 7:25 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hello, I have something similar to the below :<br><br>```<br>open import Relation.Binary.<wbr>PropositionalEquality<br><br>data A : Set where<br>  a1 : A<br>  a2 : A<br><br><br><br>fun : A → A<br>fun a1 = a2<br>fun a2 = a1<br><br>bun : A → A<br>bun a1 = a2<br>bun a2 = a1<br><br>cun : A → A<br>cun a with fun a<br>cun a | a1 = a1<br>cun a | a2 = a1<br><br>gun : (a : A) → cun a ≡ a1 → A<br>gun a c with fun a<br>gun a c | a1 with bun a<br>gun a c | a1 | a1 = a1<br>gun a c | a1 | a2 = a1<br>gun a c | a2 = a1<br><br>dun : (a : A) → cun a ≡ a1 → A<br>dun a c with bun a<br>dun a c | a1 with fun a<br>dun a c | a1 | a1 = a1<br>dun a c | a1 | a2 = a1<br>dun a c | a2 = a1<br><br>--qun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c<br>--qun a c with fun a<br>--... | z = ?<br><br><br>pun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c<br>pun a c with bun a<br>pun a c | a1 with fun a<br>pun a c | a1 | a1 with bun a<br>pun a c | a1 | a1 | a1 = refl<br>pun a c | a1 | a1 | a2 = refl<br>pun a c | a1 | a2 = refl<br>pun a c | a2 with fun a<br>pun a c | a2 | a1 with bun a<br>pun a c | a2 | a1 | a1 = refl<br>pun a c | a2 | a1 | a2 = refl<br>pun a c | a2 | a2 = refl<br><br>```<br><br></div>Could someone explain to me why qun returns an error?<br><br></div>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.<br></div><div>Given gun and dun, is there a way to simplify pun, possibly removing the second bun abstraction?<br></div><div><br> <br></div></div>
</blockquote></div><br></div>