Skip to content

Commit 3cb196d

Browse files
georgerenniegeorgerennie
committed
Better grind matching for theorems
1 parent f63557a commit 3cb196d

4 files changed

Lines changed: 158 additions & 90 deletions

File tree

‎Valaig/Aig/BasicNew.lean‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ def empty : Aig :=
136136
/--
137137
The number of nodes currently allocated in aig.
138138
-/
139-
@[local grind]
139+
@[local grind, local grind unfold]
140140
def size (aig : Aig) : Nat :=
141141
aig.aig.decls.size
142142

@@ -150,6 +150,7 @@ def Var.validIn (var : Var) (aig : Aig) : Prop :=
150150
var.idx < aig.size
151151
deriving Decidable
152152

153+
@[inline, expose, reducible, simp, grind unfold]
153154
def Lit.validIn (lit : Lit) (aig : Aig) : Prop :=
154155
lit.var.validIn aig
155156
deriving Decidable
@@ -162,7 +163,7 @@ def Aig.get (aig : Aig) (var : Var) (valid : var.validIn aig := by grind) : Node
162163
| .atom (.latch idx) => .latch idx
163164
| .gate rhs0 rhs1 => .and (.ofFanin rhs0) (.ofFanin rhs1)
164165

165-
@[inline]
166+
@[inline, expose, reducible, simp, grind unfold]
166167
instance Aig.instGetElemVar : GetElem Aig Var Node (fun aig var => var.validIn aig) where
167168
getElem aig var (h := by grind) :=
168169
aig.get var h
@@ -233,9 +234,9 @@ variable {aig : Aig}
233234
/-
234235
Lemmas to convert between specific and generic index forms.
235236
-/
236-
@[simp, grind =, grind =_] theorem iff_node (var : Var) : (node var).validIn aig ↔ var.validIn aig := by rfl
237-
@[simp, grind =, grind =_] theorem iff_input (idx : InputIdx) : (input idx).validIn aig ↔ idx.validIn aig := by rfl
238-
@[simp, grind =, grind =_] theorem iff_latch (idx : LatchIdx) : (latch idx).validIn aig ↔ idx.validIn aig := by rfl
237+
@[simp, grind =_] theorem iff_node (var : Var) : (node var).validIn aig ↔ var.validIn aig := by rfl
238+
@[simp, grind =_] theorem iff_input (idx : InputIdx) : (input idx).validIn aig ↔ idx.validIn aig := by rfl
239+
@[simp, grind =_] theorem iff_latch (idx : LatchIdx) : (latch idx).validIn aig ↔ idx.validIn aig := by rfl
239240

240241
end GenericIdx
241242

‎Valaig/Aig/GetSet.lean‎

Lines changed: 27 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -34,27 +34,28 @@ LatchIdx.setNext Lemmas.
3434
section setNext
3535
variable {setIdx : LatchIdx} {setValid : setIdx.validIn aig} {newNext : Lit}
3636

37-
@[simp, grind =>]
37+
@[simp, grind =]
3838
theorem get_LatchIdx_setNext {var : Var} {valid : var.validIn aig} :
3939
(setIdx.setNext aig newNext setValid).get var = aig.get var valid := by
4040
simp
4141

42+
@[simp, grind =]
4243
theorem InputIdx.getVar_LatchIdx_setNext {idx : InputIdx} {valid : idx.validIn aig} :
4344
idx.getVar (setIdx.setNext aig newNext setValid) = idx.getVar aig := by
4445
simp
4546

46-
@[simp, grind =>]
47+
@[simp, grind =]
4748
theorem LatchIdx.getVar_LatchIdx_setNext {idx : LatchIdx} {valid : idx.validIn aig} :
4849
idx.getVar (setIdx.setNext aig newNext setValid) = idx.getVar aig := by
4950
simp; grind
5051

51-
@[simp, grind =>]
52-
theorem LatchIdx.getNext_LatchIdx_setNext {idx : LatchIdx} {valid : idx.validIn aig} :
52+
@[simp, grind =]
53+
theorem LatchIdx.getNext_LatchIdx_setNext_self {idx : LatchIdx} {valid : idx.validIn aig} :
5354
idx.getNext (setIdx.setNext aig newNext setValid) =
5455
if idx = setIdx then newNext else idx.getNext aig := by
5556
simp; grind
5657

