Skip to main content
added 132 characters in body
Source Link

Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.

For instance if you have a hypothesis of type:

H: S n <= m

And you want to deduce that « m has necessarily shape S m’ for some m’» then inversion (on H itself) is enough. Because just matching the possible constructors for H gives that immediately.

On the other hand if you want to deduce from the same fact that n <= m then you need induction (on H itself) because it does not only follow from the shape of constructors but from the fact that unfolding constructors will eventually end up with a base case (which is the raison d’être of induction/recursion)

Hope I gave the intuition but anyways it is not always clear that a property is of one kind or another. And anyways sometimes using an already established lemma avoids induction or inversion completely.

EDIT: note that if you want to prove the inductive property above you may have to first manipulate H to be of the form n’ <= m.

Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.

For instance if you have a hypothesis of type:

H: S n <= m

And you want to deduce that « m has necessarily shape S m’ for some m’» then inversion (on H itself) is enough. Because just matching the possible constructors for H gives that immediately.

On the other hand if you want to deduce from the same fact that n <= m then you need induction (on H itself) because it does not only follow from the shape of constructors but from the fact that unfolding constructors will eventually end up with a base case (which is the raison d’être of induction/recursion)

Hope I gave the intuition but anyways it is not always clear that a property is of one kind or another. And anyways sometimes using an already established lemma avoids induction or inversion completely.

Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.

For instance if you have a hypothesis of type:

H: S n <= m

And you want to deduce that « m has necessarily shape S m’ for some m’» then inversion (on H itself) is enough. Because just matching the possible constructors for H gives that immediately.

On the other hand if you want to deduce from the same fact that n <= m then you need induction (on H itself) because it does not only follow from the shape of constructors but from the fact that unfolding constructors will eventually end up with a base case (which is the raison d’être of induction/recursion)

Hope I gave the intuition but anyways it is not always clear that a property is of one kind or another. And anyways sometimes using an already established lemma avoids induction or inversion completely.

EDIT: note that if you want to prove the inductive property above you may have to first manipulate H to be of the form n’ <= m.

Source Link

Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.

For instance if you have a hypothesis of type:

H: S n <= m

And you want to deduce that « m has necessarily shape S m’ for some m’» then inversion (on H itself) is enough. Because just matching the possible constructors for H gives that immediately.

On the other hand if you want to deduce from the same fact that n <= m then you need induction (on H itself) because it does not only follow from the shape of constructors but from the fact that unfolding constructors will eventually end up with a base case (which is the raison d’être of induction/recursion)

Hope I gave the intuition but anyways it is not always clear that a property is of one kind or another. And anyways sometimes using an already established lemma avoids induction or inversion completely.