Syntax -> Name

Stream: lean4

[Henrik Böving]

I'd like to build a macro that looks somewhat like this:

macro "(" x:ident "=" y:term ")" : term => `(λ name => if $x == name then $y else 0)

but x should be turned into a Name instead of being an identifier, I did find the function. I did find getNameOfIdent' which looks like what I need but its only used in more involved elaborators so I'm not quite sure how to use it in a macro case, can i even? If not how can I achieve what i want?

[Simon Hudon]

use x.getId

[Henrik Böving]

How exactly?

macro "(" x:ident "=" y:term ")" : term => `(λ name => if x.getId == name then $y else 0)

#check (x = 12)

didnt work

[Henrik Böving]

Also since this syntax will probably bite me sooner or later I did try other delimiters (namely <) but those ended up colliding with other syntax as well :/ Would someone happen to have better suggestion for syntax like this?

[Simon Hudon]

Can you show the error message that you get?

[Simon Hudon]

Also, sorry for the lack of details: this should work better (modulo the right choice of concrete syntax):

`(λ name => if $(Lean.Syntax.mkNameLit x.getId) == name then $y else 0)

[Henrik Böving]

Simon Hudon said:

Can you show the error message that you get?

The error is that it tells me on the next line its expecting a term, I susepect this is because it might be expecting a greater than notation at the end? not sure.

Simon Hudon said:

Also, sorry for the lack of details: this should work better (modulo the right choice of concrete syntax):

`(λ name => if $(Lean.Syntax.mkNameLit x.getId) == name then $y else 0)

Yes it diiid work better but mkNameLit takes a String so I did a .toString on the getIdent which resulted in:

