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

[Ulf Norell]

The trick is to also abstract over the recursive call:

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 | h n | f n
...                 | .b       | refl | hn  | ih = cong ca ih

/ Ulf

On Fri, May 5, 2017 at 6:43 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170505/6850cec0/attachment.html>