[Agda] Help at propositional equality proof that contains subst.

[Apostolis Xekoukoulotakis]

I think to have solved the problem by first proving heterogeneous equality
and then abstracting function h.
I made a concrete example below. You can try filling the hole and see if
you can prove the statement without using heterogeneous equality.

```
module test where

open import Data.Nat

module _ where
  open import Relation.Binary.PropositionalEquality


  data A : ℕ → Set where
    cz : A zero
    ca : {n : ℕ} → A n → A (suc n)

  h : {b : ℕ} → A b → A (b + zero)
  h cz = cz
  h (ca a) = ca (h a)

  eq : (c : ℕ) → (c + zero) ≡ c
  eq zero = refl
  eq (suc c) = cong (λ x → suc x) (eq c)

  f : {b : ℕ} → (a : A b) → subst A (eq b) (h a) ≡ a
  f {zero} cz = refl
  f {suc b} (ca n) = {!!} -- with (b + zero) | (eq b)
  -- ... | g | r = ?


module _ where
  open import Relation.Binary.HeterogeneousEquality

  g : {b : ℕ} → (a : A b) → h a ≅ a
  g cz = refl
  g (ca {n} a) = cong₂ {B = A} {C = (λ x y → A (suc x))} (λ x y → ca {n =
x} y) (≡-to-≅ (eq n)) (g a)


module _ where
  open import Relation.Binary.PropositionalEquality
  open import Relation.Binary.HeterogeneousEquality using (_≅_ ; refl ;
≅-to-≡)

  af : (b w : ℕ) (eq : w ≡ b) (a : A b) → (h : A b → A w) → (h a ≅ a)
       → subst A eq (h a) ≡ a
  af b .b refl a h hteq = ≅-to-≡ hteq


  fg : {b : ℕ} → (a : A b) → subst A (eq b) (h a) ≡ a
  fg {b} a = af b (b + zero) (eq b) a h (g a)


```

On Thu, May 4, 2017 at 3:06 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
>
> On 04/05/17 06:44, apostolis.xekoukoulotakis at gmail.com wrote:
>
>> This seems to be closer to what my code actually looks like:
>>
>> postulate
>>   B : Set
>>   A : B → Set
>>   big_expression : (c : B) → {b : B} → (a : A b) → B
>>   h : (c : B) → {b : B} → (a : A b) → A (big_expression c a)
>>   eq : (c : B) → {b : B} → (a : A b) → (big_expression c a) ≡ c
>>
>> f : {b : B} → (a : A b) → subst A (eq b a) (h b a) ≡ a
>> f = {!!}
>>
>
> We have
>
>   eq b a : big_expression b a = b
>   h b a  : A(big_expression b a)
>
> Consider the instantiations
>
>   A b = Bool
>   big_expression c {b} a = c
>   h c {b} a = true
>   eq b a = refl
>
> So the type subst A (eq b a) (h b a) ≡ a amounts to
>
>             subst A refl true = a,
>
> that is,
>             true = a.
>
> Hence we have
>
>   f : {b : B} → (a : Bool) → true ≡ a
>
> which of course can't be proved.
>
> Hence, in the generality you have things above, you can't complete the
> definition of f.
>
> Of course it may well be that for your specific B, A, big_expression,
> h and eq, you can complete the definition of f.
>
> You will need to cook-up a more specific abstraction of your code
> for us to be able to help more here in this list.
>
> I hope this helps.
>
> Martin
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170505/3758240c/attachment-0001.html>