The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

It is a feature, not a bug, that Gallina considers definitionally equal terms to be indistinguishable from each other.  [simpl] reduces a term to another that is definitionally equal to it; in other words, from Gallina's perspective, it's an identity function.  There is no way to talk about term reduction directly within Gallina.

On 08/18/2013 12:06 PM, t x wrote:

With apologies for my stupidity, this looks like a tactic, not a function. Can you wrap this in a :

Definition simp_as_function H := ...  ?

On Sun, Aug 18, 2013 at 2:07 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Does the ltac [let H0' := (eval simpl in H0) in set (H0'' := H0')] do what you want?  Alternatively, if you are trying to construct a proof without ltac, [Definition foo := Eval simpl in <_expression_>.]

-Jason

On Aug 18, 2013 9:53 AM, "t x" <txrev319 AT gmail.com> wrote:

Is there a Coq function which does the same as simpl?

I.e. "simpl in H0" vs (set H0 := magic_function H0)

I'm playing around with pattern matching / trying to construct proofs by functions -- and I find myself constantly wanting to have a "simpl" function to simplify terms.

Thanks!