With `Set Definitional UIP`

, we have the following behaviors:

```
Set Definitional UIP.
Inductive seq {A} (a:A) : A -> SProp := srefl : seq a a.
Arguments srefl {_ _}.
Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A :=
match e with srefl => eq_refl end.
Parameter d : seq 0 1.
Eval lazy head in seq_to_eq ((fun a => a) d).
(* match (fun a : seq 0 1 => a) d in (seq _ a) return (0 = a) with
| srefl => eq_refl
end *)
Eval cbv head in seq_to_eq ((fun a => a) d).
(* match d in (seq _ a) return (0 = a) with
| srefl => eq_refl
end *)
```

I suspect that `cbv`

has the intended behavior, but I'm not so sure.

IDK lazy seems fine

The reason I'm saying that `cbv`

seems to have the intended behavior is that if we see the SProp case as adding something to the non-SProp case, then, when the "adding something" does not apply, one may expect that it behaves at least as in the following non-SProp variant:

```
Inductive seq {A} (a:A) : A -> Prop := srefl : seq a a.
Arguments srefl {_ _}.
Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A :=
match e with srefl => eq_refl end.
Parameter d : seq 0 1.
Eval lazy head in seq_to_eq ((fun a => a) d).
(* match d in (seq _ a) return (0 = a) with
| srefl => eq_refl
end *)
```

why would different things behave the same?

equality in sprop (with definitional uip) has the special match reduction rule which does not look at the term which is matched on

Last updated: Oct 13 2024 at 01:02 UTC