in software foundations, they said "This induction principle is a theorem like any other: If [t] is
defined inductively, the corresponding induction principle is
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.
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
In particular you won't be able to derive the induction principle solely from
match (which correspond loosely to the
Print nat_ind. and tbh I didn't fully understand it so I thought maybe I would try doing it with tactics.
so based on my understanding the output of the print statement is really the only proof and there is not tactics equivalent ?
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.
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)
Thanks @Kenji Maillard @Paolo Giarrusso I probably need to digest that solution
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.
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)
yes once I id fix test_ind_fix 1. I got
forall n : nat, P n as a hyptothesis
then I simply performed
apply test_idn_fix and it was done.
I just don't understand how can one get away with introducting
forall n, P n
You are not yet done as long as
Defined did not pass !
you are right! qed did not pass, i am extremely lost here I just to be pointed to the right document to read.
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.
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.
so basically the induction principle is still cooked inside coq and it is not generally a provable theorem ?
I hear what you’re saying and there’s a grain of truth, but that’s not how we say it
because what we’ve seen above is exactly “proving an induction principle”
Coq’s core indeed understands structural recursion, which is pretty much equivalent
@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.
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!
I’m sure Software Foundations has exercises on writing structurally recursive functions, and that will hopefully help gain intuition :-)
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).
To CoC, not to Coq, since by definition induction is available in Coq.
(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: Oct 03 2023 at 04:02 UTC