Ssreflect Users Discussion List

[Cyril <>]

Hi,
very often, eqType (resp. choiceType, finType, countType) structures are 
obtained by an encoding which is an injection (with or without explicit 
partial inverse, depending on the structure) into a canonical eqType 
(resp...). This canonical eqType (resp...) is generally a combination of 
variable or constant eqType (resp...) using option type, sums, sigma 
types or the generic tree type (GenTree.tree from choice.v).
Unfortunately, as of today the encoding and the proof has to be provided 
by hand.

To take the example of Christian, here would be the most canonical way 
to do it.

----------------->8--------------------------------------------
Section Rec2EQ.
Variables (A : eqType) (B : A -> eqType).
Record T := mkT {fst : A ; snd : B fst}.

Definition Tencode (t : T) := Tagged B (snd t).
Definition Tdecode (t : {a : A & B a}) : T := mkT _ (tagged t).
Lemma TencodeK : cancel Tencode Tdecode. Proof. by case. Qed.

Definition T_eqMixin := CanEqMixin TencodeK.
Canonical T_eqType := EqType T T_eqMixin.
End Rec2EQ.
----------------->8--------------------------------------------

--
Cyril

On 19/06/2018 12:45, Emilio Jesús Gallego Arias wrote:
> 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.