See this example of `Equations`

raising a type error on an index mismatch of `fin`

while `Program Definition`

generates proof obligations. As far as I understand, the behavior should be to generate a proof obligation in both cases.

```
From Coq Require Import
Fin
List
Program.
From Equations Require Import
Equations.
Notation fin := t.
Equations list_replace{T}(l: list T)(i: fin (List.length l))(a: T): list T :=
list_replace (h::ts) F1 a := a :: ts;
list_replace (h::ts) (FS k) a := h :: list_replace ts k a.
Notation "v '@' i ':=' a" := (list_replace v i a) (at level 70).
Program Definition replace_twice{T}(l: list T)
(i j: fin (length l))(a: T): list T :=
let l' := l @ i := a in
l' @ j := a.
Fail Equations replace_twice{T}(l: list T)
(i j: fin (length l))(a: T): list T :=
replace_twice l i j a :=
let l' := l @ i := a in
l' @ j := a.
```

This topic was moved here from #Coq users > Equations type error on `fin t`

while `Program`

does not by Karl Palmskog.

IIUC, to summarise, `Program`

defers a failing judgemental equation as a propositional equality obligation, while `Equations`

is not doing. I'm no expert, but it seems plausible to me that these are the two natural design choices for what each mechanism is trying to achieve (simply typed programs with `Prop`

refinements vs dependently typed programs).

If you replace `l' @ j`

by `l' @ _`

then the `Equations`

command generates the same obligation. I'm not sure I find this intuitive, but it works

Last updated: Feb 27 2024 at 23:01 UTC