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: Mar 29 2024 at 04:02 UTC