The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

In an intensional type theory like Coq, even if you have types A and B that are propositionally equal (e.g. you have a proof of A=B),

a member of A is not a member of B unless A and B are definitonally equal ( A computes to B or vice versa).

This is necessary to keep typechecking decidable (definitial equality is decidable, but propositional equality is not).

So you need to do a "type-cast" with the propositional equality to do change the type of a term.

Recall that A=B is a notation for (eq A B), where eq is an inductively defined proposition.

Using the generated induction principle of eq (which is eq_rect), one can define such a "typecast" operator (see typeCast below).

After typecasting, the statement of your lemma typechecks (Coq 8.4pl2) :

Require Import List.

Definition transport {T:Type} {a b:T} {P:T -> Type} (eq:a=b) (pa: P a) : (P b):=

@eq_rect T a P pa b eq.

Definition typeCast {A B:Type}  (eq:A=B) (pa: A) : (B):=

@eq_rect Type A (fun X => X) pa B eq.

Record rec  : Type := mk_rec

  { t           : Type;            

    stateset    : list t 

  }.

Inductive t' : Type :=  

  | A: t'.

Parameter P: t' -> Prop.

Lemma requality : forall {b T l},

b = mk_rec T l

-> t b = T.

Proof.

 intros  ? ? ? H. 

rewrite H. auto.

Qed.

Example test:

  forall b (p : b = mk_rec t' (A::A::A::nil)),

   forall e, In e (@stateset b) -> P ( typeCast (requality p) e).

Proof.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Apr 13, 2014 at 11:23 AM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Hello.

Consider the following:

Require Import List.

Record rec  : Type := mk_rec

  { t           : Type;            

    stateset    : list t 

  }.

Inductive t' : Type :=  

  | A: t'.

Parameter P: t' -> Prop.

Example test:

  forall b, b = mk_rec t' (A::A::A::nil) ->

   forall e, In e (@stateset b) -> P e.

Proof.

I cannot type the above lemma, as I get

Error: In environment

b : rec

e : t b

The term "e" has type "t b" while it is expected to have type "t'".

but t b, is actually equal to t'.. how can I make it work?

Cheers.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.