Menu
How would you explain inductive predicates? What are they used for? What's the theory behind them? Are they only present in dependent type systems, or in other systems as well? Are they related to GADT's in some way? Why are they true by default in Coq?
This is an example from Coq:
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
How would you use this definition? Is it a datatype or a proposition?
866
At a nuts-and-bolts level, induction is a tool for proving that some predicate P(n) holds for any natural number n. When writing an inductive proof, you'll want to choose P(n) so that you can prove your overall result by showing that P(n) is true for every natural number n.
A proof by induction consists of two cases. The first, the base case, proves the statement for n = 0 without assuming any knowledge of other cases. The second case, the induction step, proves that if the statement holds for any given case n = k, then it must also hold for the next case n = k + 1.
I think we call inductive predicates objects that are defined inductively and sorted in Prop.
They are used for defining properties inductively (duh). The theory behind can probably be found in the literature for inductive constructions. Search papers about CIC (the Calculus of Inductive Constructions) for instance.
They are somewhat related to GADTs, though with dependent types they can express more things. If I am not mistaken, with GADTs each constructor lives in one particular family, whereas the addition of dependent types allows constructors to inhabit different families based on their arguments.
I do not know what you mean by "true by default in Coq".
even as you define it is an inductive datatype. It is not a proposition yet, as the type nat -> Prop indicates. A proposition would be even 0 or even 1. It can be inhabited (provable) as in even 0, or not as in even 1.
85
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
