Skip to content

Commit 445806d

Browse files
hargoniXhargoniX
committed
step1
1 parent 6469890 commit 445806d

File tree

26 files changed

+609
-562
lines changed

26 files changed

+609
-562
lines changed

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

Lines changed: 23 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
prelude
99
public import Std.Sat.AIG.CachedGates
10+
import Init.Grind
1011

1112
@[expose] public section
1213

@@ -47,10 +48,12 @@ private theorem imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b) := by
4748

4849
variable {α : Type} [Hashable α] [DecidableEq α]
4950

51+
@[grind! .]
5052
theorem mkNotCached_le_size (aig : AIG α) (gate : Ref aig) :
5153
aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size := by
5254
simp [mkNotCached]
5355

56+
@[grind =]
5457
theorem mkNotCached_decl_eq idx (aig : AIG α) (gate : Ref aig) {h : idx < aig.decls.size} {h2} :
5558
(aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx]'h := by
5659
simp [mkNotCached]
@@ -66,17 +69,18 @@ theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} :
6669
⟦aig.mkNotCached gate, assign⟧ = !⟦aig, gate, assign⟧ := by
6770
simp [mkNotCached]
6871

72+
@[grind! .]
6973
theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) :
7074
aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size := by
7175
simp only [mkAndCached]
72-
apply LawfulOperator.le_size_of_le_aig_size
73-
omega
76+
grind
7477

78+
@[grind =]
7579
theorem mkAndCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
7680
{h2} :
7781
(aig.mkAndCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
7882
simp only [mkAndCached]
79-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
83+
grind
8084

8185
instance : LawfulOperator α BinaryInput mkAndCached where
8286
le_size := mkAndCached_le_size
@@ -87,16 +91,18 @@ theorem denote_mkAndCached {aig : AIG α} {input : BinaryInput aig} :
8791
⟦aig.mkAndCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by
8892
simp [mkAndCached]
8993

94+
@[grind! .]
9095
theorem mkOrCached_le_size (aig : AIG α) (input : BinaryInput aig) :
9196
aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size := by
9297
simp only [mkOrCached]
93-
apply LawfulOperator.le_size
98+
grind
9499

100+
@[grind =]
95101
theorem mkOrCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
96102
{h2} :
97103
(aig.mkOrCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
98104
simp only [mkOrCached]
99-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
105+
grind
100106

101107
instance : LawfulOperator α BinaryInput mkOrCached where
102108
le_size := mkOrCached_le_size
@@ -108,27 +114,18 @@ theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} :
108114
rw [← or_as_aig]
109115
simp [mkOrCached]
110116

111-
117+
@[grind! .]
112118
theorem mkXorCached_le_size (aig : AIG α) {input : BinaryInput aig} :
113119
aig.decls.size ≤ (aig.mkXorCached input).aig.decls.size := by
114120
simp only [mkXorCached]
115-
apply LawfulOperator.le_size_of_le_aig_size
116-
apply LawfulOperator.le_size_of_le_aig_size
117-
apply LawfulOperator.le_size_of_le_aig_size
118-
omega
121+
grind
119122

123+
@[grind =]
120124
theorem mkXorCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
121125
{h2} :
122126
(aig.mkXorCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
123127
simp only [mkXorCached]
124-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
125-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
126-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
127-
· apply LawfulOperator.lt_size_of_lt_aig_size
128-
assumption
129-
· apply LawfulOperator.lt_size_of_lt_aig_size
130-
apply LawfulOperator.lt_size_of_lt_aig_size
131-
assumption
128+
grind
132129

133130
instance : LawfulOperator α BinaryInput mkXorCached where
134131
le_size := mkXorCached_le_size
@@ -144,26 +141,18 @@ theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} :
144141
LawfulOperator.denote_mem_prefix (f := mkGateCached) input.rhs.hgate
145142
]
146143

144+
@[grind! .]
147145
theorem mkBEqCached_le_size (aig : AIG α) {input : BinaryInput aig} :
148146
aig.decls.size ≤ (aig.mkBEqCached input).aig.decls.size := by
149147
simp only [mkBEqCached]
150-
apply LawfulOperator.le_size_of_le_aig_size
151-
apply LawfulOperator.le_size_of_le_aig_size
152-
apply LawfulOperator.le_size_of_le_aig_size
153-
omega
148+
grind
154149

150+
@[grind =]
155151
theorem mkBEqCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
156152
{h2} :
157153
(aig.mkBEqCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
158154
simp only [mkBEqCached]
159-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
160-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
161-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
162-
· apply LawfulOperator.lt_size_of_lt_aig_size
163-
assumption
164-
· apply LawfulOperator.lt_size_of_lt_aig_size
165-
apply LawfulOperator.lt_size_of_lt_aig_size
166-
assumption
155+
grind
167156

168157
instance : LawfulOperator α BinaryInput mkBEqCached where
169158
le_size := mkBEqCached_le_size
@@ -179,16 +168,18 @@ theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} :
179168
LawfulOperator.denote_mem_prefix (f := mkGateCached) input.rhs.hgate
180169
]
181170

