I'm a newbie in mathcomp. I followed the Section 8.5 of the Mathematical Components book, defined an inductive type and linked it to the theory of finType via `PcanXXXMixin`

family of lemmas like this:

```
Inductive traficlight: predArgType := Red | Yellow | Green.
Definition trafic2ord (t: traficlight): 'I_3 :=
match t with
| Red => inord O | Yellow => inord 1 | Green => inord 2
end.
Definition ord2trafic (o: 'I_3): option traficlight :=
match val o with
| O => Some Red | 1 => Some Yellow | 2 => Some Green
| _ => None
end.
Lemma pcan_trafic_ord: pcancel trafic2ord ord2trafic.
Proof. by case; rewrite /ord2trafic /= inordK. Qed.
Definition traficlight_eqMixin := PcanEqMixin pcan_trafic_ord.
Canonical traficlight_eqType := EqType traficlight traficlight_eqMixin.
Definition traficlight_choiceMixin := PcanChoiceMixin pcan_trafic_ord.
Canonical traficlight_choiceType := ChoiceType traficlight traficlight_choiceMixin.
Definition traficlight_countMixin := PcanCountMixin pcan_trafic_ord.
Canonical traficlight_countType := CountType traficlight traficlight_countMixin.
Definition traficlight_finMixin := PcanFinMixin pcan_trafic_ord.
Canonical traficlight_finType := FinType traficlight traficlight_finMixin.
Check (Red != Yellow) && (Red \in traficlight) && (#| traficlight | == 3).
```

Everything looks fine until I tried to prove some simple fact: `Goal #| traficlight | == 3.`

The tactic like `by rewrite cardT enumT unlock.`

does not work. Any suggestions? Thank you very much.

sorry for a probably-not-what-you-want solution, but all these canonical instances should be generatable from only the inductive type by Deriving: https://github.com/arthuraa/deriving

.. which may also make solving the goal easier.

I see. Thank you. From the README of Deriving, it seems that I still need to write a bunch of XXX_xxMixin and XXX_xxType. But I don't need to write the 1-to-1 mapping functions, right?

right, you can skip that boilerplate. I think the other boilerplate can be lessened somewhat by using Hierarchy builder

Thank you again! There are so many excellent math-comp related packages to learn. I definitely will put them in my TODO list. Let me try to get familiar with the basis of math-comp first, like proving this first simple fact.

I've been trying to prove your lemma and I also can't figure it out. My solution is to define the fin mixin in a different way:

```
Lemma traficlight_fin : Finite.axiom [:: Red; Yellow; Green].
Proof. by case. Qed.
Definition traficlight_finMixin := FinMixin traficlight_fin.
Canonical traficlight_finType := FinType traficlight traficlight_finMixin.
Goal #|traficlight| == 3.
Proof. by rewrite cardT enumT unlock. Qed.
```

I'm sure there must be a way of doing it with your encoding though.

PS: It's spelled "traffic", with two f.

Thank you very much! Sorry for the typo :smile: .

Hi @Ana de Almeida Borges , I tried you code but I can not even go through the second line `by case.`

Did you also define eq mixin in a different way?

Oh, sorry, yes I did. I was trying alternative encodings and forgot I hadn't changed it back. Here is the one I used:

```
Definition trafic2ord (t: traficlight): 'I_3 :=
match t with
| Red => @Ordinal 3 0 isT
| Yellow => @Ordinal 3 1 isT
| Green => @Ordinal 3 2 isT
end.
Definition ord2trafic (o: 'I_3): traficlight :=
match val o with
| O => Red | 1 => Yellow | 2 => Green
| _ => Red
end.
Lemma pcan_trafic_ord: cancel trafic2ord ord2trafic.
Proof. by case. Qed.
```

And then since I used `cancel`

instead of `pcancel`

, I also changed `PcanXMixin`

to `CanXMixin`

Thank you so much! Now I'm considering define all those kind of Mixin and xxType directly by the naive way. Just like bool etc in the library of ssreflect.

You can also prove it with your encoding, it just needs a little more work:

```
Lemma traficlight_fin : Finite.axiom [:: Red; Yellow; Green].
Proof. by case=> /=; do 3!case: eqP. Qed.
```

That seems strictly worse than defining everything up to `countType`

your way and then defining `finType`

manually (I mean, you already have it, so no extra work).

Still, maybe someone more knowledgeable will show up and answer your original question.

Great! Thank you very much for all the help!

Cyril Cohen has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC