/
Examples.v
123 lines (104 loc) · 3.66 KB
/
Examples.v
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
(** * Examples of Using the Rewriter *)
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Lists.List.
Require Import Rewriter.Util.ListUtil.
Require Import Rewriter.Util.LetIn.
Require Import Rewriter.Util.Notations.
Require Import Rewriter.Util.plugins.RewriterBuild.
Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
Time Make norules := Rewriter For ().
(** Now we show some simple examples. *)
Example ex1 : forall x : nat, x = x.
Proof.
Rewrite_for norules.
lazymatch goal with
| |- ?x = ?x => is_var x; reflexivity
end.
Qed.
Example ex2 : forall x : nat, id x = id x.
Proof.
Rewrite_for norules.
lazymatch goal with
| |- ?x = ?x => is_var x; reflexivity
end.
Qed.
(** ==== *)
Local Ltac t :=
repeat constructor; cbn [snd]; cbv [ident.eagerly]; intros;
try solve [ lia
| now apply ListUtil.eq_app_list_rect ].
Lemma map_eagerly_rect
: forall A B f ls, @List.map A B f ls
= (ident.eagerly (@list_rect) _ _)
[]
(fun x xs map_f_xs => f x :: map_f_xs)
ls.
Proof. t. Qed.
Lemma app_eagerly_rect
: forall A xs ys, @List.app A xs ys
= (ident.eagerly (@list_rect) _ _)
ys (fun x xs app_xs_ys => x :: app_xs_ys) xs.
Proof. t. Qed.
Lemma flat_map_rect
: forall A B f xs,
@List.flat_map A B f xs
= (list_rect (fun _ => _))
nil
(fun x _ flat_map_tl => f x ++ flat_map_tl)%list
xs.
Proof. t. Qed.
Module ForDebugging.
Definition rules_proofs :=
Eval cbv [projT2] in
projT2
(ltac:(RewriterBuildRegistry.make_rules_proofs_with_args)
: Pre.rules_proofsT_with_args
(Z.add_0_r
, (@Prod.fst_pair)
, (@Prod.snd_pair)
, map_eagerly_rect
, app_eagerly_rect
, eval_rect list
, do_again flat_map_rect)).
Definition scraped_data :=
(ltac:(cbv [projT1]; RewriterBuildRegistry.make_scraped_data_with_args)
: PreCommon.Pre.ScrapedData.t_with_args
rules_proofs
(* extra, can be anything whose subterms get added *) false).
Rewriter Emit Inductives From Scraped scraped_data As base ident raw_ident pattern_ident.
Definition myrules :=
(ltac:(RewriterBuildRegistry.make_verified_rewriter_with_args)
: ProofsCommon.Compilers.RewriteRules.GoalType.VerifiedRewriter_with_ind_args
scraped_data InductiveHList.nil base ident raw_ident pattern_ident (* inlcude_interp: *) false (* skip_early_reduction: *) false (* skip_early_reduction_no_dtree: *) true rules_proofs).
End ForDebugging.
Time Make myrules
:= Rewriter For (Z.add_0_r
, (@Prod.fst_pair)
, (@Prod.snd_pair)
, map_eagerly_rect
, app_eagerly_rect
, eval_rect list
, do_again flat_map_rect).
(** Now we show some simple examples. *)
Example ex3 : forall x, x + 0 = x.
Proof.
Rewrite_for myrules.
lazymatch goal with
| |- ?x = ?x => is_var x; reflexivity
end.
Qed.
Ltac test_rewrite :=
Rewrite_for myrules;
lazymatch goal with
| [ |- ?x = ?y ] => first [ constr_eq x y; idtac "Success:" x; reflexivity
| fail 1 x "≢" y ]
end.
Example ex4 : forall y e1 e2,
map (fun x => y + x) (dlet z := e1 + e2 in [0; 1; 2; z; z+1])
= dlet z := e1 + e2 in [y; y + 1; y + 2; y + z; y + (z + 1)].
Proof. test_rewrite. Qed.
Example ex5 : forall (x1 x2 x3 : Z),
flat_map (fun a => [a; a; a]) [x1;x2;x3]
= [x1; x1; x1; x2; x2; x2; x3; x3; x3].
Proof. test_rewrite. Qed.