macro "(" x:ident "=" y:term ")" : term => `(λ name => if $(Lean.Syntax.mkNameLit x.getId.toString) == name then $y else 0)

#check (x = 12)

but this in turn still gives me a:

overloaded, errors
  elaboration function for 'nameLit' has not been implemented
    failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)

  25:8 unknown identifier 'x'

:/

[Sebastian Ullrich]

It's not clear to me what your macro is supposed to do. Do you really want (x = 12) : Name -> Nat?

[Sebastian Ullrich]

In any case, you'll want quote x.getId

[Henrik Böving]

Sebastian Ullrich said:

It's not clear to me what your macro is supposed to do. Do you really want (x = 12) : Name -> Nat?

Yes, the original syntax I was aiming for was <x = 12> : Name -> Nat but the parser doesnt seem to like that

[Henrik Böving]

But the quote part did work out thank you!

[Mario Carneiro]

Henrik Böving said:

Sebastian Ullrich said:

It's not clear to me what your macro is supposed to do. Do you really want (x = 12) : Name -> Nat?

Yes, the original syntax I was aiming for was <x = 12> : Name -> Nat but the parser doesnt seem to like that

Umm, (x = 12) isn't really better. That syntax already means something, are you going to break all uses of = in parentheses?

[Henrik Böving]

I'm very much aware of that, I just don't know of another alternative /o\ feel free to give me one

[Mario Carneiro]

what is the context? This looks like an #xy problem

[Henrik Böving]

I'm mirroring https://isabelle.in.tum.de/library/HOL/HOL-IMP/AExp.html and they defined the syntax <''y'' := 7> so I tried to mirror that (without the '' around names, i also attempted := instead of= but that came down to the same) and this is what came out of it

[Mario Carneiro]

I recommend using a dedicated syntax category for your expressions, with a macro introducer syntax like imp { x := 7 }

[Henrik Böving]

Ah that does sound reasonable yes, thank you!

[Mario Carneiro]

also it should not expand to that if statement, it should be a definition like assign "x" (const 7)

[Henrik Böving]

Why's that?

[Mario Carneiro]

because that way you can have appropriate simp lemmas and theorems about the definition

[Mario Carneiro]

if you write a big program then using notations will lead to an unnecessarily large term

[Mario Carneiro]

also delab doesn't work as well on such expressions

[Henrik Böving]

I see

[Henrik Böving]

Oh also, I did notice that they use this blast tactic quite a lot (it's a generic tableau prover) do we have such a thing as well (maybe in Lean 3?) would it be useful for us if not?

[Mario Carneiro]

there is eblast in lean 3, but it is not used much because it has bugs and no maintainer. It would certainly be good to have a FOL prover in lean, it is not something that we handle well

[Henrik Böving]

puts that on the list of things to have a look at at some point

[Mario Carneiro]

I believe aesop will address some of the needs in this domain, although that is closer to auto than blast

[Henrik Böving]

Henrik Böving said:

puts that on the list of things to have a look at at some point

scratch that I'm just writing endless stacks of cases and apply here, I'll look into it right away

[Mario Carneiro]

did you try simp? It is probably selection bias but I don't really find a strong need for a blast like tactic most of the time

[Henrik Böving]

I did @[simp] my declarations yeah, the thing is that my proofs right now basically look like:

  apply Iff.intro
  case mp =>
    intro h
    cases h with
    | Seq h1 h2 =>
      cases h1 with
      | Seq h3 h4 =>
        apply Seq h3
        apply Seq h4
        assumption
  case mpr =>
    intro h
    cases h with
    | Seq h1 h2 =>
      cases h2 with
      | Seq h3 h4 =>
        apply Seq
        apply Seq h1
        repeat {assumption}

and simp doesnt seem to be able to apply cases on its own. But this proof would definitely be blast-able if blast was told about the cases as eleminiation rule and the Seq as intro rule since its just a tableau like this.

[Mario Carneiro]

that looks like And.assoc

[Mario Carneiro]

and you can probably write the proof as ⟨fun ⟨⟨a, b⟩, c⟩ => ⟨a, ⟨b, c⟩⟩, fun ⟨a, ⟨b, c⟩⟩ => ⟨⟨a, b⟩, c⟩⟩

[Henrik Böving]

lets see

[Henrik Böving]

Ah, no I cannot (but that's just because I didn't show the big picture here) I'm now in this theory https://isabelle.in.tum.de/library/HOL/HOL-IMP/Big_Step.html at Seq_assoc so whenever I apply Seq I can't just use the anonymous constructor.

[Henrik Böving]

If you move further down the file you'll also see that they are just able to blast most of the semantic equivalence goals

[Henrik Böving]

@Mario Carneiro do we have automation for such things with simp as well? Or does this require something new then?

[Henrik Böving]

I'm guessing the 2nd?

[Mario Carneiro]

You haven't shown a MWE so I don't know whether it can be done better. I'm just making guesses based on your code snippet

[Henrik Böving]

That would be:

-- Everything until BigStep is just setup
inductive AExp where
| N : Int → AExp
| V : String → AExp
| Plus : AExp → AExp → AExp

abbrev State := String → Int

namespace AExp
declare_syntax_cat aexp

syntax num : aexp
syntax "-" num : aexp
syntax str : aexp
syntax aexp "+" aexp : aexp
syntax "(" aexp ")" : aexp
syntax term : aexp

syntax "[AExp|" aexp "]" : term

macro_rules
| `([AExp| $num:numLit ]) => `(AExp.N $num)
| `([AExp| - $num:numLit ]) => `(AExp.N (-$num))
| `([AExp| $x:strLit ]) => `(AExp.V $x)
| `([AExp| $l + $r]) => `(AExp.Plus [AExp| $l] [AExp| $r])
| `([AExp| ( $x )]) => `([AExp| $x])
| `([AExp| $x:term ]) => `($x)

def aval : AExp → State → Int
| N n, s => n
| V n, s => s n
| Plus l r, s => (aval l s) + (aval r s)

def updateState (s : State) (n : String) (v : Int) : State := λ x => if x == n then v else s x

end AExp

inductive BExp where
| BConstant : Bool → BExp
| Not : BExp → BExp
| And : BExp → BExp → BExp
| Less : AExp → AExp → BExp

namespace BExp
open AExp

declare_syntax_cat bexp
syntax "⊤" : bexp
syntax "⊥" : bexp
syntax "¬" bexp : bexp
syntax aexp "<" aexp : bexp
syntax "(" bexp ")" : bexp
syntax term : bexp

syntax "[BExp|" bexp "]" : term

macro_rules
| `([BExp| ⊤ ]) => `(BExp.BConstant Bool.true)
| `([BExp| ⊥ ]) => `(BExp.BConstant Bool.false)
| `([BExp| ¬ $x]) => `(BExp.Not $x)
| `([BExp| $l:aexp < $r:aexp]) => `(BExp.Less [AExp| $l] [AExp| $r])
| `([BExp| ( $x )]) => `([BExp| $x])
| `([BExp| $x:term ]) => `($x)

def bval : BExp → State → Bool
| BConstant b, s => b
| Not b, s => !(bval b s)
| And l r, s => bval l s && bval r s
| Less l r, s => aval l s < aval r s

inductive Com where
| Skip : Com
| Assign : String → AExp → Com
| Seq : Com → Com → Com
| If : BExp → Com → Com → Com
| While : BExpr → Com → Com

declare_syntax_cat com

syntax "SKIP" : com
syntax str ":=" aexp : com
syntax term ":=" aexp : com
syntax com ";" com : com
syntax "if" bexp "exec" com "else" com : com
syntax "while" bexp "exec" com: com
syntax "(" com ")" : com
syntax term : com

syntax "[Com|" com "]" : term

macro_rules
| `([Com| SKIP]) => `(Com.Skip)
| `([Com| $x:strLit := $y ]) => `(Com.Assign $x [AExp| $y])
| `([Com| $x:term := $y ]) => `(Com.Assign $x [AExp| $y])
| `([Com| $x ; $y]) => `(Com.Seq [Com| $x] [Com| $y])
| `([Com| if $b exec $l else $r]) => `(Com.If [BExp| $b] [Com| $l] [Com| $r])
| `([Com| while $b exec $x]) => `(Com.While [BExp| $b] [Com| $x])
| `([Com| ( $x:com )]) => `([Com| $x])
| `([Com| $x:term ]) => `($x)

inductive BigStep : Com → State → State → Prop where
| Skip : BigStep Skip s s
| Assign : BigStep [Com| x := a] s (updateState s x (aval a s))
| Seq (h1 : BigStep c1 s1 s2) (h2 : BigStep c2 s2 s3) : BigStep [Com| c1;c2] s1 s3
| IfTrue (h1 : bval b s1) (h2 : BigStep c1 s1 s2) : BigStep [Com| if b exec c1 else c2] s1 s2
| IfFalse (h1 : ¬bval b s1) (h2 : BigStep c2 s1 s2) : BigStep [Com| if b exec c1 else c2] s1 s2
| WhileFalse (h1 : ¬bval b s) : BigStep [Com| while b exec c] s s
| WhileTrue (h1 : bval b s1) (h2 : BigStep c s1 s2) (h3 : BigStep [Com| while b exec c] s2 s3) : BigStep [Com| while b exec c] s1 s3

notation "(" c "," s ")" "→" t => BigStep c s t

theorem seq_assoc : (([Com| (c1;c2);c3], s) → s') ↔ (([Com| c1;c2;c3], s) → s') := sorry

...one can probably ignore the syntax stuff for the most part, its really about the BigStep inductive and the theorem

[Henrik Böving]

It basically comes down to "Do we have good support for automatic reasoning on inductive predicates"

[Henrik Böving]

inductive Com where
| Skip : Com
| Seq : Com → Com → Com

declare_syntax_cat com

syntax "SKIP" : com
syntax com ";" com : com
syntax "(" com ")" : com
syntax term : com

syntax "[Com|" com "]" : term

macro_rules
| `([Com| SKIP]) => `(Com.Skip)
| `([Com| $x ; $y]) => `(Com.Seq [Com| $x] [Com| $y])
| `([Com| ( $x:com )]) => `([Com| $x])
| `([Com| $x:term ]) => `($x)

inductive BigStep : Com → State → State → Prop where
| Skip : BigStep Skip s s
| Seq (h1 : BigStep c1 s1 s2) (h2 : BigStep c2 s2 s3) : BigStep [Com| c1;c2] s1 s3

notation "(" c "," s ")" "→" t => BigStep c s t

theorem seq_assoc : (([Com| (c1;c2);c3], s) → s') ↔ (([Com| c1;c2;c3], s) → s') := sorry

I guess this one would be more minimal xd

[Henrik Böving]

Hmm...actually removing things did change apparently change stuff so the original proof doesnt work anymore :/

[Mario Carneiro]

The Skip case looks wrong; it appears red in the definition of BigStep because it's actually a variable

[Henrik Böving]

Now it works, it shouldve bee Com.Skip yeah..

[Mario Carneiro]

inductive BigStep : Com → State → State → Prop where
| skip : BigStep Com.Skip s s
| assign : BigStep [Com| x := a] s (updateState s x (aval a s))
| seq (h1 : BigStep c1 s1 s2) (h2 : BigStep c2 s2 s3) : BigStep [Com| c1;c2] s1 s3
| if_true (h1 : bval b s1) (h2 : BigStep c1 s1 s2) : BigStep [Com| if b exec c1 else c2] s1 s2
| if_false (h1 : ¬bval b s1) (h2 : BigStep c2 s1 s2) : BigStep [Com| if b exec c1 else c2] s1 s2
| while_false (h1 : ¬bval b s) : BigStep [Com| while b exec c] s s
| while_true (h1 : bval b s1) (h2 : BigStep c s1 s2) (h3 : BigStep [Com| while b exec c] s2 s3) : BigStep [Com| while b exec c] s1 s3

notation "(" c ", " s ")" " → " t => BigStep c s t

theorem BigStep.seq_assoc : (([Com| (c1;c2);c3], s) → s') ↔ (([Com| c1;c2;c3], s) → s') :=
  ⟨fun | seq (seq h1 h2) h3 => seq h1 (seq h2 h3),
   fun | seq h1 (seq h2 h3) => seq (seq h1 h2) h3⟩

[Henrik Böving]

That does indeed look much better yes...but judging from this the answer to my question seems that we don't really have good automation for constructing these derivation trees automatically, just nice syntax to denote them right?

[Mario Carneiro]

Well, it would be different if you used and / or / eq instead of a custom inductive type

[Henrik Böving]

Yeah I get that...but getting that to work is exactly the point of Isabelle's blast since it's not just a FOL prover but a generic tableau prover.

[Henrik Böving]

Anyways, thanks for all the help and patience!

[Jannis Limperg]

FYI Aesop now solves this (with some appropriately tagged lemmas):

import Aesop

abbrev State := String → Int

inductive Com where
| Skip : Com
| Seq : Com → Com → Com

declare_syntax_cat com

syntax "SKIP" : com
syntax com ";" com : com
syntax "(" com ")" : com
syntax term : com

syntax "[Com|" com "]" : term

macro_rules
| `([Com| SKIP]) => `(Com.Skip)
| `([Com| $x ; $y]) => `(Com.Seq [Com| $x] [Com| $y])
| `([Com| ( $x:com )]) => `([Com| $x])
| `([Com| $x:term ]) => `($x)

@[aesop safe]
inductive BigStep : Com → State → State → Prop where
| Skip : BigStep Com.Skip s s
| Seq (h1 : BigStep c₁ s t) (h2 : BigStep c₂ t u) : BigStep [Com| c₁;c₂] s u

namespace BigStep

@[aesop norm elim]
theorem Seq_inv (h : BigStep [Com| c₁;c₂] s u) :
    ∃ t, BigStep c₁ s t ∧ BigStep c₂ t u :=
  match h with
  | Seq (t := t) h₁ h₂ => ⟨t, h₁, h₂⟩

end BigStep

theorem seq_assoc :
    BigStep [Com| (c1;c2);c3] s s' ↔ BigStep [Com| c1;c2;c3] s s' := by
  aesop

[Henrik Böving]

Yay more concrete semantics for me!