IRC log for #isabelle, 2017-03-22

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
09:06 larsrh joined #isabelle
09:11 aneas joined #isabelle
09:46 aneas i'm using isabelle to verify aspects of some formal semantics for my phd thesis. however, the semantics are large, and my knowledge of isabelle very limited, so i don't expect to be able to prove everything i'd like to. for each lemma that I can't prove, i'm creating a function definition containing the conclusion, and quickcheck it using the generated haskell code. this works much better for me than isabelles quickcheck, because i'm usi
09:46 aneas ng custom generators that fullfill my lemma premises by construction. this whole process is very tedious, and i'd like to improve it. is it possible to implement an additional lemma property like [code] or [simp] that causes the code generator to create a function of type a=>b=>...=>bool? or is it possible to provide custom generators for isabelles quickcheck?
10:02 larsrh you can create custom generators but only for your own types
10:02 larsrh that is if you want a custom generator for 'nat' or similar that won't work
10:03 larsrh But what I'm wondering is, what are the problems you're seeing with Isabelle QuickCheck?
10:05 aneas oh, isabelle quickcheck is wonderful. the problem is that my lemmas have big constraints, which quickcheck fails to fulfill. so its not actually checking anything, i think
10:06 aneas i don't think there is anything with isabelle, its just that i'm using it in a bad way :)
10:06 aneas anything wrong
10:06 pruvisto the obvious solution is to create a datatype wrapper for your arguments, write a QuickCheck generator for that datatype, and then use that
10:06 pruvisto Writing non-trivial QuickCheck generators in Isabelle is a bit annoying though.
10:07 pruvisto I'm not even sure if it's documented anywhere, I always just look at the implementation of the existing generators.
10:07 aneas pruvisto, can you point me to such an existing generator?
10:07 pruvisto hm let's see
10:08 larsrh aneas: you can check that with quickcheck [report]
10:09 pruvisto okay so you have to provide and instance for either random, exhaustive, or full_exhaustive
10:09 larsrh nvm, that flag doesn't seem to work
10:09 pruvisto I keep forgetting what the differences are
10:09 pruvisto one of them is actually obsolete, I think
10:10 aneas larsrh, yes, [report] didn't change the output
10:10 pruvisto FSet.thy in Library has a random instance
10:10 aneas pruvisto, i my case random sounds similar to what i'm doing right now with haskell quickcheck
10:10 aneas pruvisto, ok, great. thank you!
10:11 pruvisto DAList.thy has all three of them
10:11 aneas larsrh, how do you now about things like [report]? i can't find any documentation for it
10:15 pruvisto aneas: it's in the Isabelle/Isar reference manual: http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/isar-ref.pdf
10:17 aneas my bad, i was searching for [report]... thanks!
11:37 silver joined #isabelle
12:07 tautologico joined #isabelle
12:20 aneas i'm trying to use typedef to add invariants to my types, but i can still write functions that violate these invariants, e.g. typedef t = "{ x :: nat. x = 1 }" by auto ; fun f :: "nat ⇒ t" where "f x = Abs_t x"
12:21 larsrh aneas: they don't violate the invariants
12:21 larsrh Abs_t x where x ~= 1 returns an unspecified value
12:22 larsrh you might want to use lift_definition instead
12:22 pruvisto aneas: that usually isn't worth the trouble
12:22 larsrh this one ensures that you're always in specified territory
12:22 larsrh pruvisto: arguable
12:22 pruvisto I would recommend proving the well-formedness properties explicitly
12:23 pruvisto Isabelle doesn't allow you to enforce such properties with the type checker or anything fancy like that
12:23 aneas oh, i see
12:24 aneas that means i'm back to writing lots of lemmas like "[| valid x |] ==> valid (f x)"
12:24 pruvisto unfortunately, yes
12:25 pruvisto typedefs like yours can be convenient, but they do add some overhead and it takes some experience to see when it's worth it and when it isn't
12:25 pruvisto and the payoff is often not as great as one might think when one first sees that feature
12:25 aneas i just found typedefs and was very happy to finally get rid of those lemmas. it was really nice working with idris in this regard, where invariants could be encoded in the type itself or at least in the function type
12:26 aneas ok, thanks again pruvisto and larsrh, you talked me out of it :)
17:18 ammbauer is there a way to show how much time an isabelle command is taking?
17:37 pruvisto ammbauer: hover over it
21:31 JCaesar Won't work if it's just milliseconds, though…
23:21 dmiles joined #isabelle