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



For my Master's Thesis (compiling functional programs to density
functions) I effectively had to implement a fragment of typed Lambda
calculus and prove all kinds of rules about typing and substitution [1].

These rules are somewhat intricate, and I effectively proved them by
coming up with a plausible-looking conjecture and then tweaking it until
QuickCheck stopped complaining.

I don't think I've used Nitpick that much, perhaps because I have less
intuition about what kinds of things one can expect it to work on well.
With QuickCheck, I have a very clear idea of what kinds of propositions
it can and cannot do.


Speaking of "experimental mathematics" in general, I converted a big
unreadable SMT proof from the area of social choice theory (that was
found by other people) into a structured proof by experimentation in
Isabelle a few years ago [2]: I had a big list of facts that somehow
implied False together (and "by smt" could show it), but no intuitive
idea /why/ they implied False.

I then picked two or three of these facts and used "auto" to find out
what they boil down to together, deleted them from the list, and added
that consequence instead and checked whether the list was still
unsatisfiable.

Rinse and repeat until the list is a singleton and you have a structured
proof!

Manuel

[1]:
https://www.isa-afp.org/browser_info/current/AFP/Density_Compiler/PDF_Target_Semantics.html,
see e.g. "free_vars_cexpr_subst_aux"
[2]: https://link.springer.com/chapter/10.1007%2F978-3-030-29007-8_14


On 26/05/2020 16:43, Lawrence Paulson wrote:
> 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.