2

For using reflexivity, I must somehow transform n + 1 to (S n).

This should be a rather simple transformation, but I don't know how to tell Coq to do it.

How do I proceed?

Shuzheng
  • 11,288
  • 20
  • 88
  • 186
  • 5
    Possible duplicate of [How can I rewrite "+ 1" (plus one) to "S" (succ) in Coq?](http://stackoverflow.com/questions/40313702/how-can-i-rewrite-1-plus-one-to-s-succ-in-coq) – gallais Nov 15 '16 at 16:05
  • `1 + n` is equal to `S n` by normalization, so if you have a lemma proving commutativity of addition, you can go `n + 1` => `1 + n` => `S n`. – Cactus Nov 16 '16 at 04:27

1 Answers1

4

Since they are not equal, just equivalent, you can use replace (n + 1) with (S n) which will ask you to prove that fact. Or you can use rewrite with the correct lemma from the std lib, which is add_1_r iirc.

Vinz
  • 5,997
  • 1
  • 31
  • 52
  • How would I prove 0 + (S j) = (S j) then? – Shuzheng Nov 15 '16 at 16:18
  • 1
    This should be provable directly using `reflexivity`: the definition of `+` is done by recursion on the first argument, so here Coq knows how to simplify `0 + foobar` into `foobar` without rewriting. The issue with your initial question is that you wanted to rewrite `n + 1`, instead of `1 + n`. To prove that `1 + n` is equal to `S n`, you don't have to do anything, it's exactly the definition. – Vinz Nov 15 '16 at 17:02