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

[Apostolis Xekoukoulotakis]

I uploaded my code to see the actual function.

https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79f5032125a1/agda/IndexLLProp.agda#L178

The proofs I use in 'subst2' are here:

https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79f5032125a1/agda/IndexLLProp.agda#L154

https://github.com/xekoukou/sparrow/blob/750bcebeb488c52f1b95083e8cff79f5032125a1/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/20170503/5dab66d4/attachment-0001.html>