Paolo Giarrusso said:

Last link: while Théry's cited paper had non-constructive steps, both https://github.com/coq-community/buchberger and https://github.com/thery/grobner seem free of classical axioms.

`make validate`

on the first only reports axiom K (`Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq`

), which is pretty constructive :-)

I made the coq-community buchberger project axiom free now using Equations. However, `make validate`

/`coqchk`

still reports axioms since Equations itself uses some axioms, but not in the parts that I actually use. Sigh.

since `acc_A_B_lexprod`

from Stdlib uses `eq_rect_eq`

(sigh again), I reimplemented it

https://github.com/coq/coq/pull/15254

thanks a lot! I was thinking of doing that myself, but dependent pattern matching without Equations is not my strong side.

@Pierre-Marie Pédrot (followup on discussion in Gaëtan's PR) is your general advice/position that everyone who develops a Coq library should make all `well_founded`

proofs `Qed`

and use the unfolding trick?

To say something less controversial, tactics like inversion or auto in a Defined proof are suspect, and most safe tactics can be converted into proof terms (so they should); decide equality (and relatives) are among the few exceptions I'm familiar with.

yeah my general position/style has been to have stuff in Prop live separately Qed'd and to use `Program`

to split things up. But `well_founded`

has been the exception since I usually want to compute by default without trickery

I also use that policy, it's just that not all of Prop is proof-irrelevant. So stupid question: Is any part of that proof easy to Qed'ed? Is the leftover transparent code more canonical? Sorry for not trying myself.

If not, qed + "eta" (the unfolding trick) seems appropriate. That's what the ecosystem does for equality as well, tho the only "eta-like" trick is Hedberg's theorem?

Is there a simple way to de-Equationize this proof using `EqdepFacts`

while avoiding UIP?

```
From Coq Require Import Arith Relation_Definitions.
From Equations Require Import Equations.
Inductive mon : nat -> Set :=
| n_0 : mon 0
| c_n : forall d : nat, nat -> mon d -> mon (S d).
Derive Signature NoConfusion NoConfusionHom for mon.
Inductive mdiv : forall d : nat, mon d -> mon d -> Prop :=
| mdiv_nil : mdiv 0 n_0 n_0
| mdiv_cons :
forall (d : nat) (v v' : mon d) (n n' : nat),
n <= n' -> mdiv d v v' -> mdiv (S d) (c_n d n v) (c_n d n' v').
Derive Signature for mdiv.
Lemma mdiv_trans : forall d : nat, transitive (mon d) (mdiv d).
Proof.
intros d; elim d; unfold transitive in |- *; auto.
- intros x y z mdiv_xy.
depelim mdiv_xy; auto.
- intros n Rec x y z mdiv_xy mdiv_yz.
depelim mdiv_xy.
depelim mdiv_yz.
apply mdiv_cons.
* apply le_trans with (m := n'); auto.
* apply Rec with (y := v'); auto.
Qed.
```

```
From Coq Require Import Arith Relation_Definitions EqdepFacts Eqdep_dec.
Inductive mon : nat -> Set :=
| n_0 : mon 0
| c_n : forall d : nat, nat -> mon d -> mon (S d).
Inductive mdiv : forall d : nat, mon d -> mon d -> Prop :=
| mdiv_nil : mdiv 0 n_0 n_0
| mdiv_cons :
forall (d : nat) (v v' : mon d) (n n' : nat),
n <= n' -> mdiv d v v' -> mdiv (S d) (c_n d n v) (c_n d n' v').
Lemma mdiv_inv : forall d x y,
mdiv d x y <->
match d return mon d -> mon d -> Prop with
| 0 => fun x y => n_0 = x /\ n_0 = y
| S d => fun x y => exists v v' n n', n <= n' /\ mdiv d v v' /\ c_n d n v = x /\ c_n d n' v' = y
end x y.
Proof.
intros d x y;split.
- intros m;destruct m;eauto 8.
- destruct d;intros m.
+ destruct m as [[] []];constructor.
+ destruct m as [? [? [? [? [? [? [[] []]]]]]]].
constructor;assumption.
Defined.
Lemma mdiv_trans : forall d : nat, transitive (mon d) (mdiv d).
Proof.
intros d; elim d; unfold transitive in |- *; auto.
- intros x y z mxy myz.
apply mdiv_inv in mxy;apply mdiv_inv in myz.
apply mdiv_inv.
intuition.
- intros n Rec x y z mxy myz.
apply mdiv_inv in mxy;apply mdiv_inv in myz.
destruct mxy as [vxy [vxy' [nxy [nxy' [Hnxy [Hdivxy [eq1 eq2]]]]]]].
destruct myz as [vyz [vyz' [nyz [nyz' [Hnyz [Hdivyz [eq3 eq4]]]]]]].
destruct eq1,eq2,eq4.
injection eq3;clear eq3;intros eqv eqn.
destruct eqn.
pose proof (eq_sigT_snd eqv) as eqv'.
rewrite (UIP_refl_nat n _) in eqv'.
simpl in eqv';destruct eqv';clear eqv.
apply mdiv_cons.
* apply le_trans with (m := nyz); assumption.
* apply Rec with (y := vyz); assumption.
Qed.
```

Eqdep_dec should really be switched to use a EqDec class instead of a functor btw

Awesome, thanks! This made Buchberger both axiom and dependency free:

```
"coqchk" -silent -o -Q theories Buchberger <...>
CONTEXT SUMMARY
===============
* Theory: Set is predicative
* Axioms: <none>
```

was going to update `CHANGELOG.md`

as well, but apparently GitHub is down...

Last updated: Sep 15 2024 at 13:02 UTC