The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Without checking whether I'm right or not :

The rewrite tactics in the left-to-right direction needs an elimination 
principle called /inductivename/_rec_r (r is for reverse I reckon). In 
your case it would be inductive_rec_r . To prove the right rec_r lemma. 
Search the standard library for eq_rec_r ( Check eq_rec_r ).

I insist on the fact that the name of the statement matters.


Arnaud Spiwack

Eric Jaeger a écrit :
> Thanks for the tactic "inversion_set", it is really useful. But I'm now
> facing a small problem, that appears to me as a weird behaviour of the
> rewrite tactic (with Notation "A _= B":=(@identity _ A B) (no associativity,
> at level 70) where "_="  is the UTF-8 equiv):
> ...
> H:d<='i (* <= is a notation for an inductive dependant type in Set *)
> i0:d_=si
> ...
> --------
> (some term in which d occurs free as well)
> "rewrite i0 in H" causes an error "User error: the type of elimination
> clause is not well-formed" (while the goal, hypothesis and the type T of d
> and i all inhabit Set). The strangest thing however is that to make the
> rewrite, it is sufficient is such case to use instead "rewrite <- (sym_id
> i0) in H".
>
> Any clue?
>
>     Best Regards, Eric Jaeger
>
>   
> > > After some time working with Coq, I've chosen ... to work without
> > > using the Prop sort, but Set instead... It's of course fine for my
> > > definitions, etc. and I was happy to discover that tactics such as
> > >       
> rewrite
>   
> > > can use identity as well as equality. However, I still have difficulties
> > >       
> to
>   
> > > get rid of Prop - in particular as far as equality is concerned.
> > >
> > > As an example, if for "S:Set" I define "Inductive
> > > ind_id:S->S->Set:=ii_intro:forall (a:S), ind_id a a", then the inversion
> > > tactic applied to an hypothesis "ind_id a b" will return "a=b", while I
> > > would prefer "identity a b".
> > >       
> > The definitions of eq and identity are equivalent. So, a possibility
> > is to (superficially) hack inversion so that it generates equalities
> > using identity rather than eq (see below). This remains superficial as
> > the proof term still explicitly refers to eq.
> >
> >   Alternatively, some approximation of inversion relying on identity
> > could be rewritten in ltac.
> >
> > Ltac repeat_on_hyps f := repeat (match goal with [ H:_ |- _ ] => f H end).
> > Ltac coerce3 f H := let H':= fresh in (assert (H':=f _ _ _ H); clear H;
> >     
> rename H' into H).
>   
> > Ltac inversion_set c := inversion c; repeat_on_hyps ltac:(coerce3 eq_id).
> >
> > Variable S:Set.
> > Inductive ind_id:S->S->Set:=ii_intro:forall (a:S), ind_id a a.
> >
> > Goal forall x y, ind_id x y -> ind_id y x.
> > intros x y H.
> > inversion_set H.
> > (*
> >   x : S
> >   y : S
> >   H : ind_id x y
> >   a : S
> >   H1 : identity x y
> >   H0 : identity a x
> >   ============================
> >    ind_id y y
> > *)
> > Hugo Herbelin
> >     
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/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
>
>
>