57-
@[simp, grind =>]
58+
@[simp, grind =]
5859
theorem LatchIdx.getReset_LatchIdx_setNext {idx : LatchIdx} {valid : idx.validIn aig} :
5960
idx.getReset (setIdx.setNext aig newNext setValid) = idx.getReset aig := by
6061
simp; grind
@@ -67,26 +68,27 @@ LatchIdx.setReset Lemmas.
6768
section setReset
6869
variable {setIdx : LatchIdx} {setValid : setIdx.validIn aig} {newReset : Lit}
6970

70-
@[simp, grind =>]
71+
@[simp, grind =]
7172
theorem get_LatchIdx_setReset {var : Var} {valid : var.validIn aig} :
7273
(setIdx.setReset aig newReset setValid).get var = aig.get var valid := by
7374
simp
7475

76+
@[simp, grind =]
7577
theorem InputIdx.getVar_LatchIdx_setReset {idx : InputIdx} {valid : idx.validIn aig} :
7678
idx.getVar (setIdx.setReset aig newReset setValid) = idx.getVar aig := by
7779
simp
7880

79-
@[simp, grind =>]
81+
@[simp, grind =]
8082
theorem LatchIdx.getVar_LatchIdx_setReset {idx : LatchIdx} {valid : idx.validIn aig} :
8183
idx.getVar (setIdx.setReset aig newReset setValid) = idx.getVar aig := by
8284
simp; grind
8385

84-
@[simp, grind =>]
86+
@[simp, grind =]
8587
theorem LatchIdx.getNext_LatchIdx_setReset {idx : LatchIdx} {valid : idx.validIn aig} :
8688
idx.getNext (setIdx.setReset aig newReset setValid) = idx.getNext aig := by
8789
simp; grind
8890

89-
@[simp, grind =>]
91+
@[simp, grind =]
9092
theorem LatchIdx.getReset_LatchIdx_setReset {idx : LatchIdx} {valid : idx.validIn aig} :
9193
idx.getReset (setIdx.setReset aig newReset setValid) =
9294
if idx = setIdx then newReset else idx.getReset aig := by
@@ -104,27 +106,27 @@ Aig.addInput Lemmas.
104106
-/
105107
section addInput
106108

107-
@[simp, grind =>]
109+
@[simp, grind =]
108110
theorem get_Aig_addInput {var : Var} {valid : var.validIn aig} :
109111
aig.addInput.fst.get var = aig.get var valid := by
110112
simp; grind
111113

112-
@[simp, grind =>]
114+
@[simp, grind =]
113115
theorem InputIdx.getVar_Aig_addInput {idx : InputIdx} {valid : idx.validIn aig} :
114116
idx.getVar aig.addInput.fst = idx.getVar aig valid := by
115117
simp; grind
116118

117-
@[simp, grind =>]
119+
@[simp, grind =]
118120
theorem LatchIdx.getVar_Aig_addInput {idx : LatchIdx} {valid : idx.validIn aig} :
119121
idx.getVar aig.addInput.fst = idx.getVar aig valid := by
120122
simp
121123

122-
@[simp, grind =>]
124+
@[simp, grind =]
123125
theorem LatchIdx.getNext_Aig_addInput {idx : LatchIdx} {valid : idx.validIn aig} :
124126
idx.getNext aig.addInput.fst = idx.getNext aig valid := by
125127
simp
126128

127-
@[simp, grind =>]
129+
@[simp, grind =]
128130
theorem LatchIdx.getReset_Aig_addInput {idx : LatchIdx} {valid : idx.validIn aig} :
129131
idx.getReset aig.addInput.fst = idx.getReset aig valid := by
130132
simp
@@ -137,22 +139,22 @@ Aig.addLatch Lemmas.
137139
section addLatch
138140
variable {next reset : Lit}
139141

140-
@[simp, grind =>]
142+
@[simp, grind =]
141143
theorem get_Aig_addLatch {var : Var} {valid : var.validIn aig} :
142144
(aig.addLatch next reset).fst.get var = aig.get var valid := by
143145
simp; grind
144146

145-
@[simp, grind =>]
147+
@[simp, grind =]
146148
theorem InputIdx.getVar_Aig_addLatch {idx : InputIdx} {valid : idx.validIn aig} :
147149
idx.getVar (aig.addLatch next reset).fst = idx.getVar aig valid := by
148150
simp
149151

