fix: eta-expanded instances at SynthInstance.lean (#3638)
Remark: this commit removes the `jason1.lean` test. Motivation: It breaks all the time due to changes we make, and it is not clear anymore what it is testing. --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This commit is contained in:
Leonardo de Moura
GitHub
parent
6dd4f4b423
commit
b39042b32c
6 changed files with 50 additions and 180 deletions
|
|
@ -321,6 +321,26 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
|
|||
subgoals := inst.synthOrder.map (mvars[·]!) |>.toList
|
||||
}
|
||||
|
||||
/--
|
||||
Similar to `mkLambdaFVars`, but ensures result is eta-reduced.
|
||||
For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
|
||||
the result is `inst` instead of `fun x y => inst x y`.
|
||||
|
||||
We added this auxiliary function because of aliases such as `DecidablePred`. For example,
|
||||
consider the following definition.
|
||||
```
|
||||
def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
|
||||
match xs with
|
||||
| [] => []
|
||||
| x :: xs' => if p x then x :: filter p xs' else filter p xs'
|
||||
```
|
||||
Without `mkLambdaFVars'`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
|
||||
Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
|
||||
we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
|
||||
-/
|
||||
private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
|
||||
return (← mkLambdaFVars xs e).eta
|
||||
|
||||
/--
|
||||
Try to synthesize metavariable `mvar` using the instance `inst`.
|
||||
Remark: `mctx` is set using `withMCtx`.
|
||||
|
|
@ -335,7 +355,7 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
|
|||
withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
|
||||
return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
|
||||
if (← isDefEq mvarTypeBody instTypeBody) then
|
||||
let instVal ← mkLambdaFVars xs instVal
|
||||
let instVal ← mkLambdaFVars' xs instVal
|
||||
if (← isDefEq mvar instVal) then
|
||||
return some ((← getMCtx), subgoals)
|
||||
return none
|
||||
|
|
@ -448,7 +468,7 @@ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM
|
|||
let ys := ys.toArray
|
||||
let mvarType' ← mkForallFVars ys body
|
||||
withLocalDeclD `redf mvarType' fun f => do
|
||||
let transformer ← mkLambdaFVars #[f] (← mkLambdaFVars xs (mkAppN f ys))
|
||||
let transformer ← mkLambdaFVars' #[f] (← mkLambdaFVars' xs (mkAppN f ys))
|
||||
trace[Meta.synthInstance.unusedArgs] "{mvarType}\nhas unused arguments, reduced type{indentExpr mvarType'}\nTransformer{indentExpr transformer}"
|
||||
return some (mvarType', transformer)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
instReprTree
|
||||
instReprListTree
|
||||
fun a b => instDecidableEqTree a b
|
||||
fun a b => instDecidableEqListTree a b
|
||||
instDecidableEqTree
|
||||
instDecidableEqListTree
|
||||
instBEqTree
|
||||
instBEqListTree
|
||||
instHashableTree
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@
|
|||
has unused arguments, reduced type
|
||||
∀ (b : β), IsSmooth (f b)
|
||||
Transformer
|
||||
fun redf a b => redf b
|
||||
fun redf a => redf
|
||||
[Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
|
||||
[Meta.synthInstance.instances] #[inst✝]
|
||||
[Meta.synthInstance] ❌ apply inst✝ to ∀ (b : β), IsSmooth (f b)
|
||||
|
|
@ -74,7 +74,7 @@
|
|||
has unused arguments, reduced type
|
||||
∀ (b : β), IsSmooth (f b)
|
||||
Transformer
|
||||
fun redf a a b => redf b
|
||||
fun redf a a => redf
|
||||
[Meta.synthInstance] ❌ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
|
||||
[Meta.synthInstance] ✅ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
|
|
|
|||
|
|
@ -1,50 +0,0 @@
|
|||
section
|
||||
variable (G : Type) (T : Type) (Tm : Type)
|
||||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||||
(getCtx : T → G) (getTy : Tm → T)
|
||||
inductive CtxSyntaxLayer where
|
||||
| emp : CtxSyntaxLayer
|
||||
| snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
|
||||
end
|
||||
section
|
||||
variable (G : Type) (T : Type) (Tm : Type)
|
||||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||||
(getCtx : T → G) (getTy : Tm → T)
|
||||
-- : CtxSyntaxLayer G T EG getCtx → G)
|
||||
|
||||
inductive TySyntaxLayer where
|
||||
| top : {Γ : G} → TySyntaxLayer
|
||||
| bot : {Γ : G} → TySyntaxLayer
|
||||
| nat : {Γ : G} → TySyntaxLayer
|
||||
| arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
|
||||
|
||||
def getCtxStep : TySyntaxLayer G T EG getCtx → G
|
||||
| TySyntaxLayer.top (Γ := Γ) .. => Γ
|
||||
| TySyntaxLayer.bot (Γ := Γ) .. => Γ
|
||||
| TySyntaxLayer.nat (Γ := Γ) .. => Γ
|
||||
| TySyntaxLayer.arrow (Γ := Γ) .. => Γ
|
||||
end
|
||||
section
|
||||
variable (G : Type) (T : Type) (Tm : Type)
|
||||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||||
(EGrfl : ∀ {Γ}, EG Γ Γ)
|
||||
(getCtx : T → G) (getTy : Tm → T)
|
||||
(GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)
|
||||
|
||||
inductive TmSyntaxLayer where
|
||||
| tt : {Γ : G} → TmSyntaxLayer
|
||||
| zero : {Γ : G} → TmSyntaxLayer
|
||||
| succ : {Γ : G} → TmSyntaxLayer
|
||||
| app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
|
||||
→ (f x : Tm)
|
||||
→ ET (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx)) (getTy f)
|
||||
→ ET A (getTy x)
|
||||
→ TmSyntaxLayer
|
||||
|
||||
set_option pp.all true
|
||||
def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
|
||||
| TmSyntaxLayer.tt .. => TAlgebra TySyntaxLayer.top
|
||||
| TmSyntaxLayer.zero .. => TAlgebra TySyntaxLayer.nat
|
||||
| TmSyntaxLayer.succ .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra TySyntaxLayer.nat) (TAlgebra TySyntaxLayer.nat) EGrfl EGrfl)
|
||||
| TmSyntaxLayer.app (B:=B) .. => B
|
||||
end
|
||||
|
|
@ -1,124 +0,0 @@
|
|||
jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
|
||||
@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.arrow G T EG getCtx
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
|
||||
(@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
|
||||
@EGrfl
|
||||
(getCtx
|
||||
(TAlgebra
|
||||
(@TySyntaxLayer.nat G T EG getCtx
|
||||
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
|
||||
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
|
||||
context:
|
||||
G T Tm : Type
|
||||
EG : G → G → Type
|
||||
ET : T → T → Type
|
||||
ETm : Tm → Tm → Type
|
||||
EGrfl : {Γ : G} → EG Γ Γ
|
||||
getCtx : T → G
|
||||
getTy : Tm → T
|
||||
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
|
||||
TAlgebra : TySyntaxLayer G T EG getCtx → T
|
||||
Γ✝ : G
|
||||
⊢ G
|
||||
24
tests/lean/run/instEtaIssue.lean
Normal file
24
tests/lean/run/instEtaIssue.lean
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
def filter (p : α → Prop) [DecidablePred p] (xs : List α) : List α :=
|
||||
match xs with
|
||||
| [] => []
|
||||
| x :: xs' => if p x then x :: filter p xs' else filter p xs'
|
||||
|
||||
attribute [simp] filter
|
||||
|
||||
set_option pp.explicit true
|
||||
|
||||
/--
|
||||
info: filter._eq_2.{u_1} {α : Type u_1} (p : α → Prop) [@DecidablePred α p] (x : α) (xs' : List α) :
|
||||
@Eq (List α) (@filter α p inst✝ (@List.cons α x xs'))
|
||||
(@ite (List α) (p x) (inst✝ x) (@List.cons α x (@filter α p inst✝ xs')) (@filter α p inst✝ xs'))
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check filter._eq_2 -- We should not have terms of the form `@filter α p (fun x => inst✝ x) xs'`
|
||||
|
||||
|
||||
def filter_length (p : α → Prop) [DecidablePred p] : (filter p xs).length ≤ xs.length := by
|
||||
induction xs with
|
||||
| nil => simp [filter]
|
||||
| cons x xs ih =>
|
||||
simp only [filter]
|
||||
split <;> simp only [List.length] <;> omega
|
||||
Loading…
Add table
Reference in a new issue