mPlusZero.v

Inductive Nat :=
    Z : Nat
  | S : Nat -> Nat.

(* This version of Add is not tail recursive *)
Fixpoint Add a b :=
  match a with
  | Z => b
  | S n => S (Add n b)
  end.

(* And this theorem is trivial to proove *)
Theorem mPlusZero : forall m, Add m Z = m.
  
Proof.
induction m.
reflexivity.
simpl. rewrite IHm. reflexivity. Qed.

(* However, this version of Add is tail recursive *)
Fixpoint Add2 a b :=
  match a with
  | Z => b
  | S n => Add2 n (S b)
  end.

(* To prove mPlusZero2, I need two intermediate proof which are harder to write *)

Theorem moveS : forall m n, Add2 (S m) n = Add2 m (S n).
Proof.
intros.
induction m.
reflexivity.
simpl. reflexivity.
Qed.



Theorem mPlusSucc : forall m n, Add2 m (S n) = S (Add2 m n).
Proof.
intros.
rewrite <- moveS.
induction n.
simpl.
(* I'm blocked here

2 subgoals
m : Nat
______________________________________(1/2)
Add2 m (S Z) = S (Add2 m Z)
______________________________________(2/2)
Add2 (S m) (S n) = S (Add2 m (S n))

*)
Admitted.

(* This is the theorem I'd like to prove.

What really annoys me here is that this is really easy to do with the first implementation of Add.

Here I'd like to understand two things:

a) How to finish the proof in mPlusSucc that I just Admitted.
b) Is there a theory / rule of thumb on how to write fixpoint (here, Add or Add2) in order to simplify proof.
*)
Theorem mPlusZero2 : forall m, Add2 m Z = m.
  
Proof.
intros.
induction m.
simpl. reflexivity.
rewrite moveS.
rewrite mPlusSucc.
rewrite IHm.
reflexivity.
Qed.