150-
@[simp, grind =>]
152+
@[simp, grind =]
151153
theorem LatchIdx.getVar_Aig_addLatch {idx : LatchIdx} {valid : idx.validIn aig} :
152154
idx.getVar (aig.addLatch next reset).fst = idx.getVar aig valid := by
153155
simp; grind
154156

155-
@[simp, grind =>]
157+
@[simp, grind =]
156158
theorem LatchIdx.getNext_Aig_addLatch {idx : LatchIdx} {valid : idx.validIn aig} :
157159
idx.getNext (aig.addLatch next reset).fst = idx.getNext aig valid := by
158160
simp; grind
@@ -162,7 +164,7 @@ theorem LatchIdx.getNext_Aig_addLatch_eq_self :
162164
(aig.addLatch next reset).snd.getNext (aig.addLatch next reset).fst = next := by
163165
simp
164166

165-
@[simp, grind =>]
167+
@[simp, grind =]
166168
theorem LatchIdx.getReset_Aig_addLatch {idx : LatchIdx} {valid : idx.validIn aig} :
167169
idx.getReset (aig.addLatch next reset).fst = idx.getReset aig valid := by
168170
simp; grind
@@ -180,27 +182,27 @@ Aig.addAnd Lemmas.
180182
section addAnd
181183
variable {rhs0 rhs1 : Lit} {h0 : rhs0.validIn aig} {h1 : rhs1.validIn aig}
182184

183-
@[simp, grind =>]
185+
@[simp, grind =]
184186
theorem get_Aig_addAnd {var : Var} {valid : var.validIn aig} :
185187
(aig.addAnd rhs0 rhs1 h0 h1).fst.get var = aig.get var valid := by
186188
simp; grind
187189

188-
@[simp, grind =>]
190+
@[simp, grind =]
189191
theorem InputIdx.getVar_Aig_addAnd {idx : InputIdx} {valid : idx.validIn aig} :
190192
idx.getVar (aig.addAnd rhs0 rhs1 h0 h1).fst = idx.getVar aig valid := by
191193
simp
192194

193-
@[simp, grind =>]
195+
@[simp, grind =]
194196
theorem LatchIdx.getVar_Aig_addAnd {idx : LatchIdx} {valid : idx.validIn aig} :
195197
idx.getVar (aig.addAnd rhs0 rhs1 h0 h1).fst = idx.getVar aig valid := by
196198
simp
197199

198-
@[simp, grind =>]
199-
theorem LatchIdx.getNext_Aig_addAnd {idx : LatchIdx} {valid : idx.validIn aig} :
200+
@[simp, grind =]
201+
theorem LatchId.getNext_Aig_addAnd {idx : LatchIdx} {valid : idx.validIn aig} :
200202
idx.getNext (aig.addAnd rhs0 rhs1 h0 h1).fst = idx.getNext aig valid := by
201203
simp
202204

203-
@[simp, grind =>]
205+
@[simp, grind =]
204206
theorem LatchIdx.getReset_Aig_addAnd {idx : LatchIdx} {valid : idx.validIn aig} :
205207
idx.getReset (aig.addAnd rhs0 rhs1 h0 h1).fst = idx.getReset aig valid := by
206208
simp

‎Valaig/Aig/IdxValidity.lean‎

Lines changed: 31 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,12 @@ section latch
2525
variable {latch : LatchIdx} {valid : latch.validIn aig}
2626

2727
@[simp, grind =]
28-
theorem LatchIdx.setNext_genericIdx_mono {next : Lit} (idx : GenericIdx) :
28+
theorem LatchIdx.validIn_setNext {next : Lit} (idx : GenericIdx) :
2929
idx.validIn (setNext latch aig next valid) ↔ idx.validIn aig := by
3030
simp
3131

3232
@[simp, grind =]
33-
theorem LatchIdx.setReset_genericIdx_mono {reset : Lit} (idx : GenericIdx) :
33+
theorem LatchIdx.validIn_setReset {reset : Lit} (idx : GenericIdx) :
3434
idx.validIn (setReset latch aig reset valid) ↔ idx.validIn aig := by
3535
simp
3636

@@ -42,48 +42,49 @@ section atom
4242
addInput Lemmas.
4343
-/
4444