171+
@[grind! .]
182172
theorem mkImpCached_le_size (aig : AIG α) (input : BinaryInput aig) :
183173
aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size := by
184174
simp only [mkImpCached]
185-
apply LawfulOperator.le_size
175+
grind
186176

177+
@[grind =]
187178
theorem mkImpCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
188179
{h2} :
189180
(aig.mkImpCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
190181
simp only [mkImpCached]
191-
rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
182+
grind
192183

193184
instance : LawfulOperator α BinaryInput mkImpCached where
194185
le_size := mkImpCached_le_size

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

Lines changed: 12 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
prelude
99
public import Std.Sat.AIG.Cached
10+
import Init.Grind
1011

1112
@[expose] public section
1213

@@ -55,6 +56,7 @@ theorem mkAtomCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.atom var
5556
The AIG produced by `AIG.mkAtomCached` agrees with the input AIG on all indices that are valid for
5657
both.
5758
-/
59+
@[grind =]
5860
theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size}
5961
{hbound} :
6062
(aig.mkAtomCached var).aig.decls[idx]'hbound = aig.decls[idx] := by
@@ -72,12 +74,11 @@ theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < ai
7274
/--
7375
`AIG.mkAtomCached` never shrinks the underlying AIG.
7476
-/
77+
@[grind! .]
7578
theorem mkAtomCached_le_size (aig : AIG α) (var : α) :
7679
aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size := by
7780
dsimp only [mkAtomCached]
78-
split
79-
· simp
80-
· simp +arith
81+
grind
8182

8283
instance : LawfulOperator α (fun _ => α) mkAtomCached where
8384
le_size := mkAtomCached_le_size
@@ -138,6 +139,7 @@ theorem mkGateCached.go_le_size (aig : AIG α) (input : BinaryInput aig) :
138139
/--
139140
`AIG.mkGateCached` never shrinks the underlying AIG.
140141
-/
142+
@[grind! .]
141143
theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig) :
142144
aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
143145
dsimp only [mkGateCached]
@@ -147,52 +149,20 @@ theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig) :
147149

148150
theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
149151
∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
150-
generalize hres : go aig input = res
151-
unfold go at hres
152-
dsimp only at hres
153-
split at hres
154-
· rw [← hres]
155-
intros
156-
simp
157-
· split at hres
158-
· rw [← hres]
159-
simp
160-
· rw [← hres]
161-
simp
162-
· rw [← hres]
163-
intros
164-
simp
165-
· rw [← hres]
166-
intros
167-
simp
168-
· split at hres
169-
· split at hres
170-
· rw [← hres]
171-
intros
172-
simp
173-
· rw [← hres]
174-
intros
175-
simp
176-
· rw [← hres]
177-
dsimp only
178-
intro idx h1 h2
179-
rw [Array.getElem_push]
180-
simp [h2]
152+
generalize hres : go aig input = res
153+
unfold go at hres
154+
grind
181155

182156
/--
183157
The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for
184158
both.
185159
-/
160+
@[grind =]
186161
theorem mkGateCached_decl_eq (aig : AIG α) (input : BinaryInput aig) :
187162
∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
188-
generalize hres : mkGateCached aig input = res
189-
unfold mkGateCached at hres
190-
dsimp only at hres
191-
split at hres
192-
all_goals
193-
rw [← hres]
194-
intros
195-
rw [mkGateCached.go_decl_eq]
163+
generalize hres : mkGateCached aig input = res
164+
unfold mkGateCached at hres
165+
grind [mkGateCached.go_decl_eq]
196166

197167
instance : LawfulOperator α BinaryInput mkGateCached where
198168
le_size := mkGateCached_le_size

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

Lines changed: 36 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
prelude
99
public import Std.Sat.AIG.LawfulVecOperator
10+
import Init.Grind
1011

1112
@[expose] public section
1213

@@ -60,32 +61,24 @@ def mkIfCached (aig : AIG α) (input : TernaryInput aig) : Entrypoint α :=
6061
apply AIG.LawfulOperator.le_size (f := mkNotCached)
6162
aig.mkOrCached ⟨lhsRef, rhsRef⟩
6263

