## Stream: Is there code for X?

### Topic: pattern matching prop?

#### SnowFox (Oct 10 2020 at 09:24):

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.

(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).

(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***

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):

        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_exprtactic.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?

they are in C++

Okay.

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

https://github.com/leanprover-community/lean/blob/master/src/library/tactic/eval.cpp

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

the DECLARE_VM_BUILTIN at the bottom is what hooks the big eval() function to the lean constant

#### SnowFox (Oct 12 2020 at 06:11):

Speaking of the C++.. is there an ETA for Lean 4? ;)

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

heh, don't ask me, I'm just the rumor mill

:)

#### SnowFox (Oct 12 2020 at 06:20):

@Mario Carneiro I don't mean to push but I'm not sure how the pings work on zulip. I've pinged you in the RISC-V ISA thread. https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification/topic/RISC-V.20ISA.20in.20Lean/near/213000987

#### Johan Commelin (Oct 12 2020 at 06:20):

Pings are cheap. I use 100 pings per day (-;

so you have

#### SnowFox (Oct 12 2020 at 06:21):

@Johan Commelin Do they raise any indication that you've been ping'd?

@SnowFox yup

#### Johan Commelin (Oct 12 2020 at 06:23):

You can see them in the menu under Mentions

#### Johan Commelin (Oct 12 2020 at 06:23):

And the message get's a red background

#### SnowFox (Oct 12 2020 at 06:26):

Thanks. I've noticed the red but didn't notice the mentions... Actually, not sure it even lit up before I switched back here.

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

it only lights up if you have unread mentions

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

but you can click on mentions and see them all

Last updated: May 19 2021 at 02:10 UTC