Stream: Coq users

Topic: ✔ Difference between Two Definitions of an Indprop

Jiahong Lee (Jun 22 2022 at 07:34):

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:

1. 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?

Gaëtan Gilbert (Jun 22 2022 at 07:55):

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 *)

Jiahong Lee (Jun 22 2022 at 08:11):

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

Notification Bot (Jun 22 2022 at 08:11):

Jiahong Lee has marked this topic as resolved.

Ali Caglayan (Jun 22 2022 at 09:18):

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

Jiahong Lee (Jun 22 2022 at 11:23):

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?

Gaëtan Gilbert (Jun 22 2022 at 11:25):

no

Gaëtan Gilbert (Jun 22 2022 at 11:26):

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

Gaëtan Gilbert (Jun 22 2022 at 11:27):

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

Ali Caglayan (Jun 22 2022 at 11:48):

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.

Jiahong Lee (Jun 23 2022 at 00:26):

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).

Paolo Giarrusso (Jun 23 2022 at 02:39):

Indprops are normal inductive types (that live in Prop)

Paolo Giarrusso (Jun 23 2022 at 02:39):

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

Last updated: Sep 23 2023 at 13:01 UTC