CODEWITHSUNDEEP
coq
Cryptostasis
Cryptostasis

Reputation: 1216

What does the simpl tactic do in COQ

I am wondering how the simpl tactic works in COQ.
Assume the following Lemma:

Parameter n:nat. 
Lemma test: S n + 0 = S (n+0).

Now, the simpl. tactic produces 

S (n + 0) = S (n + 0)

My understanding is that simpl performs a sequence of cbv beta, delta, iota conversions. I tried that, but could not manage to get the same result as simpl. The basic problem is that after a cbv delta expansion, the plus term keeps expanded. How can I de-expand it, i.e. re-substitute the plus name for the expanded definition?
Or, can anyone show me how I can get the effect of simpl by manually performing more elementary tactics?

Upvotes: 7

Views: 2301

Answers (1)

Ptival
Ptival

Reputation: 9437

I do not believe it possible to emulate the simpl tactic using only cbv, because indeed cbv delta does not let you choose which occurences to replace, while simpl only performs delta-reduction when it leads to a iota step. (cf. https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.simpl)

So, even if informally we can say that simpl performs such a sequence of calls, it seems like it has access to a lower-level way of performing those reductions than what the cbv tactic exposes.

Upvotes: 3

Related Questions