From cd8b6ff7b33e2adfb70e4ab67e36249928189459 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Sun, 19 Jul 2026 20:20:42 +0100 Subject: [PATCH 1/3] feat: add support for `match` in `iprop(...)` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a macro expansion, such that in `iprop(match ... with ...)` the right-hand-side of each match alternative is wrapped with `iprop` again. For example, this enables the parsing of the following: ```lean4 iprop(match p with | true => P ∗ Q | false => Q ∗ P) ``` --- Iris/Iris/BI/Notation.lean | 24 ++++++++++++++++++++++-- Iris/Iris/Tests/Notation.lean | 20 +++++++++++++++++++- 2 files changed, 41 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/BI/Notation.lean b/Iris/Iris/BI/Notation.lean index 90bb10fed..b4e76d7db 100644 --- a/Iris/Iris/BI/Notation.lean +++ b/Iris/Iris/BI/Notation.lean @@ -1,16 +1,18 @@ /- Copyright (c) 2022 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König +Authors: Lars König, Alex Keizer -/ module public meta import Lean.PrettyPrinter.Delaborator +meta import Lean.Parser.Term + public meta section namespace Iris.BI -open Lean Lean.Macro +open Lean Lean.Macro Lean.Parser.Term -- define `iprop` embedding in `term` syntax:max "iprop(" term ")" : term @@ -27,6 +29,13 @@ macro_rules | `(iprop(if $c then $t else $e)) => ``(if $c then iprop($t) else iprop($e)) | `(iprop(($P : $t))) => ``((iprop($P) : $t)) | `(iprop(fun $xs* => $P)) => ``(fun $xs* => iprop($P)) + -- `iprop(match …)` expansion wraps the rhs of each match arm in `iprop(…)` + | `(iprop(match $[$g:generalizingParam]? $[$m:motive]? $[$x:matchDiscr],* with + $[$alts:matchAlt]*)) => do + let alts ← alts.mapM <| fun + | `(matchAltExpr| | $[$lhs]|* => $rhs) => `(matchAltExpr| | $[$lhs]|* => iprop($rhs)) + | alt => return ⟨alt⟩ + `(match $[$g:generalizingParam]? $[$m:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) macro:max "iprop(" P:term " : " t:term ")" : term => `((iprop($P) : $t)) @@ -48,5 +57,16 @@ partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m T `(if $c then $t else $e) | `(($P : $t)) => do ``(($(← unpackIprop P) : $t)) | `($t) => `($t:term) + | `(match $[$g:generalizingParam]? $[$mot:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) => do + -- The following type ascriptions look redundant, but, without them, the ``(match ...)` + -- syntax quotation below fails with an error about types containing metavariables. + let g : Option (TSyntax ``generalizingParam) := g + let mot : Option (TSyntax ``motive) := mot + let alts ← Array.mapM (as := alts) (m:=m) <| fun + | `(matchAltExpr| | $[$lhs]|* => $rhs) => do + let rhs ← unpackIprop rhs + `(matchAltExpr| | $[$lhs]|* => $rhs) + | alt => return ⟨alt⟩ + `(match $[$g:generalizingParam]? $[$mot:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) end Iris.BI diff --git a/Iris/Iris/Tests/Notation.lean b/Iris/Iris/Tests/Notation.lean index 9e8d950b7..dbc756381 100644 --- a/Iris/Iris/Tests/Notation.lean +++ b/Iris/Iris/Tests/Notation.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König +Authors: Lars König, Alex Keizer -/ module @@ -113,6 +113,24 @@ variable [BIBase PROP] (P Q R : PROP) (Ψ : Nat → PROP) (Φ : Nat → Nat → /-- info: iprop(□ P) : PROP -/ #guard_msgs in #check iprop((□ P : PROP)) +/-- +info: match p with +| true => Ψ 1 +| false => iprop(False) : PROP +-/ +#guard_msgs in #check iprop(match p with + | true => term(Ψ 1) + | false => False) + +/-- +info: match true with +| true => iprop(P ∗ Q) +| false => iprop(P ∗ Q) : PROP +-/ +#guard_msgs in #check iprop(match (generalizing := false) (motive := Bool → PROP) true with + | true | false => P ∗ Q +) + /-! ## Derived Connectives -/ /-- info: ⊢ P : Prop -/ From edeb27ca942a3a190a7e7997952662c49a838b21 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Tue, 21 Jul 2026 16:07:43 +0100 Subject: [PATCH 2/3] refactor: throw unsupported syntax error on unsupported match --- Iris/Iris/BI/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/Iris/BI/Notation.lean b/Iris/Iris/BI/Notation.lean index b4e76d7db..1dfa01736 100644 --- a/Iris/Iris/BI/Notation.lean +++ b/Iris/Iris/BI/Notation.lean @@ -34,7 +34,7 @@ macro_rules $[$alts:matchAlt]*)) => do let alts ← alts.mapM <| fun | `(matchAltExpr| | $[$lhs]|* => $rhs) => `(matchAltExpr| | $[$lhs]|* => iprop($rhs)) - | alt => return ⟨alt⟩ + | _ => throwUnsupported `(match $[$g:generalizingParam]? $[$m:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) macro:max "iprop(" P:term " : " t:term ")" : term => `((iprop($P) : $t)) From 0d38f619109600b35ad84cd851aeb5e13ca2cfb0 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Tue, 21 Jul 2026 23:35:52 +0100 Subject: [PATCH 3/3] fix: ensure `unpackIprop`'s fallback case is at the bottom; add corresponding test-cases --- Iris/Iris/BI/Notation.lean | 3 ++- Iris/Iris/Tests/Notation.lean | 12 ++++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/Iris/Iris/BI/Notation.lean b/Iris/Iris/BI/Notation.lean index 1dfa01736..4e4f728dd 100644 --- a/Iris/Iris/BI/Notation.lean +++ b/Iris/Iris/BI/Notation.lean @@ -56,7 +56,6 @@ partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m T let e ← unpackIprop e `(if $c then $t else $e) | `(($P : $t)) => do ``(($(← unpackIprop P) : $t)) - | `($t) => `($t:term) | `(match $[$g:generalizingParam]? $[$mot:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) => do -- The following type ascriptions look redundant, but, without them, the ``(match ...)` -- syntax quotation below fails with an error about types containing metavariables. @@ -68,5 +67,7 @@ partial def unpackIprop [Monad m] [MonadRef m] [MonadQuotation m] : Term → m T `(matchAltExpr| | $[$lhs]|* => $rhs) | alt => return ⟨alt⟩ `(match $[$g:generalizingParam]? $[$mot:motive]? $[$x:matchDiscr],* with $[$alts:matchAlt]*) + -- Fallback case + | `($t) => `($t:term) end Iris.BI diff --git a/Iris/Iris/Tests/Notation.lean b/Iris/Iris/Tests/Notation.lean index dbc756381..8fe4bb166 100644 --- a/Iris/Iris/Tests/Notation.lean +++ b/Iris/Iris/Tests/Notation.lean @@ -110,6 +110,8 @@ variable [BIBase PROP] (P Q R : PROP) (Ψ : Nat → PROP) (Φ : Nat → Nat → /-- info: if p = true then iprop(□ P) else P : PROP -/ #guard_msgs in #check iprop(if p then □ P else P) +/-- info: iprop((if p = true then □ P else P) ∗ Q) : PROP -/ +#guard_msgs in #check iprop((if p then □ P else P) ∗ Q) /-- info: iprop(□ P) : PROP -/ #guard_msgs in #check iprop((□ P : PROP)) @@ -122,6 +124,16 @@ info: match p with | true => term(Ψ 1) | false => False) +/-- +info: iprop(□ + match p with + | true => Ψ 1 + | false => False) : PROP +-/ +#guard_msgs in #check iprop(□ match p with + | true => term(Ψ 1) + | false => False) + /-- info: match true with | true => iprop(P ∗ Q)