Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-02-19

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 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/
02:54 vanila joined #isabelle
02:54 vanila hi
02:54 vanila would isabelle be good for working with modular arithmetic?
02:55 vanila just to do basica number theory stuff for example
02:55 vanila im more familiar with coq and I know that doing that is very hard there
03:02 tangentstorm probably, vanila
03:03 tangentstorm do you have an example of a proof you might want to attempt?
03:03 vanila stuff like bezouts theorem (given coprime a,b exists x,y with ax+by = 1)
03:03 vanila fermats little theorem x^p = x mod p
03:04 tangentstorm hold please
03:04 vanila squares mod p
03:06 tangentstorm there is a mod_type here but i don't yet understand it myself: http://afp.sourceforge.net/browser_info/devel/HOL/HOL-Word/Numeral_Type.html
03:08 tangentstorm not exactly pretty.
03:10 vanila well i'd like to define it myself from scratch
03:10 vanila i can use this as reference though
03:10 tangentstorm it sounds like a fun problem.
03:10 vanila I guess the best thing is to just dive in
03:11 tangentstorm i'm still basically a beginner. the nice thing i like about isabelle compared to other systems is the declarative language:
03:12 tangentstorm https://github.com/tangentstorm/tangentlabs/blob/master/isar/Exponents.thy
03:12 vanila oh yeah that's interesting! looks nice and readable
03:12 tangentstorm if you can express your proof as a series of rewrites then you can almost surely prove it in isar. i just don't have the math chops to know how yet.
03:13 tangentstorm some of these other folks in here are much better, but probably asleep :)
03:20 tangentstorm vanila: http://isabelle.in.tum.de/repos/isabelle/file/d3996d5873dd/src/HOL/Number_Theory/Primes.thy
03:20 tangentstorm (see also other things in that directory)
03:22 vanila ah!
03:22 vanila looks like they use latex for operators
03:22 vanila i guess there's an emacs mode or something thath displays it?
03:22 tangentstorm also http://isabelle.in.tum.de/repos/isabelle/file/d3996d5873dd/src/HOL/GCD.thy#l1524   bezout's theorem
03:22 vanila i use proof general before
03:22 vanila oh this is super ill reference these a bunch thanks a lot
03:22 tangentstorm no you use a custom gui that comes with it. it's very nice.
03:23 vanila oh i see!
03:23 tangentstorm it'll turn all that latex junk into pretty symbols for you, and color code the lines of your proof as you go along.
03:25 tangentstorm http://www.concrete-semantics.org/ is about writing proofs of functional programs, but the first part makes for a nice general intro to isabelle/isar and the gui
03:26 vanila ill power through part 1 and then get started then, thanks again :)
03:27 tangentstorm np. let us know how it goes. i'd love to see a beginner friendly version.
03:28 vanila sure!
10:13 JCaesar There used to be an emacs "mode"…
18:25 wagle joined #isabelle
18:27 int-e joined #isabelle
18:27 lispy joined #isabelle
23:32 JCaesar Say, is there some kind of default-defined record constructor? i.e. one that is just a plain function without any syntactic sugar.
23:49 larsrh JCaesar: try foobar.make
23:50 JCaesar ty.

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary