CODEWITHSUNDEEP
coqssreflect
Teirflegne
Teirflegne

Reputation: 99

How can we define `eqType` for dependent types?

I want to define a dependent type as eqType. For example, suppose that we have defined the following dependent type Tn:

From mathcomp Require Import all_ssreflect.

Variable T: nat -> eqType.

Inductive Tn: Type := BuildT: forall n, T n -> Tn.

To make this of eqType, I defined an equality function Tn_eq for Tn:

Definition Tn_eq: rel Tn :=
  fun '(BuildT n1 t1) '(BuildT n2 t2) =>
    (if n1 == n2 as b return (n1==n2) = b -> bool
     then fun E => t1 == eq_rect_r T t2 (elimTF eqP E)
     else fun _ => false) (erefl (n1 == n2)).

Then I tried to prove the equality axiom for Tn_eq but it fails.

Lemma Tn_eqP: Equality.axiom Tn_eq.
Proof.
  case=>n1 t1; case=>n2 t2//=.
  case_eq(n1==n2).

I had an error here:

Illegal application: 
The term "elimTF" of type
 "forall (P : Prop) (b c : bool), reflect P b -> b = c -> if c then P else ~ P"
cannot be applied to the terms
 "n1 = n2" : "Prop"
 "b" : "bool"
 "true" : "bool"
 "eqP" : "reflect (n1 = n2) (n1 == n2)"
 "E" : "b = true"
The 4th term has type "reflect (n1 = n2) (n1 == n2)" which should be coercible to
 "reflect (n1 = n2) b".

How should I prove this lemma?

Upvotes: 2

Views: 334

Answers (2)

Cyril
Cyril

Reputation: 367

The best current way to do this in mathcomp with no extra help (cf below) is to use (partial) bijections, rather than defining the equality and its proof of correctness by hand:

Definition encode x := let: BuildT _ tn := x in Tagged T tn.
Definition decode (x : sigT T) := BuildT (tagged x).
Lemma encodeK : cancel encode decode. Proof. by case. Qed.
Definition Tn_eqMixin := CanEqMixin encodeK.
Canonical Tn_eqType := EqType Tn Tn_eqMixin.

Automated approaches are:

PS: if you really need to, you can always prove equality with your own relatively easily:

Lemma Tn_eqE : Tn_eq =2 eq_op.
Proof.
case=> [n tn] [m tm]; rewrite [RHS]/eq_op/= -tag_eqE/= /tag_eq/= /tagged_as/=.
by case: eqP => //= p; rewrite [elimTF _ _](eq_irrelevance _ p).
Qed.

(Sometimes it is indeed easier to prove program equality rather than the correctness from scratch.)

Upvotes: 2

Anton Trunov
Anton Trunov

Reputation: 15404

Here we go:

From Coq Require Import EqdepFacts.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Variable T: nat -> eqType.

Inductive Tn: Type := BuildT: forall n, T n -> Tn.

Definition Tn_eq: rel Tn :=
  fun '(BuildT n1 t1) '(BuildT n2 t2) =>
    (if n1 == n2 as b return (n1==n2) = b -> bool
     then fun E => t1 == eq_rect_r T t2 (elimTF eqP E)
     else fun _ => false) (erefl (n1 == n2)).

Lemma Tn_eqP: Equality.axiom Tn_eq.
Proof.
case=> n1 t1; case=> n2 t2 /=.
case: eqP => [eq1 | neq1]; last by constructor; case.
case: eqP.
- move=> ->; constructor; move: t2; rewrite [elimTF _ _]eq_irrelevance.
  by case: _ / eq1.
move=> neq2; constructor.
case=> _ exT; move: (eq_sigT_snd exT) => Cast; apply: neq2.
rewrite -Cast.
rewrite [eq_sigT_fst _]eq_irrelevance [elimTF _ _]eq_irrelevance.
by case: _ / eq1.
Qed.

Upvotes: 1

Related Questions