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

[Apostolis Xekoukoulotakis]

I think that I introduced the cycle in my attempt to simplify the example.

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 = {!!}


```

I hope that this is cycle free.

(In my code eq holds under stricter conditions than h`s input but here
their inputs are the same. f is to be proved under these stricter
conditions.)


On Wed, May 3, 2017 at 5:47 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> I uploaded my code to see the actual function.
>
> https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79
> f5032125a1/agda/IndexLLProp.agda#L178
>
> The proofs I use in 'subst2' are here:
>
> https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79
> f5032125a1/agda/IndexLLProp.agda#L154
>
> https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79
> f5032125a1/agda/LinLogic.agda#L135
>
> Andrea,
>   I tried to use heterogeneous equality. I will give it one more try.
>
> On Wed, May 3, 2017 at 3:12 PM, Andrea Vezzosi <sanzhiyan at gmail.com>
> wrote:
>
>> It might make sense to state and prove f with heterogeneous equality
>> instead, it's possibly a weaker statement, but you won't have subst in
>> the type then.
>>
>>
>>
>> On Wed, May 3, 2017 at 10:58 AM, Apostolis Xekoukoulotakis
>> <apostolis.xekoukoulotakis at gmail.com> wrote:
>> > I tried 'with (big_expression a) | (eq a)' . It does not work because
>> of the
>> > h function.
>> >
>> > It says that the result is not well typed.
>> >
>> > From what I understand, we cannot abstract (eq a) without abstracting
>> the h
>> > function, but I need the h function to do the proof.
>> >
>> >
>> >
>> > On Wed, May 3, 2017 at 11:51 AM, Jesper Cockx <Jesper at sikanda.be>
>> wrote:
>> >>
>> >> Hi,
>> >>
>> >> Did you already try to use `with (eq a)` and then match with refl? I
>> think
>> >> that should do the trick.
>> >>
>> >> Otherwise, the brute-force way to get rid of annoying equality proofs
>> in
>> >> your types is by using the J eliminator. But the result is usually not
>> very
>> >> pretty...
>> >>
>> >> -- Jesper
>> >>
>> >> On Wed, May 3, 2017 at 9:24 AM, Apostolis Xekoukoulotakis
>> >> <apostolis.xekoukoulotakis at gmail.com> wrote:
>> >>>
>> >>> Hello,
>> >>>
>> >>> I have something like this :
>> >>>
>> >>> ```
>> >>> postulate
>> >>>   B : Set
>> >>>   A : B → Set
>> >>>   big_expression : {b : B} → (a : A b) → B
>> >>>   h : {b : B} → (a : A b) → A (big_expression a)
>> >>>   eq : {b : B} → (a : A b) → (big_expression a) ≡ b
>> >>>
>> >>> f : {b : B} → (a : A b) → subst A (eq a) (h a) ≡ a
>> >>> f = {!!}
>> >>>
>> >>> ```
>> >>>
>> >>> h is defined inductively, thus it would be very easy to prove this if
>> I
>> >>> did not have subst in the equality.
>> >>>
>> >>> Any advice on how to proceed?
>> >>>
>> >>> I can't find a way to remove subst.
>> >>>
>> >>> _______________________________________________
>> >>> Agda mailing list
>> >>> Agda at lists.chalmers.se
>> >>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>
>> >>
>> >
>> >
>> > _______________________________________________
>> > 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/20170504/01de6a56/attachment.html>