Turning a datatype expression into a Prop

Stream: general

[l1mey]

Is there a way to turn an expression AST into a proposition, for example over the naturals? Here is some code below that it would look as:

inductive Inst : Type where
  | const : (v : Nat) → Inst
  | add : Inst → Inst → Inst
  | sub : Inst → Inst → Inst
  | hole : String → Inst

def lhs : Inst := .add (.hole "x") (.hole "y")
def rhs : Inst := .add (.hole "y") (.hole "x")

theorem equal : lhs.func = rhs.func :=
  funext x y
  ...

[Niels Voss]

Sorry, I'm not quite sure what you're asking. Did you want help proving equal? Also, what is the definition of Inst.func?

[l1mey]

I'm wondering how I would write Inst.func, it would take in an Inst and create a function with an argument for every different hole and return that. Proving equal is just an example. Am I forced to use metaprogramming here?

[Aaron Liu]

can you give an example

[Aaron Liu]

what function will lhs.func be

[l1mey]

def lhs_func (x y : Nat) : Nat := x + y

[Aaron Liu]

how do you determine which strings correspond to which arguments

[l1mey]

Probably the first argument from the "left" which is x goes first. But that's an implementation detail. My question is if I am forced to use metaprogramming to construct such an expression and how would I do so.

[Aaron Liu]

it is possible to construct the function without metaprogramming

[Aaron Liu]

basically, define it recursively by pattern matching

[Aaron Liu]

you will probably have to use some sort of monad to keep track of which holes are which variables

[Ilmārs Cīrulis]

This doesn't work for you, right?

import Mathlib

inductive Inst : Type where
  | const : (v : Nat) → Inst
  | add : Inst → Inst → Inst
  | sub : Inst → Inst → Inst
  | hole : String → Inst

def meaning := String → Nat

def eval (M : meaning) (A : Inst) : Nat :=
  match A with
  | Inst.const v => v
  | Inst.add X Y => eval M X + eval M Y
  | Inst.sub X Y => eval M X - eval M Y
  | Inst.hole s => M s

def equivalent (A B : Inst): Prop :=
  forall (M : meaning), eval M A = eval M B

def lhs : Inst := .add (.hole "x") (.hole "y")
def rhs : Inst := .add (.hole "y") (.hole "x")

theorem identity : equivalent lhs rhs := by
  unfold lhs rhs
  intros M
  simp [eval]
  rw [add_comm]

I agree with Aaron Liu that it should be possible to construct what you want, of course.

[Ilmārs Cīrulis]

But I'm probably too slow to do it fast enough. :sweat_smile:

[l1mey]

After the simp [eval] it does give

M : meaning
⊢ M "x" + M "y" = M "y" + M "x"

This is okay for me, but it would be nicer to have a normal Lean expression.

[Aaron Liu]

this is a normal Lean expression???

[Aaron Liu]

what exactly are you looking for?

[l1mey]

def lhs.func (x y : Nat) : Nat := x + y
def rhs.func (x y : Nat) : Nat := y + x

which I'm guessing is only possible with metaprogramming.

[Aaron Liu]

it's possible without metaprogramming (but you won't be able to control the variable names)

[Aaron Liu]

it's just really, a weird thing to do?

[Aaron Liu]

by the way, I mean up to defeq of course

[Aaron Liu]

so you'll be able to do def lhs.func := Inst.func lhs and you'll be able to do theorem lhs.func_def : lhs.func = fun x y => x + y := rfl