Coq-Equations
Coq-Equations copied to clipboard
mattam82
Simplification gets stuck or diverges in simple use cases
Version
Coq 8.13.2
Equations 1.2.4
Operating system
Red Hat Enterprise Linux Workstation 7.4
Description of the problem
The following definition via equations cannot be simplified by any of the usual means, because they all get stuck.
From Equations Require Import Equations.
From Coq Require Import Lia.
Import PeanoNat.Nat Bool.Sumbool.
Obligation Tactic := idtac.
Equations f (n : nat) : nat :=
f n := S n.
Lemma neq_succ_f (n : nat) : f (S n) <> f n.
Proof.
simp f.
Fail progress simp f.
Fail rewrite f_equation_1.
Fail unfold f.
change (f n) with (S n).
lia. Qed.
The command has indeed failed with message:
Failed to progress.
The command has indeed failed with message:
Tactic generated a subgoal identical to the original goal.
The command has indeed failed with message:
f is opaque.
The simplification fails when the equation in question is true up to definitional equality and another instance of the result that would be produced by the equation is already present earlier in the expression.
The following definition via equations can only be simplified by some of the usual means, because most of them diverge, get stuck or produce garbage.
Equations g (n : nat) : nat by wf n :=
g n :=
if eqb (f n) 1 then 0 else
succ (g (pred (pred (f n)))).
Next Obligation.
intros n g.
simp f.
change (pred (S n)) with n.
(** Too few hypotheses. *)
Abort.
Equations g (n : nat) : nat by wf n :=
g n :=
if sumbool_of_bool (eqb (f n) 1) then 1 else
succ (g (pred (pred (f n)))).
Next Obligation.
intros n g.
simp f.
intros e.
apply eqb_neq in e.
lia. Qed.
Lemma neq_succ_g (n : nat) : g (S n) <> g n.
Proof.
Fail Timeout 1 simp g.
Fail unfold g.
rewrite g_equation_1.
simp f.
unfold eqb, sumbool_of_bool, succ, pred.
lia. Qed.
Getting provable obligations also takes some care.
The following definition via equations demonstrates how the interplay between these issues can really make life interesting.
Equations h (n : nat) : nat by wf n :=
h n :=
match f n with
| S (S p) => S (h p)
| _ => O
end.
Next Obligation.
intros n h _ p.
(** Too few hypotheses. *)
Abort.
Equations h (n : nat) : nat by wf n :=
h n :=
match f n with
| S (S p) => fun e : f n = S (S p) => S (h p)
| _ => fun e : f n = _ => O
end (eq_refl (f n)).
Next Obligation.
intros n h _ p e.
simp f in e.
lia. Qed.
Lemma neq_succ_h (n : nat) : h (S n) <> h n.
Proof.
simp f h.
Fail match goal with
| |- context [f] => fail "occurs f"
| |- context [h] => fail "occurs h"
end.
(** Too few and too many unfoldings at the same time. *)
Restart.
rewrite h_equation_1 at 1.
simp f.
lia. Qed.
Extra credit will be awarded to those
who dare replace f with g in the definition of h.
Notes
If you Set Equations Transparent before defining f and use unfold,
then the simplification will not get stuck and everything will be dandy.
Similarly, if you use rewrite instead of simp or unfold with g,
then the simplification will not diverge.
However, you always have to know beforehand
whether to use simp, rewrite or unfold,
because otherwise you will suffer.
That's a defect of rewrite/autorewrite in my opinion, the goal is clearly not the same when you rewrite f n to S n.
ssreflect's rewrite has no such problem.
The root of the problem here is linked to the fact we use Opaque but defined transparent constants that are badly handled by Coq itself.
I am sympathetic to your pleas of innocence, but since this is the reality we have to live in, I would like to know whether the appropriate course of action is to fix the underlying problems in Coq, to work around them in the equations plugin or to instruct the user to be more careful.
:) I would suggest using ssreflect's rewrite for now and reporting this issue on Coq.
While writing the report for coq/coq#14132,
I noticed that Program allows defining h by using the first presentation,
while the equations plugin fails to generate enough hypotheses.
Why do with clauses fail at the same task?
Ah, you just need to use the inspect pattern, like here: https://github.com/mattam82/Coq-Equations/blob/21967d62e62271e1bd379bdca29132881f59123d/examples/Basics.v#L520
Program automatically adds an equality at each pattern matching, but that's not something you want to do always, so Equations doesn't. Using inspect allows you to pattern match and remember the link with the value you matched on, and name the equality proof as you like.
Using that pattern in with clauses indeed works,
but also introduces definitions like h_unfold_clause_1,
which need to be unfolded by hand.
This would be a good situation to make use of autounfold,
just like we already do with autorewrite in simp.
Equations h (n : nat) : nat by wf n :=
h n with f n => {
| S (S p) => S (h p);
| _ => O
}.
Next Obligation.
intros n p h.
(** Too few hypotheses. *)
Abort.
Equations h (n : nat) : nat by wf n :=
h n with exist _ (f n) (eq_refl (f n)) => {
| exist _ (S (S p)) _ => S (h p);
| _ => O
}.
Next Obligation.
intros n p e h.
simp f in e.
lia. Qed.
Global Hint Unfold h_unfold_clause_1 : h.
Lemma neq_succ_h (n : nat) : h (S n) <> h n.
Proof.
simp f h.
autounfold with h.
Fail match goal with
| |- context [f] => fail "occurs f"
| |- context [h] => fail "occurs h"
end.
(** Too few and too many unfoldings at the same time. *)
Restart.
rewrite h_equation_1 at 1.
autounfold with h.
simp f.
lia. Qed.
The unfold hints for h_unfold are already available in the h_unfold database, so autounfold with h_unfold works (probably that's missing in the doc). We don't want to integrate that in the f database I think, as it would break the abstraction provided by the unfold definitions, which can be useful in some cases: one can name and prove things independently on these "nested" programs. Ideally they would not have those obfuscated names though...