Hi, could you confirm that funelim never terminates on ack in the following basic code ?

Would you have an idea why ? I am using Coq 8.19 and the associated equation version.

```
From Equations Require Import Equations.
Equations ack (m n : nat) : nat by wf (m, n) (Equations.Prop.Subterm.lexprod _ _ lt lt) :=
ack 0 n := S n;
ack (S m) 0 := ack m 1;
ack (S m) (S n) := ack m (ack (S m) n).
Definition ack_incr {m n} : ack m n < ack m (n+1).
Proof.
(* Bugs *)
funelim (ack m n).
```

Did you try `apply_funelim`

?

Applying the eliminator directly with apply_funelim and a few tricks most likely works, but I am not trying to prove the goal at the moment.

`apply_funelim`

does less than `funelim`

so I wanted to know which one was already looping.

apply_funelim works fine would it seems

at least it creates goal

I am mostly interested because last time we had a weird experience with Matthieu with the bug present on only my computer.

Matthieu had exactly the same config, or at least it seemed so at the moment, but with this fix https://github.com/mattam82/Coq-Equations/pull/593

So I am trying to understand if the bug is linked to a particular configuration or "solve" by the fix.

I have another weird issue with `ack`

, `simp`

does not manage to simplify even if direct rewriting works:

```
Definition ack_incr {m n} : ack m n < ack m (n+1).
Proof.
apply ack_elim.
- intro n'; simp ack. (* It does not simplify the left side ack 0 (n' + 1) to S (n' + 1) *)
rewrite ack_equation_1 at 1. (* but this works without issue *)
```

I imagine it is an issue with the rewrite, because `rewrite ack_equation_1`

doesn't work, I need to add `at 1`

for it to work.

Otherwise, I get the error message

Tactic generated a subgoal identical to the original goal.

But I really don't get why, the goal is `S n' < ack 0 (n' +1)`

and `ack_equation_1 : forall n, ack 0 n = n`

That check might be done considering ack is transparent ?

Matthieu Sozeau said:

That check might be done considering ack is transparent ?

I am not sure how to check that. It tells me ack is opque if I try to unfold. Maybe rewrite see at as transparent ?

But actually, what really surprises me is that it I only have this bug with ack, and not with any other functions I have tried

I suspect the reason is that rewrite first tries to unify `S n'`

with `ack 0 n'`

and succeeds, thus rewriting `S n'`

to `S n'`

.

By running

```
Definition ack_incr {m n} : ack m n < ack m (n+1).
Proof.
apply ack_elim.
- intro n'.
Set Debug "RAKAM".
Fail rewrite ack_equation_1.
```

You can actually see the LHS beeing selected. Which means internally Coq's rewrite performs the analogous of

```
Definition ack_incr {m n} : ack m n < ack m (n+1).
Proof.
apply ack_elim.
- intro n'.
pattern (ack 0 (n' + 1)).
rewrite ack_equation_1.
```

This is why ssreflect's rewrite first performs a purely syntactical step to match head constants (here `ack`

)

```
From Coq Require Import ssreflect.
Definition ack_incr {m n} : ack m n < ack m (n+1).
Proof.
apply ack_elim.
- intro n'.
rewrite ack_equation_1.
```

does not fail.

We looked at it with Thomas and it boils down to the following MWE:

```
(* A generic type to test rewriting of a goal *)
Inductive LULE {A : Type} (a b : A).
Definition suc (m : nat) : nat := S m.
Lemma u : forall n : nat, suc n = S n.
Proof.
intro n.
exact eq_refl.
Qed.
Goal forall (n : nat), LULE (S n) (suc n).
Proof.
intro n.
(* Without specifying n, rewrites the first index (S n) to (S n) *)
Fail rewrite u.
(* By specifying n, rewrites the second index (suc n) to (S n) *)
rewrite (u n).
Admitted.
Definition id (m : nat) : nat := m.
Lemma u' : forall n : nat, id n = n.
Proof.
intro n.
exact eq_refl.
Qed.
Goal forall (n : nat), LULE n (id n).
Proof.
intro n.
(* Without specifying n, rewrites the second index (id n) to n *)
rewrite u'.
Admitted.
```

@Cyril Cohen

this doesn't happen with `setoid_rewrite`

, so maybe it would be a better fit for `simp`

?

Is there a way to make Equations use setoid rewrite rather than rewrite by default ?

If I can give you one advice (1), stray as far as possible from setoid_rewrite as you can

scalability issues are waiting for you down the road ready to hit you with big sticks on your head

Wanna fix rewrite then ?

In other word, in my tutorial, what should I say to users if they face this issue ?

Wanna fix rewrite then ?

hard. The alternative is to use a sane pattern selection algorithm, like advocated by @Cyril Cohen yesterday

Otherwise, I am also fine with using SSReflect rewrite in Equations instead

Is there a way to make Equations use SSReflect rewrite rather than rewrite by default ?

Require ssreflect at the beginning?

no, I guess you would have to fix Equations directly ? :man_shrugging:

I think that replacing tactics under the feet of the user is a very bad practice

I cannot count the time I've lost believing I was calling some piece of code instead of the actual one

Also, for the purpose of the tutorial, couldn't you just pass the right argument to `ack_equation_1`

?

Might be the more reasonable approach indeed

The bug is due to pattern selection indeed. But also when definitions are transparent equations wrongly tried to reduce in the equality to rewrite resulting in the loop. I’m working on a fix for that one.

The pattern selection issue can also be tamed using "Set Keyed Unification", which also forces syntactic match on the head of the pattern for vanilla "rewrite".

Otherwise, @Matthieu Sozeau , do you know why funelim is slow here ? Is it the loop thing you are mentioning ?

(The original message from the thread)

Yes, it tried to reduce the ack calls. I think we hit the same issue a few times in MetaCoq actually, where we replaced calls with `apply_funelim`

due to that.

Otherwise, I love this proof :

```
Definition ack_incr {m n} : ack m n < ack m (1+n). (* notice the 1+n rather than n+1 *)
Proof.
apply ack_elim; intros.
- Fail progress autorewrite with ack. auto. (* ok . simp ack works too *)
Admitted
```

So you can actually solve the goal by pure chance with the following:

```
Definition ack_incr {m n} : ack m n < ack m (1+n).
Proof.
apply ack_elim; intros; simp ack; apply ack_min. (* ack_min m n : n < ack m n *)
Qed.
```

Pierre-Marie Pédrot said:

scalability issues are waiting for you down the road ready to hit you with big sticks on your head

Are these documented somewhere? Are there plans to fix them? (probably not)

Last updated: Oct 13 2024 at 01:02 UTC