The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 13 Apr 2014 17:23:59 +0200,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 a écrit :

> 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.
> 
> 

Something like this?

Require Import List.

Record rec  : Type := mk_rec
  { t           : Type;
    stateset    : list t
  }.

Inductive t' : Type :=
  | A: t'.
Parameter P: t' -> Prop.

Definition ex_cast (a b : rec) : a = b -> t a -> t b :=
  fun eq x => match eq in _=y return t y with eq_refl => x end.

Example test:
  forall b (H : mk_rec t' (A::A::A::nil) = b),
   forall e, In (ex_cast _ b H e) (@stateset b) -> P e.
Proof.
  intros _ [].
  simpl.