CODEWITHSUNDEEP
coq
Giwon Song
Giwon Song

Reputation: 43

proof of adding 1 to some number changes the parity in Coq

I defined even as:

Inductive even : nat -> Prop :=
  | ev0: even O
  | evSS: forall n, even n -> even (S (S n)).

But now I want to prove:

Lemma add1_diff (x: nat) : even (S x) = ~even x.

Can I prove:

even (S O) = (~ even O)

Thanks in advance.

Upvotes: 2

Views: 79

Answers (2)

M Soegtrop
M Soegtrop

Reputation: 1456

You usually can't prove the equality of two Props. An equality in Prop means that the proof terms for a logical statement are equal. This is sometimes the case, but rarely. Here are a few examples:

Require Import PeanoNat.
Import Nat.

Inductive even : nat -> Prop :=
  | ev0: even O
  | evSS: forall n, even n -> even (S (S n)).

Example ex1 (n : nat) : (n >= 1) = (1 <= n).
Proof.
  (* The proofs are equal because >= is defined in terms of <= *)
  reflexivity.
Qed.

Example ex2: even (2+2) = even 4.
Proof.
  (* The proofs are equal because 2+2 can be reduced to 4 *)
  reflexivity.
Qed.

Example ex3 (n : nat) : even (2+n) = even (n+2).
Proof.
  (* The proofs are equal because 2+n is equal to n+2 *)
  rewrite add_comm.
  reflexivity.
Qed.

Example ex4 (n : nat): even (S (S n)) = even n.
Proof.
  (* The proofs cannot be equal, because the left side proof always
     requires one evSS constructor more than the right hand side. *)
Abort.

For this reason one uses the equivalence of two Props, which is <->, rather than the equality. The equivalence of the last statement is provable:

Example ex4 (n : nat): even (S (S n)) <-> even n.
Proof.
  split; intros H.
  - inversion H.
    assumption.
  - constructor.
    assumption.
Qed.

So to answer your question: the equality of the two statements is most likely not provable, but the equivalence is. In case you need help with that, please ask.

Upvotes: 4

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1286

No, you cannot prove your goal: natively there is basically no way to prove equality of propositions. What you can do instead is to use propositional equivalence, rather than equality, that is prove

even (S 0) <-> ~ (even 0)

or more generally

Lemma add1_diff (x : nat) : even (S x) <-> ~ (even x)

Upvotes: 1

Related Questions