Zulip Chat Archive

Hello. Is it possible to pattern match against propositions? I.e. a > 1 ∨ b = 3 to extract metavariables and (in)equalities. I'd like to be able to write constraints in a monad a la do a <- get_arg "a", b <- get_arg "b", constrain (a > 1 ∨ b = 3) Let say the output is the ANDs-of-ORs-of-maybe-NOTs, as a string, canonicalized after all constraints have been added. I'd be okay with a partial solution which only recognizes some forms of propositions. Such as freely nested ANDs, ORs, and NOTs. But it needs to reduce higher level code, such as a ∈ [1, 2, 3] to ORs.

If I understand correctly, we can't pattern match directly and would need to use metaprogramming to introduce the metavariables (a and b above) and to decompose the reduced type. But this should be possible. I hope.

SnowFox (Oct 10 2020 at 09:41):

Related. It'd also be nice to be able to write arithmetic constraints too. I.e. 3 * a - 2 * b + 5 * z = 0.

SnowFox (Oct 10 2020 at 09:44):

Hmm.. Could double-quote an expression. Not as nice but certainly easier.

``(3 * `a - 2 * `b + 5 * `z = 0)

Mario Carneiro (Oct 10 2020 at 09:56):

rcases can do lots of interesting pattern matching on props

Mario Carneiro (Oct 10 2020 at 09:57):

That said it doesn't exactly match the use case you describe later, which I don't really understand

Mario Carneiro (Oct 10 2020 at 09:57):

what is get_arg

Mario Carneiro (Oct 10 2020 at 09:58):

Do you have a simple example of what you would like to do?

SnowFox (Oct 10 2020 at 10:41):

@Mario Carneiro I'd like to be able to write both logical and arithmetic constraints as ordinary propositions, to compile them to a canonicalized inductive type which I can process over. Below an example for each variant.

(Logical constraint system) Macaroons are a Hash-based credential constructed as a list of caveats where each caveat is an ORs-of-maybe-NOTs and the list is the AND of these. A naive attenuation may append many redundant caveats and grow the size of the credential quickly. Ideally, the attenuating actor can specify their caveats as propositions, then let a higher level canonicalize the prop to ANDs-of-ORs-of-maybe-NOTs, stripping out redundancies. The result should be zero or more caveats appended to the original set. The optimization must be correct / cannot match differently to the naive approach of just appending all caveats.

Macaroons => https://research.google/pubs/pub41892/

(Arithmetic constraint system) Bulletproofs are zero-knowledge proofs that a set of possibly hidden variables of a rank-1 constraint system satisfy a set of constraints. The cryptography involved is more expensive when there are more gates. Thus the propositions need to be simplified to eliminate redundancies.

Bulletproofs R1CS => https://doc-internal.dalek.rs/bulletproofs/notes/r1cs_proof/index.html

To summarize: I want to write the potentially redundant constraints as propositions, then eliminate the redundancies at a post-processing stage.

Mario Carneiro (Oct 10 2020 at 10:45):

I mean could you produce some code that approximates what you are attempting to do, perhaps with a sorry where you aren't sure what to put something

SnowFox (Oct 10 2020 at 10:49):

Sorry, yes, crude example I wrote for a friend while explaining macaroons. The get_arg results are typed as fn : string and arg1 : nat. This monad style is not necessary, it just seemed like a natural option.

def test : macaroon :=
do fn <- get_arg "fn",
   arg1 <- get_arg "1",
   constrain (fn ∈ ["f", "g", "h"]),
   implies (fn = "f") (arg1 = 1)

SnowFox (Oct 10 2020 at 10:55):

Here implies p q is constrain ((not p) or q).

Mario Carneiro (Oct 10 2020 at 11:35):

so how is macaroon defined?

Mario Carneiro (Oct 10 2020 at 11:36):

this looks doable, but it is not clear to me where "fn", "1" etc are coming from

SnowFox (Oct 10 2020 at 12:22):

Uh. Connection cut and seems my last message was lost.

Consider something like this. A caveat is a list of triples containing the key/name, (in)equality, and a value/string; where at least one must be true. Ideally the caveat should be any semi-lattice; but a string key-value should suffice for now.

inductive caveat :=
(ors : list (name × bool × string))

structure macaroon :=
(caveats : list caveat)
(tag : hmac_digest)

SnowFox (Oct 10 2020 at 12:26):

"fn" and "1" are the keys for the constraints.

SnowFox (Oct 10 2020 at 12:33):

To reiterate; I want to write Props because they are more natural and may not be canonicalized. Whereas the target type is canonically an ANDs-of-ORs-of-maybe-NOTs, or similarly structured when generalized to naturals or integers using less-than or greater-or-equal. Which is still the same thing just more expressive.

SnowFox (Oct 10 2020 at 12:35):

Or generalized further to any semilattice; but that just wouldn't need the caveats.of_prop method and would do its own thing.

SnowFox (Oct 10 2020 at 12:37):

The macaroon tag is computed as the HMAC(previous tag, new caveat) for each caveat appended to the list. The constraint builder would canonicalize and reduce the caveats before committing to them and updating the tag.

SnowFox (Oct 10 2020 at 12:53):

The test above would expand to, with these definitions, lazily treating hmac_digest as nat and arg1 of type string.

def test : macaroon :=
⟨[
    -- `fn ∈ ["f", "g", "h"]
    ⟨[
        (`fn, true, "f"),
        (`fn, true, "g"),
        (`fn, true, "h")
    ]⟩,
    -- `fn = "f" => arg1 = "1"
    ⟨[
        (`fn, false, "f"),
        (`arg1, true, "1")
    ]⟩
 ], 0⟩

Mario Carneiro (Oct 10 2020 at 14:10):

I think the nicest way to get good syntax and parse correctly is to use a tactic wrapper, like this:

import tactic.core

@[derive has_reflect]
structure caveat :=
(ors : list (name × bool × string))

@[derive has_reflect]
structure macaroon :=
(caveats : list caveat)
-- (tag : hmac_digest)

def macaroon.false : macaroon := ⟨[⟨[]⟩]⟩
def macaroon.true : macaroon := ⟨[]⟩
def macaroon.and : macaroon → macaroon → macaroon
| ⟨c₁⟩ ⟨c₂⟩ := ⟨c₁ ++ c₂⟩
def macaroon.or : macaroon → macaroon → macaroon
| ⟨c₁⟩ ⟨c₂⟩ := ⟨do ⟨a⟩ ← c₁, ⟨b⟩ ← c₂, [⟨a ++ b⟩]⟩
def macaroon.sn (n : name) (pos : bool) (s : string) : macaroon :=
⟨[⟨[(n, pos, s)]⟩]⟩

meta instance : has_repr caveat :=
⟨λ ⟨l⟩, string.intercalate " ∨ " $ l.map $ λ ⟨n, pos, s⟩,
  to_string n ++ (if pos then " = " else " ≠ ") ++ s⟩

meta instance : has_repr macaroon :=
⟨λ ⟨m⟩, string.intercalate " ∧\n " ((λ x, "(" ++ repr x ++ ")") <$> m)⟩

open tactic interactive interactive.types

meta def macaroonify_core : expr → bool → tactic macaroon
| e pos := do e ← whnf e transparency.all,
  match e with
  | `(%%e₁ ∧ %%e₂) :=
    (if pos then macaroon.and else macaroon.or)
      <$> macaroonify_core e₁ pos <*> macaroonify_core e₂ pos
  | `(%%e₁ ∨ %%e₂) :=
    (if pos then macaroon.or else macaroon.and)
      <$> macaroonify_core e₁ pos <*> macaroonify_core e₂ pos
  | `(%%e₁ → %%e₂) :=
    (if pos then macaroon.or else macaroon.and)
      <$> macaroonify_core e₁ (bnot pos) <*> macaroonify_core e₂ pos
  | `(false) := return $ if pos then macaroon.false else macaroon.true
  | `(true) := return $ if pos then macaroon.true else macaroon.false
  | `(%%a = %%b) :=
    if a.is_local_constant then do
      pb ← pp b,
      return $ macaroon.sn a.local_pp_name pos (to_string pb)
    else if b.is_local_constant then do
      pa ← pp a,
      return $ macaroon.sn b.local_pp_name pos (to_string pa)
    else failed
  | e := failed
  end

meta def tactic.interactive.macaroonify (p : parse texpr) : tactic unit :=
do e ← to_expr p,
  (args, e) ← open_lambdas e,
  m ← macaroonify_core e tt,
  exact (reflect m)

def foo : macaroon :=
by macaroonify λ fn arg1,
  fn ∈ ["f", "g", "h"] ∧
  (fn = "f" → arg1 = 1)

#eval foo
-- (fn = "f" ∨ fn = "g" ∨ fn = "h") ∧
--  (fn ≠ "f" ∨ arg1 = 1)

SnowFox (Oct 10 2020 at 14:14):

This... looks like exactly what I wanted, thanks. Just no open_lambdas. This intended as a sorry or missing an import?

SnowFox (Oct 10 2020 at 14:22):

Missing import I guess. https://leanprover-community.github.io/mathlib_docs/tactic/binder_matching.html

SnowFox (Oct 10 2020 at 14:24):

Ah, I'm a few weeks too late!

SnowFox (Oct 10 2020 at 14:52):

After updating mathlib, I can confirm it works. Thanks again! Exactly what I was after. :)

SnowFox (Oct 10 2020 at 22:35):

The whnf normalization trick is really pretty. It had me wondering how nots were handled, needed to add a tactic.trace e to see what it presented the match. Elegant. :D

SnowFox (Oct 11 2020 at 04:02):

@Mario Carneiro This produces garbage with inequalities on the LHS of an implication. Any idea how to fix this? I.e. not a = 1 -> b = 2 => (a = 1 or b = 2) and (b = 2).

SnowFox (Oct 11 2020 at 04:07):

(deleted)

Mario Carneiro (Oct 11 2020 at 05:17):

I can't replicate the issue

Mario Carneiro (Oct 11 2020 at 05:18):

but be aware that I changed the code snippet above after you first saw it, because there was a bug in the translation of true and false when in negative mode

SnowFox (Oct 11 2020 at 05:26):

Ah. I didn't notice the update. This fixes the issue. Thanks. :)

SnowFox (Oct 11 2020 at 06:04):

@Mario Carneiro I've generalized it a bit to just Conjunctive Normal Form (instead of specifically macaroons). Added <-> and it now rejects bad inputs with descriptive errors. I.e. these are invalid λ a, a = not a string ∧ b = "b may exist but isn't a valid constraint name". Next step: generalize to linear (in)equalities. For maximization, minimization and validation.

import tactic.core

@[derive has_reflect]
structure cnf :=
(ands_of_ors_of_maybe_nots : list (list (name × bool × string)))

def cnf.false : cnf := ⟨[[]]⟩
def cnf.true : cnf := ⟨[]⟩
def cnf.and : cnf → cnf → cnf
| ⟨c₁⟩ ⟨c₂⟩ := ⟨c₁ ++ c₂⟩
def cnf.or : cnf → cnf → cnf
| ⟨c₁⟩ ⟨c₂⟩ := ⟨do a ← c₁, b ← c₂, [a ++ b]⟩
def cnf.sn (n : name) (pos : bool) (s : string) : cnf :=
⟨[[(n, pos, s)]]⟩

instance : has_repr cnf :=
⟨λ ⟨m⟩, string.intercalate " ∧\n "
  ((λ x : list (name × bool × string),
    "(" ++ (string.intercalate " ∨ " $ x.map $ λ ⟨n, pos, s⟩,
          to_string n ++ (if pos then " = " else " ≠ ") ++ s)
        ++ ")")
    <$> m)⟩

open tactic interactive interactive.types

meta def cnfify_core (args : list expr) : expr → bool → tactic cnf
| e pos := do e ← whnf e transparency.all,
  -- tactic.trace e,
  match e with
  | `(%%e₁ ∧ %%e₂) :=
    (if pos then cnf.and else cnf.or)
      <$> cnfify_core e₁ pos
      <*> cnfify_core e₂ pos
  | `(%%e₁ ∨ %%e₂) :=
    (if pos then cnf.or else cnf.and)
      <$> cnfify_core e₁ pos
      <*> cnfify_core e₂ pos
  | `(%%e₁ → %%e₂) :=
    (if pos then cnf.or else cnf.and)
      <$> cnfify_core e₁ (bnot pos)
      <*> cnfify_core e₂ pos
  | `(%%e₁ ↔ %%e₂) :=
    cnf.and
      <$> ((if pos then cnf.or else cnf.and)
        <$> cnfify_core e₁ (bnot pos)
        <*> cnfify_core e₂ pos)
      <*> ((if pos then cnf.or else cnf.and)
        <$> cnfify_core e₂ (bnot pos)
        <*> cnfify_core e₁ pos)
  | `(false) := return $ if pos then cnf.false else cnf.true
  | `(true) := return $ if pos then cnf.true else cnf.false
  | `(%%a = %%b) :=
    if a ∈ args then
      do ba <- whnf b,
         pb <- pp b,
      if ba.is_app_of `string_imp.mk then
        return $ cnf.sn a.local_pp_name pos (to_string pb)
      else
        fail $ "Expected string; found: " ++ to_string pb
    else
      fail $ "Expected one of: "
        ++ string.intercalate ", " (args.map to_string)
        ++ "; found: " ++ a.local_pp_name.to_string
  | e := fail "Unhandled proposition?"
  end

meta def tactic.interactive.cnfify (p : parse texpr) : tactic unit :=
do e ← to_expr p,
  (args, e) ← open_lambdas e,
  m ← cnfify_core args e tt,
  exact (reflect m)

example := by cnfify λ fn arg1,
  fn ∈ ["f", "g", "h"] ∧
  (fn = "f" → arg1 = "1")

example := by cnfify λ fn target message,
  -- we may send and receive messages
  fn ∈ ["send", "recv"] ∧
  -- if we send a message to alice, the message must be "Hello"
  (fn = "send" ∧ target = "alice" → message = "Hello") ∧
  -- we can only receive messages as bob
  (fn = "recv" → target = "bob")

Mario Carneiro (Oct 11 2020 at 06:09):

I think your translation of <-> isn't correct. When in positive mode p <-> q should translate to (!p \/ q) /\ (!q \/ p), which looks ok, but in negative mode it should translate to (p \/ q) /\ (!p \/ !q), while you are currently translating to (p /\ !q) /\ (q /\ !p)

Mario Carneiro (Oct 11 2020 at 06:10):

The pos argument is supposed to negate the whole proposition when false, so <-> should translate to xor in negative mode

Mario Carneiro (Oct 11 2020 at 06:11):

otherwise it looks good

SnowFox (Oct 11 2020 at 06:12):

Oops, nice catch.

SnowFox (Oct 11 2020 at 06:23):

Hmm. I've adjusted it as follows but this just produces contradictions. a = 1 and b = 2 and a /= 1 and b /= 2

  | `(%%e₁ ↔ %%e₂) :=
    if pos then
      cnf.and
        <$> (cnf.or
          <$> cnfify_core e₁ ff
          <*> cnfify_core e₂ tt)
        <*> (cnf.or
          <$> cnfify_core e₁ ff
          <*> cnfify_core e₂ tt)
    else
      cnf.and
        <$> (cnf.and
          <$> cnfify_core e₁ tt
          <*> cnfify_core e₂ tt)
        <*> (cnf.and
          <$> cnfify_core e₁ ff
          <*> cnfify_core e₂ ff)

SnowFox (Oct 11 2020 at 06:23):

For not (a = "1" <-> b = "2")

SnowFox (Oct 11 2020 at 06:25):

Er duh. cnf.or***

SnowFox (Oct 11 2020 at 06:25):

All good now :)

SnowFox (Oct 11 2020 at 06:33):

Not quite.. fixed for real. :)

  | `(%%e₁ ↔ %%e₂) :=
      cnf.and
        <$> (cnf.or
          <$> cnfify_core e₁ (bnot pos)
          <*> cnfify_core e₂ tt)
        <*> (cnf.or
          <$> cnfify_core e₁ pos
          <*> cnfify_core e₂ ff)

SnowFox (Oct 12 2020 at 02:54):

@Mario Carneiro BTW: It seemed necessary to switch from tactic cnf to tactic expr to support returning arbitrary expressions from the RHS of =. For instance, this now works as expected without returning "to_string 1".

#eval let q := [1, 2, 3].map to_string in by cnfify λ fn, fn ∈ q

Do you have any tips to clean it up? Notably the return `(cnf.sn %%`(a.local_pp_name) %%`(pos) %%b) .

meta def cnfify_core (args : list expr) : expr → bool → tactic expr
| e pos := do
  e ← whnf e transparency.all,
  match e with
  | `(%%e₁ ∧ %%e₂) := do
    a ← cnfify_core e₁ pos,
    b ← cnfify_core e₂ pos,
    return $ if pos then `(cnf.and %%a %%b) else `(cnf.or %%a %%b)
  | `(%%e₁ ∨ %%e₂) := do
    a ← cnfify_core e₁ pos,
    b ← cnfify_core e₂ pos,
    return $ if pos then `(cnf.or %%a %%b) else `(cnf.and %%a %%b)
  | `(%%e₁ → %%e₂) := do
    a ← cnfify_core e₁ (bnot pos),
    b ← cnfify_core e₂ pos,
    return $ if pos then `(cnf.or %%a %%b) else `(cnf.and %%a %%b)
  | `(%%e₁ ↔ %%e₂) := do
    a ← cnfify_core e₁ (bnot pos),
    b ← cnfify_core e₂ tt,
    c ← cnfify_core e₁ pos,
    d ← cnfify_core e₂ ff,
    return $ `(cnf.and (cnf.or %%a %%b) (cnf.or %%c %%d))
  | `(false) := return $ if pos then `(cnf.false) else `(cnf.true)
  | `(true) := return $ if pos then `(cnf.true) else `(cnf.false)
  | `(%%a = %%b) :=
    if a ∈ args then do
      type ← infer_type b,
      if type = `(string) then
        return `(cnf.sn %%`(a.local_pp_name) %%`(pos) %%b)
      else do
        pb <- to_string <$> pp b,
        pt <- to_string <$> pp type,
        fail $ "Expected string; found: " ++ pb ++ " of type " ++ pt
    else
      fail $ "Invalid variable; expected one of: "
        ++ string.intercalate ", " (args.map to_string)
        ++ "; found: " ++ a.local_pp_name.to_string
  | e := fail "Unhandled proposition?"
  end

meta def tactic.interactive.cnfify (p : parse texpr) : tactic unit := do
  (args, e) ← to_expr p >>= open_lambdas,
  cnfify_core args e tt >>= exact

SnowFox (Oct 12 2020 at 02:58):

OOps that should read as

        let n := a.local_pp_name in
        return `(cnf.sn %%`(n) %%`(pos) %%b)

Necessary because a.local_pp_name is meta and I don't want that meta to leak into the result.

SnowFox (Oct 12 2020 at 03:09):

The dynamic handling falls apart if the tactic can't reduce it to the terms it matches; so this fails.

example (l : list string) := by cnfify λ fn, fn ∈ l

But it is really nice that I could just implement this. Adding it to the special cases, but there will likely be more and it could be a bad objective to try to handle everything. More dynamic code should probably construct the CNF itself, without this sugar.

SnowFox (Oct 12 2020 at 05:03):

Hm. Counterexample discovered. cnfify λ a b, (a = "1" -> b = "1") \or (a = "2" -> b = "2") compiles to (a /= "1" or b = "1" or a /= "2" or b = "2") which incorrectly accepts a = "1" and b = 2.

SnowFox (Oct 12 2020 at 05:12):

Actually I'm not sure if it is incorrect... a = "1" and b = "2" does indeed satisfy the right implication.

SnowFox (Oct 12 2020 at 05:12):

Just a weird concept to think of, heh.

Mario Carneiro (Oct 12 2020 at 05:34):

@SnowFox I sort of dodged the question of how you want to represent the RHS of the CNF equalities. All your examples so far have been integers or strings, so if that is sufficient you can evaluate the expression at the appropriate type, which would allow running arbitrary string returning functions like to_string 1

SnowFox (Oct 12 2020 at 05:38):

My current code with a few working as intended examples. These do run the arbitrary code. Just nothing "too dynamic" as demonstrated above where we can't reduce around an unknown list; but we can reduce around promised terms so long that their eventual result has type string. https://gist.github.com/1fe4300d59a830320f603ab3f5a9a0b6

SnowFox (Oct 12 2020 at 05:41):

I'm not sure what you mean by evaluating the expression at the appropriate type? Do you mean the tactic cnf variant could evaluate the expression to produce its string in its result?

SnowFox (Oct 12 2020 at 05:43):

If so, then I don't think that'd cover the first two examples in this file. Which both work as intended with the tactic expr variant.

example (s : string) := by cnfify λ fn arg1,
  fn ∈ ["f", "g", s] ∧
  (fn = "f" → arg1 = "1")

example (n : nat) := let q := [1, n, 3].map to_string in by cnfify λ fn, fn ∈ q

Mario Carneiro (Oct 12 2020 at 05:47):

If you stick this in the variable case:

        if type = `(string) then do
          let n := a.local_pp_name,
          s ← (do s ← eval_expr' string b, return (reflect s : expr)) <|> return b,
          return `(cnf.new %%(reflect n) %%(reflect pos) %%s)

it works here

def F (n : nat) := by cnfify λ fn, fn ∈ [1, n, 3].map to_string
#print F
-- def F : ℕ → cnf :=
-- λ (n : ℕ),
--   (cnf.new (name.mk_string "fn" name.anonymous) tt "1").or
--     ((cnf.new (name.mk_string "fn" name.anonymous) tt (to_string n)).or
--        ((cnf.new (name.mk_string "fn" name.anonymous) tt "3").or cnf.false))

Mario Carneiro (Oct 12 2020 at 05:49):

It's kind of a hack, but here we are either evaluating the string or sticking the expression inline

SnowFox (Oct 12 2020 at 05:56):

Right, but if I understand correctly this wouldn't work in the tactic cnf case due to the return b part. It'd only work when the expression can be reduced to a string. Thus little benefit to adding this tweak to my current code. The hack might be useful to reduce computation at runtime if the virtual machine doesn't hold onto a partially reduced program.

SnowFox (Oct 12 2020 at 06:00):

Thanks for the eval_expr' tip, I was looking for this earlier but didn't find it.

Mario Carneiro (Oct 12 2020 at 06:05):

That's about right. It falls back to the behavior that you originally wrote, so it's really just a fancy inliner

SnowFox (Oct 12 2020 at 06:06):

Where are these magical constants defined? In the C++? tactic.eval_expr``tactic.whnf et al.

SnowFox (Oct 12 2020 at 06:06):

Fancy inliner, yes. Unnecessary here but certainly useful for other uses.

Mario Carneiro (Oct 12 2020 at 06:06):

eval_expr and whnf are in core, init.meta.tactic

Mario Carneiro (Oct 12 2020 at 06:07):

if you have vscode you should be able to ctrl-click on definitions to go to the source

Mario Carneiro (Oct 12 2020 at 06:07):

eval_expr' is a mathlib patch of eval_expr because it has a bug

SnowFox (Oct 12 2020 at 06:08):

I mean, I did exactly that and they are just constant, not code. Yet we use them as code. Are they defined in the C++ or are they just ordinary constants being reduced by other code?