Stream: Equations devs & users

Topic: Equations type error on `fin t` while `Program` does not

Lef Ioannidis (Mar 08 2022 at 16:04):

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.

Notification Bot (Mar 08 2022 at 16:04):

This topic was moved here from #Coq users > Equations type error on fin t while Program does not by Karl Palmskog.

James Wood (Mar 10 2022 at 14:09):

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

Yannick Forster (Mar 10 2022 at 14:53):

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: May 28 2023 at 18:29 UTC