eq_rect_eq in buchberger project · Coq users

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.

Karl Palmskog (Nov 27 2021 at 11:36):

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

Gaëtan Gilbert (Nov 27 2021 at 11:59):

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.

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?

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.

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

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.

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?

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.

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.

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

Stream: Coq users

Topic: eq_rect_eq in buchberger project

Karl Palmskog (Nov 27 2021 at 11:28):