Three Dollar Quill

Instead of rewriting my following-along code, I wrote an IsTotalOrder predicate in terms of named properties, and now I'm thinking about the finite sum stuff. What I'd like to figure out is if there's some way to establish the equivalence between the explicitly ordered non-ghost version, and the unordered ghost version.

Going to speculate on ways to do that.

Suppose I do induction that "builds up" stuff. Given a set s and an order r, I want to build things up something like:

• If s == {}, then both versions sum to 0.0.
• Suppose both versions have the same sum for some s. Now, given an element k (not in s?), I want to try establishing that s + {k} increases both results by summand(k).

Hm, I've got some time to try this out. I also need to get a handle on the import system in Dafny, but I want to work that out at some point anyway...

"By default (in the absence of any export set declarations) all the names declared in a module are available outside the module using the import mechanism."

Neat, thank you for that.

"Error: module Relation does not exist"

No thank you for that. What am I doing wrong here... Tinker, fiddle...

"Error: Import declaration uses same name as a module in the same scope: Relation"

Huh. That implies that it doesn't really work the way that I think it does... Let's try what it looks like that should allow.

Huh, yeah, module names are just globally available, and import does rebinding? That... freaks me out a little bit.

Anyway, I got the code reuse wrangled, copied over the code, and now I'm working on constructing a lemma to prove that addition of a finite collection of numbers works the way everyone knows it does. Dafny does not yet know it, at least not in a way germane to the way I phrased the lemma.

Unfortunately, it's now late, and I'll have to wait until sometime tomorrow to get this worked out, if not later.

Bed.

Good night.