How to repeat proof tactics in case in Coq?

Question

I would like to extend the exercise 6.10 in Coq'Art by adding a theorem that for all months which are not January, is_January will equal false.

My definition of months looks like this:

Inductive month : Set :=
| January : month
| February : month
| March : month
| April : month
| May : month
| June : month
| July : month
| August : month
| September : month
| October : month
| November : month
| December : month.

My definition of is_January looks like this:

Definition is_January (m : month) : Prop :=
  match m with
  | January => True
  | _       => False
  end.

I am doing the following to test that it is correct.

Eval compute in (is_January January).
= True
: Prop
Eval compute in (is_January December).
= False
: Prop

Theorem is_January_eq_January :
  forall m : month, m = January -> is_January m = True.
forall m : month, m = January -> is_January m = True
Proof.
forall m : month, m = January -> is_January m = True
  intros m H.
m: month
H: m = January
is_January m = True rewrite H.
m: month
H: m = January
is_January January = True compute.
m: month
H: m = January
True = True reflexivity.
Qed.

I am not very happy with this theorem's proof.

Theorem is_January_neq_not_January :
  forall m : month, m <> January -> is_January m = False.
forall m : month, m <> January -> is_January m = False
Proof.
forall m : month, m <> January -> is_January m = False
  induction m.
January <> January -> is_January January = False
February <> January -> is_January February = False
March <> January -> is_January March = False
April <> January -> is_January April = False
May <> January -> is_January May = False
June <> January -> is_January June = False
July <> January -> is_January July = False
August <> January -> is_January August = False
September <> January -> is_January September = False
October <> January -> is_January October = False
November <> January -> is_January November = False
December <> January -> is_January December = False
  -
January <> January -> is_January January = False contradiction.
  -
February <> January -> is_January February = False intro H.
H: February <> January
is_January February = False simpl.
H: February <> January
False = False reflexivity.
  -
March <> January -> is_January March = False intro H.
H: March <> January
is_January March = False simpl.
H: March <> January
False = False reflexivity.
  -
April <> January -> is_January April = False intro H.
H: April <> January
is_January April = False simpl.
H: April <> January
False = False reflexivity.
  -
May <> January -> is_January May = False intro H.
H: May <> January
is_January May = False simpl.
H: May <> January
False = False reflexivity.
  -
June <> January -> is_January June = False intro H.
H: June <> January
is_January June = False simpl.
H: June <> January
False = False reflexivity.
  -
July <> January -> is_January July = False intro H.
H: July <> January
is_January July = False simpl.
H: July <> January
False = False reflexivity.
  -
August <> January -> is_January August = False intro H.
H: August <> January
is_January August = False simpl.
H: August <> January
False = False reflexivity.
  -
September <> January -> is_January September = False intro H.
H: September <> January
is_January September = False simpl.
H: September <> January
False = False reflexivity.
  -
October <> January -> is_January October = False intro H.
H: October <> January
is_January October = False simpl.
H: October <> January
False = False reflexivity.
  -
November <> January -> is_January November = False intro H.
H: November <> January
is_January November = False simpl.
H: November <> January
False = False reflexivity.
  -
December <> January -> is_January December = False intro H.
H: December <> January
is_January December = False simpl.
H: December <> January
False = False reflexivity.
Qed.

Is there anyway in Coq to repeat the - intro H. simpl. reflexivity. case proof for non-January months (so I would only have two - or something similar so I do not have to repeat myself)? Or am I just completely going about this proof the wrong way?

A: You probably want your is_January function to return bool, not Prop. Prop is a type of logical propositions (there are plenty of them), so it's not supposed to be used as a usual boolean-like type with only two values (true and false).

Answer

One way to do this is to

Theorem is_January_neq_not_January :
  forall m : month, m <> January -> is_January m = False.
forall m : month, m <> January -> is_January m = False
Proof.
forall m : month, m <> January -> is_January m = False
  induction m; try reflexivity.
January <> January -> is_January January = False contradiction.
Qed.

• simpl is implicit in reflexivity and hence unnecessary.

• t1 ; t2 applies tactic t2 to all branches created by the application of tactic t1.

• try t tries to apply tactic t (as the name implies) or does nothing if t fails.

What this does is run induction as before and then immediately run reflexivity on all branches (which works on & solves all but the January branch). After that, you're left with that single branch, which can be solved by contradiction as before.

Other potentially useful constructions for more complex situations are

• (t1 ; t2) which groups tactics t1 and t2,

• t1 | t2, t1 || t2, t1 + t2 which are variations on "try t1 and if that fails / doesn't do anything useful / ..., do t2 instead",

• fail which explicitly fails (this is useful if you want to un-do/reset what happened in a branch)

  (As a complex example from one of my proofs, consider try (split; unfold not; intro H'; inversion H'; fail). This attempts to create several sub-branches (split) hoping that they're all contradictory and can be solved by inversion H'. If that doesn't work, the inversions would just create a big mess, so it explicitly fails in order to un-do the effects of the tactic chain. End result is that many boring cases get solved automatically and the interesting ones remain unchanged for manual solving.)

• and many more – look at Chapter 9 of the Coq Reference Manual ("The tactic language") for longer descriptions of these and many other useful constructions.

A: now destruct m. will do the trick as well -- it's equivalent to destruct m; easy. and the easy tactic is clever enough to use contradiction and reflexivity.