18702bdd47
This PR implements `instantiateRevBetaS`, which is similar to
`instantiateRevS` but beta-reduces nested applications whose function
becomes a lambda after substitution.
For example, if `e` contains a subterm `#0 a` and we apply the
substitution `#0 := fun x => x + 1`, then `instantiateRevBetaS` produces
`a + 1` instead of `(fun x => x + 1) a`.
This is useful when applying theorems. For example, when applying
`Exists.intro`:
```lean
Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
```
to a goal of the form `∃ x : Nat, p x ∧ q x`, we create metavariables
`?w` and `?h`. With `instantiateRevBetaS`, the type of `?h` becomes `p
?w ∧ q ?w` instead of `(fun x => p x ∧ q x) ?w`.
29 lines
696 B
Text
29 lines
696 B
Text
import Lean.Meta.Sym
|
|
open Lean Meta Sym
|
|
|
|
opaque p : Nat → Prop
|
|
opaque q : Nat → Nat → Prop
|
|
|
|
def ex := ∃ x : Nat, p x ∧ q x .zero
|
|
|
|
def test : SymM Unit := do
|
|
let p ← mkPatternFromTheorem ``Exists.intro
|
|
let e := (← getConstInfo ``ex).value!
|
|
let some r ← p.match? e | throwError "failed"
|
|
let app := mkAppN (mkConst ``Exists.intro r.us) r.args
|
|
logInfo app
|
|
for arg in r.args do
|
|
if arg.isMVar then
|
|
logInfo m!"{arg} : {← inferType arg}"
|
|
return ()
|
|
|
|
/--
|
|
info: @Exists.intro Nat (fun x => And (p x) (q x Nat.zero)) ?m.1 ?m.2
|
|
---
|
|
info: ?m.1 : Nat
|
|
---
|
|
info: ?m.2 : And (p ?m.1) (q ?m.1 Nat.zero)
|
|
-/
|
|
#guard_msgs in
|
|
set_option pp.explicit true in
|
|
#eval SymM.run' test
|