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?
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 =>
.
Strangely, some of the doc Coq code using => seems to pass fine, in the doc itself
Ah, maybe I have the rc installed
Yep, rc1
Yes, I can confirm I have the issue on 8.20+rc1 but 8.20.0 is fine
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