Ssreflect Users Discussion List

[Emilio Jesús Gallego Arias <>]

Christian Doczkal 
<>
 writes:

> Section Rec2EQ.
>   Variables (A : eqType) (B : A -> eqType).
>   Record T := mkT { fst : A ; snd : B fst}.
>
>   Definition rec2_eq (x y : T) :=
>     let: (mkT x1 x2,mkT y1 y2) := (x,y) in Tagged B x2 == Tagged B y2.
>
>   Lemma rec2_eqP : Equality.axiom rec2_eq.
>   Proof.
>     move => [x1 x2] [y1 y2]. apply: (iffP idP); rewrite /rec2_eq.
>     - rewrite -tag_eqE /tag_eq /= => /andP [/eqP ?]. subst x1.
>       by rewrite tagged_asE => /eqP->.
>     - case => ? H ; subst y1. by rewrite /Tagged H.
>   Qed.
>
>   Canonical T_eqType := EqType T (EqMixin rec2_eqP).
> End Rec2EQ.

Also note that I think that using the subtype interface is preferable in
this case, so you can inherit all the interfaces that record members
possess:

8<----------------------------------------------------------------------8<
From mathcomp Require Import all_ssreflect.

Section Rec2Sub.

Variables (A : Type) (B : A -> Type).
Record T := mkT { fst : A ; snd : B fst}.

Definition of_T f : { fst : A & B fst } := existT _ f.(fst) f.(snd).
Definition to_T '(existT fst snd) := {| fst := fst; snd := snd |}.

Definition T_sub : @subType { fst : A & B fst} xpredT.
apply: (@NewType _ _ of_T to_T); last by case.
by move=> P K [fst snd]; have := K (existT _ fst snd).
Defined.

Canonical T_subType := Eval hnf in T_sub.
End Rec2Sub.

Section Rec2EqType.
Variables (A : eqType) (B : A -> eqType).
Canonical T_eqType  := Eval hnf in EqType _ [eqMixin of (@T A B) by <: ].
End Rec2EqType.

Section Rec2ChoiceType.
Variables (A : choiceType) (B : A -> choiceType).
Canonical T_choiceType  := Eval hnf in ChoiceType _ [choiceMixin of (@T A B) 
by <: ].
End Rec2ChoiceType.
8<----------------------------------------------------------------------8<

E.