Re: [isabelle] Any fans of "try"?



 Also used Nitpick to compute and exhibit compositions of event structures, basically using it as a constraint solver.
Nice and faster than using other approaches, though some times you need to fiddle a bit with parameters.
Let's see who else :)

     Il martedì 26 maggio 2020, 15:45:01 GMT+1, Lawrence Paulson <lp15 at cam.ac.uk> ha scritto:  
 
 This is amazing and shows that we are nearly able to do experimental mathematics.

In fact, I have used nitpick in some tricky combinatorial proofs to check corner cases. It was very effective.

Larry Paulson



> On 26 May 2020, at 14:36, John F. Hughes <jfh at cs.brown.edu> wrote:
> 
> Another note in praise of nitpick: in doing some work in synthetic affine
> and projective geometry, I wanted to exhibit a four-point affine plane. To
> do so required writing out the incidence relation (which points are on
> which lines), which was a case-by-case nightmare to write and read. But
> when instead I asked "try" to prove the theorem that every affine plane
> contains at least 5 points, nitpick instantly generated the standard
> 4-point affine plane for me. That's kind of a backwards approach, but it
> was, as I say, very useful.
> 

  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.