CODEWITHSUNDEEP
logiccoqinduction
mercury0114
mercury0114

Reputation: 1449

How in Coq to make `simpl` command perform only one step reduction?

My definition of add is as follows:

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => add p (S m)
end.

Later in the file I am trying to prove the following goal: add (S n) 0 = S n

I call simpl command expecting it to reduce

add (S n) 0 to add n (S 0).

Instead it reduces

add (S n) 0 to add n 1

I suspect simpl command executes multiple steps as long as it can execute.

My question: is there a command that would make a one step reduction, reducing

add (S n) 0 = S n

to

add n (S 0) = S n

?

Upvotes: 0

Views: 293

Answers (1)

Kazuhiro Kobayashi
Kazuhiro Kobayashi

Reputation: 193

S 0 and 1 are the same expressions.

"Same" doesn't only mean S 0 = 1 holds, but the coq's system cannot distinguish them. In contrast, 1 + 0 and 1 are not the same while 1 + 0 = 1 holds.

0 is a Notation for O, and 1 is a Notation for S O. So both S 0 and 1 represent the same expression S O.

If you start to prove S 0 = 1, you will immediately see the goal is 1 = 1, or eq (S O) (S O) if you disable Notations by Unset Printing Notations.

Upvotes: 3

Related Questions