The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

I am not sure it is required but the link you gave lack a lot of stuff.
Indicate at least what libraries you use (and try to interpret your
file, as the first non comment line cannot even be interpreted).


Le Sat,  8 Dec 2012 02:23:54 +0100 (CET),
<kennethadammiller AT gmail.com>
 a écrit :

> 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?