Wellfounded induction in Coq

Question

Let's say that I know certain natural numbers are good. I know 1 is good, if n is good then 3n is, and if n is good then n+5 is, and those are only ways of constructing good numbers. It seems to me that the adequate formalization of this in Coq is

Inductive good : nat -> Prop :=
| g1 : good 1
| g3 : forall n, good n -> good (n * 3)
| g5 : forall n, good n -> good (n + 5).

However, despite being obvious, the fact that 0 is not good seems not being provable using this definition (because when I invert, in case of g3 I only get the same thing in the hypothesis).

Now it isn't so obvious what exactly are good numbers. And it really seems that I don't need to characterize them totally in order to know that 0 is not good. For example, I can know that 2 is not good just by doing few inversions.

Answer (eponier)

Indeed g3 can be applied an unbounded number of times when trying to disprove good 0. That is why we can think this proof requires induction (and we can see that the auxiliary lemma needed in the solution of @AntonTrunov uses induction). The same idea is used in theorem loop_never_stop of http://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html#lab428.

Require Import Lia.

Example not_good_0 : ~ good 0.~ good 0
Proof.~ good 0
  intros contra.contra: good 0
False remember 0 as n.n: nat
Heqn: n = 0
contra: good n
False induction contra.Heqn: 1 = 0
False
n: nat
Heqn: n * 3 = 0
contra: good n
IHcontra: n = 0 -> False
False
n: nat
Heqn: n + 5 = 0
contra: good n
IHcontra: n = 0 -> False
False
  -Heqn: 1 = 0
False discriminate.
  -n: nat
Heqn: n * 3 = 0
contra: good n
IHcontra: n = 0 -> False
False apply IHcontra.n: nat
Heqn: n * 3 = 0
contra: good n
IHcontra: n = 0 -> False
n = 0 lia.
  -n: nat
Heqn: n + 5 = 0
contra: good n
IHcontra: n = 0 -> False
False lia.
Qed.

A: And remember 0 as n is a crucial component of this solution. It sort of replaces the original statement with forall n, n = 0 -> ~ good n.. Great answer!

Answer (Anton Trunov)

This problem needs induction. And induction needs some predicate P : nat -> Prop to work with. A primitive (constant) predicate like (fun n => ~good 0) doesn't give you much: you won't be able to prove the base case for 1 (which corresponds to the constructor g1), because the predicate "forgets" its argument.

So you need to prove some logically equivalent (or stronger) statement which readily will give you the necessary predicate. An example of such equivalent statement is forall n, good n -> n > 0, which you can later use to disprove good 0. The corresponding predicate P is (fun n => n > 0).

Require Import Coq.Arith.Arith.
Require Import Coq.micromega.Lia.

Inductive good : nat -> Prop :=
| g1 : good 1
| g3 : forall n, good n -> good (n * 3)
| g5 : forall n, good n -> good (n + 5).

Lemma good_gt_O : forall n, good n -> n > 0.forall n : nat, good n -> n > 0
Proof.forall n : nat, good n -> n > 0
  intros n H.n: nat
H: good n
n > 0 induction H; lia.
Qed.

Goal ~ good 0.~ good 0
  intro H.H: good 0
False now apply good_gt_O in H.
Qed.

Here is a proof of the aforementioned equivalence:

Lemma not_good0_gt_zero_equiv_not_good0 :
  (forall n, good n -> n > 0) <-> ~ good 0.(forall n : nat, good n -> n > 0) <-> ~ good 0
Proof.(forall n : nat, good n -> n > 0) <-> ~ good 0
  split; intros ? ?.H: forall n : nat, good n -> n > 0
H0: good 0
False
H: ~ good 0
n: nat
good n -> n > 0
  -H: forall n : nat, good n -> n > 0
H0: good 0
False apply H in H0.H: forall n : nat, good n -> n > 0
H0: 0 > 0
False lia.
  -H: ~ good 0
n: nat
good n -> n > 0 destruct n; [tauto | lia].
Qed.

And it's easy to show that forall n, n = 0 -> ~ good n which implicitly appears in @eponier's answer is equivalent to ~ good 0 too.

Lemma not_good0_eq_zero_equiv_not_good0 :
  (forall n, n = 0 -> ~ good n) <-> ~ good 0.(forall n : nat, n = 0 -> ~ good n) <-> ~ good 0
Proof.(forall n : nat, n = 0 -> ~ good n) <-> ~ good 0
  split; intros; subst; auto.
Qed.

Now, the corresponding predicate used to prove forall n, n = 0 -> ~ good n is fun n => n = 0 -> False. This can be shown by using manual application of the goal_ind induction principle, automatically generated by Coq:

Example not_good_0_manual : forall n, n = 0 -> ~ good n.forall n : nat, n = 0 -> ~ good n
Proof.forall n : nat, n = 0 -> ~ good n
  intros n Eq contra.n: nat
Eq: n = 0
contra: good n
False
  generalize Eq.n: nat
Eq: n = 0
contra: good n
n = 0 -> False
  refine (good_ind (fun n => n = 0 -> False) _ _ _ _ _);
    try eassumption; intros; lia.
Qed.

generalize Eq. introduces n = 0 as a premise to the current goal. Without it the goal to prove would be False and the corresponding predicate would be the boring fun n => False again.