Add rewrite rules to Coq #18038
Merged
Add rewrite rules to Coq #18038
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
coqbot-app
bot
added
the
needs: full CI
proux01
reviewed
Sep 13, 2023
yannl35133
force-pushed
the
rewrite-rules
branch
4 times, most recently
from
a0bfcb1
to
e64bbb5
Compare
|
I think we could discuss at a call a strategy to review and merge this one. It is large and could be split into smaller pieces. I know it is some work but it would also mean we can integrate it step by step (and finding what a good step is, is part of the job to be done). Maybe what I'd like to see is a more detailed technical roadmap, at the level of detail of a stream of PRs. |
yannl35133
force-pushed
the
rewrite-rules
branch
3 times, most recently
from
4cca8a7
to
b7af997
Compare
|
The commits are now organised thematically so that they can be read individually |
github-actions
bot
added
the
needs: rebase
yannl35133
force-pushed
the
rewrite-rules
branch
from
b7af997
to
118f53d
Compare
coqbot-app
bot
removed
the
needs: rebase
yannl35133
force-pushed
the
rewrite-rules
branch
2 times, most recently
from
f09b1da
to
83d8688
Compare
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install coq-metacoq-erasure (dependency coq-metacoq-template failed) 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 143.3660 145.9360 2.5700 1.79% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 19.7980 21.9770 2.1790 11.01% 413 coq-perennial/src/program_proof/vrsm/replica/setstate_proof.v.html │ │ 55.0730 56.9480 1.8750 3.40% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 161.7940 163.6660 1.8720 1.16% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 54.9540 56.2540 1.3000 2.37% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 53.7380 54.9310 1.1930 2.22% 915 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 8.6800 9.5970 0.9170 10.56% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 16.3760 17.2270 0.8510 5.20% 642 coq-perennial/src/program_proof/vrsm/paxos/tryacquire_proof.v.html │ │ 11.5020 12.3360 0.8340 7.25% 462 coq-perennial/src/program_proof/simple/write.v.html │ │ 36.0890 36.8990 0.8100 2.24% 12 coq-fourcolor/theories/job439to465.v.html │ │ 28.8270 29.5990 0.7720 2.68% 12 coq-fourcolor/theories/job531to534.v.html │ │ 8.6520 9.4230 0.7710 8.91% 1508 coq-perennial/src/program_proof/wal/recovery_proof.v.html │ │ 17.5260 18.2840 0.7580 4.33% 3269 coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html │ │ 1.8770 2.6200 0.7430 39.58% 209 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 27.3170 28.0110 0.6940 2.54% 12 coq-fourcolor/theories/job291to294.v.html │ │ 32.0620 32.7380 0.6760 2.11% 12 coq-fourcolor/theories/job589to610.v.html │ │ 27.2960 27.9000 0.6040 2.21% 12 coq-fourcolor/theories/job618to622.v.html │ │ 25.3500 25.9350 0.5850 2.31% 12 coq-fourcolor/theories/job495to498.v.html │ │ 111.4550 112.0330 0.5780 0.52% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 26.5810 27.1500 0.5690 2.14% 12 coq-fourcolor/theories/job503to506.v.html │ │ 20.1140 20.6760 0.5620 2.79% 12 coq-fourcolor/theories/job315to318.v.html │ │ 28.3470 28.8870 0.5400 1.90% 12 coq-fourcolor/theories/job466to485.v.html │ │ 28.7300 29.2660 0.5360 1.87% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 19.1520 19.6800 0.5280 2.76% 12 coq-fourcolor/theories/job623to633.v.html │ │ 27.9040 28.4060 0.5020 1.80% 194 coq-vst/veric/expr_lemmas4.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 45.2810 41.7100 -3.5710 -7.89% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 42.5700 41.0690 -1.5010 -3.53% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 23.5140 22.0180 -1.4960 -6.36% 660 coq-perennial/src/program_proof/vrsm/replica/roapply_proof.v.html │ │ 61.4880 60.2880 -1.2000 -1.95% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 25.5100 24.3690 -1.1410 -4.47% 25 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 42.8100 41.6720 -1.1380 -2.66% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 25.4880 24.3560 -1.1320 -4.44% 20 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 34.7260 33.6750 -1.0510 -3.03% 522 coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html │ │ 127.6270 126.6000 -1.0270 -0.80% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 23.0700 22.1780 -0.8920 -3.87% 233 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 19.9110 19.0700 -0.8410 -4.22% 28 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 43.2890 42.4500 -0.8390 -1.94% 368 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 212.8040 211.9720 -0.8320 -0.39% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 8.9120 8.1790 -0.7330 -8.22% 1510 coq-perennial/src/program_proof/vrsm/configservice/config_proof.v.html │ │ 113.9190 113.2540 -0.6650 -0.58% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 82.9430 82.3390 -0.6040 -0.73% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 13.2950 12.6910 -0.6040 -4.54% 187 coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html │ │ 52.7730 52.1800 -0.5930 -1.12% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 13.2620 12.6990 -0.5630 -4.25% 15 coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html │ │ 11.4080 10.8760 -0.5320 -4.66% 601 coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html │ │ 14.5320 14.0000 -0.5320 -3.66% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 28.8530 28.3230 -0.5300 -1.84% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 52.1290 51.6110 -0.5180 -0.99% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 16.0770 15.5780 -0.4990 -3.10% 262 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 21.6340 21.1350 -0.4990 -2.31% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
yannl35133
force-pushed
the
rewrite-rules
branch
from
83d8688
to
705d5c6
Compare
|
The last two commits are somewhat experimental :
Please tell me if that broke anything, or if you have suggestions |
|
Set Allow Rewrite Rules.
#[unfold_fix] Symbol raise : forall P: Type, P.
Definition bad : False := @Wf.Fix_F unit (fun _ _ => True) (fun _ => False) (fun x f => f x I) tt (raise _).
Eval lazy in bad.Note that this relies on |
yannl35133
force-pushed
the
rewrite-rules
branch
from
705d5c6
to
a003af9
Compare
This behaviour is now removed, with unfold_fix symbols unfolding a fixpoint only in an app context / only when the eliminations are all applications |
|
I cannot see a way for simpl to be able to reduce on rules with a match without either slowing it down even when no symbols are involved (i.e. I look for symbols at each step) or changing its general behaviour on match |
|
Did I make a mistake in my rewrite rule or is it a bug that produces |
|
The bug is fixed, but now I see that the types for lambdas to abstract the extended contexts may be wrong in instances where substitutions happen at the same time as the rewriting. They are immediately erased by beta reduction in most cases, but if a user wants to enable rewriting but not beta it will show. Set Allow Rewrite Rules.
Symbol raise : forall P: Type, P.
Rewrite Rule raise_rew :=
match raise (@eq ?A ?a ?b) as e in _ = b return ?P with
| eq_refl => _
end ==> raise ?P@{b := _; e := raise (?a = ?b)}.
Definition bad :=
Eval lazy delta in
let n := 0 in
match raise (n = n) in (_ = a) return (n = a) with
| eq_refl => raise _
end.(that's |
|
Is this expected? Set Allow Rewrite Rules.
#[unfold_fix] Symbol raise : forall P: Type, P.
Rewrite Rules raise_rew :=
raise (forall x:?A, ?B) ==> fun x:?A => raise ?B
.
Eval lazy in raise (forall x:nat, x = 0). (* works: fun x => raise (x = 0) *)
Eval lazy in raise (forall x y:nat, x = y). (* does nothing *)
Lemma gen A B : raise (forall x:A, B x) = fun x => raise (B x).
Proof. lazy. reflexivity. Defined.
Lemma hide T : T -> T. Proof. auto. Qed.
Lemma specific : raise (forall x y:nat, x = y) = fun x => raise (forall y, x = y).
Proof.
apply hide,gen.
Defined.
Definition specific' := Eval lazy in specific.
(* type error (SR broken) *) |
No, it is now fixed |
|
Now we have non termination with Set Allow Rewrite Rules.
#[unfold_fix] Symbol raise : forall P: Type, P.
Rewrite Rules raise_rew :=
raise (forall x:?A, ?B) ==> fun x:?A => raise ?B
with
match raise (@Acc ?A ?R ?x) as a return ?P with
| Acc_intro _ _ => _
end ==> raise (?P@{a := raise (@Acc ?A ?R ?x)}).
Definition bad : False := @Wf.Fix_F unit (fun _ _ => True) (fun _ => False) (fun x f => f x I) tt (raise _).
Eval lazy in bad.I don't know if this one can be fixed. (meanwhile Definition Fix_F' {A} {R:A->A->Prop} P
(F:forall x : A, (forall y : A, R y x -> P y) -> P x)
: forall x, Acc R x -> P x
:= fix Fix_F x a {struct a} :=
match a with
| Acc_intro _ b => F x (fun y h => Fix_F y (b y h))
end.
Definition good : False := @Fix_F' unit (fun _ _ => True) (fun _ => False) (fun x f => f x I) tt (raise _).
Eval lazy in good.
(* raise False *)does the right thing) |
github-actions
bot
added
the
needs: rebase
added 7 commits
February 16, 2024 02:09
…) and add report on RR in coqchk
yannl35133
force-pushed
the
rewrite-rules
branch
from
7455c2b
to
a1c5f39
Compare
|
FTR am I correct in thinking this doesn't support rewriting arbitrary terms but only symbols? For example, something I wanted to try was: Inductive paths {A} (x : A) : A -> Type :=
| idpath : paths x x.
Axiom Circle : Set.
Symbol base : Circle.
Symbol loop : paths base base.
Symbol Circle_rec : forall (P : Type), P -> (paths base base) -> Circle -> P.
Definition ap {A B} (f : A -> B) {x y} (p : paths x y) : paths (f x) (f y) :=
match p in paths _ y return paths (f x) (f y) with
| idpath _ => idpath (f x)
end.
Rewrite Rule loop_rew :=
| Circle_rec _ ?b ?loop base ==> ?b
| ap (Circle_rec _ ?b ?loop) loop ==> ?loop
.but that doesn't seem to work. IIRC Agda is able to accept that definition, so is it something that might be possible with the right backdoor? |
|
No, you can only add rewrite rules to symbols. Otherwise, reduction would trigger unfolding before it triggers the rule. There might some workarounds but I don't think anything has been implemented. If you want the rule for |
|
You can also define your rewrite rule using the normal form for the left-hand side, it can be made into a pattern | match loop with idpath _ => idpath (Circle_rec ?B ?b ?loop base) end ==> ?loop |
SkySkimmer
approved these changes
Feb 20, 2024
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
I'll probably merge tomorrow. |
|
@yannl35133 With that pattern Coq complains about an unknown existential variable. Is that expected? |
|
This is indeed not expected. I found the reason and I'll see how I can fix it |
|
Do you want to wait for the fix to merge or do you prefer doing it after merge? |
|
offline: don't care @coqbot merge now |
|
@SkySkimmer: Please take care of the following overlays:
|
yannl35133
added a commit
to MetaCoq/metacoq
that referenced
this pull request
Feb 21, 2024
Adapt to coq/coq#18038 (rewrite rules)
LasseBlaauwbroek
added a commit
to coq-tactician/coq-tactician
that referenced
this pull request
Feb 21, 2024
Adapt to coq/coq#18038 (rewrite rules)
lukaszcz
pushed a commit
to lukaszcz/coqhammer
that referenced
this pull request
Feb 22, 2024
Janno
added a commit
to Mtac2/Mtac2
that referenced
this pull request
Feb 22, 2024
Adapt to coq/coq#18038 (rewrite rules)
herbelin
added a commit
to herbelin/template-coq
that referenced
this pull request
Feb 25, 2024
This reverts commit 61e75d2.
|
@yannl35133 Should I create an issue about the unexpected error? |
|
@Alizter Sorry for the delay, I opened the issue and a PR to fix half of the issue, the other half will need more work |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
NB: last bench #18038 (comment)
This adds support for rewrite rules (Coq roadmap), (associated CEP).
What is currently missing :