45-
@[grind .]
46-
theorem addInput_genericIdx_mono_impl (idx : GenericIdx) :
45+
theorem validIn_addInput (idx : GenericIdx) :
4746
idx.validIn aig → idx.validIn aig.addInput.fst := by
4847
simp; grind only
4948

50-
@[simp, grind =]
51-
theorem addInput_genericIdx_mono (idx : GenericIdx) :
52-
idx.validIn aig.addInput.fst ↔
53-
(idx.validIn aig
54-
∨ idx = .input aig.addInput.snd
55-
∨ idx = .node (aig.addInput.snd.getVar aig.addInput.fst)) := by
56-
simp; grind
49+
grind_pattern validIn_addInput => idx.validIn aig.addInput.fst where
50+
idx =/= .input aig.addInput.snd
51+
idx =/= .node (aig.addInput.snd.getVar aig.addInput.fst)
5752

58-
@[grind .]
59-
theorem addInput_self_validIn :
53+
@[simp, grind .]
54+
theorem addInput_validIn :
6055
aig.addInput.snd.validIn aig.addInput.fst := by
6156
simp
6257

58+
@[simp, grind .]
59+
theorem addInput_getVar_validIn :
60+
(aig.addInput.snd.getVar aig.addInput.fst).validIn aig.addInput.fst := by
61+
simp
62+
6363
/-
6464
addLatch Lemmas.
6565
-/
6666
section latch
6767
variable {next reset : Lit}
6868

69-
@[grind .]
70-
theorem addLatch_genericIdx_mono_impl (idx : GenericIdx) :
69+
theorem validIn_addLatch (idx : GenericIdx) :
7170
idx.validIn aig → idx.validIn (aig.addLatch next reset).fst := by
7271
simp; grind only
7372

74-
@[simp, grind =]
75-
theorem addLatch_genericIdx_mono (idx : GenericIdx) :
76-
idx.validIn (aig.addLatch next reset).fst ↔
77-
(idx.validIn aig
78-
∨ idx = .latch (aig.addLatch next reset).snd
79-
∨ idx = .node ((aig.addLatch next reset).snd.getVar (aig.addLatch next reset).fst)) := by
80-
simp; grind
73+
grind_pattern validIn_addLatch => idx.validIn (aig.addLatch next reset).fst where
74+
idx =/= .latch (aig.addLatch next reset).snd
75+
idx =/= .node ((aig.addLatch next reset).snd.getVar (aig.addLatch next reset).fst)
8176

82-
@[grind .]
83-
theorem addLatch_self_validIn :
77+
@[simp, grind .]
78+
theorem addLatch_validIn :
8479
(aig.addLatch next reset).snd.validIn (aig.addLatch next reset).fst := by
8580
simp
8681

82+
@[simp, grind .]
83+
theorem addLatch_getVar_validIn :
84+
(aig.addLatch next reset).snd.getVar (aig.addLatch next reset).fst |>.validIn
85+
(aig.addLatch next reset).fst := by
86+
simp
87+
8788
end latch
8889
end atom
8990

@@ -93,16 +94,17 @@ addAnd Lemmas.
9394
section gate
9495
variable {rhs0 rhs1 : Lit} {h0 : rhs0.validIn aig} {h1 : rhs1.validIn aig}
9596

96-
@[grind .]
97-
theorem addAnd_genericIdx_mono_impl (idx : GenericIdx) :
97+
theorem validIn_addAnd (idx : GenericIdx) :
9898
idx.validIn aig → idx.validIn (aig.addAnd rhs0 rhs1 h0 h1).fst := by
9999
simp; grind
100100

101-
@[grind .]
102-
theorem addAnd_self_validIn :
101+
grind_pattern validIn_addAnd => idx.validIn (aig.addAnd rhs0 rhs1 h0 h1).fst where
102+
idx =/= .node (aig.addAnd rhs0 rhs1 h0 h1).snd.var
103+
104+
@[simp, grind .]
105+
theorem addAnd_validIn :
103106
(aig.addAnd rhs0 rhs1 h0 h1).snd.validIn (aig.addAnd rhs0 rhs1 h0 h1).fst := by
104107
simp
105-
-- TODO: Whycan't I get grind to see this another way
106108
have {aig : Std.Sat.AIG AtomIdx} {entry: aig.Ref} := entry.hgate
107109
grind only
108110

0 commit comments

Comments
 (0)