Stream: Coq devs & plugin devs

Topic: Rewrite rule syntax


view this post on Zulip Matthieu Sozeau (Sep 11 2024 at 09:20):

While trying to write a demo for rewrite rules in 8.20, I get a syntax error using "=>" to declare rules, the parser asks for ">->" instead. E.g. the following works:

Rewrite Rule pplus_rewrite :=
| ?n ++ 0 >-> ?n
| ?n ++ S ?m >-> S (?n ++ ?m)
| 0 ++ ?n >-> ?n
| S ?n ++ ?m >-> S (?n ++ ?m).

While the same example with => fails with a parse error (example taken from the doc). What gives?

view this post on Zulip Yann Leray (Sep 11 2024 at 09:46):

Are you sure you're using the correct version ? I just tested with a freshly installed Coq 8.20 switch and it correctly asks for =>.

view this post on Zulip Matthieu Sozeau (Sep 11 2024 at 09:46):

Strangely, some of the doc Coq code using => seems to pass fine, in the doc itself

view this post on Zulip Matthieu Sozeau (Sep 11 2024 at 09:46):

Ah, maybe I have the rc installed

view this post on Zulip Matthieu Sozeau (Sep 11 2024 at 09:46):

Yep, rc1

view this post on Zulip Pierre Roux (Sep 11 2024 at 09:47):

Yes, I can confirm I have the issue on 8.20+rc1 but 8.20.0 is fine

view this post on Zulip Matthieu Sozeau (Sep 11 2024 at 09:48):

Anyway, this exemple is cool, albeit probably not for everyone's taste :)

Rewrite Rule pplus_rewrite :=
| ?n ++ 0 >-> ?n
| ?n ++ S ?m >-> S (?n ++ ?m)
| 0 ++ ?n >-> ?n
| S ?n ++ ?m >-> S (?n ++ ?m)
| ?n ++ (?m ++ ?k) >-> (?n ++ ?m) ++ ?k.

Check ((fun n => eq_refl) : forall n, n ++ 0 = n).
Check ((fun n m => eq_refl) : forall n m, n ++ S m = S (n ++ m)).


(** Using rewrite rules in an index type *)
Require Vector.
Arguments Vector.nil {A}.
Arguments Vector.cons {A} a {n} v : rename.

Equations vapp {A} {m n} (v : Vector.t A m) (w : Vector.t A n) : Vector.t A (m ++ n) :=
  | Vector.nil | w := w
  | Vector.cons a v | w := Vector.cons a (vapp v w).
Infix "@" := vapp (at level 40).

Set Default Proof Mode "Classic".

(** We are now free of reasoning on the associativity of plus in the indices here *)
Lemma vapp_assoc {A} {m n o} (v : Vector.t A m) (w : Vector.t A n) (x : Vector.t A o) :
  v @ (w @ x) = (v @ w) @ x.
Proof.
  funelim (v @ w); simp vapp.
  - reflexivity.
  - rewrite H. now rewrite vapp_equation_2.
Qed.

Last updated: Oct 13 2024 at 01:02 UTC