Stream: Coq users

Topic: How to prove induction principle


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip walker (Feb 18 2022 at 21:15):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip walker (Feb 18 2022 at 21:53):

then I simply performed apply test_idn_fix and it was done.

view this post on Zulip walker (Feb 18 2022 at 21:53):

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

view this post on Zulip Kenji Maillard (Feb 18 2022 at 21:55):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 22:04):

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

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 22:04):

_however_

view this post on Zulip Paolo Giarrusso (Feb 18 2022 at 22:06):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 :-)

view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (Feb 18 2022 at 22:22):

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

view this post on Zulip 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: Mar 29 2024 at 05:40 UTC