## Stream: Coq users

### Topic: How to prove induction principle

#### walker (Feb 18 2022 at 20:46):

in software foundations, they said "This induction principle is a theorem like any other: If [t] is
defined inductively, the corresponding induction principle is
called [t_ind]"

I tried to prove nat_ind since it is a theorem and not an axiom, ofc without using induction myself. and I am getting no where: It feels like it is an axiom more than a theorem, the word "principle" is hinting that
Here is my failing attempt and I cannot figure out how to do it correctly:

``````Theorem test_ind:
forall P : nat -> Prop, P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n.
Proof.
intros P H H' n.
destruct n as [|n'] eqn: E.
- (*n = 0*)apply H.
- (* n = S n'*) apply H'. Abort.
``````

#### Kenji Maillard (Feb 18 2022 at 20:56):

`nat_ind` and other induction principles are indeed Gallina terms like any other theorems. You can see how they are implemented by printing them, e.g. `Print nat_ind.`. Now, this won't be provable out of thin air. In Gallina, the basic notions are rather structural fixpointpoints `fix` and pattern matches `match`.

#### Kenji Maillard (Feb 18 2022 at 20:57):

In particular you won't be able to derive the induction principle solely from `match` (which correspond loosely to the `destruct` tactic)

#### walker (Feb 18 2022 at 20:58):

I checked `Print nat_ind.` and tbh I didn't fully understand it so I thought maybe I would try doing it with tactics.

#### walker (Feb 18 2022 at 20:59):

so based on my understanding the output of the print statement is really the only proof and there is not tactics equivalent ?

#### Kenji Maillard (Feb 18 2022 at 21:05):

You can also do it using tactics, here is a slight modification of your attempt:

``````Theorem test_ind:
forall P : nat -> Prop, P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n.
Proof.
intros P h0 hsuc.
fix test_ind_fix 1. (*Introduces a variable test_ind_fix : forall n, P n in the context *)
intro n.
destruct n as [|n'] eqn:E.
- exact h0.
- apply hsuc. apply test_ind_fix.
Qed.
``````

#### Paolo Giarrusso (Feb 18 2022 at 21:05):

If you want to avoid induction, you can (a) use "Fixpoint" instead of "Theorem", and recurse on a smaller number by using test_ind (b) IIRC, use the fix tactic (it's in the manual, but it's harder). (ninjaed)

#### walker (Feb 18 2022 at 21:15):

Thanks @Kenji Maillard @Paolo Giarrusso I probably need to digest that solution

#### walker (Feb 18 2022 at 21:47):

I don't really understand what is going on ! `fix` somehow introduced the goal as hypothesis I don't get how was that considered sound, but then intros and destruct feels redundant because we can just apply `test_ind_fix` as it is.

#### Kenji Maillard (Feb 18 2022 at 21:52):

Did you experiment by yourself to see what happens if you try to do that ?

(there are explanation in the documentation linked above to explain what happens in that case, the keywords are `guard condition` and the `Guarded.` command inside a script)

#### walker (Feb 18 2022 at 21:53):

yes once I id fix test_ind_fix 1. I got `forall n : nat, P n` as a hyptothesis

#### walker (Feb 18 2022 at 21:53):

then I simply performed `apply test_idn_fix` and it was done.

#### walker (Feb 18 2022 at 21:53):

I just don't understand how can one get away with introducting `forall n, P n`

#### Kenji Maillard (Feb 18 2022 at 21:55):

You are not yet done as long as `Qed`/`Defined` did not pass !

#### walker (Feb 18 2022 at 21:56):

you are right! qed did not pass, i am extremely lost here I just to be pointed to the right document to read.

#### Kenji Maillard (Feb 18 2022 at 21:57):

Tactics need not to be sound (even if they usually strive to be sound), so just discharging a goal is not enough to be sure that you have proved your theorem, you need to pass the check of Qed.

#### Kenji Maillard (Feb 18 2022 at 21:58):

In two words, there are quite a few checks that are global to your proof that are done at Qed-time. One of these check is verifying that all the use of fixpoints are structurally decreasing. And it is this check that does not go through in your later attempt.

#### walker (Feb 18 2022 at 22:00):

so basically the induction principle is still cooked inside coq and it is not generally a provable theorem ?

#### Paolo Giarrusso (Feb 18 2022 at 22:03):

I hear what you’re saying and there’s a grain of truth, but that’s not how we say it

#### Paolo Giarrusso (Feb 18 2022 at 22:04):

because what we’ve seen above is exactly “proving an induction principle”

_however_

#### Paolo Giarrusso (Feb 18 2022 at 22:06):

Coq’s core indeed understands structural recursion, which is pretty much equivalent

#### Paolo Giarrusso (Feb 18 2022 at 22:07):

@walker to put it in simpler words, the induction principle (on naturals) is precisely a recursive function that invokes itself recursively on smaller inputs — hence, we can be certain it terminates.

#### walker (Feb 18 2022 at 22:09):

I understand, to be clear I am not implying anything I just need to truly understand how coq, because deeper understanding always helps. thanks a lot everyone!

#### Paolo Giarrusso (Feb 18 2022 at 22:09):

I’m sure Software Foundations has exercises on writing structurally recursive functions, and that will hopefully help gain intuition :-)

#### Kenji Maillard (Feb 18 2022 at 22:12):

On a more theoretical POV, I think you are forced to add something to Coq to support induction. The closest reference I have is this paper by Herman Geuvers, Induction is Not Derivable in Second Order Dependent Type Theory (2000).

#### Pierre-Marie Pédrot (Feb 18 2022 at 22:22):

To CoC, not to Coq, since by definition induction is available in Coq.

#### Pierre-Marie Pédrot (Feb 18 2022 at 22:24):

(You can also show this independence result using some rather simple syntactic models that introduce side-effects, in which you can show that there are not types that behave like e.g. boolean + large elimination. I've never written that anywhere, but it's actually not very hard.)

Last updated: May 18 2024 at 10:02 UTC