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 validateon 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,
coqchk still reports axioms since Equations itself uses some axioms, but not in the parts that I actually use. Sigh.
acc_A_B_lexprod from Stdlib uses
eq_rect_eq (sigh again), I reimplemented it
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
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: Oct 05 2023 at 02:01 UTC