The Coq mailing list

[<kennethadammiller AT gmail.com>]

So, I've proved simple things before with Coq, which is like the boolean
expressions and handling lists such as what are at the Software Foundations
(up to the part on polymorphism on Lists).

http://www.cis.upenn.edu/~bcpierce/sf/

But I haven't yet done anything about proving a function, or at least maybe
it's just that I'm having a hard time getting started. Anyway, I don't know if
just proceeding to the part on functions will help me enough, because I need
to get this done rather quickly, but the issue is explained at the gist link
below.

https://gist.github.com/1a09c8fc1cdd98bd40d4

I talked on IRC, and I was told that I needed some sub-lemmas that related 1)
lequ and <= 2) Int32Set.for_all xs P with forall x, Int32Set.In x xs -> P x 3)
+32 with Word.add

I agree that this should be a relatively trivial solve, but I guess its the
first of this type that I've done before, and I need some help. One thing I
should note is that
by the time I get to "Proof. intros. split.", coqide is showing this:

2 subgoals
addrs : Int32Set.t
a : int32
b : int32
H : checkIATAddresses (iatbounds (a, b)) addrs = true
addr : int32
H0 : Int32Set.In addr addrs
______________________________________(1/2)
(unsigned a <= unsigned addr)%Z


______________________________________(2/2)
(unsigned addr <= unsigned (add a b))%Z

So, I'm confused; I don't know where to start. Can anyone give me a pointer?