Skip to content

Commit f325ac7

Browse files
nomeatanomeata
committed
With -underLambda a bit of progress
1 parent 7438e1b commit f325ac7

File tree

2 files changed

+141
-17
lines changed

2 files changed

+141
-17
lines changed

‎src/Lean/Elab/PreDefinition/Structural/Eqns.lean‎

Lines changed: 31 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,34 @@ structure EqnInfo extends EqnInfoCore where
2626

2727
builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
2828

29+
def getSimpMatchContext : MetaM Simp.Context := do
30+
Simp.mkContext
31+
(simpTheorems := {})
32+
(congrTheorems := (← getSimpCongrTheorems))
33+
(config := { Simp.neutralConfig with dsimp := false, etaStruct := .none, underLambda := false })
34+
35+
def simpMatch (e : Expr) : MetaM Simp.Result := do
36+
let discharge? ← SplitIf.mkDischarge?
37+
(·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre, discharge? })
38+
where
39+
pre (e : Expr) : SimpM Simp.Step := do
40+
unless (← isMatcherApp e) do
41+
return Simp.Step.continue
42+
let matcherDeclName := e.getAppFn.constName!
43+
-- First try to reduce matcher
44+
match (← reduceRecMatcher? e) with
45+
| some e' => return Simp.Step.done { expr := e' }
46+
| none => Simp.simpMatchCore matcherDeclName e
47+
48+
def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
49+
let target ← instantiateMVars (← mvarId.getType)
50+
let r ← simpMatch target
51+
applySimpResultToTarget mvarId target r
52+
53+
def simpMatch? (mvarId : MVarId) : MetaM (Option MVarId) := do
54+
let mvarId' ← simpMatchTarget mvarId
55+
if mvarId != mvarId' then return some mvarId' else return none
56+
2957
private partial def mkProof (declName : Name) (unfold : MVarId → MetaM MVarId) (type : Expr) : MetaM Expr := do
3058
trace[Elab.definition.structural.eqns] "proving: {type}"
3159
withNewMCtxDepth do
@@ -39,8 +67,8 @@ where
3967
trace[Elab.definition.structural.eqns] "go1\n{MessageData.ofGoal mvarId}"
4068
if let some mvarId ← simpIf? mvarId then
4169
go1 mvarId
42-
else if let some mvarId ← deltaRHS? mvarId declName then
43-
go1 mvarId
70+
-- else if let some mvarId ← deltaRHS? mvarId declName then
71+
-- go1 mvarId
4472
else if let some mvarIds ← splitTarget? mvarId then
4573
mvarIds.forM go1
4674
else
@@ -56,7 +84,7 @@ where
5684
else if let some mvarId ← simpMatch? mvarId then
5785
go2 mvarId
5886
else
59-
let ctx ← Simp.mkContext (config := { iota := false })
87+
let ctx ← Simp.mkContext (config := { iota := false, underLambda := false })
6088
match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
6189
| TacticResultCNM.closed => return ()
6290
| TacticResultCNM.modified mvarId => go2 mvarId

‎tests/lean/run/5667.lean‎

Lines changed: 110 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -10,25 +10,121 @@ def optimize : Expr → Expr
1010
| _, _ => .const 0
1111

