Skip to content

Commit 97c07db

Browse files
hargoniXhargoniX
committed
chore: use dsimp only 
1 parent 95adf6e commit 97c07db

File tree

8 files changed

+43
-43
lines changed

8 files changed

+43
-43
lines changed

‎src/Std/Sat/AIG/CNF.lean

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,7 @@ def Cache.addConst (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size
284284
rw [Array.getElem_set] at hmarked
285285
split at hmarked
286286
. next heq =>
287-
dsimp at heq
287+
dsimp only at heq
288288
simp only [heq, CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq]
289289
at htip heval
290290
simp only [denote_idx_const htip, projectRightAssign_property, heval]
@@ -322,7 +322,7 @@ def Cache.addAtom (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size)
322322
rw [Array.getElem_set] at hmarked
323323
split at hmarked
324324
. next heq =>
325-
dsimp at heq
325+
dsimp only at heq
326326
simp only [heq, CNF.eval_append, Decl.atomToCNF_eval, Bool.and_eq_true, beq_iff_eq] at htip heval
327327
simp [heval, denote_idx_atom htip]
328328
. next heq =>
@@ -374,7 +374,7 @@ def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig
374374
rw [Array.getElem_set] at hmarked
375375
split at hmarked
376376
. next heq =>
377-
dsimp at heq
377+
dsimp only at heq
378378
simp only [heq, CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq]
379379
at htip heval
380380
have hleval := cache.inv.heval assign heval.right lhs (by omega) hl
@@ -632,21 +632,21 @@ theorem toCNF.inj_is_injection {aig : AIG Nat} (a b : CNFVar aig) :
632632
| inl =>
633633
cases b with
634634
| inl =>
635-
dsimp [inj] at h
635+
dsimp only [inj] at h
636636
congr
637637
omega
638638
| inr rhs =>
639639
exfalso
640-
dsimp [inj] at h
640+
dsimp only [inj] at h
641641
have := rhs.isLt
642642
omega
643643
| inr lhs =>
644644
cases b with
645645
| inl =>
646-
dsimp [inj] at h
646+
dsimp only [inj] at h
647647
omega
648648
| inr =>
649-
dsimp [inj] at h
649+
dsimp only [inj] at h
650650
congr
651651
omega
652652

@@ -700,7 +700,7 @@ theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool}:
700700
An AIG is unsat iff its CNF is unsat.
701701
-/
702702
theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.Unsat := by
703-
dsimp [toCNF]
703+
dsimp only [toCNF]
704704
rw [CNF.unsat_relabel_iff]
705705
. constructor
706706
. intro h assign1

‎src/Std/Sat/AIG/CachedLemmas.lean

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < ai
6969
-/
7070
theorem mkAtomCached_le_size (aig : AIG α) (var : α) :
7171
aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size := by
72-
dsimp [mkAtomCached]
72+
dsimp only [mkAtomCached]
7373
split
7474
. simp
7575
. simp_arith
@@ -143,7 +143,7 @@ theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx <
143143
-/
144144
theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
145145
aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size := by
146-
dsimp [mkConstCached]
146+
dsimp only [mkConstCached]
147147
split
148148
. simp
149149
. simp_arith
@@ -185,7 +185,7 @@ theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
185185

186186
theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
187187
aig.decls.size ≤ (go aig input).aig.decls.size := by
188-
dsimp [go]
188+
dsimp only [go]
189189
split
190190
. simp
191191
. split
@@ -206,7 +206,7 @@ theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
206206
-/
207207
theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig)
208208
: aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
209-
dsimp [mkGateCached]
209+
dsimp only [mkGateCached]
210210
split
211211
. apply mkGateCached.go_le_size
212212
. apply mkGateCached.go_le_size
@@ -215,7 +215,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
215215
∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
216216
generalize hres : go aig input = res
217217
unfold go at hres
218-
dsimp at hres
218+
dsimp only at hres
219219
split at hres
220220
. rw [← hres]
221221
intros
@@ -254,7 +254,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
254254
intros
255255
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
256256
. rw [← hres]
257-
dsimp
257+
dsimp only
258258
intro idx h1 h2
259259
rw [Array.get_push]
260260
simp [h2]
@@ -267,7 +267,7 @@ theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
267267
∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
268268
generalize hres : mkGateCached aig input = res
269269
unfold mkGateCached at hres
270-
dsimp at hres
270+
dsimp only at hres
271271
split at hres
272272
all_goals
273273
rw [← hres]

