Stream: math-comp users

Topic: Coercion issue


view this post on Zulip Pierre Jouvelot (Dec 15 2021 at 10:24):

I don't understand why the baz lemma fails, as apparently the coercion is not applied as it is in fooor bar. Since I don't know much about coercions I must be doing something wrong, and any suggestion would be appreciated.

From Coq Require Import Unicode.Utf8.
From mathcomp Require Import all_ssreflect.

Variable (n k : nat).

Record O :=
   Outcome {seq : (k.+1.-tuple 'I_n.+1);
            ouniq : uniq seq}.

Coercion seq_of x := seq x.

Canonical O_subType :=
  Eval hnf in [subType for seq_of].
Canonical O_eqType :=
  Eval hnf in EqType _     [eqMixin     of O by <: ].
Canonical O_choiceType :=
  Eval hnf in ChoiceType _ [choiceMixin of O by <:].
Canonical O_countType :=
  Eval hnf in CountType  _ [countMixin  of O by <:].
Canonical O_subCountType :=
  Eval hnf in [subCountType of O].
Canonical O_finType :=
  Eval hnf in FinType    _ [finMixin    of O by <:].
Canonical O_subFinType :=
  Eval hnf in [subFinType of O].

Lemma foo (o : O) : tnth o ord0 = ord0.
Admitted.

Lemma bar (o : O) (i : 'I_n.+1) : i \in seq_of o.
Admitted.

Fail Lemma baz (o : O) (i : 'I_n.+1) : i \in o.

view this post on Zulip Cyril Cohen (Dec 15 2021 at 12:07):

predType do not force the insertion of coercions, that's why you must instead add a new canonical instance:

From Coq Require Import Unicode.Utf8.
From mathcomp Require Import all_ssreflect.

Variable (n k : nat).

Record O :=
   Outcome {seq_of : (k.+1.-tuple 'I_n.+1);
            ouniq : uniq seq_of}.

Coercion seq_of : O >-> tuple_of.

Canonical O_subType :=
  Eval hnf in [subType for seq_of].
Canonical O_eqType :=
  Eval hnf in EqType _     [eqMixin     of O by <: ].
Canonical O_choiceType :=
  Eval hnf in ChoiceType _ [choiceMixin of O by <:].
Canonical O_countType :=
  Eval hnf in CountType  _ [countMixin  of O by <:].
Canonical O_subCountType :=
  Eval hnf in [subCountType of O].
Canonical O_finType :=
  Eval hnf in FinType    _ [finMixin    of O by <:].
Canonical O_subFinType :=
  Eval hnf in [subFinType of O].

Canonical O_predType := PredType (fun o x => x \in seq_of o).

Lemma inOE (o : O) (i : 'I_n.+1) : (i \in o) = (i \in seq_of o).
Proof. reflexivity. Qed.

view this post on Zulip Pierre Jouvelot (Dec 15 2021 at 13:36):

Thanks a lot, Cyril. This works like a charm.

view this post on Zulip Cyril Cohen (Dec 15 2021 at 13:40):

BTW I removed the detour through seq + seq_of, the point of which I did not understand, but feel free to restore it if I missed a point.


Last updated: Jan 29 2023 at 17:02 UTC