CODEWITHSUNDEEP
coq
Giwon Song
Giwon Song

Reputation: 43

How to add "assumed true" statements in Coq

I tried to add a definition of a natural number in CoqIDE.

Inductive nat : Set :=
  | O: nat
  | S: nat -> nat.

But I couldn't add this as "assumed true":

forall (n m: nat, S n = S m -> n = m).

How do I add this?

Upvotes: 0

Views: 216

Answers (1)

Ana Borges
Ana Borges

Reputation: 1376

I'm not completely clear on what you want to do, but your formula is not syntactically correct. I believe you meant forall (n m: nat), S n = S m -> n = m (note the parenthesis' placement).

Your statement is actually provable, no need to assume it:

Lemma S_inj : forall (n m: nat), S n = S m -> n = m.
Proof. intros n m [=]. assumption. Qed.

The [=] intro pattern expresses the built-in injectivity of the S constructor.

Upvotes: 1

Related Questions