1212
/--
13-
info: optimize.eq_def (x✝ : Expr) :
14-
optimize x✝ =
15-
match x✝ with
16-
| Expr.const i => Expr.const i
17-
| Expr.op bop e1 =>
18-
match bop, optimize e1 with
19-
| x, Expr.const i => Expr.op bop (Expr.const 0)
20-
| x, x_1 => Expr.const 0
13+
error: Failed to realize constant optimize.eq_def:
14+
failed to generate equational theorem for 'optimize'
15+
case h_2.h_1
16+
x e1 : Expr
17+
bop✝ bop_1 : Unit
18+
x_1 : Expr
19+
i : BitVec 32
20+
heq✝ : optimize e1 = Expr.const i
21+
⊢ (match bop✝,
22+
(Expr.rec
23+
(fun i =>
24+
⟨(fun x f =>
25+
(match (motive := (x : Expr) → Expr.below x → Expr) x with
26+
| Expr.const i => fun x => Expr.const i
27+
| Expr.op bop e1 => fun x =>
28+
match bop, x.1 with
29+
| x, Expr.const i => Expr.op bop (Expr.const 0)
30+
| x, x_2 => Expr.const 0)
31+
f)
32+
(Expr.const i) PUnit.unit,
33+
PUnit.unit⟩)
34+
(fun op e1 e1_ih =>
35+
⟨(fun x f =>
36+
(match (motive := (x : Expr) → Expr.below x → Expr) x with
37+
| Expr.const i => fun x => Expr.const i
38+
| Expr.op bop e1 => fun x =>
39+
match bop, x.1 with
40+
| x, Expr.const i => Expr.op bop (Expr.const 0)
41+
| x, x_2 => Expr.const 0)
42+
f)
43+
(Expr.op op e1) e1_ih,
44+
e1_ih⟩)
45+
e1).1 with
46+
| x, Expr.const i => Expr.op bop✝ (Expr.const 0)
47+
| x, x_2 => Expr.const 0) =
48+
Expr.op bop✝ (Expr.const 0)
49+
---
50+
error: Failed to realize constant optimize.eq_def:
51+
failed to generate equational theorem for 'optimize'
52+
case h_2.h_1
53+
x e1 : Expr
54+
bop✝ bop_1 : Unit
55+
x_1 : Expr
56+
i : BitVec 32
57+
heq✝ : optimize e1 = Expr.const i
58+
⊢ (match bop✝,
59+
(Expr.rec
60+
(fun i =>
61+
⟨(fun x f =>
62+
(match (motive := (x : Expr) → Expr.below x → Expr) x with
63+
| Expr.const i => fun x => Expr.const i
64+
| Expr.op bop e1 => fun x =>
65+
match bop, x.1 with
66+
| x, Expr.const i => Expr.op bop (Expr.const 0)
67+
| x, x_2 => Expr.const 0)
68+
f)
69+
(Expr.const i) PUnit.unit,
70+
PUnit.unit⟩)
71+
(fun op e1 e1_ih =>
72+
⟨(fun x f =>
73+
(match (motive := (x : Expr) → Expr.below x → Expr) x with
74+
| Expr.const i => fun x => Expr.const i
75+
| Expr.op bop e1 => fun x =>
76+
match bop, x.1 with
77+
| x, Expr.const i => Expr.op bop (Expr.const 0)
78+
| x, x_2 => Expr.const 0)
79+
f)
80+
(Expr.op op e1) e1_ih,
81+
e1_ih⟩)
82+
e1).1 with
83+
| x, Expr.const i => Expr.op bop✝ (Expr.const 0)
84+
| x, x_2 => Expr.const 0) =
85+
Expr.op bop✝ (Expr.const 0)
86+
---
87+
error: unknown identifier 'optimize.eq_def'
2188
-/
2289
#guard_msgs in
2390
#check optimize.eq_def
2491

2592
/--
26-
info: equations:
27-
theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
28-
theorem optimize.eq_2 : ∀ (e1 : Expr) (bop : Unit) (i : BitVec 32),
29-
optimize e1 = Expr.const i → optimize (Expr.op bop e1) = Expr.op bop (Expr.const 0)
30-
theorem optimize.eq_3 : ∀ (e1 : Expr) (bop : Unit),
31-
(∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop e1) = Expr.const 0
93+
error: failed to generate equational theorem for 'optimize'
94+
case h_2.h_1
95+
x e1 : Expr
96+
bop✝ bop_1 : Unit
97+
x_1 : Expr
98+
i : BitVec 32
99+
heq✝ : optimize e1 = Expr.const i
100+
⊢ (match bop✝,
101+
(Expr.rec
102+
(fun i =>
103+
⟨(fun x f =>
104+
(match (motive := (x : Expr) → Expr.below x → Expr) x with
105+
| Expr.const i => fun x => Expr.const i
106+
| Expr.op bop e1 => fun x =>
107+
match bop, x.1 with
108+
| x, Expr.const i => Expr.op bop (Expr.const 0)
109+
| x, x_2 => Expr.const 0)
110+
f)
111+
(Expr.const i) PUnit.unit,
112+
PUnit.unit⟩)
113+
(fun op e1 e1_ih =>
114+
⟨(fun x f =>
115+
(match (motive := (x : Expr) → Expr.below x → Expr) x with
116+
| Expr.const i => fun x => Expr.const i
117+
| Expr.op bop e1 => fun x =>
118+
match bop, x.1 with
119+
| x, Expr.const i => Expr.op bop (Expr.const 0)
120+
| x, x_2 => Expr.const 0)
121+
f)
122+
(Expr.op op e1) e1_ih,
123+
e1_ih⟩)
124+
e1).1 with
125+
| x, Expr.const i => Expr.op bop✝ (Expr.const 0)
126+
| x, x_2 => Expr.const 0) =
127+
Expr.op bop✝ (Expr.const 0)
32128
-/
33129
#guard_msgs in
34130
#print equations optimize

0 commit comments

Comments
 (0)