Stream: Coq users

Topic: eq_rect_eq in buchberger project


view this post on Zulip Karl Palmskog (Nov 27 2021 at 11:28):

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.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 11:36):

since acc_A_B_lexprod from Stdlib uses eq_rect_eq (sigh again), I reimplemented it

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 11:59):

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

view this post on Zulip Karl Palmskog (Nov 27 2021 at 12:03):

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

view this post on Zulip Karl Palmskog (Nov 27 2021 at 16:02):

@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?

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 16:05):

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.

view this post on Zulip Karl Palmskog (Nov 27 2021 at 16:09):

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

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 16:32):

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.

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 16:38):

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?

view this post on Zulip Karl Palmskog (Nov 27 2021 at 19:11):

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.

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 19:39):

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.

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 19:47):

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

view this post on Zulip Karl Palmskog (Nov 27 2021 at 20:06):

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

"coqchk" -silent -o  -Q theories Buchberger <...>

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms: <none>

view this post on Zulip Karl Palmskog (Nov 27 2021 at 20:46):

was going to update CHANGELOG.md as well, but apparently GitHub is down...


Last updated: Jan 31 2023 at 14:03 UTC