CODEWITHSUNDEEP
coq
tomjerry7
tomjerry7

Reputation: 101

How to introduce n distinct symbols in Coq

I have built a record for group. Now I would like to build a group with n elements (e.g. 10 elements) by specifying the group multiplication table.

My issue is that I would need n symbols to serve as a ground set for my group. I will need Coq to know that these n elements are all distinct.

So far I have figured

Inductive ground_set : Type :=  A : ground_set | B : ground_set.
Axiom diff: A<>B.

which works for n=2. I don't know how to scale this to many elements without creating some ugly code.

I would guess that there is a better way to generate such a set, but I couldn't find any.

Upvotes: 1

Views: 145

Answers (3)

ejgallego
ejgallego

Reputation: 6852

Indeed the best thing is to use the approach outlined by Vinz. Using some libraries would help, for instance, in mathcomp, which is specialized for reasoning about finite groups, you can create a type with n distinct elements just by writing 'I_n, and you will get for free many properties, such as finiteness.

Upvotes: 1

Vinz
Vinz

Reputation: 6047

Wild guess, but maybe something like:

Inductive ground_set (limit: nat): Set :=
  | Elem : forall n, n < limit -> ground_set limit.

Lemma ground_set_discr (limit:nat): forall n p (hn: n < limit) (hp: p < limit),
  n <> p -> Elem _ n hn <> Elem _ p hp.
Proof.
intros n p hn hp hdiff h.
inversion h; subst; clear h.
now apply hdiff.
Qed.

Upvotes: 4

Isabelle Newbie
Isabelle Newbie

Reputation: 9378

For Inductive definitions, you get inequalities between constructors for free:

Inductive ground_set : Type :=  A : ground_set | B : ground_set.

Lemma diff: A <> B.
Proof.
  discriminate.
Qed.

Upvotes: 2

Related Questions