Re: [Hol-info] Proving a trivial goal

[Ramana K. <Ram...@cl...>]

I didn't know about ELIM_UNCURRY - cool!

I would have done rw[GSYM pairTheory.LAMBDA_PROD] (after trying a bunch of
things that didn't work..)
Also, rw[FORALL_DEF,Once FUN_EQ_THM,pairTheory.UNCURRY] seems to work.

As for where this goal came from, I've seen it coming from EVAL_TAC before.

On 17 November 2016 at 03:38, Johannes Åman Pohjola <po...@ch...>
wrote:

> (forgot to reply to list the first time)
>
> On 2016-11-16 17:35, Scott Owens wrote:
> > Thanks, that works.
> >
> > For the curious, the ELIM_UNCURRY theorem is ``∀f. UNCURRY f = (λx. f
> (FST x) (SND x))``. Not obviously relevant...
> >
> > Scott
> >
> >> On 2016/11/16, at 16:23, Johannes Åman Pohjola <po...@ch...>
> wrote:
> >>
> >> Try this:
> >>
> >> REWRITE_TAC [pairTheory.ELIM_UNCURRY]
> >>
> >> Cheers / Johannes
> >>
> >>
> >> On 2016-11-16 17:04, Scott Owens wrote:
> >>> Does anyone know how to prove this goal:
> >>>
> >>> ∀(p1,p1',p2). T
> >>>
> >>> I’m not sure how I got it, and I can’t work out how to prove it, but
> it’s probably true :)
> >>>
> >>> Scott
> >>> ------------------------------------------------------------
> ------------------
> >>> _______________________________________________
> >>> hol-info mailing list
> >>> hol...@li...
> >>> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> ------------------------------------------------------------
> ------------------
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>