The Coq mailing list

[Craig McL <mr_mcl AT live.co.uk>]

Hi all,

I am trying to reason inductively about an abstract set type (FSetWeakList)
using set_induction_bis from FSetProperties (I'm using Coq v8.4pl4). In my
goal, I have a fold operation which takes the set in question as an
argument. I wish to use fold_add from FSetProperties so that I can apply the
induction hypothesis but the equivalence relation that fold_add uses is not
suitable for the function I provide to fold. In particular, my function does
not satisfy the transpose property generated by the fold lemmas (fold_add and
fold_equal).

I have attached a small Coq source file that illustrates the idea. I am using
the Metatheory library from UPenn to represent a free variable as an atom;
atoms is the FSetWeakList instance I wish to reason about inductively. You
will therefore need the Metatheory library if you wish to execute the
example. I use the version of the library available at
http://pl.postech.ac.kr/poplmark/ for the paper ``Mechanizing Metatheory
Without Typing Contexts'' by Jonghyun Park, Jeongbong Seo, Sungwoo Park,
Gyesik Lee.

I am wondering if it's possible to provide an alternative equivalence relation
to the FSeInterace such that transpose will hold e.g. a relation defining
equality up-to renaming of variables or permuting binds.

Regards,
Craig

Attachment: CoqMLAtoms.v
Description: Binary data