Hi, I'm self-learning Coq. I've stumbled upon these two similar inductive propositions (indprops).

```
Inductive le' : nat -> nat -> Prop :=
| le_n': forall n : nat, le' n n
| le_S': forall (n m : nat), le' n m -> le' n (S m).
Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m:nat, le n m -> le n (S m).
```

`le'`

is from DMFP; `le`

is from stdlib.

I've played with both a little bit. Both seems to behave the same. The only difference I observed is that both produce different hypotheses with `inversion`

and `induction`

tactics. Notably, `le`

produces one less `n`

variable than `le'`

.

My questions:

- Is the difference simply a matter of style?

1.1 If so, can I always "factor out" the common variables to the parameter of an indprop? E.g.`n : nat`

as shown above.

1.2 If not, when to prefer one style over another?

factoring variables to parameters behaves nicer as you have seen

you will get more benefit when your induction is over a non variable n, ie

```
Goal forall n, le' 1 n -> n <> 0.
intros n H;induction H.
(* goals n <> 0 and S m <> 0 *)
(* can't prove the first goal *)
Undo.
(* instead we have to do eg *)
intros n H;remember 1 as n1;induction H.
(* goals n = 1 |- n <> 0 and n=1, le' n m, (n=1 -> m <> 0) |- S m <> 0 *)
Abort.
Goal forall n, le 1 n -> n <> 0.
intros n H;induction H.
(* goals 1 <> 0 and S m <> 0 *)
```

Makes sense! I'll prefer factoring variables to parameters then :D

Jiahong Lee has marked this topic as resolved.

Indexes can allow you to have "more strict" types, but they come at the cost of being awkward to pattern match.

Ali Caglayan said:

Indexes can allow you to have "more strict" types, but they come at the cost of being awkward to pattern match.

I suppose by index, you meant the `n : nat`

in `le'`

that is not parameterised. Is there a benefit to having a "more strict" type?

no

the types are equivalent, indices are just more annoying to work with

I don't know what Ali means by "more strict"

I didn't mean much by it, just this:

```
Inductive TheSkyIsBlue : bool -> Prop :=
| i_agree_that : TheSkyIsBlue true
.
Fail
Inductive TheSkyIsBlue' (b : bool) : Prop :=
i_agree_that' : TheSkyIsBlue' true
.
```

There is no way to write the type with a parameter and in that sense having a parameter is more lax, and an index lets you be more specific.

My understanding is that the type of an indprop has to be a function `X -> Prop`

, for any `X : Type`

. Without breaking that constraint, you're free to factor out variables as the parameters. So it's not about "strictness", but how Coq recognises an indprop as an indprop (instead of treating it as normal inductive data type).

Indprops are normal inductive types (that live in Prop)

Both indices and parameters are supported for all sorts — Prop, Set, Type

Last updated: Jun 25 2024 at 14:01 UTC