Stream: math-comp users

Topic: finType and card


view this post on Zulip Shengyi Wang (Oct 24 2022 at 14:48):

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.

view this post on Zulip Karl Palmskog (Oct 24 2022 at 14:54):

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.

view this post on Zulip Shengyi Wang (Oct 24 2022 at 15:02):

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?

view this post on Zulip Karl Palmskog (Oct 24 2022 at 15:03):

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

view this post on Zulip Shengyi Wang (Oct 24 2022 at 15:09):

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.

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 15:54):

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.

view this post on Zulip Shengyi Wang (Oct 24 2022 at 16:03):

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

view this post on Zulip Shengyi Wang (Oct 24 2022 at 16:19):

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?

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 16:26):

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.

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 16:28):

And then since I used cancel instead of pcancel, I also changed PcanXMixin to CanXMixin

view this post on Zulip Shengyi Wang (Oct 24 2022 at 16:31):

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.

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 16:33):

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.

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 16:34):

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

view this post on Zulip Ana de Almeida Borges (Oct 24 2022 at 16:35):

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

view this post on Zulip Shengyi Wang (Oct 24 2022 at 16:41):

Great! Thank you very much for all the help!


Last updated: Jan 29 2023 at 18:03 UTC