Proving even + even = even with mutual induction using tactics

Question

I was trying out mutual induction in Coq, the first type I defined was

Inductive IsEven : nat -> Prop :=
| EvenO : IsEven O
| EvenS n : IsOdd n -> IsEven (S n)
with IsOdd : nat -> Prop :=
| OddS n : IsEven n -> IsOdd (S n).

I now wanted to prove that the sum of even numbers is even. I was able to do this using a Fixpoint and pattern matching:

Fixpoint even_plus_even (n m : nat) (evenn : IsEven n) (evenm : IsEven m) :
  IsEven (n + m) :=
  match evenn with
  | EvenO => evenm
  | EvenS n' oddn' => EvenS (n' + m) (odd_plus_even n' m oddn' evenm)
  end
with odd_plus_even (n m : nat) (oddn : IsOdd n) (evenm : IsEven m) :
  IsOdd (n + m) :=
  match oddn with
  | OddS n' evenn' => OddS (n' + m) (even_plus_even n' m evenn' evenm)
  end.

This defines both even_plus_even and odd_plus_even. I would now like to prove this using tactics in a more terse way (preferably without using many predefined lemmas to keep the code as self-contained as possible) but I haven't gotten very far.

Specifically, is it possible to prove both even_plus_even and odd_plus_even using only one Lemma like we can with the Fixpoint?

Edit: Thank you very much for your answers, the Lemma ... with ... syntax was exactly what I was looking for. In fact

Lemma even_plus_even2 (n m : nat) (evenn : IsEven n) (evenm : IsEven m) :
  IsEven (n + m)
with odd_plus_even2 (n m : nat) (oddn : IsOdd n) (evenm : IsEven m) :
  IsOdd  (n + m).
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
n, m: nat
evenn: IsEven n
evenm: IsEven m
IsEven (n + m)
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
n, m: nat
oddn: IsOdd n
evenm: IsEven m
IsOdd (n + m)
Proof.
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
n, m: nat
evenn: IsEven n
evenm: IsEven m
IsEven (n + m)
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
n, m: nat
oddn: IsOdd n
evenm: IsEven m
IsOdd (n + m)
  induction evenn; simpl.
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m: nat
evenm: IsEven m
IsEven m
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m, n: nat
H: IsOdd n
evenm: IsEven m
IsEven (S (n + m))
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
n, m: nat
oddn: IsOdd n
evenm: IsEven m
IsOdd (n + m)
  -
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m: nat
evenm: IsEven m
IsEven m assumption.
  -
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m, n: nat
H: IsOdd n
evenm: IsEven m
IsEven (S (n + m)) constructor.
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m, n: nat
H: IsOdd n
evenm: IsEven m
IsOdd (n + m) auto.
  -
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
n, m: nat
oddn: IsOdd n
evenm: IsEven m
IsOdd (n + m) induction oddn; simpl.
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m, n: nat
H: IsEven n
evenm: IsEven m
IsOdd (S (n + m)) constructor.
even_plus_even2: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even2: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
m, n: nat
H: IsEven n
evenm: IsEven m
IsEven (n + m) auto.
Defined.

generates exactly the same proof term as the Fixpoint in my originial question.

Answer (Vinz)

There is support for mutual induction in Coq. I know of two ways, but I only recall how to use one:

1. Combined Schemes

   Here is how it works:

   Scheme IsEven_ind2 := Induction for IsEven Sort Prop
       with IsOdd_ind2 := Induction for IsOdd Sort Prop.
   
   Combined Scheme IsEvenOdd_ind from IsEven_ind2, IsOdd_ind2.
   
   Lemma foo : (forall (n : nat) (evenn : IsEven n), forall m (evenm : IsEven m),
                   IsEven (n + m)) /\
                 (forall (n : nat) (oddn : IsOdd n), forall m (evenm : IsEven m),
                     IsOdd (n + m)).
   (forall n : nat,
    IsEven n ->
    forall m : nat, IsEven m -> IsEven (n + m)) /\
   (forall n : nat,
    IsOdd n -> forall m : nat, IsEven m -> IsOdd (n + m))
   Proof.
   (forall n : nat,
    IsEven n ->
    forall m : nat, IsEven m -> IsEven (n + m)) /\
   (forall n : nat,
    IsOdd n -> forall m : nat, IsEven m -> IsOdd (n + m))
     apply IsEvenOdd_ind.
   forall m : nat, IsEven m -> IsEven (0 + m)
   forall n : nat,
   IsOdd n ->
   (forall m : nat, IsEven m -> IsOdd (n + m)) ->
   forall m : nat, IsEven m -> IsEven (S n + m)
   forall n : nat,
   IsEven n ->
   (forall m : nat, IsEven m -> IsEven (n + m)) ->
   forall m : nat, IsEven m -> IsOdd (S n + m)
     -
   forall m : nat, IsEven m -> IsEven (0 + m) now intros m hm.
     -
   forall n : nat,
   IsOdd n ->
   (forall m : nat, IsEven m -> IsOdd (n + m)) ->
   forall m : nat, IsEven m -> IsEven (S n + m) intros h hn hi m hm.
   h: nat
   hn: IsOdd h
   hi: forall m : nat, IsEven m -> IsOdd (h + m)
   m: nat
   hm: IsEven m
   IsEven (S h + m) rewrite plus_Sn_m.
   h: nat
   hn: IsOdd h
   hi: forall m : nat, IsEven m -> IsOdd (h + m)
   m: nat
   hm: IsEven m
   IsEven (S (h + m)) apply EvenS.
   h: nat
   hn: IsOdd h
   hi: forall m : nat, IsEven m -> IsOdd (h + m)
   m: nat
   hm: IsEven m
   IsOdd (h + m) now apply hi.
     -
   forall n : nat,
   IsEven n ->
   (forall m : nat, IsEven m -> IsEven (n + m)) ->
   forall m : nat, IsEven m -> IsOdd (S n + m) intros h hn hi m hm.
   h: nat
   hn: IsEven h
   hi: forall m : nat, IsEven m -> IsEven (h + m)
   m: nat
   hm: IsEven m
   IsOdd (S h + m) rewrite plus_Sn_m.
   h: nat
   hn: IsEven h
   hi: forall m : nat, IsEven m -> IsEven (h + m)
   m: nat
   hm: IsEven m
   IsOdd (S (h + m)) apply OddS.
   h: nat
   hn: IsEven h
   hi: forall m : nat, IsEven m -> IsEven (h + m)
   m: nat
   hm: IsEven m
   IsEven (h + m) now apply hi.
   Qed.

1. Lemma with

   On this one I just don't know how to finish it but that's a syntax issue iirc:

   Lemma foo : forall (n m : nat) (evenn : IsEven n) (evenm : IsEven m),
       IsEven (n + m)
   with bar : forall (n m : nat) (oddn : IsOdd n) (evenm : IsEven m),
       IsOdd (n + m).
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   forall n m : nat,
   IsEven n -> IsEven m -> IsEven (n + m)
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   Proof.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   forall n m : nat,
   IsEven n -> IsEven m -> IsEven (n + m)
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
     -
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   forall n m : nat,
   IsEven n -> IsEven m -> IsEven (n + m) intros n m hn.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   n, m: nat
   hn: IsEven n
   IsEven m -> IsEven (n + m) revert m.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   n: nat
   hn: IsEven n
   forall m : nat, IsEven m -> IsEven (n + m)
       induction hn as [| p hp]; intros m hm; simpl in *.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   m: nat
   hm: IsEven m
   IsEven m
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   p: nat
   hp: IsOdd p
   m: nat
   hm: IsEven m
   IsEven (S (p + m))
       +
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   m: nat
   hm: IsEven m
   IsEven m exact hm.
       +
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   p: nat
   hp: IsOdd p
   m: nat
   hm: IsEven m
   IsEven (S (p + m)) now apply EvenS; apply bar.
     -
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m) intros n m hn hm.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   n, m: nat
   hn: IsOdd n
   hm: IsEven m
   IsOdd (n + m) revert n hn.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   m: nat
   hm: IsEven m
   forall n : nat, IsOdd n -> IsOdd (n + m)
       induction hm as [| p hp]; intros n hn; simpl in *.
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   n: nat
   hn: IsOdd n
   IsOdd (n + 0)
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   p: nat
   hp: IsOdd p
   n: nat
   hn: IsOdd n
   IsOdd (n + S p)
       +
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   n: nat
   hn: IsOdd n
   IsOdd (n + 0) now apply bar; [exact hn | apply EvenO].
       +
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   p: nat
   hp: IsOdd p
   n: nat
   hn: IsOdd n
   IsOdd (n + S p) apply bar; [exact hn |].
   foo: forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
   bar: forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
   p: nat
   hp: IsOdd p
   n: nat
   hn: IsOdd n
   IsEven (S p) now apply EvenS.
   Qed.
   Cannot guess decreasing argument of fix.
   

Edit: Here is a valid syntax for the Lemma with solution.

Lemma foo (n : nat) (evenn : IsEven n) :
  forall (m : nat) (evenm : IsEven m), IsEven (n + m)
with bar (n : nat) (oddn : IsOdd n) :
  forall (m : nat) (evenm : IsEven m), IsOdd (n + m).
foo: forall n : nat, IsEven n -> forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat, IsOdd n -> forall m : nat, IsEven m -> IsOdd (n + m)
n: nat
evenn: IsEven n
forall m : nat, IsEven m -> IsEven (n + m)
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
n: nat
oddn: IsOdd n
forall m : nat, IsEven m -> IsOdd (n + m)
Proof.
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
n: nat
evenn: IsEven n
forall m : nat, IsEven m -> IsEven (n + m)
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
n: nat
oddn: IsOdd n
forall m : nat, IsEven m -> IsOdd (n + m)
  -
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
n: nat
evenn: IsEven n
forall m : nat, IsEven m -> IsEven (n + m) induction evenn as [| p hp]; intros m hm; simpl in *.
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
m: nat
hm: IsEven m
IsEven m
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
p: nat
hp: IsOdd p
m: nat
hm: IsEven m
IsEven (S (p + m))
    +
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
m: nat
hm: IsEven m
IsEven m exact hm.
    +
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
p: nat
hp: IsOdd p
m: nat
hm: IsEven m
IsEven (S (p + m)) now apply EvenS; apply bar.
  -
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
n: nat
oddn: IsOdd n
forall m : nat, IsEven m -> IsOdd (n + m) induction oddn as [p hp].
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
p: nat
hp: IsEven p
forall m : nat, IsEven m -> IsOdd (S p + m) intros n hn.
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
p: nat
hp: IsEven p
n: nat
hn: IsEven n
IsOdd (S p + n) simpl in *.
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
p: nat
hp: IsEven p
n: nat
hn: IsEven n
IsOdd (S (p + n))
    apply OddS.
foo: forall n : nat,
IsEven n ->
forall m : nat, IsEven m -> IsEven (n + m)
bar: forall n : nat,
IsOdd n ->
forall m : nat, IsEven m -> IsOdd (n + m)
p: nat
hp: IsEven p
n: nat
hn: IsEven n
IsEven (p + n) now apply foo.
Qed.

Answer (larsr)

You can for instance prove both lemmas at the same time by "anding" them together into one lemma, and then extract the left or right part of the clause using proj1 and proj2.

Lemma even_or_odd_plus_even: forall (n m : nat),
    (forall (evenn : IsEven n) (evenm : IsEven m), IsEven (n + m)) /\
      (forall (oddn : IsOdd n) (evenm : IsEven m), IsOdd (n + m)).
forall n m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
Proof.
forall n m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
  induction n; split; intros.
m: nat
evenn: IsEven 0
evenm: IsEven m
IsEven (0 + m)
m: nat
oddn: IsOdd 0
evenm: IsEven m
IsOdd (0 + m)
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
evenn: IsEven (S n)
evenm: IsEven m
IsEven (S n + m)
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
oddn: IsOdd (S n)
evenm: IsEven m
IsOdd (S n + m)
  -
m: nat
evenn: IsEven 0
evenm: IsEven m
IsEven (0 + m) auto.
  -
m: nat
oddn: IsOdd 0
evenm: IsEven m
IsOdd (0 + m) inversion oddn.
  -
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
evenn: IsEven (S n)
evenm: IsEven m
IsEven (S n + m) destruct (IHn m) as [He Ho].
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
evenn: IsEven (S n)
evenm: IsEven m
He: IsEven n -> IsEven m -> IsEven (n + m)
Ho: IsOdd n -> IsEven m -> IsOdd (n + m)
IsEven (S n + m) inversion evenn.
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
evenn: IsEven (S n)
evenm: IsEven m
He: IsEven n -> IsEven m -> IsEven (n + m)
Ho: IsOdd n -> IsEven m -> IsOdd (n + m)
n0: nat
H0: IsOdd n
H: n0 = n
IsEven (S n + m)
    constructor.
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
evenn: IsEven (S n)
evenm: IsEven m
He: IsEven n -> IsEven m -> IsEven (n + m)
Ho: IsOdd n -> IsEven m -> IsOdd (n + m)
n0: nat
H0: IsOdd n
H: n0 = n
IsOdd
  ((fix add (n m : nat) {struct n} : nat :=
      match n with
      | 0 => m
      | S p => S (add p m)
      end) n m) auto.
  -
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
oddn: IsOdd (S n)
evenm: IsEven m
IsOdd (S n + m) destruct (IHn m) as [He Ho].
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
oddn: IsOdd (S n)
evenm: IsEven m
He: IsEven n -> IsEven m -> IsEven (n + m)
Ho: IsOdd n -> IsEven m -> IsOdd (n + m)
IsOdd (S n + m) inversion oddn.
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
oddn: IsOdd (S n)
evenm: IsEven m
He: IsEven n -> IsEven m -> IsEven (n + m)
Ho: IsOdd n -> IsEven m -> IsOdd (n + m)
n0: nat
H0: IsEven n
H: n0 = n
IsOdd (S n + m)
    constructor.
n: nat
IHn: forall m : nat,
(IsEven n -> IsEven m -> IsEven (n + m)) /\
(IsOdd n -> IsEven m -> IsOdd (n + m))
m: nat
oddn: IsOdd (S n)
evenm: IsEven m
He: IsEven n -> IsEven m -> IsEven (n + m)
Ho: IsOdd n -> IsEven m -> IsOdd (n + m)
n0: nat
H0: IsEven n
H: n0 = n
IsEven
  ((fix add (n m : nat) {struct n} : nat :=
      match n with
      | 0 => m
      | S p => S (add p m)
      end) n m) auto.
Qed.

Definition even_plus_even n m := proj1 (even_or_odd_plus_even n m).
Definition odd_plus_even n m := proj2 (even_or_odd_plus_even n m).

gives you

even_plus_even
     : forall n m : nat,
       IsEven n -> IsEven m -> IsEven (n + m)
odd_plus_even
     : forall n m : nat,
       IsOdd n -> IsEven m -> IsOdd (n + m)

Notice that the two clauses share share the n and m, which you need if the clauses can't be proved separately because they need to depend on each other. (In this particular case they don't, though. You could prove the statements separately, as Anton showed.)

