The Coq mailing list

[Wojciech Meyer <wojciech.meyer AT googlemail.com>]

Hi,

I am very new to Coq. I'm currently trying to implement some abstract
interpreter for formal verification of translation rules.

I wish to model state after executing statement as a set of possible
side effects.

I am trying to use ListSet from the standard library.

It seems like I was able to make my verification engine happy, apart
from that for certain rules, where I got irreducible fix point at
set_add.  (I am not sure why it's happening).

The goal looks like this:

set_add Edec (E A) (set_add Edec (E B) (set_add Edec (E C) (if
    effect_dec (E D) (E D) then E D :: nil else E D :: E D :: nil))) =
    denoteOperation (Operation1 a1 a2)


Now the right hand side is being kept happy, I can unfold it, simplify
it, and reduce to list.

However, left side seems to not be reducible with simpl to set
despite all of the arguments are being constants.

What I suspect I think is that I declare Edec, as a Hypothesis as
defined in the documentation for set, so probably sort of the
implementation is missing. I still don't understand how to implement
it correctly, because Edec in terms of functional programming should
be a set element comparision function, but this definition is on type
level and it's Prop, and don't know how it should look like.

So, I have two questions, how to use ListSet by example and also what
would be a different or better/easier way of handling this kind of
code?

I hope this questions is not too basic,
Thanks,
Wojciech