search

coq-community / aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
https://coq-community.org/aac-tactics
Other
29 stars 21 forks source link

Transfer general Instances.v lemma to Stdlib #123

Closed palmskog closed 1 year ago

palmskog commented 1 year ago

The following lemma should be transferred to Coq's Stdlib:

  Lemma Pmult_1_l (x : positive) : 1 * x = x.
  Proof. reflexivity. Qed.
SkySkimmer commented 1 year ago

aac_append_Proper

What is this good for? 

Require Import Morphisms List.

Type fun A => _ : Proper (eq ==> eq ==> eq) (@app A).

already succeeds

palmskog commented 1 year ago

@SkySkimmer I didn't write the code, it's likely been around for 10+ years. But if I want the automatic Proper instance available to library users, I'd have to export Morphisms, right?

palmskog commented 1 year ago

OK, let's skip the Proper lemma then.