The Coq mailing list

["Eric Jaeger" <eric.jaeger AT sgdn.pm.gouv.fr>]

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