diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /test-suite/success/rewrite_strat.v | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
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 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 |