EDIT: just saw Vinz solution. I didn't know Lemma had the with syntax (thanks for showing!), but that makes sense and is I think a neater way to do this mutually dependent definition.

Lemma even_plus_even : forall n m, IsEven n -> IsEven m -> IsEven (n + m)
with odd_plus_even: forall n m, IsOdd n -> IsEven m -> IsOdd (n + m).
even_plus_even: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
forall n m : nat,
IsEven n -> IsEven m -> IsEven (n + m)
even_plus_even: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
Proof.
even_plus_even: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
forall n m : nat,
IsEven n -> IsEven m -> IsEven (n + m)
even_plus_even: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)
  -
even_plus_even: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
forall n m : nat,
IsEven n -> IsEven m -> IsEven (n + m) induction 1; simpl; auto using EvenS.
  -
even_plus_even: forall n m : nat,
IsEven n ->
IsEven m -> IsEven (n + m)
odd_plus_even: forall n m : nat,
IsOdd n -> IsEven m -> IsOdd (n + m)
forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m) induction 1; simpl; auto using OddS.
Qed.

A: Actually, both Lemma and Fixpoint are just aliases for Theorem, see here, which means that you can also define Fixpoint definitions with proof tactics, without giving the explicit proof term upfront. By the way, the refine tactic is useful if you want to give parts of the proof term explicitly, while leaving holes to fill in by tactics.