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...
You probably need to add
Instance WellFounded_lt : WellFounded lt := lt_wf.
There is both well_founded
(a type scheme) and WellFounded
the type class
This topic was moved here from #Coq users > Equations in an abstract setting by Théo Zimmermann
Thx Jakob, this solves my question.
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: Oct 13 2024 at 01:02 UTC