From 330ee3a5e23ec66aeb9ade13f6298afcadefda51 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 9 Oct 2018 23:44:17 -0400 Subject: Add interp-correctness condition for rewriter The NBE-rewrite rules are proven correct. The arith and fancy rewrite rules are reduced to lemmas about Z, most of which are inconsistent (and therefore indicate rewrite rules which are missing side-conditions). One bad rewrite rule was found in this process, and corrected in 0842563b23f8d780f4ff1080d7620fc3f368191f The next step after this will be using the rewrite rule correctness to prove the rewriter correct. --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 70fca8fd2..0b4816189 100644 --- a/_CoqProject +++ b/_CoqProject @@ -264,6 +264,7 @@ src/Experiments/NewPipeline/MiscCompilerPassesProofs.v src/Experiments/NewPipeline/Rewriter.v src/Experiments/NewPipeline/RewriterProofs.v src/Experiments/NewPipeline/RewriterRulesGood.v +src/Experiments/NewPipeline/RewriterRulesInterpGood.v src/Experiments/NewPipeline/RewriterWf1.v src/Experiments/NewPipeline/RewriterWf2.v src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v -- cgit v1.2.3