Inductive Predicate for Addition in Coq

Question

I'm new to inductive predicates in Coq. I have learned how to define simple inductive predicates such as "even" (as in adam.chlipala.net/cpdt/html/Predicates.html) or "last" (as in http://www.cse.chalmers.se/research/group/logic/TypesSS05/resources/coq/CoqArt/inductive-prop-chap/SRC/last.v).

Now I wanted to try something slightly more complicated: to define addition as an inductive predicate, but I got stuck. I did the following:

Inductive N : Type :=
| z : N  (* zero *)
| s : N -> N.  (* successor *)

Inductive Add: N -> N -> N -> Prop :=
| add_z: forall n, (Add n z n)
| add_s: forall m n r, (Add m n r) -> (Add m (s n) (s r)).

Fixpoint plus (x y : N) := 
  match y with
  | z => x
  | (s n) => (s (plus x n))
  end.

And I would like to prove a simple theorem (analogously to what has been done for last and last_fun in www.cse.chalmers.se/research/group/logic/TypesSS05/resources/coq/CoqArt/inductive-prop-chap/SRC/last.v):

Theorem T1: forall x y r, (plus x y) = r -> (Add x y r).
Proof.
intros x y r. induction y.
  simpl. intro H. rewrite H. apply add_z.

  case r.
    simpl. intro H. discriminate H.

    ???

But then I get stuck. The induction hypothesis seems strange. I don't know if I defined Add wrongly, or if I am just using wrong tactics. Could you please help me, by either correcting my inductive Add or telling me how to complete this proof?

Answer 1

You introduced r before using induction on y. In general you'll want to use induction before introducing anything so the induction hypothesis is as general as possible.

Conjecture injectivity : forall n m, s n = s m -> n = m.

Theorem T1: forall x y r, (plus x y) = r -> (Add x y r).
Proof.
intros x y. induction y.
  simpl. intros r H. rewrite H. apply add_z.

  intro r. case r.
    simpl. intro H. discriminate H.

    simpl. intros n H. apply add_s. apply IHy. apply injectivity. apply H.
Qed.