create alias

Stream: general

[Zesen Qian]

How can I create an alias to anther declaration? Say, in my namespace foo I want to create a true such that users can see foo.true and the prover treats it equally to true from core.

[Mario Carneiro]

equally is hard, but there are a few ways to get close

[Zesen Qian]

right now I'm thinking about def with attribute [reducible]

[Mario Carneiro]

@[reducible] def makes rw and simp see through the definition, as well as typeclass inference

[Zesen Qian]

I guess that should work, but really I'm looking for shorter path.

[Mario Carneiro]

abbreviation does something similar with kernel reduction, I'm not sure exactly

[Mario Carneiro]

what do you mean "shorter path"?

[Zesen Qian]

I mean, less characters to type.

[Zesen Qian]

alias true = true would be the best.

[Mario Carneiro]

mathlib has an alias tactic, but it doesn't set reducible

[Mario Carneiro]

what's wrong with just def true := true?

[Chris Hughes]

notation?

[Mario Carneiro]

also, what is your use case? I wrote alias to support alias constructions but it doesn't get much use since I specifically try to avoid aliases

[Zesen Qian]

I need something in my namespace that's definitionally equal to true

[Zesen Qian]

@Chris Hughes I haven't used notation before, can you give an example?

[Mario Carneiro]

def true := true is the easiest way to accomplish that

[Mario Carneiro]

notation `true'` := true

[Mario Carneiro]

but notation is not a def

[Mario Carneiro]

so there will be no foo.true' that way

[Zesen Qian]

yeah, I realize that.

[Zesen Qian]

ok, so the best way is reducible def.

[Mario Carneiro]

but you still haven't said why you need this

[Zesen Qian]

I'm doing some metaprogramming. A proof given by SMT solvers is mapped to a proof in lean.

[Zesen Qian]

so a true in source proof mapped to true in lean.

[Mario Carneiro]

then just map to the real true

[Zesen Qian]

I have a file containing all stuff that source proofs will refer.

[Zesen Qian]

so I don't need to write the mapping myself. The meta program will look it up itself.

[Mario Carneiro]

but then your output statements will just be needlessly encoded with reducible defs

[Mario Carneiro]

you are writing the mapping just by giving these defs

[Zesen Qian]

yeah, but that's not big problem, no one is gonna read the proof as long as it's correct.

[Zesen Qian]

machine generated proofs are never intended for people.

[Mario Carneiro]

heh, you would be surprised

[Zesen Qian]

I hope I will never be suprised.

[Zesen Qian]

anyway, I'm going reducible defs.

[Mario Carneiro]

I don't think there is any point in using reducible here though. if it's in the proof term it's in the proof term

[Zesen Qian]

I don't know what you meant.

[Mario Carneiro]

you aren't using it with rw or anything so it won't be unfolded

[Mario Carneiro]

if you put together a proof using these variant definitions, it will make no difference to the type-correctness as long as it's defeq, and a regular def accomplishes that

[Zesen Qian]

I think you are right.

[Zesen Qian]

I can now get it work without reducible, but I will see it can keep working.

[Zesen Qian]

yeah, but I'm thinking about if the user provides me with the "real" true.

[Zesen Qian]

and when a proof depends on the definitional equality between these two true, will that still work?

[Mario Carneiro]

yes, that's what defeq does

[Zesen Qian]

ok then!

[Mario Carneiro]

you can replace true with true' anywhere in the proof with no changes

[Zesen Qian]

ok. I guess I overlooked lean's ability of identifying equalities.