Как ввести n различных символов в Coq

Question

Я создал запись для группы. Теперь я хотел бы построить группу с n элементами (например, 10 элементов), указав таблицу групповой умножения.

Моя проблема в том, что мне нужны n символов, которые будут служить в качестве основного набора для моей группы. Мне понадобится Кок, чтобы знать, что эти n элементов различны.

До сих пор я понял

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

, который работает при п = 2. Я не знаю, как масштабировать это для многих элементов, не создавая какой-то уродливый код.

Я бы предположил, что есть лучший способ создать такой набор, но я не смог его найти.

Answer 1

Wild догадка, но, возможно, что-то вроде:

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. 

Answer 2

Для Inductive определения, вы получите неравенства между конструкторами бесплатно:

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

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

Answer 3

Действительно, лучше всего использовать подход, изложенный Vinz , Использование некоторых библиотек поможет, например, в mathcomp, который специализируется на рассуждениях о конечных группах, вы можете создать тип с n отдельными элементами, просто написав 'I_n, и вы получите бесплатно многие свойства, такие как конечность.