IRC log for #isabelle, 2017-04-07

All times shown according to UTC.

Time Nick Message
01:17 silver joined #isabelle
01:48 ilbot3 joined #isabelle
01: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/
06:08 pruvisto chindy: well, for every positive integer n there is a type n with exactly n elements from 0 to n - 1
06:08 pruvisto internally, e.g. "5" is just syntactic sugar for 1 bit1 bit0 bit1
06:09 pruvisto where "typedef 1 = "{0::nat}""
06:09 pruvisto and if 'a is a type with n elements, 'a bit0 is a type with 2*n elements and 'a bit1 is a type with 2*n+1 elements
06:10 pruvisto and "('a, 'b)" vec is essentially a type copy of "'b ⇒ 'a"
06:11 pruvisto so if you have a "('a, 3) vec", that's essentially a function that maps any element of the type 3 (i.e. 0, 1, 2) to an element of type 'a
06:11 pruvisto and that's pretty much the essence of a vector w.r.t. a standard basis
07:38 aneas joined #isabelle
11:26 silver joined #isabelle
13:03 larsrh so I tuned the function package to give me exactly the things I need and all so that my tactic will be deterministic and really clean and cool
13:03 larsrh turns out the dumb thing (non-deterministically applying congruence rules) works far better
13:40 larsrh I am very tempted to call this thing dumb_tac
13:50 JCaesar Come up with some cool backronym, and it's on.
13:51 JCaesar determinism-unaware modification builder.
13:51 JCaesar mmmmh.
15:14 pruvisto larsrh: so what did you do in the end?
15:15 pruvisto I for one spent pretty much the entire day proving something completely obvious
18:15 larsrh pruvisto: a terrible REPEAT_ALL_NEW thingy which just resolve_tacs ALL THE CONGRUENCE RULES
18:15 pruvisto larsrh: no I mean what did you improve w.r.t. the function package?
18:16 larsrh only a tiny bit: I generalised the signature of the code which descends a rhs of a function definition and figures out recursive calls
18:16 larsrh I had another combinator which helped traversing this tree but in the end it was too simplistic
18:16 larsrh so I didn't push it
18:17 larsrh the problem, in a nutshell: if you have mutually recursive definitions, that code in the function package assumes that the terms you shove into it already assumes that you have the Inl/Inr representation
18:17 larsrh but I don't have that, so it was useless for me
18:18 larsrh and I couldn't be bothered to figure out where exactly that code that does that transformation lies
18:18 larsrh *lives
18:18 larsrh in an ideal world this tree structure would obviously be in function_info