<div dir="ltr">The trick is to also abstract over the recursive call:<div><br></div><div><div><div><font face="monospace, monospace" size="1">f : {b : ℕ} → (a : A b) → subst A (eq b) (h a) ≡ a</font></div><div><font face="monospace, monospace" size="1">f {zero} cz = refl</font></div><div><font face="monospace, monospace" size="1">f {suc b} (ca n) with b + zero | eq b | h n | f n</font></div><div><font face="monospace, monospace" size="1">... | .b | refl | hn | ih = cong ca ih</font></div></div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, May 5, 2017 at 6:43 AM, 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>I think to have solved the problem by first proving heterogeneous equality and then abstracting function h.<br></div>I made a concrete example below. You can try filling the hole and see if you can prove the statement without using heterogeneous equality.<br><div><div><br>```<br>module test where<br><br>open import Data.Nat<br><br>module _ where<br> open import Relation.Binary.<wbr>PropositionalEquality<br> <br> <br> data A : ℕ → Set where<br> cz : A zero<br> ca : {n : ℕ} → A n → A (suc n)<br> <br> h : {b : ℕ} → A b → A (b + zero)<br> h cz = cz<br> h (ca a) = ca (h a)<br> <br> eq : (c : ℕ) → (c + zero) ≡ c<br> eq zero = refl<br> eq (suc c) = cong (λ x → suc x) (eq c)<br> <br> f : {b : ℕ} → (a : A b) → subst A (eq b) (h a) ≡ a<br> f {zero} cz = refl<br> f {suc b} (ca n) = {!!} -- with (b + zero) | (eq b)<br> -- ... | g | r = ?<br> <br><br>module _ where<br> open import Relation.Binary.<wbr>HeterogeneousEquality<br><br> g : {b : ℕ} → (a : A b) → h a ≅ a<br> g cz = refl<br> g (ca {n} a) = cong₂ {B = A} {C = (λ x y → A (suc x))} (λ x y → ca {n = x} y) (≡-to-≅ (eq n)) (g a)<br><br><br>module _ where<br> open import Relation.Binary.<wbr>PropositionalEquality<br> open import Relation.Binary.<wbr>HeterogeneousEquality using (_≅_ ; refl ; ≅-to-≡)<br><br> af : (b w : ℕ) (eq : w ≡ b) (a : A b) → (h : A b → A w) → (h a ≅ a)<br> → subst A eq (h a) ≡ a<br> af b .b refl a h hteq = ≅-to-≡ hteq <br><br><br> fg : {b : ℕ} → (a : A b) → subst A (eq b) (h a) ≡ a<br> fg {b} a = af b (b + zero) (eq b) a h (g a)<br><br><br>```<br></div></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, May 4, 2017 at 3:06 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><br>
<br>
On 04/05/17 06:44, <a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmai<wbr>l.com</a> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This seems to be closer to what my code actually looks like:<br>
<br>
postulate<br>
B : Set<br>
A : B → Set<br>
big_expression : (c : B) → {b : B} → (a : A b) → B<br>
h : (c : B) → {b : B} → (a : A b) → A (big_expression c a)<br>
eq : (c : B) → {b : B} → (a : A b) → (big_expression c a) ≡ c<br>
<br>
f : {b : B} → (a : A b) → subst A (eq b a) (h b a) ≡ a<br>
f = {!!}<br>
</blockquote>
<br></span>
We have<br>
<br>
eq b a : big_expression b a = b<br>
h b a : A(big_expression b a)<br>
<br>
Consider the instantiations<br>
<br>
A b = Bool<br>
big_expression c {b} a = c<br>
h c {b} a = true<br>
eq b a = refl<br>
<br>
So the type subst A (eq b a) (h b a) ≡ a amounts to<br>
<br>
subst A refl true = a,<br>
<br>
that is,<br>
true = a.<br>
<br>
Hence we have<br>
<br>
f : {b : B} → (a : Bool) → true ≡ a<br>
<br>
which of course can't be proved.<br>
<br>
Hence, in the generality you have things above, you can't complete the<br>
definition of f.<br>
<br>
Of course it may well be that for your specific B, A, big_expression,<br>
h and eq, you can complete the definition of f.<br>
<br>
You will need to cook-up a more specific abstraction of your code<br>
for us to be able to help more here in this list.<br>
<br>
I hope this helps.<span class="m_-3071020664679365667HOEnZb"><font color="#888888"><br>
<br>
Martin<br>
</font></span></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>