get target or hyp type

Stream: general

[Johan Commelin]

Is there something like this already? Or am I approaching things wrong?

meta def target_or_hyp_type : option expr → tactic expr
| none     := target
| (some h) := infer_type h

[Mario Carneiro]

that seems fine to me, but it also looks specific to your use case

[Mario Carneiro]

if you want something more general, I would suggest something taking a loc as input

[Johan Commelin]

Does something like that already exist?

[Johan Commelin]

Similarly something like this...??

meta def replace' : option expr → expr → expr → tactic unit
| none     := tactic.replace_target
| (some h) := λ e p, tactic.replace_hyp h e p >> skip

[Johan Commelin]

Or should that also be done with loc?

[Mario Carneiro]

I think you are asking the wrong question. What is this for? Usually the goal and the hypotheses have to be treated differently, since in one you can reason forward and the other you reason backward

[Johan Commelin]

Except for rw, I think

[Mario Carneiro]

There is a function, loc.apply, where you give it a tactic to operate on hypotheses and another to operate on the goal, and it will do what it needs to on any loc, using any combination of h, |- and *

[Johan Commelin]

Yep, I'm already using that one

[Mario Carneiro]

as such, there is no option expr involved

[Mario Carneiro]

just two separate functions

[Johan Commelin]

But that leads to lots of duplication, I think

[Johan Commelin]

See the nth-rewrite branch

[Mario Carneiro]

it's not really duplication, it only looks like it

[Mario Carneiro]

the actual tactics you have to use and the order stuff flows around is different

[Mario Carneiro]

once you get to something rewrite-like, it does turn into just one tactic, with the form expr -> tactic (expr x expr)

[Mario Carneiro]

looking at your branch, I think you should indeed factor everything through a conversion and applying a conversion

[Johan Commelin]

What is a conversion?

[Mario Carneiro]

expr -> tactic (expr x expr), given input e produces e' and a proof of p : e = e'

[Mario Carneiro]

you can cleanly express descending into subterms with this type

[Mario Carneiro]

and given such a conversion you can apply it to the target as one tactic, or apply it to a hypothesis

[Johan Commelin]

Are such conversions already used in mathlib? Are there supporting functions?

[Johan Commelin]

Or should I roll my own?

[Mario Carneiro]

there are a couple, I use it a lot in ring

[Mario Carneiro]

but mostly it's just a pattern that doesn't require much support

[Johan Commelin]

Ok, but it hasn't been factored out in some sort of reusable package?

[Johan Commelin]

Ok... fine

[Mario Carneiro]

see for instance simp_target and simp_hyp that rely on tactic.simplify which is basically a conversion like I described (although it takes some extra arguments)

[Mario Carneiro]

they just get the result from the conversion and pass to replace_target and replace_hyp respectively

[Mario Carneiro]

so I think these functions are the reusable package

[Mario Carneiro]

In the tactic.norm_num file there are some orphaned conversion operations refl_conv and trans_conv that could go in tactic.core

[Johan Commelin]

@Mario Carneiro I have no idea whether I did things right, but I think I've deduplicated the code quite far. See #2471