64+
@[grind! .]
65+
theorem mkIfCached_le_size (aig : AIG α) (input : aig.TernaryInput) :
66+
aig.decls.size ≤ (aig.mkIfCached input).aig.decls.size := by
67+
intros
68+
unfold mkIfCached
69+
grind
70+
71+
@[grind =]
72+
theorem mkIfCached_decl_eq (aig : AIG α) (input : aig.TernaryInput) (idx : Nat)
73+
(h1 : idx < aig.decls.size) (h2 : idx < (aig.mkIfCached input).aig.decls.size) :
74+
(aig.mkIfCached input).aig.decls[idx] = aig.decls[idx] := by
75+
intros
76+
unfold mkIfCached
77+
grind
78+
6379
instance : LawfulOperator α TernaryInput mkIfCached where
64-
le_size := by
65-
intros
66-
unfold mkIfCached
67-
dsimp only
68-
apply LawfulOperator.le_size_of_le_aig_size (f := mkOrCached)
69-
apply LawfulOperator.le_size_of_le_aig_size (f := mkAndCached)
70-
apply LawfulOperator.le_size_of_le_aig_size (f := mkNotCached)
71-
apply LawfulOperator.le_size (f := mkAndCached)
72-
decl_eq := by
73-
intros
74-
unfold mkIfCached
75-
dsimp only
76-
rw [LawfulOperator.decl_eq (f := mkOrCached)]
77-
rw [LawfulOperator.decl_eq (f := mkAndCached)]
78-
rw [LawfulOperator.decl_eq (f := mkNotCached)]
79-
rw [LawfulOperator.decl_eq (f := mkAndCached)]
80-
· apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
81-
omega
82-
· apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached)
83-
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
84-
omega
85-
· apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
86-
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkNotCached)
87-
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkAndCached)
88-
omega
80+
le_size := mkIfCached_le_size
81+
decl_eq := mkIfCached_decl_eq
8982

9083
theorem if_as_bool (d l r : Bool) : (if d then l else r) = ((d && l) || (!d && r)) := by
9184
revert d l r
@@ -172,15 +165,25 @@ termination_by w - curr
172165

173166
end ite
174167

168+
@[grind! .]
169+
theorem ite_le_size (aig : AIG α) (input : IfInput aig w) :
170+
aig.decls.size ≤ (ite aig input).aig.decls.size := by
171+
intros
172+
unfold ite
173+
apply ite.go_le_size
174+
175+
176+
@[grind =]
177+
theorem ite_decl_eq (aig : AIG α) (input : IfInput aig w) (idx : Nat) (h1 : idx < aig.decls.size)
178+
(h2 : idx < (ite aig input).aig.decls.size) :
179+
(ite aig input).aig.decls[idx] = aig.decls[idx] := by
180+
intros
181+
unfold ite
182+
rw [ite.go_decl_eq]
183+
175184
instance : LawfulVecOperator α IfInput ite where
176-
le_size := by
177-
intros
178-
unfold ite
179-
apply ite.go_le_size
180-
decl_eq := by
181-
intros
182-
unfold ite
183-
rw [ite.go_decl_eq]
185+
le_size := ite_le_size
186+
decl_eq := ite_decl_eq
184187

185188
namespace ite
186189

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefVec a
5454
· simp
5555
termination_by len - idx
5656

57+
@[grind! .]
5758
theorem fold_le_size {aig : AIG α} (vec : RefVec aig len)
5859
(func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
5960
[LawfulOperator α BinaryInput func] :
@@ -81,6 +82,7 @@ theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig
8182
simp
8283
termination_by len - i
8384

85+
@[grind =]
8486
theorem fold_decl_eq {aig : AIG α} (vec : RefVec aig len)
8587
(func : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput func] :
8688
∀ idx (h1 : idx < aig.decls.size) (h2),

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,7 @@ theorem map.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx)
9393
· simp
9494
termination_by len - idx
9595

96+
@[grind! .]
9697
theorem map_le_size {aig : AIG α} (target : MapTarget aig len) :
9798
aig.decls.size ≤ (map aig target).aig.decls.size := by
9899
unfold map
@@ -118,6 +119,7 @@ theorem map.go_decl_eq {aig : AIG α} (i) (hi)
118119
simp
119120
termination_by len - i
120121

122+
@[grind =]
121123
theorem map_decl_eq {aig : AIG α} (target : MapTarget aig len) :
122124
∀ idx (h1 : idx < aig.decls.size) (h2),
123125
(map aig target).1.decls[idx]'h2

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,7 @@ theorem zip.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx)
115115
· simp
116116
termination_by len - idx
117117

118+
@[grind! .]
118119
theorem zip_le_size (aig : AIG α) (input : BinaryRefVec aig len)
119120
(func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
120121
[LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :
@@ -143,6 +144,7 @@ theorem zip.go_decl_eq {aig : AIG α} (i) (hi) (lhs rhs : RefVec aig len)
143144
simp
144145
termination_by len - i
145146

147+
@[grind =]
146148
theorem zip_decl_eq {aig : AIG α} (input : BinaryRefVec aig len)
147149
(func : (aig : AIG α) → BinaryInput aig → Entrypoint α)
148150
[LawfulOperator α BinaryInput func] [LawfulZipOperator α func] :

0 commit comments

Comments
 (0)