I don't understand why the `baz`

lemma fails, as apparently the coercion is not applied as it is in `foo`

or `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.
```

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

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

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: Jul 25 2024 at 14:01 UTC