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 <pohj...@chalmers.se> 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 <pohj...@chalmers.se> > 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-info@lists.sourceforge.net > >>> https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------ > ------------------ > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
