-
Notifications
You must be signed in to change notification settings - Fork 0
/
tutorial1.v
119 lines (99 loc) · 2.91 KB
/
tutorial1.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
From Ltac2 Require Import Ltac2.
From Coq Require Import List.
(* This file shows how to do proof by reflection with Ltac2, *)
(* See http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html for a more detailed explanation of the high-level idea *)
Module Type Monoid.
(* Carrier *)
Parameter M : Type.
(* Neutral element *)
Parameter mzero : M.
(* Binary operator *)
Parameter madd : M -> M -> M.
(* Axioms *)
Axiom madd_assoc : forall a b c, madd (madd a b) c = madd a (madd b c).
Axiom madd_idl : forall a, madd mzero a = a.
Axiom madd_idr : forall a, madd a mzero = a.
End Monoid.
Module MonoidSimp (M : Monoid).
Import M.
Inductive mexp : Type :=
| Id : mexp
| Var : M -> mexp
| Op : mexp -> mexp -> mexp.
Fixpoint denote_mexp (e : mexp) :=
match e with
| Id => mzero
| Var a => a
| Op a b => madd (denote_mexp a) (denote_mexp b)
end.
Definition denote_mexps :=
fold_right madd mzero.
Fixpoint flatten (e : mexp) :=
match e with
| Id => nil
| Var a => cons a nil
| Op e0 e1 => flatten e0 ++ flatten e1
end.
Lemma denote_append L1 L2 :
denote_mexps (L1 ++ L2) = madd (denote_mexps L1) (denote_mexps L2).
Proof.
revert L2.
induction L1 as [|m L1 ihL1].
- simpl. intros L2.
rewrite madd_idl.
reflexivity.
- intros L2. simpl.
rewrite ihL1.
rewrite madd_assoc.
reflexivity.
Qed.
Lemma flatten_correct (e : mexp) :
denote_mexp e = denote_mexps (flatten e).
Proof.
induction e; simpl.
- reflexivity.
- rewrite madd_idr. reflexivity.
- rewrite denote_append.
rewrite IHe1.
rewrite IHe2.
reflexivity.
Qed.
(* To show that two expressions are equal, it suffices to show that their simplified versions are equal *)
Lemma monoid_reflect (e0 e1 : mexp) :
denote_mexps (flatten e0) = denote_mexps (flatten e1) ->
denote_mexp e0 = denote_mexp e1.
Proof.
do 2 (rewrite flatten_correct).
apply id.
Qed.
(* Convert a Gallina expression as a term of the type mexp *)
Ltac2 rec reify a :=
lazy_match! a with
| mzero => 'Id
| madd ?a ?b =>
let e0 := reify a in
let e1 := reify b in
'(Op $e0 $e1)
| _ => '(Var $a)
end.
(* Apply monoid_reflect and simplify the result for a goal of the
form a = b where a and b are both of type M *)
Ltac2 rec monoid_simp () :=
lazy_match! goal with
| [ |- ?a = ?b] =>
let m0 := reify a in
let m1 := reify b in
apply (monoid_reflect $m0 $m1)
| [ |- _] => Control.backtrack_tactic_failure "Wrong goal type"
end.
End MonoidSimp.
(* Let's try out the simplifier *)
Module MonoidSimpTest (Import A : Monoid).
Module AS := MonoidSimp A.
Import AS.
Example test0 : forall (a b c d : M),
madd a (madd (madd b c) d) = madd (madd a b) (madd c d).
Proof.
intros a b c d. monoid_simp(). simpl. reflexivity.
Qed.
End MonoidSimpTest.