Removed tics from ADT notation.
Added BuildADT compatible simplify tactic.
Remove reserved call notations
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
Fully qualify some imports
More qualification
Add some more general refinements
Partial work on min+max

Now the observer refinement is a bit nicer.  I feel like it's still
ad-hoc, though, which is why I named the tactics "dubiously
specialized".
More helper lemmas

Some about [exists], some about refining mutators, some about hProps.
More incomplete work on min+max

Mutator is partially refined.  But not having [refineADT] in [Type] is
really crippling here, so I'm going to move it into [Type].
Put [refineADT] in [Type]

Make all the necessary changes to make everything compile.

This way, we get to pull the simulation relation out of [refineADT].
(And, really, it's not an (h)Prop.  If we want to erase it on
extraction, we can wrap it in [inhabited].)
Add some refinement lemmas about sig
Make progress on the mutator in min+max

The mutator now calls the two separate mutators from the min&max and
the spec implementation.  However, it has some very unfortunate
constructs, like

  x <- { _ : { x : A | computes_to bar x } | True };
  ...

This is necessary to generate (inside the computation monad) the proof
that the the [x] which [bar] computes to satisfies some properties,
which mention [bar].  I suspect that I'll be able to remove these
constructs later in the refinement process, when I figure out how to
say that you can strip off the proof part of a [sig] representation if
it's only ever used to compute the proof part of a mutator.  But I
don't think I can hide all the details behind the "general delegation
refinement".

I kind-of want to thread the proofs through variants of, e.g., [Pick],
so that we can get [Comp] support for this.  Alternatively, I kind-of
want to build the representation invariants into the ADT structure, so
we don't have to use the proofs in the [Comp].  But there might be
another better way to do this, that I'm not seeing.
Use open_constr for hone representation'

This way, we can give a simulation relation without giving all of the
types.
More cleaning up in anticipation of our intern.
Updated README with descriptions of project layout
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
First (crappy) attempt at an introduction to the project.
More code clean for Clement.
Split out some general computation refinements

Because they're just lemmas about logic.
Add some more logic lemmas