aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/rewrite_strat.v
blob: a6e59fdda06554ccd2b8cf048a012dd99aa2eb12 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
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.