In the following simplified example, the induction principle generated by Equations (in `bar_elim`

) is not helpful; it just unfolds the function body but without any useful hypotheses:

```
From Equations Require Import Equations.
Variable (A: Type) (B: Type).
Axiom foo : A -> option A.
Axiom measure : A -> nat.
Axiom foo_some: forall x y,
foo x = Some y ->
measure y < measure x.
Equations bar (a: A) : nat by wf (measure a) lt :=
bar x :=
match (foo x) as b return foo x = b -> nat with
| Some y => fun Heq => 1 + bar y
| None => fun _ => 1
end eq_refl.
Next Obligation.
apply foo_some in Heq; assumption.
Defined.
```

The induction principle is:

```
bar_elim
: forall P : A -> nat -> Type,
(forall x : A,
P x
(match foo x as b return (foo x = b -> nat) with
| Some y => fun _ : foo x = Some y => 1 + bar y
| None => fun _ : foo x = None => 1
end eq_refl)) -> forall a : A, P a (bar a)
```

Is there a different way to write this type of function so that Equations generates a useful induction principle? Or should I just do well-founded recursion on `measure a`

directly? Thanks

It does not seem surprising to me as you are not using Equations mechanism to write function like with clauses, so elaboration and automatic generation have no reasons to do anything interresting. Would the following work better ?

```
Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl.
Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
Equations bar (a: A) : nat by wf (measure a) lt :=
bar a with inspect (foo a) => {
| Some y eqn: Heq => 1 + bar y
| None eqn: _ => 1
}.
Next Obligation.
now apply foo_some.
Qed.
```

c.f. https://www.theozimmermann.net/platform-docs/ in particular https://www.theozimmermann.net/platform-docs/Tutorial_Equations_wf.html section 3.1

Thanks, that is very helpful. Is there a way to nest the `with`

clauses? I have two things I need to `inspect`

, but the second depends on the first being `Some`

.

Is that what you are thinking of?

```
Equations bar (a: A) : nat by wf (measure a) lt :=
bar a with inspect (foo a) => {
| Some y eqn: Heq with inspect (foo y) => {
| Some z eqn:Heq' => 1 + bar z
| None eqn:_ => _
}
| None eqn: _ => 1
}.
Next Obligation.
etransitivity.
all: apply foo_some ; eassumption.
Qed.
```

Yes that is what I am thinking of, thank you. One further question: is there a way to use this pattern with a nested function? I.e. inside `bar`

, I have a function that looks up the argument in a map, and if it is `Some`

, makes a recursive call to `bar`

. (I need this function in multiple places so it would be very inconvenient to inline). I again need the `Some`

proof to prove termination. I tried to use a mutually recursive function (with a `where`

clause), but Equations does not support mutual well-founded definitions.

I am not sure I understand. Could you try to write it down even if does not work so I can get an idea of what you want to do ?

It is something like this:

```
Axiom map: Type. (*maps from A to A, for instance*)
Axiom lookup: A -> map -> option A.
Equations bar (a: A) : nat by wf (measure a) lt :=
bar a with inspect (foo a) => {
| Some y eqn: Heq with inspect (foo y) => {
| Some z eqn:Heq' =>
let m := ... in (*map containing smaller elements*)
1 + baz z m
| None eqn:_ => _
}
| None eqn: _ => 1
}
where baz (z: A) (m: map) :=
baz z with inspect(lookup m z) => {
| Some y eqn:Heq => 1 + bar y
| None eqn:_ => _
}.
```

The crucial part is that `baz`

is a separate function (it also depends on other information from the context) and that it cannot be (nicely) inlined. We also need to know that `lookup`

gives `Some`

- we maintain invariants about the contents of the map that allow us to conclude that the elements arising from `lookup`

are smaller.

It is a bit specialised but what about sth like that ?

```
From Equations Require Import Equations.
Variable (A: Type).
Axiom measure : A -> nat.
Axiom foo : A -> option A.
Axiom foo_some: forall x y, foo x = Some y -> measure y < measure x.
Axiom map: Type. (*maps from A to A, for instance*)
Axiom lookup: A -> map -> option A.
Axiom lookup_some : forall x m y, lookup x m = Some y -> measure y < measure x.
Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl.
Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
Variable (m : map).
Equations? baz (a : A) (f : forall x, measure x < measure a -> nat)
(z : A) (H : measure z < measure a) (m : map) : nat :=
baz a f z H m with inspect(lookup z m) => {
| Some x eqn:Heq => 1 + f x _
| None eqn:_ => 1
}.
Proof.
etransitivity; [eapply lookup_some |]; eassumption.
Qed.
Equations? bar (a: A) : nat by wf (measure a) lt :=
bar a with inspect (foo a) => {
| Some y eqn: Heq with inspect (foo y) => {
| Some z eqn:Heq' =>
1 + baz a bar z _ m
| None eqn:_ => 1
}
| None eqn: _ => 1
}.
Proof.
etransitivity; apply foo_some; eassumption.
Qed.
```

Note the addition of a

```
Axiom lookup_some : forall x m y, lookup x m = Some y -> measure y < measure x.
```

Last updated: Oct 13 2024 at 01:02 UTC