CODEWITHSUNDEEP
coq
Attila Karoly
Attila Karoly

Reputation: 1021

Symbolic manipulation of terms in Coq

Proof states like this often arise in my Coq studies:

1 goal
n : nat
IHn : fib_v1 n <= fib_v1 (S n)
______________________________________(1/1)
fib_v1 (S n) <= fib_v1 (S (S n))

Coq complains that it can't unify n with S n and S n with S (S n). In paper and pen, it would be easy to introduce a symbolic manipulation within the goal, say t = S n, or even n = S n, then the induction hypothesis would become applicable. It doesn't seem to work that way in Coq. How one moves on in a situation like this?

Upvotes: 1

Views: 56

Answers (1)

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

I think here Coq rightfully complains. If you are proving you property by induction, it’s normal that you induction hypothesis is some P(n) and that your conclusion is P(S n) and you can’t simply use the former to prove the latter… Otherwise anything would be provable by induction!

In your case, what you probably would have to do is to unfold the definitions of fib_v1 in the conclusion, so that you can relate fib_v1 (S n) and fib_v1 (S (S n)) to fib_v1 n and hopefully use your induction hypothesis to conclude.

If you wish to do a local definition, you can do that in Coq, using eg set (t := S n) in *. (the set tactic introduces the definition, and the in * part replaces every occurrence of the body in your hypotheses and goal by the variable name).

Upvotes: 3

Related Questions