Zulip Chat Archive

Stream: new members

Topic: Product meta program


view this post on Zulip Ken Roe (Jul 29 2018 at 18:48):

Here is a simple meta program to simplify a product expression. It does not seem to match anything. Can someone explain what is happening?

meta def simplifyProd : expr  expr
| (expr.app
    (expr.app
      (expr.app `(prod.fst) tt1a)
      tt1b)
     (expr.app
        (expr.app
          (expr.app
            (expr.app `(prod.mk) tt1) tt2) a) b)) := a
| (expr.app a b) := expr.app (simplifyProd a) (simplifyProd b)
| (expr.lam v b t e) := expr.lam v b (simplifyProd t) (simplifyProd e)
| (expr.pi v b t e) := expr.pi v b (simplifyProd t) (simplifyProd e)
| x := x

theorem testit (f:) (s:) :
    (f,s).fst=f :=
begin
   do {
       t  target,
       trace "Start",
       trace t.to_raw_fmt,
       tq  some (simplifyProd t),
       trace tq.to_raw_fmt,
       change tq
   },
   refl
end

view this post on Zulip Reid Barton (Jul 29 2018 at 19:26):

Well, I don't know, but replacing the first case with | `(prod.fst (prod.mk %%a %%b)) := a works.
Maybe something involving universe variables?

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 19:32):

@Ken Roe Just to let you know that probably nobody is reading the Lean bug reports. The developers are working on Lean 4 and anything that isn't obviously a serious issue in 3.4.1 which needs addressing (e.g. a proof of false) is very likely to be ignored.

view this post on Zulip Ken Roe (Jul 29 2018 at 21:18):

Actually, `(prod.fst (prod.mk %%a %%b)) probably works but I'm trying to avoid quoting. I doing pattern matching that is breaking apart \lambda expressions and I found that %%x inside a lambda lifts the variables (which I would like to avoid). I've also been running into type checking issues. If people are interested, I can post more cases illustrating more issues.

Right now, I'm pretty frustrated. I'm trying to build a separation logic using Lean. Right now, all paths to building the necessary tactics are blocked due to missing documentation or bugs.

view this post on Zulip Patrick Massot (Jul 29 2018 at 21:20):

You should talk to Simon, he knows both tactics and separation logic in Lean

view this post on Zulip Simon Hudon (Jul 29 2018 at 21:25):

If you want, I have started on a separation logic package: https://github.com/unitb/separation-logic. It might be easier to collaborate on it.

view this post on Zulip Simon Hudon (Jul 29 2018 at 21:26):

So far, my tactics can handle a twenty-line proof of the list reversal program: https://github.com/unitb/separation-logic/blob/master/src/separation/examples.lean#L118-L137

view this post on Zulip Ken Roe (Jul 29 2018 at 21:34):

Can someone send me a private message with Simon's contact information? By the way, to illustrate another issue, I just added another case which causes simplifyProd to not compile.

meta def simplifyProd : expr  expr
| (expr.app
    (expr.app
      (expr.app `(prod.fst) tt1a)
      tt1b)
     (expr.app
        (expr.app
          (expr.app
            (expr.app `(prod.mk) tt1) tt2) a) b)) := a
| `((λ x, (%%f) x) (%%z)) := `(%%f (%%z+1))
| (expr.app a b) := expr.app (simplifyProd a) (simplifyProd b)
| (expr.lam v b t e) := expr.lam v b (simplifyProd t) (simplifyProd e)
| (expr.pi v b t e) := expr.pi v b (simplifyProd t) (simplifyProd e)
| x := x

theorem testit (f:) (s:) :
    (f,s).fst=f :=
begin
   do {
       t  target,
       trace "Start",
       trace t.to_raw_fmt,
       tq  some (simplifyProd t),
       trace tq.to_raw_fmt,
       change tq
   },
   refl
end

This case with the lambda gives the following error on the %%f:

function expected at
  _x_1
term has type
  ?m_1

view this post on Zulip Patrick Massot (Jul 29 2018 at 21:35):

you can click on his name, right above your question

view this post on Zulip Patrick Massot (Jul 29 2018 at 21:36):

I mean: right above in this thread

view this post on Zulip Ken Roe (Jul 29 2018 at 21:37):

Never mind on the contact info--I just saw a message from Simon.

I'm more than happy to collaborate on separation logic. I did work on separation logic using Coq for my PhD. You can check out my home page at www.cs.jhu.edu/~roe. I'm working on porting my system to Lean.

view this post on Zulip Simon Hudon (Jul 29 2018 at 21:40):

Cool thanks, that should be helpful. You can have a look at how far I got right here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/subject/Product.20meta.20program/near/130540986

view this post on Zulip Ken Roe (Jul 30 2018 at 18:48):

Actually, an ideal solution would be not to use `(prod.mk). Is there an alternative that I can plug in without changing the surrounding text? I would like to find a way of expression my product meta program without using any back quote annotations. The motivation is that I actually have some more complex meta programs where I'm finding the back quote notation has semantics that is causing a number of problems.

view this post on Zulip Simon Hudon (Jul 30 2018 at 18:57):

Can you show us that other program?

view this post on Zulip Ken Roe (Jul 30 2018 at 21:39):

I'll put it up in a day or two. The code isn't stand alone. It is dependent on the infrastructure in my separation logic framework. I need to put the work into a github repository and then post the critical meta functions.

view this post on Zulip Ken Roe (Aug 06 2018 at 03:52):

I've posted the source code that I have of my separation framework so far here: https://github.com/kendroe/pedantic2. Some of my future questions will point to this repository. I'm porting the Coq implementation. Information on this implementation (and repository link) can be found here: http://www.cs.jhu.edu/~roe.


Last updated: May 07 2021 at 00:30 UTC