The Coq mailing list

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

  Hi,

> After some time working with Coq, I've chosen for one of my projects (in 
> which I don't care about impredicativity or proof irrelevance, but have 
> difficulties to "eliminate" Prop hypothesis with a Set goal) 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".
> 
> Is there a solution to work with Coq without using Prop at all ? Or, at 
> least, to have Coq generate indentity results instead of equality results ?

  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.

  Conversely, if inversion were internally changed so that it
generates equalities in identity, I'm afraid this would become odd for
users used to think about equality as a proposition.

  Alternatively, some approximation of inversion relying on identity
could be rewritten in ltac.

  Hope it helps,

  Hugo Herbelin

------------------------------
Lemma eq_id : forall A (x y:A), x=y -> identity x y.
Proof. intros A x y H; rewrite H; constructor. Qed.

Lemma id_eq : forall A (x y:A), identity x y -> x=y.
Proof. intros A x y H; rewrite H; constructor. Qed.

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
*)