diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 01:11:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 01:11:52 +0200 |
| commit | d34e1eed232c84590ddb80d70db9f7f7cf13584a (patch) | |
| tree | 75782f47ebe381d84ea66409569167f9ba229c78 /test-suite/success/rewrite_strat.v | |
| parent | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (diff) | |
Update test-suite files after last commit. Add a file for rewrite_strat
examples.
Diffstat (limited to 'test-suite/success/rewrite_strat.v')
| -rw-r--r-- | test-suite/success/rewrite_strat.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v new file mode 100644 index 000000000..04c675563 --- /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 |