example attributes

Stream: general

[Yaël Dillies]

Can examples be tagged with attributes?

[Kevin Buzzard]

#xy?

[Yaël Dillies]

The context is that I am writing many proofs about Heyting algebras and I derive those proofs from intuitionistic proofs about props, thanks to the correspondance between intuitionistic logic and Heyting algebras. I am then leaving the examples behind as a source for a future tactic that would automatically use that metatheorem to write the proofs.

[Yaël Dillies]

So in particular I don't want someone to golf my proofs using classical logic because that would break the point! So I would like to tag examples with @[intuit], where intuit would be an attribute checking that you only use propext and quot.sound as axioms.

[Yaël Dillies]

I could also make those examples lemmas, but they are of little use in the propositional world.

[Kevin Buzzard]

Removing the tag would then golf it even more ;-)

[Yaël Dillies]

Yes but hopefully that will reduce the probability of someone doing so!

[Yaël Dillies]

And of course I will write a library note explaining the role of those examples.

[Kevin Buzzard]

Are examples called weird auto-generated names internally? I suppose you could just give them silly private names

[Reid Barton]

Are examples even added to the environment?

[Kevin Buzzard]

import tactic

example : ℕ := (⟨2, rfl⟩ : ∃ x, x = 2).some
/-
missing 'noncomputable' modifier, definition '_example' depends on 'Exists.some'
-/

[Kevin Buzzard]

doesn't seem to survive long though, if it ever even existed

[Eric Rodriguez]

They get some awful auto-generated name iirc

[Alex J. Best]

Examples aren't added to the environment I believe. Maybe you can just add a comment telling people not to golf them?

[Yaël Dillies]

I don't care about lasting attributes. I only want "immediate action" attributes.

[Reid Barton]

How about just not using example?

[Yaël Dillies]

As I said, that would result in pretty useless lemmas about Prop (because assumptions would be uncurried and quite unnatural), and I would need to come up with names.

[Reid Barton]

I don't understand what you want to do but example seems needlessly obscure

[Kevin Buzzard]

Just make them private and call them example1, example2, ...