Ssreflect Users Discussion List

[Christian Doczkal <>]

Hi, 

On 06/18/2018 05:37 PM, Bas Spitters wrote:
> I'd imagine first proving that eqTypes are closed under Sigma-types
> and then converting records to Sigma-types, as e.g. is done in the
> HoTT library:

Closure of eqTypes (and also finTypes) under Sigma-Types is already in the 
library (see tag_eqType)

From that it is not to hard to get an eqType instance also for dependent 
record types (see below). Not sure though how to best generalize this over 
the constructors of a concrete record type or how to best iterate this.

Best,
Christian

--------------------8<---------------------------------

From mathcomp Require Import all_ssreflect.

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.