The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

Your example lacks of context for a precise answer. At least, in the
following simple example, "destruct H" does what I guess you are
expecting.

<<<<
Notation "[ 'rew' H 'in' a ]" := (eq_rect _ _ a _ H) (at level 0, H at level 
8).

Variable P:nat->Prop.
Variables t u:nat.

Goal forall (H:t=u) (a:P t) (b:P u), [rew H in a] = b.
intros.
destruct H.
simpl.
...
>>>>

Note that my few own experiments in using eq_rect to coerce types
required some energy but I'm far from an expert on this topic.

Hugo

> Hello everyone.
> 
> I have a serious problem with "eq_rect". Here is an example of what I want
> to prove. Unfortunately, my proof contains numerous equalities of that 
> kind. 
> 
> Lemma test i   n (el:list Expr_IL) l t u w db H :
> eq_rect (nth i (repeat_list st_iota n) ds) SDom
>         (sem_il (nth_typ i l (refl_equal (length el)) t) u w) st_iota
>        H db = 
> sem_il (eq_rect (nth i (repeat_list st_iota n) ds)
>                  (fun s => typExpr_IL pi (nth i el dE) s)
>                  (nth_typ i l (refl_equal (length el)) t) st_iota
>                  H)
>         u w db.
> Proof.
>   intros .
>   pattern H.
>   rewrite H.
> 
> These give me the error:
> 
> Abstracting over the term "nth i (repeat_list st_iota n) ds"
> leads to a term which is ill-typed.
> 
> Is there a way to prove such equalities, where dependent types are painful?
> 
> Thanks in advance. 
> 
> 
> -----
> Never say never.
> -- 
> View this message in context: 
> http://www.nabble.com/Problem-with-eq_rect-tp25062341p25062341.html
> Sent from the Coq mailing list archive at Nabble.com.
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club