From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/rewrite_strat.v | 53 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 test-suite/success/rewrite_strat.v (limited to 'test-suite/success/rewrite_strat.v') diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v new file mode 100644 index 00000000..04c67556 --- /dev/null +++ b/test-suite/success/rewrite_strat.v @@ -0,0 +1,53 @@ +Require Import Setoid. + +Variable X : Set. + +Variable f : X -> X. +Variable g : X -> X -> X. +Variable h : nat -> X -> X. + +Variable lem0 : forall x, f (f x) = f x. +Variable lem1 : forall x, g x x = f x. +Variable lem2 : forall n x, h (S n) x = g (h n x) (h n x). +Variable lem3 : forall x, h 0 x = x. + +Hint Rewrite lem0 lem1 lem2 lem3 : rew. + +Goal forall x, h 10 x = f x. +Proof. + intros. + Time autorewrite with rew. (* 0.586 *) + reflexivity. +Time Qed. (* 0.53 *) + +Goal forall x, h 6 x = f x. +intros. + Time rewrite_strat topdown lem2. + Time rewrite_strat topdown lem1. + Time rewrite_strat topdown lem0. + Time rewrite_strat topdown lem3. + reflexivity. +Undo 5. + Time rewrite_strat topdown (choice lem2 lem1). + Time rewrite_strat topdown (choice lem0 lem3). + reflexivity. +Undo 3. + Time rewrite_strat (topdown (choice lem2 lem1); topdown (choice lem0 lem3)). + reflexivity. +Undo 2. + Time rewrite_strat (topdown (choice lem2 (choice lem1 (choice lem0 lem3)))). + reflexivity. +Undo 2. + Time rewrite_strat (topdown (choice lem2 (choice lem1 (choice lem0 lem3)))). + reflexivity. +Qed. + +Goal forall x, h 10 x = f x. +Proof. + intros. + Time rewrite_strat topdown (hints rew). (* 0.38 *) + reflexivity. +Time Qed. (* 0.06 s *) + +Set Printing All. +Set Printing Depth 100000. \ No newline at end of file -- cgit v1.2.3