construct a name for a new def

Stream: new members

[Mark Aagaard]

I'm teaching a course on logic to first year computer engineering students. One of the topics is formalizing English sentences in logic. To do this, we construct some uninterpreted types and functions, then write additional formulas in terms of these uninterpreted types and functions.

Sometimes we need to define an ordering relation (e.g., ≤) on the uninterpreted type. I would like the students to be able to write:

axiom Rank : Type
Overload (≤) Rank

and have Overload (≤) Rank expand to:

axiom LE_Rank : Rank → Rank → Prop
instance : LE Rank where
  le := LE_Rank

The macro I have written is:

macro "Overload" "(≤)" ty:term : command =>
  `(axiom LE_foo : $ty → $ty → Prop
    instance : LE $ty where
      le := LE_foo
  )

which works, except that the name of the definition LE_foo is hard coded. I would like to construct a name based on $ty.

-mark

[Eric Wieser]

How's this?

import Lean

open Lean

elab cmd:"Overload" "(≤)" ty:term : command => do
  let name ← Elab.Command.liftTermElabM do
    let e ← Lean.Elab.Term.elabTerm ty none
    let .const name _ ← Meta.whnf e | throwErrorAt ty "Could not guess name"
    return name

  let ident ← mkIdentFromRef (name ++ `LE)

  Elab.Command.elabCommand <| ← `(
    axiom $ident : $ty → $ty → Prop
    instance : LE $ty where
      le := $ident)

  Elab.addConstInfo cmd (name ++ `LE)


axiom Rank : Type
Overload (≤) Rank

[Eric Wieser]

Though axiom is not a great pattern here

[Eric Wieser]

If you do really want axiom, you could also skip the Overload syntax with @[instance] axiom Rank.instLE : LE Rank

[Mark Aagaard]

@Eric Wieser - thanks.

One question, you wrote "axiom is not a great pattern here". What would be a better alternative? I chose axiomsimply because it was the first idea I had that worked.

-mark

[Aaron Liu]

You can use variable

[Mark Aagaard]

I originally tried variable, but ran into problems:

variable (Ty:Type)
variable (p : Ty → Prop)
def q (x:Ty) := p x
def r (x:Ty) := q x

gives an error on q x, because Lean expects the first argument of q to be an instantiation of p.

If either Ty or x is a variable, I get an error with the q x in the definition of r. For Ty, I could use either inductive Ty or axiom Ty : Type. For p, the only solution I've found is axiom:

inductive Ty
axiom p : Ty → Prop
def q (x:Ty) := p x
def r (x:Ty) := q x

-mark

[Eric Wieser]

Another option is to use

class MyContext (Ty : Type*) where
  p : Ty → Prop

export MyContext (p)

variable [MyContext Ty]

def q (x : Ty) := p x

This has the big advantage over axiom that you can go back and apply these results to some concrete Ty

[Robin Arnez]

If you don't care about which relation you get, you can use opaque instead of axiom (the rhs is just to show that LE $id is inhabited):

import Lean.Elab.Command

open Lean Elab Command in

elab cmd:"Overload" "(≤)" id:ident : command => do
  let name ← liftCoreM (realizeGlobalConstNoOverload id)
  let ident ← mkIdentFromRef (name ++ `LE)
  elabCommand <| ← `(@[instance] opaque $ident : LE $id := ⟨fun _ _ => True⟩)
  addConstInfo cmd (name ++ `LE)

axiom MyType : Type
Overload (≤) MyType

Although I'm not quite sure why you'd want an LE relation without any knowledge about its properties.

[Mark Aagaard]

Aaron, Eric, Robin -
Thanks for the insightful answers. It's very helpful to see a variety of alternatives.

@Robin Arnez : I'm teaching students to formalize English sentences into logic. The first step is to define an environment of uninterpreted types, functions, relations, etc. Hence, I want < as uninterpreted.

-mark

[Matt Diamond]

@Robin Arnez I would do it in exactly the opposite way: define opaque MyType : Type and then set up LE MyType as an axiom

[Matt Diamond]

but maybe it's just a question of personal style

[Matt Diamond]

opaque is good because it prevents the introduction of a proof of false (or at least that's my understanding)

[Robin Arnez]

Or both opaque! And yes, axioms by nature can introduce proofs of False if you are not careful enough. That, and it's slightly weird to see a ton of obscure axioms when you look at #print axioms (which is probably not relevant here but I just wanted to note).

[Mark Aagaard]

I like the idea of making both the type and LE function opaque.

@Robin Arnez - I'm having difficulty understanding your elaboration function. Superficially, it looks like it is the equivalent of:

opaque Ty1 : Type
@[instance] opaque LE_Ty1 : LE Ty1 := (fun _ _ => True)

But, the above doesn't typecheck because fun _ _ => True doesn't have the type LE Ty1. What am I missing?

[Aaron Liu]

Not (fun _ _ => True), but ⟨fun _ _ => True⟩.

[Aaron Liu]

(note the brackets)

[Mark Aagaard]

Ah, ok. Thanks. I've been bitten by that before when transcribing code. I should have thought of the brackets.