The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You should be able to go a bit further: you can implement an alternate version of `inversion_sigma` which uses alternate versions of the the *_rect lemmas where all transports across equality proofs are instead transports across `seq2eq (eq2seq e)`, and then you won't need to explicitly invoke UIP at all, as things will just reduce.  Alternatively, you can add yet another postprocessing tactic which looks for equality proofs in the context which are used in places not under eq2seq and replaces all uses of them with a round-trip through seq.

On Sat, Jun 5, 2021, 23:19 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

Thanks, Jason!  Here it is:

Set Definitional UIP.

Inductive seq {A} (a:A) : A -> SProp :=
  srefl : seq a a.

Definition seq2eq{T}{a b:T}(s:seq a b) : a=b :=
  match s with srefl _ => eq_refl end.

Definition eq2seq{T}{a b:T}(e:a=b) : seq a b :=
  match e with eq_refl => srefl _ end.

Lemma invseqeq: forall {T}{a b:T}(e:a = b), e = seq2eq (eq2seq e).
Proof.
  intros T a b e. destruct e. reflexivity.
Qed.

Lemma UIP_refl: forall T (a:T)(e:a = a), e = eq_refl.
Proof.
  intros T a e. rewrite (invseqeq e). reflexivity.
Qed.


On Sat, 5 Jun 2021 22:11:47 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> Based on the documentation in
> https://coq.inria.fr/refman/addendum/sprop.html#coq:flag.Definitional-UIP,
> it looks like you should be able to define a function `f : seq x y ->
> x = y` and then you can prove that this function is the inverse of
> the function `g : x = y -> seq x y`.  With this flag on, it should be
> the case that matches on `f (g p)` will reduce away whenever x and y
> are definitionally equal, hence avoiding the need to invoke UIP
> explicitly.
>
> Does this work?
>
> On Sat, Jun 5, 2021, 20:16 jonikelee AT gmail.com <jonikelee AT gmail.com>
> wrote:
>
> > I just noticed Set Definitional UIP.  Is there a way to use this to
> > avoid needing to define a normal Prop (non SProp) UIP to handle
> > inversions that result in sigT equalities?  Normally, these cases
> > involve inversion; inversion_sigma; UIP to replace the equality arg
> > of the eq_rect with eq_refl to allow it to reduce. Do I still need
> > normal Prop UIP for such cases, or is there a way to bypass it?
> >
> >
> >