‎src/Std/Sat/AIG/If.lean

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -37,15 +37,15 @@ instance : LawfulOperator α TernaryInput mkIfCached where
3737
le_size := by
3838
intros
3939
unfold mkIfCached
40-
dsimp
40+
dsimp only
4141
apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached)
4242
apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached)
4343
apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached)
4444
apply LawfulOperator.le_size (f := mkAndCached)
4545
decl_eq := by
4646
intros
4747
unfold mkIfCached
48-
dsimp
48+
dsimp only
4949
rw [LawfulOperator.decl_eq (f := mkOrCached)]
5050
rw [LawfulOperator.decl_eq (f := mkAndCached)]
5151
rw [LawfulOperator.decl_eq (f := mkNotCached)]
@@ -71,7 +71,7 @@ theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} :
7171
if ⟦aig, input.discr, assign⟧ then ⟦aig, input.lhs, assign⟧ else ⟦aig, input.rhs, assign⟧ := by
7272
rw [if_as_bool]
7373
unfold mkIfCached
74-
dsimp
74+
dsimp only
7575
simp only [TernaryInput.cast, Ref_cast', id_eq, Int.reduceNeg, denote_mkOrCached,
7676
denote_projected_entry, denote_mkAndCached, denote_mkNotCached]
7777
congr 2
@@ -120,7 +120,7 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref
120120
(lhs rhs : RefStream aig w) (s : RefStream aig curr) :
121121
aig.decls.size ≤ (go aig curr hcurr discr lhs rhs s).aig.decls.size := by
122122
unfold go
123-
dsimp
123+
dsimp only
124124
split
125125
. refine Nat.le_trans ?_ (by apply go_le_size)
126126
apply LawfulOperator.le_size (f := mkIfCached)
@@ -133,7 +133,7 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref
133133
(go aig curr hcurr discr lhs rhs s).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
134134
generalize hgo : go aig curr hcurr discr lhs rhs s = res
135135
unfold go at hgo
136-
dsimp at hgo
136+
dsimp only at hgo
137137
split at hgo
138138
. rw [← hgo]
139139
intro idx h1 h2
@@ -167,7 +167,7 @@ theorem go_get_aux {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (d
167167
intro idx hidx
168168
generalize hgo : go aig curr hcurr discr lhs rhs s = res
169169
unfold go at hgo
170-
dsimp at hgo
170+
dsimp only at hgo
171171
split at hgo
172172
. rw [← hgo]
173173
intros
@@ -228,7 +228,7 @@ theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (di
228228
intro idx hidx1 hidx2
229229
generalize hgo : go aig curr hcurr discr lhs rhs s = res
230230
unfold go at hgo
231-
dsimp at hgo
231+
dsimp only at hgo
232232
split at hgo
233233
. cases Nat.eq_or_lt_of_le hidx2 with
234234
| inl heq =>
@@ -267,7 +267,7 @@ theorem denote_ite {aig : AIG α} {input : IfInput aig w} :
267267
⟦aig, input.rhs.get idx hidx, assign⟧ := by
268268
intro idx hidx
269269
unfold ite
270-
dsimp
270+
dsimp only
271271
rw [ite.denote_go]
272272
omega
273273
end RefStream

‎src/Std/Sat/AIG/Lemmas.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
110110
. next heq =>
111111
rw [mkGate, Array.get_push_eq] at heq
112112
injection heq with heq1 heq2 heq3 heq4
113-
dsimp
113+
dsimp only
114114
congr 2
115115
. unfold denote
116116
simp only [heq1]

‎src/Std/Sat/AIG/RefStreamOperator/Fold.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefStrea
6161
unfold go
6262
split
6363
. next h =>
64-
dsimp
64+
dsimp only
6565
refine Nat.le_trans ?_ (by apply fold.go_le_size)
6666
apply LawfulOperator.le_size
6767
. simp
@@ -70,7 +70,7 @@ theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefStrea
7070
theorem fold_le_size {aig : AIG α} (target : FoldTarget aig) :
7171
aig.decls.size ≤ (fold aig target).1.decls.size := by
7272
unfold fold
73-
dsimp
73+
dsimp only
7474
refine Nat.le_trans ?_ (by apply fold.go_le_size)
7575
apply LawfulOperator.le_size (f := mkConstCached)
7676

@@ -81,7 +81,7 @@ theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefStream
8181
generalize hgo : go aig acc i len s f = res
8282
unfold go at hgo
8383
split at hgo
84-
. dsimp at hgo
84+
. dsimp only at hgo
8585
rw [← hgo]
8686
intros
8787
rw [go_decl_eq]
@@ -100,7 +100,7 @@ theorem fold_decl_eq {aig : AIG α} (target : FoldTarget aig) :
100100
aig.decls[idx]'h1 := by
101101
intros
102102
unfold fold
103-
dsimp
103+
dsimp only
104104
rw [fold.go_decl_eq]
105105
rw [LawfulOperator.decl_eq (f := mkConstCached)]
106106
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
@@ -128,7 +128,7 @@ theorem denote_go_and {aig : AIG α} (acc : AIG.Ref aig) (curr : Nat) (hcurr : c
128128
generalize hgo : go aig acc curr len input mkAndCached = res
129129
unfold go at hgo
130130
split at hgo
131-
. dsimp at hgo
131+
. dsimp only at hgo
132132
rw [← hgo]
133133
rw [denote_go_and]
134134
. simp only [denote_projected_entry, denote_mkAndCached, Bool.and_eq_true, get_cast,

‎src/Std/Sat/AIG/RefStreamOperator/Map.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ theorem map.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefStream aig idx)
8383
unfold go
8484
split
8585
. next h =>
86-
dsimp
86+
dsimp only
8787
refine Nat.le_trans ?_ (by apply map.go_le_size)
8888
apply LawfulOperator.le_size
8989
. simp
@@ -101,14 +101,14 @@ theorem map.go_decl_eq {aig : AIG α} (i) (hi)
101101
generalize hgo : go aig i hi s input f = res
102102
unfold go at hgo
103103
split at hgo
104-
. dsimp at hgo
104+
. dsimp only at hgo
105105
rw [← hgo]
106106
intros
107107
rw [go_decl_eq]
108108
rw [LawfulOperator.decl_eq]
109109
apply LawfulOperator.lt_size_of_lt_aig_size
110110
assumption
111-
. dsimp at hgo
111+
. dsimp only at hgo
112112
rw [← hgo]
113113
intros
114114
simp
@@ -141,7 +141,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefSt
141141
generalize hgo : go aig curr hcurr s input f = res
142142
unfold go at hgo
143143
split at hgo
144-
. dsimp at hgo
144+
. dsimp only at hgo
145145
rw [← hgo]
146146
intro hfoo
147147
rw [go_get_aux]
@@ -151,7 +151,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefSt
151151
. simp
152152
. assumption
153153
. apply go_le_size
154-
. dsimp at hgo
154+
. dsimp only at hgo
155155
rw [← hgo]
156156
simp only [Nat.le_refl, get, Ref_cast', Ref.mk.injEq, true_implies]
157157
have : curr = len := by omega
@@ -200,7 +200,7 @@ theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefStr
200200
generalize hgo : go aig curr hcurr s input f = res
201201
unfold go at hgo
202202
split at hgo
203-
. dsimp at hgo
203+
. dsimp only at hgo
204204
cases Nat.eq_or_lt_of_le hidx2 with
205205
| inl heq =>
206206
rw [← hgo]

‎src/Std/Sat/AIG/RefStreamOperator/Zip.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,7 @@ theorem zip.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefStream aig idx)
111111
aig.decls.size ≤ (go aig idx s hidx lhs rhs f).1.decls.size := by
112112
unfold go
113113
split
114-
. dsimp
114+
. dsimp only
115115
refine Nat.le_trans ?_ (by apply zip.go_le_size)
116116
apply LawfulOperator.le_size
117117
. simp
@@ -129,15 +129,15 @@ theorem zip.go_decl_eq {aig : AIG α} (i) (hi) (lhs rhs : RefStream aig len)
129129
generalize hgo : go aig i s hi lhs rhs f = res
130130
unfold go at hgo
131131
split at hgo
132-
. dsimp at hgo
132+
. dsimp only at hgo
133133
rw [← hgo]
134134
intros
135135
intros
136136
rw [go_decl_eq]
137137
rw [LawfulOperator.decl_eq]
138138
apply LawfulOperator.lt_size_of_lt_aig_size
139139
assumption
140-
. dsimp at hgo
140+
. dsimp only at hgo
141141
rw [← hgo]
142142
intros
143143
simp
@@ -168,7 +168,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefSt
168168
generalize hgo : go aig curr s hcurr lhs rhs f = res
169169
unfold go at hgo
170170
split at hgo
171-
. dsimp at hgo
171+
. dsimp only at hgo
172172
rw [← hgo]
173173
intro hfoo
174174
rw [go_get_aux]
@@ -178,7 +178,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefSt
178178
. simp
179179
. assumption
180180
. apply go_le_size
181-
. dsimp at hgo
181+
. dsimp only at hgo
182182
rw [← hgo]
183183
simp only [Nat.le_refl, get, Ref_cast', Ref.mk.injEq, true_implies]
184184
have : curr = len := by omega
@@ -231,7 +231,7 @@ theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefStr
231231
generalize hgo : go aig curr s hcurr lhs rhs f = res
232232
unfold go at hgo
233233
split at hgo
234-
. dsimp at hgo
234+
. dsimp only at hgo
235235
cases Nat.eq_or_lt_of_le hidx2 with
236236
| inl heq =>
237237
rw [← hgo]

‎src/Std/Sat/AIG/RelabelNat.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -265,7 +265,7 @@ The map returned by `ofAIG` fulfills the `Inv1` property.
265265
-/
266266
theorem ofAIG.Inv1 (aig : AIG α) : ∃ n, Inv1 n (ofAIG aig) := by
267267
exists (ofAIGAux aig).max
268-
dsimp [ofAIG]
268+
dsimp only [ofAIG]
269269
exact (ofAIGAux aig).inv1
270270

271271
/--
@@ -329,7 +329,7 @@ theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig
329329
-/
330330
theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
331331
(aig.relabelNat).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by
332-
dsimp [relabelNat, relabelNat']
332+
dsimp only [relabelNat, relabelNat']
333333
rw [relabel_unsat_iff]
334334
intro x y hx hy heq
335335
split at heq

0 commit comments

Comments
 (0)