Stream: Equations devs & users

Topic: Equations in an abstract setting


view this post on Zulip Yves Bertot (Jun 12 2020 at 09:07):

Hello, I try to develop a minimal teaching example of Equations where inspect patterns are used. I would like this example to run in an abstract context.

From Equations Require Import Equations.
Require Import List.

Inductive hide (P : Prop) := hide_cons : P -> hide P.

Section iterates.

Variable (A : Type) (f : A -> option A) (lt : A -> A -> Prop).
Hypothesis lt_wf : well_founded lt.

(* We don't want this hypothesis to be used automatically by Equations. *)
Hypothesis decr_f : hide (forall n p, f n = Some p -> lt p n ).

Definition f_inspect (n : A) : {p' | f n = p'} :=
  exist _ (f n) eq_refl.

Equations f_sequence (n : A) : list A by wf n lt :=
  f_sequence n with f_inspect n := {
    | exist _ (Some p) eq1 => p :: f_sequence p;
    | exist _ None  _ => nil
    }.

But this fails with a message "Unable to satisfy the following constraints: .... ?w : WellFounded ,,,". What should I add to avoid this message? I understand it is a configuration of the type classes mechanism...

view this post on Zulip Jakob Botsch Nielsen (Jun 12 2020 at 09:08):

You probably need to add

Instance WellFounded_lt : WellFounded lt := lt_wf.

view this post on Zulip Jakob Botsch Nielsen (Jun 12 2020 at 09:09):

There is both well_founded (a type scheme) and WellFounded the type class

view this post on Zulip Notification Bot (Jun 12 2020 at 09:37):

This topic was moved here from #Coq users > Equations in an abstract setting by Théo Zimmermann

view this post on Zulip Yves Bertot (Jun 12 2020 at 09:46):

Thx Jakob, this solves my question.

view this post on Zulip Yves Bertot (Jun 12 2020 at 10:09):

In fact, another solution is to declare the various variables in the following manner.

Context {A : Type} (f : A -> option A) {lt : A -> A -> Prop}
 `{WellFounded A lt}.

Last updated: Jan 29 2023 at 16:02 UTC