Increase the depth of all de Bruijn indices

Stream: Is there code for X?

[Leni Aniva]

Is there a function for increasing all De Bruijn indices in an Expr by 1?

I'm building a tactic that converts a goal from ?m to let a := ...; ?m, so all indices in ?m would have to go up by 1.

[Kyle Miller]

docs#Lean.Expr.liftLooseBVars but there are also higher-level interfaces such as docs#Lean.Meta.mkLetFVars.

Does ?m refer to a at all? Do you want ?m to have a in the local context? If so, then you need other approaches.

[Leni Aniva]

Kyle Miller said:

docs#Lean.Expr.liftLooseBVars but there are also higher-level interfaces such as docs#Lean.Meta.mkLetFVars.

Does ?m refer to a at all? Do you want ?m to have a in the local context? If so, then you need other approaches.

It doesn't need to have a in the local context, but out of curiosity how should it be done if ?m needs to refer to a? What I was thinking of is to just refer to a by .deBruijnIndex 0

[Kyle Miller]

I'm not really understanding what you're wanting to do. But, one thing to know is that there's a lot of API to avoid ever having to ever use .bvar 0 terms.

Could you give an example of what the tactic would do in some concrete scenario?

[Leni Aniva]

Kyle Miller said:

I'm not really understanding what you're wanting to do. But, one thing to know is that there's a lot of API to avoid ever having to ever use .bvar 0 terms.

Could you give an example of what the tactic would do in some concrete scenario?

I want to build a tactic that makes the motive in functions such as Nat.brecOn a separate goal, so the tactic would transform a metavariable ?0: target into

?0 := Nat.brecOn (motive := ?1) ?zero ?succ n ...

?1: Nat -> target
?zero: ?1 0
?succ: ... -> ?1 m

where n is the value for which we want to prove that the motive holds. The Nat.brecOn gives ?1 n as the resultant type and this unifies with ?0.

[Kyle Miller]

I'm not sure how you can assign a motive so that this Nat.brecOn assignment is type correct (also, by the way, Nat.brecOn has only one minor premise, not two).

Do you mean "tactic" like syntax in a by block, or do you mean "tactic" like a Meta tactic? If it's the first, could you give a concrete example of how the tactic would look like in practice?

[Leni Aniva]

Kyle Miller said:

I'm not sure how you can assign a motive so that this Nat.brecOn assignment is type correct (also, by the way, Nat.brecOn has only one minor premise, not two).

Do you mean "tactic" like syntax in a by block, or do you mean "tactic" like a Meta tactic? If it's the first, could you give a concrete example of how the tactic would look like in practice?

The reason I want to use let ...; is so that the type correctness could depend on the value of the motive.

An example would be

g1
n: Nat
p: (some proposition of n)
|- p

and when the tactic acts on this goal ?g1, it produces 3 goals:

?motive
|- Nat -> Prop
?zero
|- ?motive 0
?succ
m: Nat
|- ?motive m -> ?motive m.succ

and it assigns ?g1 to the value

Nat.recOn {motive := ?motive} n ?zero ?succ

Would this be possible?