From 6f30322577c200006aaedc583700cc0138e32c3a Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Mon, 2 Mar 2026 13:14:25 +0100 Subject: [PATCH 1/7] First attempt --- src/Iris.lean | 16 +++--- src/Iris/Algebra.lean | 32 ++++++------ src/Iris/Algebra/Agree.lean | 7 ++- src/Iris/Algebra/Auth.lean | 8 ++- src/Iris/Algebra/CMRA.lean | 6 ++- src/Iris/Algebra/COFESolver.lean | 6 ++- src/Iris/Algebra/DFrac.lean | 13 +++-- src/Iris/Algebra/Excl.lean | 5 +- src/Iris/Algebra/Frac.lean | 7 ++- src/Iris/Algebra/GenMap.lean | 10 ++-- src/Iris/Algebra/Heap.lean | 11 +++-- src/Iris/Algebra/HeapView.lean | 12 +++-- src/Iris/Algebra/IProp.lean | 15 +++--- src/Iris/Algebra/LocalUpdates.lean | 6 ++- src/Iris/Algebra/Numbers.lean | 9 ++-- src/Iris/Algebra/OFE.lean | 3 ++ src/Iris/Algebra/UPred.lean | 7 ++- src/Iris/Algebra/Updates.lean | 6 ++- src/Iris/Algebra/View.lean | 18 ++++--- src/Iris/BI.lean | 18 ++++--- src/Iris/BI/BI.lean | 8 ++- src/Iris/BI/BIBase.lean | 14 ++++-- src/Iris/BI/Classes.lean | 6 ++- src/Iris/BI/DerivedLaws.lean | 16 +++--- src/Iris/BI/DerivedLawsLater.lean | 18 ++++--- src/Iris/BI/Extensions.lean | 8 ++- src/Iris/BI/Instances.lean | 14 ++++-- src/Iris/BI/Lib/BUpdPlain.lean | 18 ++++--- src/Iris/BI/Lib/Fixpoint.lean | 7 ++- src/Iris/BI/Notation.lean | 6 ++- src/Iris/BI/Plainly.lean | 11 +++-- src/Iris/BI/Updates.lean | 15 +++--- src/Iris/Examples.lean | 4 +- src/Iris/Examples/IProp.lean | 14 ++++-- src/Iris/Examples/Proofs.lean | 8 ++- src/Iris/Examples/Resources.lean | 14 ++++-- src/Iris/Instances.lean | 6 ++- src/Iris/Instances/Classical.lean | 6 ++- src/Iris/Instances/Classical/Instance.lean | 10 ++-- src/Iris/Instances/Classical/Notation.lean | 6 ++- src/Iris/Instances/Data.lean | 6 ++- src/Iris/Instances/Data/SetNotation.lean | 3 ++ src/Iris/Instances/Data/State.lean | 6 ++- src/Iris/Instances/IProp.lean | 4 +- src/Iris/Instances/IProp/Instance.lean | 9 ++-- src/Iris/Instances/UPred.lean | 4 +- src/Iris/Instances/UPred/Instance.lean | 15 +++--- src/Iris/ProofMode.lean | 26 +++++----- src/Iris/ProofMode/Classes.lean | 10 ++-- src/Iris/ProofMode/ClassesMake.lean | 8 ++- src/Iris/ProofMode/Display.lean | 10 ++-- src/Iris/ProofMode/Expr.lean | 49 ++++++++++--------- src/Iris/ProofMode/Instances.lean | 12 +++-- src/Iris/ProofMode/InstancesLater.lean | 14 ++++-- src/Iris/ProofMode/InstancesMake.lean | 8 ++- src/Iris/ProofMode/InstancesPlainly.lean | 12 +++-- src/Iris/ProofMode/InstancesUpdates.lean | 10 ++-- src/Iris/ProofMode/Modalities.lean | 6 ++- src/Iris/ProofMode/ModalityInstances.lean | 12 +++-- src/Iris/ProofMode/Patterns.lean | 10 ++-- src/Iris/ProofMode/Patterns/CasesPattern.lean | 6 ++- src/Iris/ProofMode/Patterns/IntroPattern.lean | 6 ++- .../ProofMode/Patterns/ProofModeTerm.lean | 6 ++- src/Iris/ProofMode/Patterns/SpecPattern.lean | 4 ++ src/Iris/ProofMode/ProofModeM.lean | 8 ++- src/Iris/ProofMode/SynthInstance.lean | 14 ++++-- src/Iris/ProofMode/Tactics.lean | 36 +++++++------- src/Iris/ProofMode/Tactics/Apply.lean | 12 +++-- src/Iris/ProofMode/Tactics/Assumption.lean | 6 ++- src/Iris/ProofMode/Tactics/Basic.lean | 12 +++-- src/Iris/ProofMode/Tactics/Cases.lean | 40 ++++++++------- src/Iris/ProofMode/Tactics/Clear.lean | 10 ++-- src/Iris/ProofMode/Tactics/ExFalso.lean | 8 ++- src/Iris/ProofMode/Tactics/Exact.lean | 8 ++- src/Iris/ProofMode/Tactics/Exists.lean | 8 ++- src/Iris/ProofMode/Tactics/Have.lean | 12 +++-- src/Iris/ProofMode/Tactics/HaveCore.lean | 14 ++++-- src/Iris/ProofMode/Tactics/Intro.lean | 22 +++++---- src/Iris/ProofMode/Tactics/LeftRight.lean | 10 ++-- src/Iris/ProofMode/Tactics/Mod.lean | 8 ++- src/Iris/ProofMode/Tactics/ModIntro.lean | 30 +++++++----- src/Iris/ProofMode/Tactics/Pure.lean | 16 +++--- src/Iris/ProofMode/Tactics/Rename.lean | 6 ++- src/Iris/ProofMode/Tactics/Specialize.lean | 22 +++++---- src/Iris/ProofMode/Tactics/Split.lean | 10 ++-- src/Iris/ProofMode/UnifHints.lean | 6 ++- src/Iris/Std.lean | 24 ++++----- src/Iris/Std/BigOp.lean | 3 ++ src/Iris/Std/Classes.lean | 4 ++ src/Iris/Std/DelabRule.lean | 13 +++-- src/Iris/Std/Equivalence.lean | 3 ++ src/Iris/Std/Expr.lean | 8 ++- src/Iris/Std/HeapInstances.lean | 11 +++-- src/Iris/Std/Infinite.lean | 3 ++ src/Iris/Std/Nat.lean | 4 ++ src/Iris/Std/PartialMap.lean | 3 +- src/Iris/Std/Prod.lean | 4 ++ src/Iris/Std/Qq.lean | 6 ++- src/Iris/Std/Rewrite.lean | 10 ++-- src/Iris/Std/Set.lean | 2 + src/Iris/Std/TC.lean | 4 ++ src/Iris/Std/Tactic.lean | 8 ++- src/Iris/Std/Try.lean | 3 ++ src/Iris/Tests.lean | 8 +-- src/Iris/Tests/Instances.lean | 8 ++- src/Iris/Tests/Notation.lean | 6 ++- src/Iris/Tests/Tactics.lean | 8 ++- 107 files changed, 759 insertions(+), 382 deletions(-) diff --git a/src/Iris.lean b/src/Iris.lean index 2bd468667..96f2ce5c3 100644 --- a/src/Iris.lean +++ b/src/Iris.lean @@ -1,7 +1,9 @@ -import Iris.Algebra -import Iris.BI -import Iris.Examples -import Iris.Instances -import Iris.ProofMode -import Iris.Std -import Iris.Tests +module + +public import Iris.Algebra +public import Iris.BI +public import Iris.Examples +public import Iris.Instances +public import Iris.ProofMode +public import Iris.Std +public import Iris.Tests diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean index 30043dc56..3ad44600b 100644 --- a/src/Iris/Algebra.lean +++ b/src/Iris/Algebra.lean @@ -1,15 +1,17 @@ -import Iris.Algebra.Agree -import Iris.Algebra.CMRA -import Iris.Algebra.COFESolver -import Iris.Algebra.DFrac -import Iris.Algebra.Excl -import Iris.Algebra.Frac -import Iris.Algebra.GenMap -import Iris.Algebra.LocalUpdates -import Iris.Algebra.IProp -import Iris.Algebra.OFE -import Iris.Algebra.Updates -import Iris.Algebra.UPred -import Iris.Algebra.Heap -import Iris.Algebra.View -import Iris.Algebra.HeapView +module + +public import Iris.Algebra.Agree +public import Iris.Algebra.CMRA +public import Iris.Algebra.COFESolver +public import Iris.Algebra.DFrac +public import Iris.Algebra.Excl +public import Iris.Algebra.Frac +public import Iris.Algebra.GenMap +public import Iris.Algebra.LocalUpdates +public import Iris.Algebra.IProp +public import Iris.Algebra.OFE +public import Iris.Algebra.Updates +public import Iris.Algebra.UPred +public import Iris.Algebra.Heap +public import Iris.Algebra.View +public import Iris.Algebra.HeapView diff --git a/src/Iris/Algebra/Agree.lean b/src/Iris/Algebra/Agree.lean index 5d22ba2e2..d765dde22 100644 --- a/src/Iris/Algebra/Agree.lean +++ b/src/Iris/Algebra/Agree.lean @@ -3,9 +3,12 @@ Copyright (c) 2025 Leo Stefanesco. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leo Stefanesco, Puming Liu -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/Auth.lean b/src/Iris/Algebra/Auth.lean index 899a32c4c..e0a230a1b 100644 --- a/src/Iris/Algebra/Auth.lean +++ b/src/Iris/Algebra/Auth.lean @@ -3,8 +3,10 @@ Copyright (c) 2025 Alexander Bai. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Alexander Bai -/ -import Iris.Algebra.View -import Iris.Algebra.LocalUpdates +module + +public import Iris.Algebra.View +public import Iris.Algebra.LocalUpdates /-! # Authoritative Camera @@ -14,6 +16,8 @@ The authoritative camera has 2 types of elements: - and the fragment `◯ b` -/ +@[expose] public section + open Iris open OFE CMRA UCMRA View diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean index f81f9b54d..cd763fa6b 100644 --- a/src/Iris/Algebra/CMRA.lean +++ b/src/Iris/Algebra/CMRA.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Сухарик (@suhr), Markus de Medeiros, Puming Liu -/ -import Iris.Algebra.OFE +module + +public import Iris.Algebra.OFE + +@[expose] public section namespace Iris open OFE diff --git a/src/Iris/Algebra/COFESolver.lean b/src/Iris/Algebra/COFESolver.lean index 9e9cacf30..9a84d8f57 100644 --- a/src/Iris/Algebra/COFESolver.lean +++ b/src/Iris/Algebra/COFESolver.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Iris.Algebra.OFE +module + +public import Iris.Algebra.OFE + +@[expose] public section namespace Iris.COFE.OFunctor open OFE diff --git a/src/Iris/Algebra/DFrac.lean b/src/Iris/Algebra/DFrac.lean index 44cb62ddc..002336a38 100644 --- a/src/Iris/Algebra/DFrac.lean +++ b/src/Iris/Algebra/DFrac.lean @@ -3,12 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Mario Carneiro -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE -import Iris.Algebra.Frac -import Iris.Algebra.Updates -import Iris.Algebra.LocalUpdates +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE +public import Iris.Algebra.Frac +public import Iris.Algebra.Updates +public import Iris.Algebra.LocalUpdates + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/Excl.lean b/src/Iris/Algebra/Excl.lean index 5d11e3ca9..b5def0463 100644 --- a/src/Iris/Algebra/Excl.lean +++ b/src/Iris/Algebra/Excl.lean @@ -3,8 +3,11 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Soeser, Mario Carneiro -/ +module -import Iris.Algebra.CMRA +public import Iris.Algebra.CMRA + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/Frac.lean b/src/Iris/Algebra/Frac.lean index 3f94d9058..1e640c368 100644 --- a/src/Iris/Algebra/Frac.lean +++ b/src/Iris/Algebra/Frac.lean @@ -3,9 +3,10 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Shreyas Srinivas, Mario Carneiro -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE /-! # The Frac CMRA @@ -14,6 +15,8 @@ This CMRA captures the notion of fractional ownership of another resource. Traditionally the underlying set is assumed to be the half open interval $$(0,1]$$. -/ +@[expose] public section + namespace Iris class Fraction (α : Type _) extends Add α where diff --git a/src/Iris/Algebra/GenMap.lean b/src/Iris/Algebra/GenMap.lean index b375256d6..49654aca7 100644 --- a/src/Iris/Algebra/GenMap.lean +++ b/src/Iris/Algebra/GenMap.lean @@ -3,9 +3,13 @@ Copyright (c) 2025 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ -import Iris.Algebra.OFE -import Iris.Algebra.CMRA -import Iris.Algebra.Updates +module + +public import Iris.Algebra.OFE +public import Iris.Algebra.CMRA +public import Iris.Algebra.Updates + +@[expose] public section namespace Iris open OFE diff --git a/src/Iris/Algebra/Heap.lean b/src/Iris/Algebra/Heap.lean index 9925dff95..7f0c272cf 100644 --- a/src/Iris/Algebra/Heap.lean +++ b/src/Iris/Algebra/Heap.lean @@ -3,11 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Puming Liu -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE -import Iris.Std.Set -import Iris.Std.PartialMap +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE +public import Iris.Std.Set +public import Iris.Std.PartialMap + +@[expose] public section open Iris Std diff --git a/src/Iris/Algebra/HeapView.lean b/src/Iris/Algebra/HeapView.lean index 988e3d31f..a5c877bae 100644 --- a/src/Iris/Algebra/HeapView.lean +++ b/src/Iris/Algebra/HeapView.lean @@ -3,10 +3,12 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Puming Liu -/ -import Iris.Algebra.Heap -import Iris.Algebra.View -import Iris.Algebra.DFrac -import Iris.Algebra.Frac +module + +public import Iris.Algebra.Heap +public import Iris.Algebra.View +public import Iris.Algebra.DFrac +public import Iris.Algebra.Frac /-! # Heap Views @@ -28,6 +30,8 @@ It provides authoritative and fragmental ownership over heap elements with fract * `HeapView.update_replace`: Replacement update lemma -/ +@[expose] public section + open Iris section heapView diff --git a/src/Iris/Algebra/IProp.lean b/src/Iris/Algebra/IProp.lean index 743ded04b..2b3afa62e 100644 --- a/src/Iris/Algebra/IProp.lean +++ b/src/Iris/Algebra/IProp.lean @@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE -import Iris.Algebra.UPred -import Iris.Algebra.GenMap -import Iris.Algebra.COFESolver -import Init.Data.Vector +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE +public import Iris.Algebra.UPred +public import Iris.Algebra.GenMap +public import Iris.Algebra.COFESolver +public import Init.Data.Vector + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/LocalUpdates.lean b/src/Iris/Algebra/LocalUpdates.lean index 346b6ef6c..1888c892c 100644 --- a/src/Iris/Algebra/LocalUpdates.lean +++ b/src/Iris/Algebra/LocalUpdates.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Сухарик. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Сухарик (@suhr), Mario Carneiro -/ -import Iris.Algebra.CMRA +module + +public import Iris.Algebra.CMRA + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/Numbers.lean b/src/Iris/Algebra/Numbers.lean index 2682cc91f..0225d1a8b 100644 --- a/src/Iris/Algebra/Numbers.lean +++ b/src/Iris/Algebra/Numbers.lean @@ -3,10 +3,11 @@ Copyright (c) 2025 Shreyas Srinivas. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Shreyas Srinivas, Markus de Medeiros -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE -import Iris.Algebra.LocalUpdates +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE +public import Iris.Algebra.LocalUpdates /-! ## Numbers CMRA Simple CMRA's for commutative monoids. @@ -17,6 +18,8 @@ There are three variants: - "No core": there is no core (eg. (PNat, +)) -/ +@[expose] public section + open Std class IdentityFree (α : Type _) [Add α] where diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean index 95af9ff26..f94debd39 100644 --- a/src/Iris/Algebra/OFE.lean +++ b/src/Iris/Algebra/OFE.lean @@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/UPred.lean b/src/Iris/Algebra/UPred.lean index 6890ff206..806e9b599 100644 --- a/src/Iris/Algebra/UPred.lean +++ b/src/Iris/Algebra/UPred.lean @@ -3,9 +3,12 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module -import Iris.Algebra.CMRA -import Iris.Algebra.OFE +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE + +@[expose] public section namespace Iris open CMRA diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean index b506f62e7..688b6622c 100644 --- a/src/Iris/Algebra/Updates.lean +++ b/src/Iris/Algebra/Updates.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Сухарик. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Сухарик (@suhr) -/ -import Iris.Algebra.CMRA +module + +public import Iris.Algebra.CMRA + +@[expose] public section namespace Iris diff --git a/src/Iris/Algebra/View.lean b/src/Iris/Algebra/View.lean index 37a879c88..ee563a2e3 100644 --- a/src/Iris/Algebra/View.lean +++ b/src/Iris/Algebra/View.lean @@ -3,13 +3,17 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Puming Liu -/ -import Iris.Algebra.CMRA -import Iris.Algebra.OFE -import Iris.Algebra.Frac -import Iris.Algebra.DFrac -import Iris.Algebra.Agree -import Iris.Algebra.Updates -import Iris.Algebra.LocalUpdates +module + +public import Iris.Algebra.CMRA +public import Iris.Algebra.OFE +public import Iris.Algebra.Frac +public import Iris.Algebra.DFrac +public import Iris.Algebra.Agree +public import Iris.Algebra.Updates +public import Iris.Algebra.LocalUpdates + +@[expose] public section open Iris diff --git a/src/Iris/BI.lean b/src/Iris/BI.lean index 3bea992cc..89a666f0d 100644 --- a/src/Iris/BI.lean +++ b/src/Iris/BI.lean @@ -1,8 +1,10 @@ -import Iris.BI.Classes -import Iris.BI.DerivedLaws -import Iris.BI.DerivedLawsLater -import Iris.BI.Extensions -import Iris.BI.Instances -import Iris.BI.BI -import Iris.BI.Notation -import Iris.BI.Updates +module + +public import Iris.BI.Classes +public import Iris.BI.DerivedLaws +public import Iris.BI.DerivedLawsLater +public import Iris.BI.Extensions +public import Iris.BI.Instances +public import Iris.BI.BI +public import Iris.BI.Notation +public import Iris.BI.Updates diff --git a/src/Iris/BI/BI.lean b/src/Iris/BI/BI.lean index 0f91953fc..7feb1184d 100644 --- a/src/Iris/BI/BI.lean +++ b/src/Iris/BI/BI.lean @@ -3,8 +3,12 @@ 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, Mario Carneiro -/ -import Iris.Algebra.OFE -import Iris.BI.BIBase +module + +public import Iris.Algebra.OFE +public import Iris.BI.BIBase + +@[expose] public section namespace Iris open Iris.Std OFE diff --git a/src/Iris/BI/BIBase.lean b/src/Iris/BI/BIBase.lean index 8a98aa3f0..85d118556 100644 --- a/src/Iris/BI/BIBase.lean +++ b/src/Iris/BI/BIBase.lean @@ -3,11 +3,15 @@ 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, Mario Carneiro -/ -import Iris.BI.Notation -import Iris.Std.Classes -import Iris.Std.DelabRule -import Iris.Std.Rewrite -import Iris.Std.BigOp +module + +public meta import Iris.BI.Notation +public import Iris.Std.Classes +public meta import Iris.Std.DelabRule +public meta import Iris.Std.Rewrite +public import Iris.Std.BigOp + +@[expose] public section namespace Iris.BI open Iris.Std diff --git a/src/Iris/BI/Classes.lean b/src/Iris/BI/Classes.lean index 5d645601b..a41627fbb 100644 --- a/src/Iris/BI/Classes.lean +++ b/src/Iris/BI/Classes.lean @@ -3,7 +3,11 @@ 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, Mario Carneiro -/ -import Iris.BI.BI +module + +public import Iris.BI.BI + +@[expose] public section namespace Iris.BI diff --git a/src/Iris/BI/DerivedLaws.lean b/src/Iris/BI/DerivedLaws.lean index 289aad33c..3f85c92af 100644 --- a/src/Iris/BI/DerivedLaws.lean +++ b/src/Iris/BI/DerivedLaws.lean @@ -3,12 +3,16 @@ 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, Mario Carneiro, Markus de Medeiros, Michael Sammler -/ -import Iris.BI.Classes -import Iris.BI.Extensions -import Iris.BI.BI -import Iris.Std.Classes -import Iris.Std.Rewrite -import Iris.Std.TC +module + +public import Iris.BI.Classes +public import Iris.BI.Extensions +public import Iris.BI.BI +public import Iris.Std.Classes +public import Iris.Std.Rewrite +public import Iris.Std.TC + +@[expose] public section namespace Iris.BI open Iris.Std BI diff --git a/src/Iris/BI/DerivedLawsLater.lean b/src/Iris/BI/DerivedLawsLater.lean index e5e6528d6..e2acf9060 100644 --- a/src/Iris/BI/DerivedLawsLater.lean +++ b/src/Iris/BI/DerivedLawsLater.lean @@ -3,13 +3,17 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI.Classes -import Iris.BI.Extensions -import Iris.BI.BI -import Iris.BI.DerivedLaws -import Iris.Std.Classes -import Iris.Std.Rewrite -import Iris.Std.TC +module + +public import Iris.BI.Classes +public import Iris.BI.Extensions +public import Iris.BI.BI +public import Iris.BI.DerivedLaws +public import Iris.Std.Classes +public import Iris.Std.Rewrite +public import Iris.Std.TC + +@[expose] public section namespace Iris.BI open Iris.Std BI diff --git a/src/Iris/BI/Extensions.lean b/src/Iris/BI/Extensions.lean index b78e5186a..97d34564d 100644 --- a/src/Iris/BI/Extensions.lean +++ b/src/Iris/BI/Extensions.lean @@ -3,8 +3,12 @@ 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 -/ -import Iris.BI.Classes -import Iris.BI.BI +module + +public import Iris.BI.Classes +public import Iris.BI.BI + +@[expose] public section namespace Iris.BI diff --git a/src/Iris/BI/Instances.lean b/src/Iris/BI/Instances.lean index 37e3c0620..74e7cde7d 100644 --- a/src/Iris/BI/Instances.lean +++ b/src/Iris/BI/Instances.lean @@ -3,11 +3,15 @@ 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, Mario Carneiro -/ -import Iris.BI.Classes -import Iris.BI.DerivedLaws -import Iris.BI.Extensions -import Iris.BI.BI -import Iris.Std.Classes +module + +public import Iris.BI.Classes +public import Iris.BI.DerivedLaws +public import Iris.BI.Extensions +public import Iris.BI.BI +public import Iris.Std.Classes + +@[expose] public section namespace Iris.BI open Iris.Std diff --git a/src/Iris/BI/Lib/BUpdPlain.lean b/src/Iris/BI/Lib/BUpdPlain.lean index d54ad1737..ad34ccb60 100644 --- a/src/Iris/BI/Lib/BUpdPlain.lean +++ b/src/Iris/BI/Lib/BUpdPlain.lean @@ -1,10 +1,14 @@ -import Iris.Std -import Iris.BI -import Iris.Algebra.Updates -import Iris.ProofMode.Classes -import Iris.ProofMode.Tactics -import Iris.ProofMode.Display -import Iris.ProofMode.InstancesUpdates +module + +public import Iris.Std +public import Iris.BI +public import Iris.Algebra.Updates +public import Iris.ProofMode.Classes +public import Iris.ProofMode.Tactics +public import Iris.ProofMode.Display +public import Iris.ProofMode.InstancesUpdates + +@[expose] public section namespace Iris open Iris.Std BI diff --git a/src/Iris/BI/Lib/Fixpoint.lean b/src/Iris/BI/Lib/Fixpoint.lean index 42eb56cc9..eb78350c4 100644 --- a/src/Iris/BI/Lib/Fixpoint.lean +++ b/src/Iris/BI/Lib/Fixpoint.lean @@ -3,9 +3,12 @@ Copyright (c) 2026 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module -import Iris.BI -import Iris.ProofMode +public import Iris.BI +public import Iris.ProofMode + +@[expose] public section namespace Iris open Iris.Std BI OFE diff --git a/src/Iris/BI/Notation.lean b/src/Iris/BI/Notation.lean index 825a36c06..177fc7516 100644 --- a/src/Iris/BI/Notation.lean +++ b/src/Iris/BI/Notation.lean @@ -3,7 +3,11 @@ 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 -/ -import Lean.PrettyPrinter.Delaborator +module + +public meta import Lean.PrettyPrinter.Delaborator + +public meta section namespace Iris.BI open Lean Lean.Macro diff --git a/src/Iris/BI/Plainly.lean b/src/Iris/BI/Plainly.lean index c8b49fb4f..f4020b475 100644 --- a/src/Iris/BI/Plainly.lean +++ b/src/Iris/BI/Plainly.lean @@ -3,11 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module -import Iris.BI.Classes -import Iris.BI.BI -import Iris.BI.DerivedLaws -import Iris.Algebra +public import Iris.BI.Classes +public import Iris.BI.BI +public import Iris.BI.DerivedLaws +public import Iris.Algebra + +@[expose] public section namespace Iris open BI diff --git a/src/Iris/BI/Updates.lean b/src/Iris/BI/Updates.lean index bb78296b1..5a595a539 100644 --- a/src/Iris/BI/Updates.lean +++ b/src/Iris/BI/Updates.lean @@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module -import Iris.BI.BI -import Iris.BI.BIBase -import Iris.BI.Classes -import Iris.BI.DerivedLaws -import Iris.Algebra -import Iris.BI.Plainly +public import Iris.BI.BI +public import Iris.BI.BIBase +public import Iris.BI.Classes +public import Iris.BI.DerivedLaws +public import Iris.Algebra +public import Iris.BI.Plainly + +@[expose] public section namespace Iris open Iris.Std BI diff --git a/src/Iris/Examples.lean b/src/Iris/Examples.lean index a831b63e6..1c5929295 100644 --- a/src/Iris/Examples.lean +++ b/src/Iris/Examples.lean @@ -1 +1,3 @@ -import Iris.Examples.Proofs +module + +public import Iris.Examples.Proofs diff --git a/src/Iris/Examples/IProp.lean b/src/Iris/Examples/IProp.lean index 93bce0df6..b4f4b5054 100644 --- a/src/Iris/Examples/IProp.lean +++ b/src/Iris/Examples/IProp.lean @@ -3,11 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ -import Iris.BI -import Iris.ProofMode -import Iris.Instances.IProp -import Iris.Algebra -import Iris.Std.HeapInstances +module + +public import Iris.BI +public import Iris.ProofMode +public import Iris.Instances.IProp +public import Iris.Algebra +public import Iris.Std.HeapInstances + +@[expose] public section namespace Iris.Examples open Iris.BI COFE diff --git a/src/Iris/Examples/Proofs.lean b/src/Iris/Examples/Proofs.lean index e742de19d..cdada7968 100644 --- a/src/Iris/Examples/Proofs.lean +++ b/src/Iris/Examples/Proofs.lean @@ -3,8 +3,12 @@ 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 -/ -import Iris.BI -import Iris.ProofMode +module + +public import Iris.BI +public import Iris.ProofMode + +@[expose] public section namespace Iris.Examples open Iris.BI diff --git a/src/Iris/Examples/Resources.lean b/src/Iris/Examples/Resources.lean index b771fb97d..2973a9696 100644 --- a/src/Iris/Examples/Resources.lean +++ b/src/Iris/Examples/Resources.lean @@ -3,11 +3,15 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ -import Iris.ProofMode -import Iris.Algebra.IProp -import Iris.Instances.UPred.Instance -import Iris.Instances.IProp.Instance -import Iris.Algebra.Agree +module + +public import Iris.ProofMode +public import Iris.Algebra.IProp +public import Iris.Instances.UPred.Instance +public import Iris.Instances.IProp.Instance +public import Iris.Algebra.Agree + +@[expose] public section namespace Iris.Examples open Iris.BI COFE diff --git a/src/Iris/Instances.lean b/src/Iris/Instances.lean index 995cfb742..52446176e 100644 --- a/src/Iris/Instances.lean +++ b/src/Iris/Instances.lean @@ -1,2 +1,4 @@ -import Iris.Instances.Classical -import Iris.Instances.Data +module + +public import Iris.Instances.Classical +public import Iris.Instances.Data diff --git a/src/Iris/Instances/Classical.lean b/src/Iris/Instances/Classical.lean index dfcc4702a..d31ec3b2f 100644 --- a/src/Iris/Instances/Classical.lean +++ b/src/Iris/Instances/Classical.lean @@ -1,2 +1,4 @@ -import Iris.Instances.Classical.Instance -import Iris.Instances.Classical.Notation +module + +public import Iris.Instances.Classical.Instance +public import Iris.Instances.Classical.Notation diff --git a/src/Iris/Instances/Classical/Instance.lean b/src/Iris/Instances/Classical/Instance.lean index 78a8aef51..442274b41 100644 --- a/src/Iris/Instances/Classical/Instance.lean +++ b/src/Iris/Instances/Classical/Instance.lean @@ -3,9 +3,13 @@ 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 -/ -import Iris.BI -import Iris.Instances.Data -import Iris.Std.Equivalence +module + +public import Iris.BI +public import Iris.Instances.Data +public import Iris.Std.Equivalence + +@[expose] public section namespace Iris.Instances.Classical open Iris.BI Iris.Instances.Data Std diff --git a/src/Iris/Instances/Classical/Notation.lean b/src/Iris/Instances/Classical/Notation.lean index 51e1c1143..1d21dd449 100644 --- a/src/Iris/Instances/Classical/Notation.lean +++ b/src/Iris/Instances/Classical/Notation.lean @@ -3,7 +3,11 @@ 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 -/ -import Iris.Instances.Classical.Instance +module + +public import Iris.Instances.Classical.Instance + +@[expose] public section namespace Iris.Instances.Classical open Iris.Instances.Data diff --git a/src/Iris/Instances/Data.lean b/src/Iris/Instances/Data.lean index d7db7d9d8..c975aca9d 100644 --- a/src/Iris/Instances/Data.lean +++ b/src/Iris/Instances/Data.lean @@ -1,2 +1,4 @@ -import Iris.Instances.Data.SetNotation -import Iris.Instances.Data.State +module + +public import Iris.Instances.Data.SetNotation +public import Iris.Instances.Data.State diff --git a/src/Iris/Instances/Data/SetNotation.lean b/src/Iris/Instances/Data/SetNotation.lean index 0eed8b344..0155d488a 100644 --- a/src/Iris/Instances/Data/SetNotation.lean +++ b/src/Iris/Instances/Data/SetNotation.lean @@ -3,6 +3,9 @@ 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 -/ +module + +@[expose] public section namespace Iris.Instances.Data diff --git a/src/Iris/Instances/Data/State.lean b/src/Iris/Instances/Data/State.lean index 02bf804dd..d78fc998b 100644 --- a/src/Iris/Instances/Data/State.lean +++ b/src/Iris/Instances/Data/State.lean @@ -3,7 +3,11 @@ 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 -/ -import Iris.Instances.Data.SetNotation +module + +public import Iris.Instances.Data.SetNotation + +@[expose] public section namespace Iris.Instances.Data diff --git a/src/Iris/Instances/IProp.lean b/src/Iris/Instances/IProp.lean index 0e63032ba..30a27a1be 100644 --- a/src/Iris/Instances/IProp.lean +++ b/src/Iris/Instances/IProp.lean @@ -1 +1,3 @@ -import Iris.Instances.IProp.Instance +module + +public import Iris.Instances.IProp.Instance diff --git a/src/Iris/Instances/IProp/Instance.lean b/src/Iris/Instances/IProp/Instance.lean index 60a17cdfe..e7e2f7647 100644 --- a/src/Iris/Instances/IProp/Instance.lean +++ b/src/Iris/Instances/IProp/Instance.lean @@ -3,10 +3,13 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Zongyuan Liu, Remy Seassau -/ +module -import Iris.BI -import Iris.Algebra -import Iris.Instances.UPred +public import Iris.BI +public import Iris.Algebra +public import Iris.Instances.UPred + +@[expose] public section namespace Iris open COFE diff --git a/src/Iris/Instances/UPred.lean b/src/Iris/Instances/UPred.lean index 8930d2dc3..68821abe0 100644 --- a/src/Iris/Instances/UPred.lean +++ b/src/Iris/Instances/UPred.lean @@ -1 +1,3 @@ -import Iris.Instances.UPred.Instance +module + +public import Iris.Instances.UPred.Instance diff --git a/src/Iris/Instances/UPred/Instance.lean b/src/Iris/Instances/UPred/Instance.lean index d62fd1c4e..5d1da7373 100644 --- a/src/Iris/Instances/UPred/Instance.lean +++ b/src/Iris/Instances/UPred/Instance.lean @@ -3,13 +3,16 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Mario Carneiro -/ +module -import Iris.BI -import Iris.Algebra.OFE -import Iris.Algebra.CMRA -import Iris.Algebra.UPred -import Iris.Algebra.Updates -import Iris.BI.Lib.BUpdPlain +public import Iris.BI +public import Iris.Algebra.OFE +public import Iris.Algebra.CMRA +public import Iris.Algebra.UPred +public import Iris.Algebra.Updates +public import Iris.BI.Lib.BUpdPlain + +@[expose] public section section UPredInstance diff --git a/src/Iris/ProofMode.lean b/src/Iris/ProofMode.lean index f2462941b..34761f9c8 100644 --- a/src/Iris/ProofMode.lean +++ b/src/Iris/ProofMode.lean @@ -1,12 +1,14 @@ -import Iris.ProofMode.Classes -import Iris.ProofMode.ClassesMake -import Iris.ProofMode.Display -import Iris.ProofMode.Expr -import Iris.ProofMode.Instances -import Iris.ProofMode.InstancesLater -import Iris.ProofMode.InstancesMake -import Iris.ProofMode.InstancesPlainly -import Iris.ProofMode.InstancesUpdates -import Iris.ProofMode.Patterns -import Iris.ProofMode.Tactics -import Iris.ProofMode.UnifHints +module + +public import Iris.ProofMode.Classes +public import Iris.ProofMode.ClassesMake +public meta import Iris.ProofMode.Display +public meta import Iris.ProofMode.Expr +public import Iris.ProofMode.Instances +public import Iris.ProofMode.InstancesLater +public import Iris.ProofMode.InstancesMake +public import Iris.ProofMode.InstancesPlainly +public import Iris.ProofMode.InstancesUpdates +public import Iris.ProofMode.Patterns +public meta import Iris.ProofMode.Tactics +public import Iris.ProofMode.UnifHints diff --git a/src/Iris/ProofMode/Classes.lean b/src/Iris/ProofMode/Classes.lean index 7ab75b303..4d3c4cbb4 100644 --- a/src/Iris/ProofMode/Classes.lean +++ b/src/Iris/ProofMode/Classes.lean @@ -3,9 +3,13 @@ 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, Michael Sammler -/ -import Iris.BI -import Iris.ProofMode.SynthInstance -import Iris.ProofMode.Modalities +module + +public import Iris.BI +public meta import Iris.ProofMode.SynthInstance +public import Iris.ProofMode.Modalities + +@[expose] public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/ClassesMake.lean b/src/Iris/ProofMode/ClassesMake.lean index 235e4781e..c28ae6e21 100644 --- a/src/Iris/ProofMode/ClassesMake.lean +++ b/src/Iris/ProofMode/ClassesMake.lean @@ -3,8 +3,12 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI -import Iris.ProofMode.SynthInstance +module + +public import Iris.BI +public meta import Iris.ProofMode.SynthInstance + +@[expose] public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Display.lean b/src/Iris/ProofMode/Display.lean index 627c56926..cdb21e64c 100644 --- a/src/Iris/ProofMode/Display.lean +++ b/src/Iris/ProofMode/Display.lean @@ -3,10 +3,14 @@ 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, Mario Carneiro -/ -import Iris.BI.Notation -import Iris.ProofMode.Expr +module -import Lean.PrettyPrinter.Delaborator +public meta import Iris.BI.Notation +public meta import Iris.ProofMode.Expr + +public meta import Lean.PrettyPrinter.Delaborator + +public meta section namespace Iris.ProofMode open Iris.BI Qq diff --git a/src/Iris/ProofMode/Expr.lean b/src/Iris/ProofMode/Expr.lean index 88e49762a..612ff9081 100644 --- a/src/Iris/ProofMode/Expr.lean +++ b/src/Iris/ProofMode/Expr.lean @@ -3,17 +3,22 @@ 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, Mario Carneiro, Michael Sammler -/ -import Qq -import Iris.BI -import Iris.ProofMode.Classes -import Iris.Std +module + +public meta import Qq +public import Iris.BI +public import Iris.ProofMode.Classes +public import Iris.Std +public meta import Iris.Std.Expr + +public meta section namespace Iris.ProofMode open Iris.BI Iris.Std open Lean Lean.Expr Lean.Meta Qq -@[match_pattern] def nameAnnotation := `name -@[match_pattern] def uniqAnnotation := `uniq +@[expose, match_pattern] def nameAnnotation := `name +@[expose, match_pattern] def uniqAnnotation := `uniq def parseName? : Expr → Option (Name × Name × Expr) | .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ e => do @@ -112,32 +117,32 @@ def Hyps.select (ty : Expr) : ∀ {s}, @Hyps u prop bi s → MetaM (Name × Q(Bo | _, .sep _ _ _ _ lhs rhs => try Hyps.select ty rhs catch _ => Hyps.select ty lhs -private theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P := +theorem intuitionistically_sep_dup [BI PROP] {P : PROP} : □ P ⊣⊢ □ P ∗ □ P := intuitionistically_sep_idem.symm -private theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp := sep_emp.symm +theorem sep_emp_rev [BI PROP] {P : PROP} : P ⊣⊢ P ∗ emp := sep_emp.symm -private theorem emp_sep_rev [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P := emp_sep.symm +theorem emp_sep_rev [BI PROP] {P : PROP} : P ⊣⊢ emp ∗ P := emp_sep.symm section split -private theorem split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2 := +theorem split_es [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : emp ∗ Q ⊣⊢ Q1 ∗ Q2 := emp_sep.trans h -private theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2 := +theorem split_ls [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2 := (sep_congr_r h).trans sep_assoc.symm -private theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2) := +theorem split_rs [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ Q1 ∗ (P ∗ Q2) := (sep_congr_r h).trans sep_left_comm -private theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2 := +theorem split_se [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ emp ⊣⊢ P1 ∗ P2 := sep_emp.trans h -private theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2 := +theorem split_sl [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2 := (sep_congr_l h).trans sep_right_comm -private theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q) := +theorem split_sr [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) : P ∗ Q ⊣⊢ P1 ∗ (P2 ∗ Q) := (sep_congr_l h).trans sep_assoc -private theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP} +theorem split_ss [BI PROP] {P Q P1 P2 Q1 Q2 : PROP} (h1 : P ⊣⊢ P1 ∗ P2) (h2 : Q ⊣⊢ Q1 ∗ Q2) : P ∗ Q ⊣⊢ (P1 ∗ Q1) ∗ (P2 ∗ Q2) := (sep_congr h1 h2).trans sep_sep_sep_comm -private inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where +inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where | emp (_ : $e =Q BI.emp) | left | right @@ -145,7 +150,7 @@ private inductive SplitResult {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop (pf : Q($e ⊣⊢ $elhs ∗ $erhs)) variable {prop : Q(Type u)} (bi : Q(BI $prop)) (toRight : Name → Name → Bool) in -private def Hyps.splitCore : ∀ {e}, Hyps bi e → SplitResult bi e +def Hyps.splitCore : ∀ {e}, Hyps bi e → SplitResult bi e | _, .emp _ => .emp ⟨⟩ | ehyp, h@(.hyp _ name uniq b ty _) => match matchBool b with @@ -188,23 +193,23 @@ structure RemoveHyp {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) where (pf : Q($e ⊣⊢ $e' ∗ $out)) deriving Inhabited -private inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where +inductive RemoveHypCore {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop)) (α : Type) where | none | one (a : α) (out' : Q($prop)) (p : Q(Bool)) (eq : $e =Q iprop(□?$p $out')) | main (a : α) (_ : RemoveHyp bi e) -private theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) : +theorem remove_l [BI PROP] {P P' Q R : PROP} (h : P ⊣⊢ P' ∗ R) : P ∗ Q ⊣⊢ (P' ∗ Q) ∗ R := (sep_congr_l h).trans sep_right_comm -private theorem remove_r [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) : +theorem remove_r [BI PROP] {P Q Q' R : PROP} (h : Q ⊣⊢ Q' ∗ R) : P ∗ Q ⊣⊢ (P ∗ Q') ∗ R := (sep_congr_r h).trans sep_assoc.symm variable [Monad m] {prop : Q(Type u)} (bi : Q(BI $prop)) (rp : Bool) (check : Name → Name → Q(Bool) → Q($prop) → m (Option α)) in /-- If `rp` is true, the hyp will be removed even if it is in the intuitionistic context. -/ -private def Hyps.removeCore : ∀ {e}, Hyps bi e → m (RemoveHypCore bi e α) +def Hyps.removeCore : ∀ {e}, Hyps bi e → m (RemoveHypCore bi e α) | _, .emp _ => pure .none | e, h@(.hyp _ name uniq p ty _) => do if let some a ← check name uniq p ty then diff --git a/src/Iris/ProofMode/Instances.lean b/src/Iris/ProofMode/Instances.lean index 6163d839d..a7227b276 100644 --- a/src/Iris/ProofMode/Instances.lean +++ b/src/Iris/ProofMode/Instances.lean @@ -3,10 +3,14 @@ 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, Mario Carneiro -/ -import Iris.BI -import Iris.ProofMode.Classes -import Iris.ProofMode.ModalityInstances -import Iris.Std.TC +module + +public import Iris.BI +public import Iris.ProofMode.Classes +public import Iris.ProofMode.ModalityInstances +public import Iris.Std.TC + +@[expose] public section namespace Iris.ProofMode open Iris.BI Iris.Std diff --git a/src/Iris/ProofMode/InstancesLater.lean b/src/Iris/ProofMode/InstancesLater.lean index cf80210d9..affa072ed 100644 --- a/src/Iris/ProofMode/InstancesLater.lean +++ b/src/Iris/ProofMode/InstancesLater.lean @@ -3,11 +3,15 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI -import Iris.ProofMode.Classes -import Iris.ProofMode.ClassesMake -import Iris.ProofMode.ModalityInstances -import Iris.Std.TC +module + +public import Iris.BI +public import Iris.ProofMode.Classes +public import Iris.ProofMode.ClassesMake +public import Iris.ProofMode.ModalityInstances +public import Iris.Std.TC + +@[expose] public section namespace Iris.ProofMode open Iris.BI Iris.Std diff --git a/src/Iris/ProofMode/InstancesMake.lean b/src/Iris/ProofMode/InstancesMake.lean index a70cbaf34..2edcfb174 100644 --- a/src/Iris/ProofMode/InstancesMake.lean +++ b/src/Iris/ProofMode/InstancesMake.lean @@ -3,8 +3,12 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI -import Iris.ProofMode.ClassesMake +module + +public import Iris.BI +public import Iris.ProofMode.ClassesMake + +@[expose] public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/InstancesPlainly.lean b/src/Iris/ProofMode/InstancesPlainly.lean index ffa3f7cec..7769451c9 100644 --- a/src/Iris/ProofMode/InstancesPlainly.lean +++ b/src/Iris/ProofMode/InstancesPlainly.lean @@ -3,10 +3,14 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI -import Iris.ProofMode.Classes -import Iris.ProofMode.ModalityInstances -import Iris.Std.TC +module + +public import Iris.BI +public import Iris.ProofMode.Classes +public import Iris.ProofMode.ModalityInstances +public import Iris.Std.TC + +@[expose] public section namespace Iris.ProofMode open Iris.BI Iris.Std diff --git a/src/Iris/ProofMode/InstancesUpdates.lean b/src/Iris/ProofMode/InstancesUpdates.lean index 9571edf6c..c50e2b1f4 100644 --- a/src/Iris/ProofMode/InstancesUpdates.lean +++ b/src/Iris/ProofMode/InstancesUpdates.lean @@ -3,9 +3,13 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI -import Iris.ProofMode.Classes -import Iris.Std.TC +module + +public import Iris.BI +public import Iris.ProofMode.Classes +public import Iris.Std.TC + +@[expose] public section namespace Iris.ProofMode open Iris.BI Iris.Std diff --git a/src/Iris/ProofMode/Modalities.lean b/src/Iris/ProofMode/Modalities.lean index 48125cf87..5aef8677d 100644 --- a/src/Iris/ProofMode/Modalities.lean +++ b/src/Iris/ProofMode/Modalities.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Michael Sammler -/ -import Iris.BI +module + +public import Iris.BI + +@[expose] public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/ModalityInstances.lean b/src/Iris/ProofMode/ModalityInstances.lean index e532e6ece..57b0f0866 100644 --- a/src/Iris/ProofMode/ModalityInstances.lean +++ b/src/Iris/ProofMode/ModalityInstances.lean @@ -3,10 +3,14 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros, Michael Sammler -/ -import Iris.BI -import Iris.BI.DerivedLaws -import Iris.ProofMode.Modalities -import Iris.ProofMode.Classes +module + +public import Iris.BI +public import Iris.BI.DerivedLaws +public import Iris.ProofMode.Modalities +public import Iris.ProofMode.Classes + +@[expose] public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Patterns.lean b/src/Iris/ProofMode/Patterns.lean index 3125976c8..09f22c48d 100644 --- a/src/Iris/ProofMode/Patterns.lean +++ b/src/Iris/ProofMode/Patterns.lean @@ -1,4 +1,6 @@ -import Iris.ProofMode.Patterns.CasesPattern -import Iris.ProofMode.Patterns.IntroPattern -import Iris.ProofMode.Patterns.ProofModeTerm -import Iris.ProofMode.Patterns.SpecPattern +module + +public import Iris.ProofMode.Patterns.CasesPattern +public import Iris.ProofMode.Patterns.IntroPattern +public import Iris.ProofMode.Patterns.ProofModeTerm +public import Iris.ProofMode.Patterns.SpecPattern diff --git a/src/Iris/ProofMode/Patterns/CasesPattern.lean b/src/Iris/ProofMode/Patterns/CasesPattern.lean index 90d7072b9..77d3b0f23 100644 --- a/src/Iris/ProofMode/Patterns/CasesPattern.lean +++ b/src/Iris/ProofMode/Patterns/CasesPattern.lean @@ -3,7 +3,11 @@ 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 -/ -import Lean.Data.Name +module + +public import Lean.Data.Name + +@[expose] public section namespace Iris.ProofMode open Lean diff --git a/src/Iris/ProofMode/Patterns/IntroPattern.lean b/src/Iris/ProofMode/Patterns/IntroPattern.lean index 64780e78a..cb0477e6c 100644 --- a/src/Iris/ProofMode/Patterns/IntroPattern.lean +++ b/src/Iris/ProofMode/Patterns/IntroPattern.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.ProofMode.Patterns.CasesPattern +module + +public import Iris.ProofMode.Patterns.CasesPattern + +@[expose] public section namespace Iris.ProofMode open Lean diff --git a/src/Iris/ProofMode/Patterns/ProofModeTerm.lean b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean index 51e6b974d..2657e6df7 100644 --- a/src/Iris/ProofMode/Patterns/ProofModeTerm.lean +++ b/src/Iris/ProofMode/Patterns/ProofModeTerm.lean @@ -3,7 +3,11 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Soeser -/ -import Iris.ProofMode.Patterns.SpecPattern +module + +public import Iris.ProofMode.Patterns.SpecPattern + +@[expose] public section namespace Iris.ProofMode open Lean diff --git a/src/Iris/ProofMode/Patterns/SpecPattern.lean b/src/Iris/ProofMode/Patterns/SpecPattern.lean index a482ca60c..ac5c12527 100644 --- a/src/Iris/ProofMode/Patterns/SpecPattern.lean +++ b/src/Iris/ProofMode/Patterns/SpecPattern.lean @@ -3,6 +3,10 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Soeser -/ +module + +@[expose] public section + namespace Iris.ProofMode open Lean diff --git a/src/Iris/ProofMode/ProofModeM.lean b/src/Iris/ProofMode/ProofModeM.lean index da3c746c0..399f1dffb 100644 --- a/src/Iris/ProofMode/ProofModeM.lean +++ b/src/Iris/ProofMode/ProofModeM.lean @@ -3,8 +3,12 @@ Copyright (c) 2025 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler, Zongyuan Liu -/ -import Iris.ProofMode.Expr -import Iris.ProofMode.Classes +module + +public meta import Iris.ProofMode.Expr +public import Iris.ProofMode.Classes + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std diff --git a/src/Iris/ProofMode/SynthInstance.lean b/src/Iris/ProofMode/SynthInstance.lean index dad465b5e..11f7bbccd 100644 --- a/src/Iris/ProofMode/SynthInstance.lean +++ b/src/Iris/ProofMode/SynthInstance.lean @@ -3,8 +3,12 @@ Copyright (c) 2025 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Qq -import Iris.BI +module + +public import Qq +public import Iris.BI + +public meta section /- This file implements a custom typeclass synthesis algorithm that is used for the proof mode typeclasses. @@ -70,7 +74,7 @@ initialize registerBuiltinAttribute { } -private partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do +partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := do withIncRecDepth do let backtrackSet := ipmBacktrackExt.getState (← getEnv) let mvarType ← inferType mvar @@ -103,7 +107,7 @@ private partial def synthInstanceMainCore (mvar : Expr) : MetaM (Option Unit) := return res return none -private def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Option Expr) := +def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Option Expr) := withCurrHeartbeats do let mvar ← mkFreshExprMVar type tryCatchRuntimeEx (do @@ -115,7 +119,7 @@ private def synthInstanceMain (type : Expr) (_maxResultSize : Nat) : MetaM (Opti else throw ex -private def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do +def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do let opts ← getOptions let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts) withTraceNode `Meta.synthInstance diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean index c5b37ed56..006c80d8e 100644 --- a/src/Iris/ProofMode/Tactics.lean +++ b/src/Iris/ProofMode/Tactics.lean @@ -1,18 +1,20 @@ /- A description of the tactics can be found in `tactics.md`. -/ -import Iris.ProofMode.Tactics.Apply -import Iris.ProofMode.Tactics.Assumption -import Iris.ProofMode.Tactics.Basic -import Iris.ProofMode.Tactics.Cases -import Iris.ProofMode.Tactics.Clear -import Iris.ProofMode.Tactics.Exact -import Iris.ProofMode.Tactics.ExFalso -import Iris.ProofMode.Tactics.Exists -import Iris.ProofMode.Tactics.Have -import Iris.ProofMode.Tactics.Intro -import Iris.ProofMode.Tactics.LeftRight -import Iris.ProofMode.Tactics.Mod -import Iris.ProofMode.Tactics.ModIntro -import Iris.ProofMode.Tactics.Pure -import Iris.ProofMode.Tactics.Rename -import Iris.ProofMode.Tactics.Specialize -import Iris.ProofMode.Tactics.Split +module + +public meta import Iris.ProofMode.Tactics.Apply +public meta import Iris.ProofMode.Tactics.Assumption +public meta import Iris.ProofMode.Tactics.Basic +public meta import Iris.ProofMode.Tactics.Cases +public meta import Iris.ProofMode.Tactics.Clear +public meta import Iris.ProofMode.Tactics.Exact +public meta import Iris.ProofMode.Tactics.ExFalso +public meta import Iris.ProofMode.Tactics.Exists +public meta import Iris.ProofMode.Tactics.Have +public meta import Iris.ProofMode.Tactics.Intro +public meta import Iris.ProofMode.Tactics.LeftRight +public meta import Iris.ProofMode.Tactics.Mod +public meta import Iris.ProofMode.Tactics.ModIntro +public meta import Iris.ProofMode.Tactics.Pure +public meta import Iris.ProofMode.Tactics.Rename +public meta import Iris.ProofMode.Tactics.Specialize +public meta import Iris.ProofMode.Tactics.Split diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean index 9ea2c2702..3e0033dba 100644 --- a/src/Iris/ProofMode/Tactics/Apply.lean +++ b/src/Iris/ProofMode/Tactics/Apply.lean @@ -3,14 +3,18 @@ Copyright (c) 2025 Oliver Soeser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Soeser, Michael Sammler -/ -import Iris.ProofMode.Patterns.ProofModeTerm -import Iris.ProofMode.Tactics.Assumption -import Iris.ProofMode.Tactics.HaveCore +module + +public meta import Iris.ProofMode.Patterns.ProofModeTerm +public meta import Iris.ProofMode.Tactics.Assumption +public meta import Iris.ProofMode.Tactics.HaveCore + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem apply [BI PROP] {p} {P Q Q1 R : PROP} +theorem apply [BI PROP] {p} {P Q Q1 R : PROP} (h1 : P ⊢ Q1) [h2 : IntoWand p false Q .out Q1 .in R] : P ∗ □?p Q ⊢ R := (Entails.trans (sep_mono_l h1) (wand_elim' h2.1)) diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean index a3d9076bd..d30d73c7f 100644 --- a/src/Iris/ProofMode/Tactics/Assumption.lean +++ b/src/Iris/ProofMode/Tactics/Assumption.lean @@ -3,7 +3,11 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean index d28b88c55..8178b95de 100644 --- a/src/Iris/ProofMode/Tactics/Basic.lean +++ b/src/Iris/ProofMode/Tactics/Basic.lean @@ -3,10 +3,14 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Expr -import Iris.ProofMode.Classes -import Iris.ProofMode.ProofModeM -import Iris.ProofMode.SynthInstance +module + +public meta import Iris.ProofMode.Expr +public import Iris.ProofMode.Classes +public meta import Iris.ProofMode.ProofModeM +public meta import Iris.ProofMode.SynthInstance + +public meta section namespace Iris.ProofMode open Lean Elab.Tactic Meta Qq BI Std diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean index 9dbedad83..1af929932 100644 --- a/src/Iris/ProofMode/Tactics/Cases.lean +++ b/src/Iris/ProofMode/Tactics/Cases.lean @@ -3,18 +3,22 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Patterns.ProofModeTerm -import Iris.ProofMode.Patterns.CasesPattern -import Iris.ProofMode.Tactics.Basic -import Iris.ProofMode.Tactics.Clear -import Iris.ProofMode.Tactics.Pure -import Iris.ProofMode.Tactics.HaveCore -import Iris.ProofMode.Tactics.Mod +module + +public meta import Iris.ProofMode.Patterns.ProofModeTerm +public meta import Iris.ProofMode.Patterns.CasesPattern +public meta import Iris.ProofMode.Tactics.Basic +public meta import Iris.ProofMode.Tactics.Clear +public meta import Iris.ProofMode.Tactics.Pure +public meta import Iris.ProofMode.Tactics.HaveCore +public meta import Iris.ProofMode.Tactics.Mod + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q := +theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q := wand_elim' <| intuitionisticallyIf_elim.trans false_elim def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) @@ -27,7 +31,7 @@ def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) throwError "icases: cannot destruct {A'} as an empty conjunct" -private theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ] +theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ] (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h) @@ -50,11 +54,11 @@ def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : return q(exists_elim' (A := $A') $pf) -private theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] +theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_l).trans h -private theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] +theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h @@ -72,11 +76,11 @@ def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1 return some q(sep_and_elim_l $(← k A1' A1 ⟨⟩)) -private theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2] +theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2] (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q := (sep_mono_r inst.1).trans <| sep_assoc.2.trans <| wand_elim h -private theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2] +theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2] (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q := (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <| sep_assoc.2.trans <| wand_elim h @@ -107,7 +111,7 @@ def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) return q(wand_intro $pf) return q(sep_elim_spatial (A := $A') $pf) -private theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2] +theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2] (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2 @@ -124,11 +128,11 @@ def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bo let pf2 ← k2 A2' A2 ⟨⟩ return q(or_elim' (A := $A') $pf1 $pf2) -private theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP} +theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP} [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)] (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h -private theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A'] +theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A'] (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) @@ -145,7 +149,7 @@ def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($pro | throwError "icases: {A'} not affine and the goal not absorbing" return q(intuitionistic_elim_spatial (A := $A') $(← k B')) -private theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p] +theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p] (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h @@ -157,7 +161,7 @@ def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B' $A' $p) return q(spatial_elim (A := $A') $(← k B')) -private theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h +theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h -- TODO: Why does this function require both A and A' instead of just A'? variable {u : Level} {prop : Q(Type u)} (bi : Q(BI $prop)) in diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean index 6b339533d..add233254 100644 --- a/src/Iris/ProofMode/Tactics/Clear.lean +++ b/src/Iris/ProofMode/Tactics/Clear.lean @@ -3,16 +3,20 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)] +theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)] (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q := h_rem.1.trans <| (sep_mono_l h).trans sep_elim_l -private theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP} +theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP} (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q := clear_spatial h_rem h def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean index 3d0ab97d6..649ee89c4 100644 --- a/src/Iris/ProofMode/Tactics/ExFalso.lean +++ b/src/Iris/ProofMode/Tactics/ExFalso.lean @@ -3,12 +3,16 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab.Tactic Meta Qq BI -private theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim +theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim elab "iexfalso" : tactic => do ProofModeM.runTactic λ mvar { hyps, goal, .. } => do diff --git a/src/Iris/ProofMode/Tactics/Exact.lean b/src/Iris/ProofMode/Tactics/Exact.lean index 7cdc3d74f..ac1378b35 100644 --- a/src/Iris/ProofMode/Tactics/Exact.lean +++ b/src/Iris/ProofMode/Tactics/Exact.lean @@ -3,8 +3,12 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic -import Iris.ProofMode.Tactics.Assumption +module + +public meta import Iris.ProofMode.Tactics.Basic +public meta import Iris.ProofMode.Tactics.Assumption + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean index 9c8a5594b..5d3337e2c 100644 --- a/src/Iris/ProofMode/Tactics/Exists.lean +++ b/src/Iris/ProofMode/Tactics/Exists.lean @@ -3,12 +3,16 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI -private theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ] +theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ] (a : α) (h : P ⊢ Q) : Φ a ⊢ Q := ((exists_intro a).trans inst.1).trans h diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean index d3ec48236..d45382c37 100644 --- a/src/Iris/ProofMode/Tactics/Have.lean +++ b/src/Iris/ProofMode/Tactics/Have.lean @@ -3,16 +3,20 @@ Copyright (c) 2025 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.ProofMode.Patterns.CasesPattern -import Iris.ProofMode.Tactics.HaveCore -import Iris.ProofMode.Tactics.Cases +module + +public meta import Iris.ProofMode.Patterns.CasesPattern +public meta import Iris.ProofMode.Tactics.HaveCore +public meta import Iris.ProofMode.Tactics.Cases + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std macro "ihave" colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icases +keep $pmt with $pat) -private theorem ihave_assert [BI PROP] {A B C : PROP} +theorem ihave_assert [BI PROP] {A B C : PROP} (h1 : A ∗ □ (B -∗ B) ⊢ C) : A ⊢ C := (and_intro .rfl (persistently_emp_intro.trans (persistently_mono $ wand_intro emp_sep.1))).trans $ persistently_and_intuitionistically_sep_r.1.trans h1 diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean index 32817481b..8bdc44979 100644 --- a/src/Iris/ProofMode/Tactics/HaveCore.lean +++ b/src/Iris/ProofMode/Tactics/HaveCore.lean @@ -3,9 +3,13 @@ Copyright (c) 2025 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler, Zongyuan Liu -/ -import Iris.ProofMode.Patterns.ProofModeTerm -import Iris.ProofMode.Tactics.Basic -import Iris.ProofMode.Tactics.Specialize +module + +public meta import Iris.ProofMode.Patterns.ProofModeTerm +public meta import Iris.ProofMode.Tactics.Basic +public meta import Iris.ProofMode.Tactics.Specialize + +public meta section /- This file contains the `iHave` function for asserting a ProofModeTerm. It is separate from the implementation of `ihave` in `Have.lean` since @@ -16,7 +20,7 @@ import Iris.ProofMode.Tactics.Specialize namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP} +theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP} [h1 : AsEmpValid .into φ P] (h : φ) : Q ⊢ Q ∗ □ P := sep_emp.2.trans (sep_mono_r $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h))) @@ -37,7 +41,7 @@ A tuple containing: - `out`: Asserted proposition - `pf`: Proof of `hyps ⊢ hyps' ∗ □?p out` -/ -private def iHaveCore {e} (hyps : @Hyps u prop bi e) +def iHaveCore {e} (hyps : @Hyps u prop bi e) (tm : Term) (keep : Bool) (mayPostpone : Bool) : ProofModeM ((e' : _) × Hyps bi e' × (p : Q(Bool)) × (out : Q($prop)) × Q($e ⊢ $e' ∗ □?$p $out)) := do if let some uniq ← try? <| hyps.findWithInfo ⟨tm⟩ then diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean index 0419d8270..7dd3317d3 100644 --- a/src/Iris/ProofMode/Tactics/Intro.lean +++ b/src/Iris/ProofMode/Tactics/Intro.lean @@ -3,26 +3,30 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Patterns.IntroPattern -import Iris.ProofMode.Tactics.Cases -import Iris.ProofMode.Tactics.ModIntro +module + +public meta import Iris.ProofMode.Patterns.IntroPattern +public meta import Iris.ProofMode.Tactics.Cases +public meta import Iris.ProofMode.Tactics.ModIntro + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q := +theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q := BI.imp_intro (and_elim_l' h) |>.trans inst.1 -private theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ] +theorem from_forall_intro [BI PROP] {P Q : PROP} {Φ : α → PROP} [inst : FromForall Q Φ] (h : ∀ a, P ⊢ Φ a) : P ⊢ Q := (forall_intro h).trans inst.1 -private theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} +theorem imp_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} [FromImp Q A1 A2] [inst : IntoPersistently false A1 B] (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by refine BI.imp_intro ?_ |>.trans from_imp exact (and_mono_r inst.1).trans <| persistently_and_intuitionistically_sep_r.1.trans h -private theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} +theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} [FromWand Q A1 A2] [inst : IntoPersistently false A1 B] [or : TCOr (Affine A1) (Absorbing A2)] (h : P ∗ □ B ⊢ A2) : P ⊢ Q := by refine (wand_intro ?_).trans from_wand @@ -31,7 +35,7 @@ private theorem wand_intro_intuitionistic [BI PROP] {P Q A1 A2 B : PROP} | TCOr.r => (sep_mono_r <| inst.1.trans absorbingly_intuitionistically.2).trans <| absorbingly_sep_r.1.trans <| (absorbingly_mono h).trans absorbing -private theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP} +theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP} [FromImp Q A1 A2] [inst : FromAffinely B A1] [or : TCOr (Persistent A1) (Intuitionistic P)] (h : P ∗ B ⊢ A2) : P ⊢ Q := by refine (BI.imp_intro ?_).trans from_imp @@ -42,7 +46,7 @@ private theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP} (and_mono_l u.1).trans <| affinely_and_lr.1.trans <| persistently_and_intuitionistically_sep_l.1.trans <| sep_mono_l intuitionistically_elim -private theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} +theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans from_wand partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean index 49985aa1e..70059c21b 100644 --- a/src/Iris/ProofMode/Tactics/LeftRight.lean +++ b/src/Iris/ProofMode/Tactics/LeftRight.lean @@ -3,12 +3,16 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab.Tactic Meta Qq BI Std -private theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] +theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A1) : P ⊢ Q := (or_intro_l' h1).trans inst.1 @@ -23,7 +27,7 @@ elab "ileft" : tactic => do let m : Q($e ⊢ $A1) ← addBIGoal hyps A1 mvar.assign q(from_or_l (Q := $goal) $m) -private theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] +theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A2) : P ⊢ Q := (or_intro_r' h1).trans inst.1 diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean index b70f9d649..083d89c43 100644 --- a/src/Iris/ProofMode/Tactics/Mod.lean +++ b/src/Iris/ProofMode/Tactics/Mod.lean @@ -3,12 +3,16 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q'] +theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q'] (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q := (sep_comm.1.trans (sep_mono_r (wand_intro h1))).trans (he.1 hΦ) diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean index e5b3c43a5..e9f0278cb 100644 --- a/src/Iris/ProofMode/Tactics/ModIntro.lean +++ b/src/Iris/ProofMode/Tactics/ModIntro.lean @@ -3,21 +3,25 @@ Copyright (c) 2026 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic -import Iris.ProofMode.Modalities +module + +public meta import Iris.ProofMode.Tactics.Basic +public import Iris.ProofMode.Modalities + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std /-- Reified version of ModalityAction -/ -private inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where +inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where | isEmpty | forall (C : Q($PROP1 → Prop)) | transform (C : Q($PROP2 → $PROP1 → Prop)) | clear | id -private def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) : +def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) : ProofModeM (ModalityActionQ prop1 prop2) := do let act ← whnf q($act) match_expr act with @@ -28,19 +32,19 @@ private def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAct | ModalityAction.id _ => return .id | _ => throwError "imodintro: unknown modality action {act}" -private theorem modaction_forall [BI PROP] {p P} (M : Modality PROP PROP) {C} (h : M.action p = .forall C) (hC : C P) +theorem modaction_forall [BI PROP] {p P} (M : Modality PROP PROP) {C} (h : M.action p = .forall C) (hC : C P) : □?p P ⊢ M.M iprop(□?p P) := by have hs := M.spec p rw [h] at hs apply (hs _ hC) -private theorem modaction_transform [BI PROP1] [BI PROP2] {p P Q} (M : Modality PROP1 PROP2) {C} (h : M.action p = .transform C) (hC : C P Q) +theorem modaction_transform [BI PROP1] [BI PROP2] {p P Q} (M : Modality PROP1 PROP2) {C} (h : M.action p = .transform C) (hC : C P Q) : □?p P ⊢ M.M iprop(□?p Q) := by have hs := M.spec p rw [h] at hs apply (hs _ _ hC) -private theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1 PROP2) (h : M.action p = .clear) +theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1 PROP2) (h : M.action p = .clear) : □?p P ⊢ M.M emp := match p, h with | true, _ => affine.trans M.emp @@ -49,20 +53,20 @@ private theorem modaction_clear [BI PROP1] [BI PROP2] {p P} (M : Modality PROP1 simp [h] at hs apply Entails.trans (sep_emp.2.trans (sep_mono true_intro M.emp)) absorbing -private theorem modaction_id [BI PROP] {p P} (M : Modality PROP PROP) (h : M.action p = .id) +theorem modaction_id [BI PROP] {p P} (M : Modality PROP PROP) (h : M.action p = .id) : □?p P ⊢ M.M iprop(□?p P) := by have hs := M.spec p rw [h] at hs apply hs -private theorem modaction_sep_emp_l [BI PROP1] [bi2: BI PROP2] {elhs erhs erhs'} {M : Modality PROP1 PROP2} +theorem modaction_sep_emp_l [BI PROP1] [bi2: BI PROP2] {elhs erhs erhs'} {M : Modality PROP1 PROP2} (h1 : elhs ⊢ M.M emp) (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(erhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono emp_sep.1) -private theorem modaction_sep_emp_r [BI PROP1] [bi2: BI PROP2] {elhs elhs' erhs} {M : Modality PROP1 PROP2} +theorem modaction_sep_emp_r [BI PROP1] [bi2: BI PROP2] {elhs elhs' erhs} {M : Modality PROP1 PROP2} (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M emp) : elhs ∗ erhs ⊢ M.M iprop(elhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono sep_emp.1) -private theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'} {M : Modality PROP1 PROP2} +theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'} {M : Modality PROP1 PROP2} (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(elhs' ∗ erhs') := (sep_mono h1 h2).trans M.sep @@ -80,7 +84,7 @@ A tuple containing: - Transformed context `hyps'` in `prop1` - Proof of `hyps ⊢ M hyps'` -/ -private def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e} +def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e} (hyps : @Hyps u prop2 bi2 e) (M : Q(Modality $prop1 $prop2)) (act : Bool → ModalityActionQ prop1 prop2) : ProofModeM ((e' : _) × Hyps bi1 e' × Q($e ⊢ $(M).M $e')) := match hyps with @@ -125,7 +129,7 @@ private def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e} return ⟨_, lhs', q(modaction_sep_emp_r $pflhs $pfrhs)⟩ return ⟨_, .mkSep lhs' rhs', q(modaction_sep $pflhs $pfrhs)⟩ -private theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q] +theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q] (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P := (h1.trans (M.mono h2)).trans (from_modal sel hΦ) diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean index 34c9e165e..56cf7fad2 100644 --- a/src/Iris/ProofMode/Tactics/Pure.lean +++ b/src/Iris/ProofMode/Tactics/Pure.lean @@ -3,13 +3,17 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Instances -import Iris.ProofMode.Tactics.Basic +module + +public import Iris.ProofMode.Instances +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop} +theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop} [hA : IntoPure A φ] [or : TCOr (Affine A) (Absorbing Q)] (h : P ⊣⊢ P' ∗ A) (h_entails : φ → P' ⊢ Q) : P ⊢ Q := h.1.trans <| match or with @@ -21,7 +25,7 @@ private theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop} absorbingly_sep_lr.2.trans <| persistent_and_affinely_sep_r.2.trans <| pure_elim_r fun hφ => (absorbingly_mono <| h_entails hφ).trans absorbing -private theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop} +theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop} [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q := pure_elim_spatial h h' @@ -64,11 +68,11 @@ elab "iemp_intro" : tactic => do | throwError "iemp_intro: context is not affine" mvar.assign q(affine (P := $e)) -private theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop} +theorem pure_intro_affine [BI PROP] {Q : PROP} {φ : Prop} [h : FromPure true Q φ] [Affine P] (hφ : φ) : P ⊢ Q := (affine.trans (eq_true hφ ▸ affinely_true.2)).trans h.1 -private theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} +theorem pure_intro_spatial [BI PROP] {Q : PROP} {φ : Prop} [h : FromPure false Q φ] (hφ : φ) : P ⊢ Q := (pure_intro hφ).trans h.1 diff --git a/src/Iris/ProofMode/Tactics/Rename.lean b/src/Iris/ProofMode/Tactics/Rename.lean index c29bf7cc0..d943dafdc 100644 --- a/src/Iris/ProofMode/Tactics/Rename.lean +++ b/src/Iris/ProofMode/Tactics/Rename.lean @@ -3,7 +3,11 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Qq diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean index 862bdb229..ad6370a7e 100644 --- a/src/Iris/ProofMode/Tactics/Specialize.lean +++ b/src/Iris/ProofMode/Tactics/Specialize.lean @@ -3,18 +3,22 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Patterns.ProofModeTerm -import Iris.ProofMode.Patterns.CasesPattern -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Patterns.ProofModeTerm +public meta import Iris.ProofMode.Patterns.CasesPattern +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI Std -private structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where +structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop)) pf : Q($orig ⊢ $e ∗ □?$p $out) -private theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP} +theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP} (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1) [h3 : IntoWand q p Q .in P1 .out P2] : A1 ⊢ A3 ∗ □?(p && q) P2 := by @@ -27,17 +31,17 @@ private theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP} -- TODO: if q is true and A1 is persistent, this proof can guarantee □ P2 instead of P2 -- see https://gitlab.mpi-sws.org/iris/iris/-/blob/846ed45bed6951035c6204fef365d9a344022ae6/iris/proofmode/coq_tactics.v#L336 -private theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2 +theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2 (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ A4) (h3 : A4 ⊢ P1) [inst : IntoWand q false Q .out P1 .out P2] : A1 ⊢ A3 ∗ P2 := by refine h1.trans <| (sep_mono_l h2.1).trans <| sep_assoc.1.trans (sep_mono_r ((sep_mono_l h3).trans ?_)) exact (sep_mono_r inst.1).trans wand_elim_r -private theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP} +theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP} [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a) := by refine h.trans <| sep_mono_r <| intuitionisticallyIf_mono <| inst.1.trans (forall_elim a) -private def SpecializeState.process_wand : +def SpecializeState.process_wand : @SpecializeState u prop bi orig → SpecPat → ProofModeM (SpecializeState bi orig) | { hyps, p, out, pf, .. }, .ident i => do let uniq ← hyps.findWithInfo i @@ -87,7 +91,7 @@ def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool := | .pure _ => true | _ => false -private theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B} +theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B} (h : P ∗ □?pa A ⊢ P' ∗ □?pb B) (h2 : pa = true ∨ Affine A) [IntoPersistently pb B B'] diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean index 3fcb23eaf..7cfc9d725 100644 --- a/src/Iris/ProofMode/Tactics/Split.lean +++ b/src/Iris/ProofMode/Tactics/Split.lean @@ -3,12 +3,16 @@ 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, Mario Carneiro, Michael Sammler -/ -import Iris.ProofMode.Tactics.Basic +module + +public meta import Iris.ProofMode.Tactics.Basic + +public meta section namespace Iris.ProofMode open Lean Elab Tactic Meta Qq BI -private theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2] +theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2] (h1 : P ⊢ A1) (h2 : P ⊢ A2) : P ⊢ Q := (and_intro h1 h2).trans inst.1 @@ -22,7 +26,7 @@ elab "isplit" : tactic => do let m2 ← addBIGoal hyps A2 mvar.assign q(from_and_intro (Q := $goal) $m1 $m2) -private theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] +theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q := h.1.trans <| (sep_mono h1 h2).trans inst.1 diff --git a/src/Iris/ProofMode/UnifHints.lean b/src/Iris/ProofMode/UnifHints.lean index 58cf0ef0b..f3a5fa1b7 100644 --- a/src/Iris/ProofMode/UnifHints.lean +++ b/src/Iris/ProofMode/UnifHints.lean @@ -3,7 +3,11 @@ 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 -/ -import Iris.BI +module + +public import Iris.BI + +@[expose] public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/Std.lean b/src/Iris/Std.lean index 13967d062..6539947bf 100644 --- a/src/Iris/Std.lean +++ b/src/Iris/Std.lean @@ -1,11 +1,13 @@ -import Iris.Std.Classes -import Iris.Std.Expr -import Iris.Std.HeapInstances -import Iris.Std.Infinite -import Iris.Std.Nat -import Iris.Std.Prod -import Iris.Std.Qq -import Iris.Std.Rewrite -import Iris.Std.Tactic -import Iris.Std.TC -import Iris.Std.Try +module + +public import Iris.Std.Classes +public import Iris.Std.Expr +public import Iris.Std.HeapInstances +public import Iris.Std.Infinite +public import Iris.Std.Nat +public import Iris.Std.Prod +public import Iris.Std.Qq +public import Iris.Std.Rewrite +public import Iris.Std.Tactic +public import Iris.Std.TC +public import Iris.Std.Try diff --git a/src/Iris/Std/BigOp.lean b/src/Iris/Std/BigOp.lean index d28518cf3..17eea983f 100644 --- a/src/Iris/Std/BigOp.lean +++ b/src/Iris/Std/BigOp.lean @@ -3,6 +3,9 @@ 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, Mario Carneiro -/ +module + +@[expose] public section namespace Iris.Std diff --git a/src/Iris/Std/Classes.lean b/src/Iris/Std/Classes.lean index a2e88a817..e91c724cb 100644 --- a/src/Iris/Std/Classes.lean +++ b/src/Iris/Std/Classes.lean @@ -3,6 +3,10 @@ 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 -/ +module + +@[expose] public section + namespace Iris.Std /-- Represents a binary relation with two arguments of the same type `α`. -/ diff --git a/src/Iris/Std/DelabRule.lean b/src/Iris/Std/DelabRule.lean index aef1a2056..f27dbe9bb 100644 --- a/src/Iris/Std/DelabRule.lean +++ b/src/Iris/Std/DelabRule.lean @@ -3,14 +3,19 @@ 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 -/ -import Lean.PrettyPrinter.Delaborator +module + +public meta import Lean.PrettyPrinter.Delaborator +public meta import Lean.Parser.Term + +public meta section namespace Iris.Std open Lean Lean.Macro -- macro for adding unexpanders for function applications open Lean.Parser.Term in -private def matchAlts' := leading_parser matchAlts +def matchAlts' := leading_parser matchAlts syntax "delab_rule" ident matchAlts' : command macro_rules @@ -24,10 +29,10 @@ macro_rules if p.any fun t : TSyntax _ ↦ t matches `(`($$_)) then `(@[app_unexpander $(mkIdent f)] - def unexpand : Lean.PrettyPrinter.Unexpander + meta def unexpand : Lean.PrettyPrinter.Unexpander $[| $p => $s]*) else `(@[app_unexpander $(mkIdent f)] - def unexpand : Lean.PrettyPrinter.Unexpander + meta def unexpand : Lean.PrettyPrinter.Unexpander $[| $p => $s]* | _ => throw ()) diff --git a/src/Iris/Std/Equivalence.lean b/src/Iris/Std/Equivalence.lean index c993fdf49..878b8b8ea 100644 --- a/src/Iris/Std/Equivalence.lean +++ b/src/Iris/Std/Equivalence.lean @@ -3,5 +3,8 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + +@[expose] public section theorem equivalence_eq : Equivalence (@Eq α) := ⟨.refl, .symm, .trans⟩ diff --git a/src/Iris/Std/Expr.lean b/src/Iris/Std/Expr.lean index 52757c398..defa01aa1 100644 --- a/src/Iris/Std/Expr.lean +++ b/src/Iris/Std/Expr.lean @@ -3,8 +3,12 @@ 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 -/ -import Lean.Expr -import Lean.Meta +module + +public import Lean.Expr +public import Lean.Meta + +@[expose] public section namespace Lean.Expr open Lean.Meta diff --git a/src/Iris/Std/HeapInstances.lean b/src/Iris/Std/HeapInstances.lean index e7d6660a1..2d9f08ac2 100644 --- a/src/Iris/Std/HeapInstances.lean +++ b/src/Iris/Std/HeapInstances.lean @@ -3,11 +3,12 @@ Copyright (c) 2025 Alok Singh. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Alok Singh, Markus de Medeiros -/ +module -import Iris.Std.PartialMap -import Iris.Std.Infinite -import Std.Data.TreeMap -import Std.Data.ExtTreeMap +public import Iris.Std.PartialMap +public import Iris.Std.Infinite +public import Std.Data.TreeMap +public import Std.Data.ExtTreeMap /-! # Heap Instances for Standard Types @@ -24,6 +25,8 @@ instances for types from the Lean standard library. - `ExtTreeMap`: `PartialMap` -/ +@[expose] public section + namespace Iris.Std /-! ## Function PartialMap Instance -/ diff --git a/src/Iris/Std/Infinite.lean b/src/Iris/Std/Infinite.lean index f41dc0e68..4897b434b 100644 --- a/src/Iris/Std/Infinite.lean +++ b/src/Iris/Std/Infinite.lean @@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module + +@[expose] public section /-- A set S is infinite if there exists an injection from Nat into the set of elements such that S holds. -/ diff --git a/src/Iris/Std/Nat.lean b/src/Iris/Std/Nat.lean index 8a7302f4c..4ea7f7a41 100644 --- a/src/Iris/Std/Nat.lean +++ b/src/Iris/Std/Nat.lean @@ -3,6 +3,10 @@ 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 -/ +module + +@[expose] public section + namespace Nat theorem eq_of_not_lt_not_lt {a b : Nat} : ¬(a < b) → ¬(b < a) → a = b := by diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean index ea687dc93..62fcf462c 100644 --- a/src/Iris/Std/PartialMap.lean +++ b/src/Iris/Std/PartialMap.lean @@ -3,6 +3,7 @@ Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zongyuan Liu, Markus de Medeiros -/ +module /-! ## Partial Maps @@ -23,7 +24,7 @@ that the resource algebra construction only applies to these types anyways. The PartialMap interface does not require that the representation of a partial map be unique, ie. all constructions reason extensionally about the get? function rather than intensionally about map equalities. PartialMaps are free to be non-uniquely represented. --/ +-/@[expose] public section namespace Iris.Std /-- Base typeclass for partial maps: maps from keys `K` to optional values `V`. -/ diff --git a/src/Iris/Std/Prod.lean b/src/Iris/Std/Prod.lean index 6a0df6fb8..5a9729e01 100644 --- a/src/Iris/Std/Prod.lean +++ b/src/Iris/Std/Prod.lean @@ -3,6 +3,10 @@ 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 -/ +module + +@[expose] public section + namespace Prod /-- Apply `f` to all elements of a tuple. All elements of the tuple must have the same type `α`. -/ diff --git a/src/Iris/Std/Qq.lean b/src/Iris/Std/Qq.lean index c16e896da..41b962dbd 100644 --- a/src/Iris/Std/Qq.lean +++ b/src/Iris/Std/Qq.lean @@ -3,7 +3,11 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Qq +module + +public import Qq + +@[expose] public section open Qq instance : Inhabited (QuotedDefEq a b) := ⟨⟨⟩⟩ diff --git a/src/Iris/Std/Rewrite.lean b/src/Iris/Std/Rewrite.lean index 5fa2410f3..25d2794a2 100644 --- a/src/Iris/Std/Rewrite.lean +++ b/src/Iris/Std/Rewrite.lean @@ -3,10 +3,14 @@ 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 -/ -import Iris.Std.Classes -import Iris.Std.Tactic +module -import Lean.Elab.Tactic +public import Iris.Std.Classes +public meta import Iris.Std.Tactic + +public meta import Lean.Elab.Tactic + +public meta section namespace Iris.Std open Lean Lean.Elab Lean.Elab.Tactic Lean.Meta Lean.Parser.Tactic diff --git a/src/Iris/Std/Set.lean b/src/Iris/Std/Set.lean index 6ec6222ef..c4f1818b8 100644 --- a/src/Iris/Std/Set.lean +++ b/src/Iris/Std/Set.lean @@ -3,7 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus de Medeiros -/ +module +@[expose] public section namespace Set diff --git a/src/Iris/Std/TC.lean b/src/Iris/Std/TC.lean index f55d0f416..6ce7579b1 100644 --- a/src/Iris/Std/TC.lean +++ b/src/Iris/Std/TC.lean @@ -3,6 +3,10 @@ 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 -/ +module + +@[expose] public section + namespace Iris.Std set_option checkBinderAnnotations false diff --git a/src/Iris/Std/Tactic.lean b/src/Iris/Std/Tactic.lean index 416e06a7e..ac69f46e8 100644 --- a/src/Iris/Std/Tactic.lean +++ b/src/Iris/Std/Tactic.lean @@ -3,8 +3,12 @@ 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 -/ -import Lean.Elab.Tactic -import Lean.Meta.Tactic.Util +module + +public meta import Lean.Elab.Tactic +public meta import Lean.Meta.Tactic.Util + +public meta section namespace Iris.Std open Lean Lean.Elab.Tactic Lean.Meta diff --git a/src/Iris/Std/Try.lean b/src/Iris/Std/Try.lean index 40a9494c6..5466baffd 100644 --- a/src/Iris/Std/Try.lean +++ b/src/Iris/Std/Try.lean @@ -3,6 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ +module + +@[expose] public section namespace Iris.ProofMode diff --git a/src/Iris/Tests.lean b/src/Iris/Tests.lean index a5dd1ca4f..8ea520df2 100644 --- a/src/Iris/Tests.lean +++ b/src/Iris/Tests.lean @@ -1,3 +1,5 @@ -import Iris.Tests.Instances -import Iris.Tests.Notation -import Iris.Tests.Tactics +module + +public import Iris.Tests.Instances +public import Iris.Tests.Notation +public import Iris.Tests.Tactics diff --git a/src/Iris/Tests/Instances.lean b/src/Iris/Tests/Instances.lean index 78dac4c0b..a23f0d491 100644 --- a/src/Iris/Tests/Instances.lean +++ b/src/Iris/Tests/Instances.lean @@ -3,8 +3,12 @@ Copyright (c) 2025 Michael Sammler. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michael Sammler -/ -import Iris.BI -import Iris.ProofMode +module + +public import Iris.BI +public import Iris.ProofMode + +@[expose] public section namespace Iris.Tests open BI ProofMode diff --git a/src/Iris/Tests/Notation.lean b/src/Iris/Tests/Notation.lean index a60467191..3eb1eec2d 100644 --- a/src/Iris/Tests/Notation.lean +++ b/src/Iris/Tests/Notation.lean @@ -3,7 +3,11 @@ 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 -/ -import Iris.BI.BIBase +module + +public import Iris.BI.BIBase + +@[expose] public section namespace Iris.Tests open Iris.BI diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean index ed8c26046..7ed08f415 100644 --- a/src/Iris/Tests/Tactics.lean +++ b/src/Iris/Tests/Tactics.lean @@ -3,8 +3,12 @@ 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, Oliver Soeser, Michael Sammler -/ -import Iris.BI -import Iris.ProofMode +module + +public import Iris.BI +public import Iris.ProofMode + +@[expose] public section namespace Iris.Tests open Iris.BI From 2d96279eb3710ed2610fb6302b3574541fd65410 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Mon, 2 Mar 2026 13:39:12 +0100 Subject: [PATCH 2/7] Make helper functions private --- src/Iris/ProofMode/Tactics/Apply.lean | 2 +- src/Iris/ProofMode/Tactics/Cases.lean | 14 +++++++------- src/Iris/ProofMode/Tactics/HaveCore.lean | 2 +- src/Iris/ProofMode/Tactics/Intro.lean | 2 +- src/Iris/ProofMode/Tactics/ModIntro.lean | 8 ++++---- src/Iris/ProofMode/Tactics/Specialize.lean | 4 ++-- src/Iris/ProofMode/Tactics/Split.lean | 2 +- 7 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean index 3e0033dba..10a13ebab 100644 --- a/src/Iris/ProofMode/Tactics/Apply.lean +++ b/src/Iris/ProofMode/Tactics/Apply.lean @@ -29,7 +29,7 @@ Apply a hypothesis `A` to the `goal` by eliminating the wands recursively ## Returns The proof of `hyps ∗ □?p A ⊢ goal` -/ -partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (p : Q(Bool)) (A : Q($prop)) (goal : Q($prop)) : ProofModeM Q($e ∗ □?$p $A ⊢ $goal) := do +private partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (p : Q(Bool)) (A : Q($prop)) (goal : Q($prop)) : ProofModeM Q($e ∗ □?$p $A ⊢ $goal) := do let B ← mkFreshExprMVarQ q($prop) -- if `A := ?B -∗ goal`, add `B` as a new subgoal and conclude `goal` if let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $A .out $B .in $goal) then diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean index 1af929932..c09f9b4ab 100644 --- a/src/Iris/ProofMode/Tactics/Cases.lean +++ b/src/Iris/ProofMode/Tactics/Cases.lean @@ -21,7 +21,7 @@ open Lean Elab Tactic Meta Qq BI Std theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q := wand_elim' <| intuitionisticallyIf_elim.trans false_elim -def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) +private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) {P} (_hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool)) (_k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do @@ -35,7 +35,7 @@ theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : Int (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h) -def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) +private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (name : TSyntax ``binderIdent) (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do @@ -62,7 +62,7 @@ theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h -def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool) +private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool) (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) : ProofModeM (Option Q($P ∗ □?$p $A' ⊢ $Q)) := do let A1 ← mkFreshExprMVarQ q($prop) @@ -85,7 +85,7 @@ theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd t (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <| sep_assoc.2.trans <| wand_elim h -def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) +private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool)) (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) (k1 k2 : ∀ {P}, Hyps bi P → (Q B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → @@ -115,7 +115,7 @@ theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2] (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2 -def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) +private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (k1 k2 : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do let A1 ← mkFreshExprMVarQ q($prop) @@ -135,7 +135,7 @@ theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP} theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A'] (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h -def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) +private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (k : (B' : Q($prop)) → ProofModeM Q($P ∗ □ $B' ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do let B' ← mkFreshExprMVarQ q($prop) @@ -153,7 +153,7 @@ theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p] (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q := (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h -def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) +private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (k : (B' : Q($prop)) → ProofModeM Q($P ∗ $B' ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do let B' ← mkFreshExprMVarQ q($prop) diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean index 8bdc44979..a0f656566 100644 --- a/src/Iris/ProofMode/Tactics/HaveCore.lean +++ b/src/Iris/ProofMode/Tactics/HaveCore.lean @@ -41,7 +41,7 @@ A tuple containing: - `out`: Asserted proposition - `pf`: Proof of `hyps ⊢ hyps' ∗ □?p out` -/ -def iHaveCore {e} (hyps : @Hyps u prop bi e) +private def iHaveCore {e} (hyps : @Hyps u prop bi e) (tm : Term) (keep : Bool) (mayPostpone : Bool) : ProofModeM ((e' : _) × Hyps bi e' × (p : Q(Bool)) × (out : Q($prop)) × Q($e ⊢ $e' ∗ □?$p $out)) := do if let some uniq ← try? <| hyps.findWithInfo ⟨tm⟩ then diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean index 7dd3317d3..537ff197d 100644 --- a/src/Iris/ProofMode/Tactics/Intro.lean +++ b/src/Iris/ProofMode/Tactics/Intro.lean @@ -49,7 +49,7 @@ theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP} theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans from_wand -partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} +private partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) : ProofModeM (Q($P ⊢ $Q)) := do match pats with diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean index e9f0278cb..e195c459b 100644 --- a/src/Iris/ProofMode/Tactics/ModIntro.lean +++ b/src/Iris/ProofMode/Tactics/ModIntro.lean @@ -21,7 +21,7 @@ inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where | clear | id -def ModalityActionQ.parse {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) : +private def parseModalityActionQ {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) : ProofModeM (ModalityActionQ prop1 prop2) := do let act ← whnf q($act) match_expr act with @@ -84,7 +84,7 @@ A tuple containing: - Transformed context `hyps'` in `prop1` - Proof of `hyps ⊢ M hyps'` -/ -def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e} +private def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e} (hyps : @Hyps u prop2 bi2 e) (M : Q(Modality $prop1 $prop2)) (act : Bool → ModalityActionQ prop1 prop2) : ProofModeM ((e' : _) × Hyps bi1 e' × Q($e ⊢ $(M).M $e')) := match hyps with @@ -161,8 +161,8 @@ def iModIntroCore {e} (hyps : @Hyps u prop bi e) (goal : Q($prop)) (sel : TSynta let hΦ ← mkFreshExprMVarQ q($Φ) iSolveSideconditionAt hΦ.mvarId! -- pre-compute the actions - let iact ← ModalityActionQ.parse q($(M).action true) - let sact ← ModalityActionQ.parse q($(M).action false) + let iact ← parseModalityActionQ q($(M).action true) + let sact ← parseModalityActionQ q($(M).action false) -- perform modality actions, get transformed context `hyps'` and `pf : hyps ⊢ M hyps'` let ⟨_, hyps', pf⟩ ← iModAction hyps M (λ p => if p then iact else sact) -- get proof `hyps' ⊢ Q` diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean index ad6370a7e..52215dc9e 100644 --- a/src/Iris/ProofMode/Tactics/Specialize.lean +++ b/src/Iris/ProofMode/Tactics/Specialize.lean @@ -41,7 +41,7 @@ theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} { [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a) := by refine h.trans <| sep_mono_r <| intuitionisticallyIf_mono <| inst.1.trans (forall_elim a) -def SpecializeState.process_wand : +private def processWand : @SpecializeState u prop bi orig → SpecPat → ProofModeM (SpecializeState bi orig) | { hyps, p, out, pf, .. }, .ident i => do let uniq ← hyps.findWithInfo i @@ -120,7 +120,7 @@ A tuple containing: def iSpecializeCore {e} (hyps : @Hyps u prop bi e) (pa : Q(Bool)) (A : Q($prop)) (spats : List SpecPat) (try_dup_context : Bool := false) : ProofModeM ((e' : _) × Hyps bi e' × (pb : Q(Bool)) × (B : Q($prop)) × Q($e ∗ □?$pa $A ⊢ $e' ∗ □?$pb $B)) := do let state := { hyps, out := A, p := pa, pf := q(.rfl), .. } - let ⟨_, hyps', pb, B, pf⟩ ← spats.foldlM SpecializeState.process_wand state + let ⟨_, hyps', pb, B, pf⟩ ← spats.foldlM processWand state if try_dup_context then -- context duplication succeeds if `B` is persistent, and `A` is persistent or affine let B' : Q($prop) ← mkFreshExprMVarQ q($prop) diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean index 7cfc9d725..4147e4511 100644 --- a/src/Iris/ProofMode/Tactics/Split.lean +++ b/src/Iris/ProofMode/Tactics/Split.lean @@ -33,7 +33,7 @@ theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] inductive splitSide where | splitLeft | splitRight -def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do +private def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do let splitRight := match side with | .splitLeft => false | .splitRight => true From fbf42cd421a4b17c43ba91ddf65921967caa1687 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Mon, 2 Mar 2026 14:20:18 +0100 Subject: [PATCH 3/7] Split ProofMode files into non-meta and meta sections --- src/Iris/ProofMode/Tactics/Apply.lean | 14 ++++++++++++-- src/Iris/ProofMode/Tactics/Assumption.lean | 14 ++++++++++++-- src/Iris/ProofMode/Tactics/Clear.lean | 14 ++++++++++++-- src/Iris/ProofMode/Tactics/ExFalso.lean | 13 +++++++++++-- src/Iris/ProofMode/Tactics/Exists.lean | 14 ++++++++++++-- src/Iris/ProofMode/Tactics/Have.lean | 17 +++++++++++++---- src/Iris/ProofMode/Tactics/HaveCore.lean | 16 +++++++++++++--- src/Iris/ProofMode/Tactics/LeftRight.lean | 22 ++++++++++++++++------ src/Iris/ProofMode/Tactics/Mod.lean | 14 ++++++++++++-- src/Iris/ProofMode/Tactics/Split.lean | 22 ++++++++++++++++------ 10 files changed, 129 insertions(+), 31 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean index 10a13ebab..dc3cde878 100644 --- a/src/Iris/ProofMode/Tactics/Apply.lean +++ b/src/Iris/ProofMode/Tactics/Apply.lean @@ -5,20 +5,30 @@ Authors: Oliver Soeser, Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Patterns.ProofModeTerm public meta import Iris.ProofMode.Tactics.Assumption public meta import Iris.ProofMode.Tactics.HaveCore -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Iris.BI theorem apply [BI PROP] {p} {P Q Q1 R : PROP} (h1 : P ⊢ Q1) [h2 : IntoWand p false Q .out Q1 .in R] : P ∗ □?p Q ⊢ R := (Entails.trans (sep_mono_l h1) (wand_elim' h2.1)) +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + /-- Apply a hypothesis `A` to the `goal` by eliminating the wands recursively diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean index d30d73c7f..da7d52f1d 100644 --- a/src/Iris/ProofMode/Tactics/Assumption.lean +++ b/src/Iris/ProofMode/Tactics/Assumption.lean @@ -5,17 +5,27 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Iris.BI Iris.Std theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p .in A Q] [TCOr (Affine P') (Absorbing Q)] (h : P ⊣⊢ P' ∗ □?p A) : P ⊢ Q := h.1.trans <| (sep_mono_r inst.1).trans sep_elim_r +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + elab "iassumption" : tactic => do ProofModeM.runTactic λ mvar { hyps, goal, .. } => do diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean index add233254..1f8f183fa 100644 --- a/src/Iris/ProofMode/Tactics/Clear.lean +++ b/src/Iris/ProofMode/Tactics/Clear.lean @@ -5,12 +5,14 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Iris.BI Iris.Std theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)] (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q := @@ -19,6 +21,14 @@ theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q) theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP} (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q := clear_spatial h_rem h +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) (p : Q(Bool)) (out goal : Q($prop)) (pf : Q($e ⊣⊢ $e' ∗ □?$p $out)) : ProofModeM Q(($e' ⊢ $goal) → $e ⊢ $goal) := do diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean index 649ee89c4..e59bdefc8 100644 --- a/src/Iris/ProofMode/Tactics/ExFalso.lean +++ b/src/Iris/ProofMode/Tactics/ExFalso.lean @@ -5,15 +5,24 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module +public import Iris.BI public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab.Tactic Meta Qq BI +open Iris.BI theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab.Tactic Meta Qq BI + elab "iexfalso" : tactic => do ProofModeM.runTactic λ mvar { hyps, goal, .. } => do let m ← addBIGoal hyps q(iprop(False)) diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean index 5d3337e2c..1cb745df7 100644 --- a/src/Iris/ProofMode/Tactics/Exists.lean +++ b/src/Iris/ProofMode/Tactics/Exists.lean @@ -5,17 +5,27 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI +open Iris.BI theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ] (a : α) (h : P ⊢ Q) : Φ a ⊢ Q := ((exists_intro a).trans inst.1).trans h +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI + elab "iexists" xs:term,+ : tactic => do -- resolve existential quantifier with the given argument ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean index d45382c37..a50182804 100644 --- a/src/Iris/ProofMode/Tactics/Have.lean +++ b/src/Iris/ProofMode/Tactics/Have.lean @@ -5,22 +5,31 @@ Authors: Michael Sammler -/ module +public import Iris.BI public meta import Iris.ProofMode.Patterns.CasesPattern public meta import Iris.ProofMode.Tactics.HaveCore public meta import Iris.ProofMode.Tactics.Cases -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std - -macro "ihave" colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icases +keep $pmt with $pat) +open Iris.BI theorem ihave_assert [BI PROP] {A B C : PROP} (h1 : A ∗ □ (B -∗ B) ⊢ C) : A ⊢ C := (and_intro .rfl (persistently_emp_intro.trans (persistently_mono $ wand_intro emp_sep.1))).trans $ persistently_and_intuitionistically_sep_r.1.trans h1 +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + +macro "ihave" colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icases +keep $pmt with $pat) + elab "ihave" colGt pat:icasesPat " : " P:term "$$" spat:specPat : tactic => do let spat ← liftMacroM <| SpecPat.parse spat let pat ← liftMacroM <| iCasesPat.parse pat diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean index a0f656566..aed8b4d0d 100644 --- a/src/Iris/ProofMode/Tactics/HaveCore.lean +++ b/src/Iris/ProofMode/Tactics/HaveCore.lean @@ -5,25 +5,35 @@ Authors: Michael Sammler, Zongyuan Liu -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Patterns.ProofModeTerm public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.Specialize -public meta section - /- This file contains the `iHave` function for asserting a ProofModeTerm. It is separate from the implementation of `ihave` in `Have.lean` since the `ihave` tactic in (`Have.lean`) depends on `Cases.lean`, which in turn depends on `iHave` in this file. -/ +@[expose] public section + namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Iris.BI theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP} [h1 : AsEmpValid .into φ P] (h : φ) : Q ⊢ Q ∗ □ P := sep_emp.2.trans (sep_mono_r $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h))) +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + /-- Assert a hypothesis from either a hypothesis name or a Lean proof term `tm`. diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean index 70059c21b..42766f5fb 100644 --- a/src/Iris/ProofMode/Tactics/LeftRight.lean +++ b/src/Iris/ProofMode/Tactics/LeftRight.lean @@ -5,17 +5,31 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab.Tactic Meta Qq BI Std +open Iris.BI theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A1) : P ⊢ Q := (or_intro_l' h1).trans inst.1 +theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] + (h1 : P ⊢ A2) : P ⊢ Q := + (or_intro_r' h1).trans inst.1 + +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab.Tactic Meta Qq BI Std + elab "ileft" : tactic => do ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do -- choose left side of disjunction @@ -27,10 +41,6 @@ elab "ileft" : tactic => do let m : Q($e ⊢ $A1) ← addBIGoal hyps A1 mvar.assign q(from_or_l (Q := $goal) $m) -theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] - (h1 : P ⊢ A2) : P ⊢ Q := - (or_intro_r' h1).trans inst.1 - elab "iright" : tactic => do ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do -- choose right side of disjunction diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean index 083d89c43..84dddbb46 100644 --- a/src/Iris/ProofMode/Tactics/Mod.lean +++ b/src/Iris/ProofMode/Tactics/Mod.lean @@ -5,17 +5,27 @@ Authors: Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Iris.BI theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q'] (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q := (sep_comm.1.trans (sep_mono_r (wand_intro h1))).trans (he.1 hΦ) +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + /-- Eliminate a modality from `A` by transforming the goal from `P ∗ □?p A ⊢ Q` to `P ∗ □?p' A' ⊢ Q'`, where `p'`, `A'`, and `Q'` are determined by `ElimModal`. diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean index 4147e4511..c24e6153b 100644 --- a/src/Iris/ProofMode/Tactics/Split.lean +++ b/src/Iris/ProofMode/Tactics/Split.lean @@ -5,17 +5,31 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module +public import Iris.BI +public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public meta section +@[expose] public section namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI +open Iris.BI theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2] (h1 : P ⊢ A1) (h2 : P ⊢ A2) : P ⊢ Q := (and_intro h1 h2).trans inst.1 +theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] + (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q := + h.1.trans <| (sep_mono h1 h2).trans inst.1 + +end Iris.ProofMode +end + +public meta section + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI + elab "isplit" : tactic => do ProofModeM.runTactic λ mvar { prop, hyps, goal, .. } => do @@ -26,10 +40,6 @@ elab "isplit" : tactic => do let m2 ← addBIGoal hyps A2 mvar.assign q(from_and_intro (Q := $goal) $m1 $m2) -theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] - (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q := - h.1.trans <| (sep_mono h1 h2).trans inst.1 - inductive splitSide where | splitLeft | splitRight From 952082e3a70c3048b8c3f43b57ab873ef239ef87 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Mon, 2 Mar 2026 14:46:19 +0100 Subject: [PATCH 4/7] Tightening --- src/Iris/ProofMode/Tactics/Apply.lean | 2 +- src/Iris/ProofMode/Tactics/Assumption.lean | 2 +- src/Iris/ProofMode/Tactics/Clear.lean | 2 +- src/Iris/ProofMode/Tactics/ExFalso.lean | 2 +- src/Iris/ProofMode/Tactics/Exists.lean | 2 +- src/Iris/ProofMode/Tactics/Have.lean | 2 +- src/Iris/ProofMode/Tactics/HaveCore.lean | 2 +- src/Iris/ProofMode/Tactics/LeftRight.lean | 2 +- src/Iris/ProofMode/Tactics/Mod.lean | 2 +- src/Iris/ProofMode/Tactics/Split.lean | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean index dc3cde878..1d68ebb14 100644 --- a/src/Iris/ProofMode/Tactics/Apply.lean +++ b/src/Iris/ProofMode/Tactics/Apply.lean @@ -11,7 +11,7 @@ public meta import Iris.ProofMode.Patterns.ProofModeTerm public meta import Iris.ProofMode.Tactics.Assumption public meta import Iris.ProofMode.Tactics.HaveCore -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean index da7d52f1d..49df135b6 100644 --- a/src/Iris/ProofMode/Tactics/Assumption.lean +++ b/src/Iris/ProofMode/Tactics/Assumption.lean @@ -9,7 +9,7 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI Iris.Std diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean index 1f8f183fa..968e85627 100644 --- a/src/Iris/ProofMode/Tactics/Clear.lean +++ b/src/Iris/ProofMode/Tactics/Clear.lean @@ -9,7 +9,7 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI Iris.Std diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean index e59bdefc8..108953e1b 100644 --- a/src/Iris/ProofMode/Tactics/ExFalso.lean +++ b/src/Iris/ProofMode/Tactics/ExFalso.lean @@ -8,7 +8,7 @@ module public import Iris.BI public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean index 1cb745df7..bb9aec1c8 100644 --- a/src/Iris/ProofMode/Tactics/Exists.lean +++ b/src/Iris/ProofMode/Tactics/Exists.lean @@ -9,7 +9,7 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean index a50182804..16f98c538 100644 --- a/src/Iris/ProofMode/Tactics/Have.lean +++ b/src/Iris/ProofMode/Tactics/Have.lean @@ -10,7 +10,7 @@ public meta import Iris.ProofMode.Patterns.CasesPattern public meta import Iris.ProofMode.Tactics.HaveCore public meta import Iris.ProofMode.Tactics.Cases -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean index aed8b4d0d..5b5418b4b 100644 --- a/src/Iris/ProofMode/Tactics/HaveCore.lean +++ b/src/Iris/ProofMode/Tactics/HaveCore.lean @@ -17,7 +17,7 @@ public meta import Iris.ProofMode.Tactics.Specialize depends on `iHave` in this file. -/ -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean index 42766f5fb..708b2c6ba 100644 --- a/src/Iris/ProofMode/Tactics/LeftRight.lean +++ b/src/Iris/ProofMode/Tactics/LeftRight.lean @@ -9,7 +9,7 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean index 84dddbb46..000437219 100644 --- a/src/Iris/ProofMode/Tactics/Mod.lean +++ b/src/Iris/ProofMode/Tactics/Mod.lean @@ -9,7 +9,7 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean index c24e6153b..3589b60da 100644 --- a/src/Iris/ProofMode/Tactics/Split.lean +++ b/src/Iris/ProofMode/Tactics/Split.lean @@ -9,7 +9,7 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -@[expose] public section +public section namespace Iris.ProofMode open Iris.BI From eeacb4c8dc848e047ec5d8faa723dd957732bd82 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Mon, 2 Mar 2026 15:08:20 +0100 Subject: [PATCH 5/7] Tweaks --- src/Iris/ProofMode/Tactics/Apply.lean | 13 +--- src/Iris/ProofMode/Tactics/Assumption.lean | 12 +-- src/Iris/ProofMode/Tactics/Cases.lean | 87 +++++++++++----------- src/Iris/ProofMode/Tactics/Clear.lean | 13 +--- src/Iris/ProofMode/Tactics/ExFalso.lean | 13 +--- src/Iris/ProofMode/Tactics/Exact.lean | 4 +- src/Iris/ProofMode/Tactics/Exists.lean | 13 +--- src/Iris/ProofMode/Tactics/Have.lean | 13 +--- src/Iris/ProofMode/Tactics/HaveCore.lean | 12 +-- src/Iris/ProofMode/Tactics/Intro.lean | 9 ++- src/Iris/ProofMode/Tactics/LeftRight.lean | 13 +--- src/Iris/ProofMode/Tactics/Mod.lean | 13 +--- src/Iris/ProofMode/Tactics/ModIntro.lean | 39 +++++----- src/Iris/ProofMode/Tactics/Pure.lean | 10 ++- src/Iris/ProofMode/Tactics/Rename.lean | 4 +- src/Iris/ProofMode/Tactics/Specialize.lean | 35 +++++---- src/Iris/ProofMode/Tactics/Split.lean | 13 +--- 17 files changed, 139 insertions(+), 177 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean index 1d68ebb14..da37d0f12 100644 --- a/src/Iris/ProofMode/Tactics/Apply.lean +++ b/src/Iris/ProofMode/Tactics/Apply.lean @@ -11,23 +11,18 @@ public meta import Iris.ProofMode.Patterns.ProofModeTerm public meta import Iris.ProofMode.Tactics.Assumption public meta import Iris.ProofMode.Tactics.HaveCore -public section - namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem apply [BI PROP] {p} {P Q Q1 R : PROP} (h1 : P ⊢ Q1) [h2 : IntoWand p false Q .out Q1 .in R] : P ∗ □?p Q ⊢ R := (Entails.trans (sep_mono_l h1) (wand_elim' h2.1)) -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Lean Elab Tactic Meta Qq Std /-- Apply a hypothesis `A` to the `goal` by eliminating the wands recursively diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean index 49df135b6..f7b9d7d07 100644 --- a/src/Iris/ProofMode/Tactics/Assumption.lean +++ b/src/Iris/ProofMode/Tactics/Assumption.lean @@ -9,22 +9,16 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI Iris.Std +public section +open BI Std theorem assumption [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p .in A Q] [TCOr (Affine P') (Absorbing Q)] (h : P ⊣⊢ P' ∗ □?p A) : P ⊢ Q := h.1.trans <| (sep_mono_r inst.1).trans sep_elim_r -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Lean Elab Tactic Meta Qq elab "iassumption" : tactic => do ProofModeM.runTactic λ mvar { hyps, goal, .. } => do diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean index c09f9b4ab..8682013e2 100644 --- a/src/Iris/ProofMode/Tactics/Cases.lean +++ b/src/Iris/ProofMode/Tactics/Cases.lean @@ -13,14 +13,55 @@ public meta import Iris.ProofMode.Tactics.Pure public meta import Iris.ProofMode.Tactics.HaveCore public meta import Iris.ProofMode.Tactics.Mod -public meta section - namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std + +public section +open BI Std theorem false_elim' [BI PROP] {P Q : PROP} : P ∗ □?p False ⊢ Q := wand_elim' <| intuitionisticallyIf_elim.trans false_elim +theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ] + (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q := + (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h) + +theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] + (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q := + (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_l).trans h + +theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] + (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := + (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h + +theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2] + (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q := + (sep_mono_r inst.1).trans <| sep_assoc.2.trans <| wand_elim h + +theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2] + (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q := + (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <| + sep_assoc.2.trans <| wand_elim h + +theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2] + (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := + (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2 + +theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP} + [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)] + (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h + +theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A'] + (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h + +theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p] + (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q := + (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h + +theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h + +public meta section +open Lean Elab Tactic Meta Qq Std + private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) {P} (_hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool)) (_k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) : @@ -30,11 +71,6 @@ private def iCasesEmptyConj {prop : Q(Type u)} (bi : Q(BI $prop)) else throwError "icases: cannot destruct {A'} as an empty conjunct" - -theorem exists_elim' [BI PROP] {p} {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ] - (h : ∀ a, P ∗ □?p Φ a ⊢ Q) : P ∗ □?p A ⊢ Q := - (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans intuitionisticallyIf_exists.1).trans <| sep_exists_l.1.trans (exists_elim h) - private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (name : TSyntax ``binderIdent) (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) : @@ -53,15 +89,6 @@ private def iCasesExists {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop let pf : Q(∀ x, $P ∗ □?$p $Φ x ⊢ $Q) ← mkLambdaFVars #[x] <|← k B B' ⟨⟩ return q(exists_elim' (A := $A') $pf) - -theorem sep_and_elim_l [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] - (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q := - (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_l).trans h - -theorem sep_and_elim_r [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] - (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := - (sep_mono_r <| inst.1.trans <| intuitionisticallyIf_mono and_elim_r).trans h - private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (right : Bool) (k : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) : ProofModeM (Option Q($P ∗ □?$p $A' ⊢ $Q)) := do @@ -76,15 +103,6 @@ private def iCasesAndLR {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop) have ⟨A1', _⟩ := mkIntuitionisticIf bi p A1 return some q(sep_and_elim_l $(← k A1' A1 ⟨⟩)) -theorem sep_elim_spatial [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2] - (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q := - (sep_mono_r inst.1).trans <| sep_assoc.2.trans <| wand_elim h - -theorem and_elim_intuitionistic [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2] - (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q := - (sep_mono_r <| inst.1.trans intuitionistically_and_sep.1).trans <| - sep_assoc.2.trans <| wand_elim h - private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) {P} (hyps : Hyps bi P) (Q A' : Q($prop)) (p : Q(Bool)) (k : ∀ {P}, Hyps bi P → ProofModeM Q($P ⊢ $Q)) @@ -111,10 +129,6 @@ private def iCasesSep {prop : Q(Type u)} (bi : Q(BI $prop)) return q(wand_intro $pf) return q(sep_elim_spatial (A := $A') $pf) -theorem or_elim' [BI PROP] {p} {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2] - (h1 : P ∗ □?p A1 ⊢ Q) (h2 : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q := - (sep_mono_r <| (intuitionisticallyIf_mono inst.1).trans (intuitionisticallyIf_or _).1).trans <| BI.sep_or_l.1.trans <| or_elim h1 h2 - private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (k1 k2 : (B B' : Q($prop)) → (_ : $B =Q iprop(□?$p $B')) → ProofModeM Q($P ∗ $B ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do @@ -128,13 +142,6 @@ private def iCasesOr {prop : Q(Type u)} (bi : Q(BI $prop)) (P Q A' : Q($prop)) ( let pf2 ← k2 A2' A2 ⟨⟩ return q(or_elim' (A := $A') $pf1 $pf2) -theorem intuitionistic_elim_spatial [BI PROP] {A A' Q : PROP} - [IntoPersistently false A A'] [TCOr (Affine A) (Absorbing Q)] - (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q := (replaces_r to_persistent_spatial).apply h - -theorem intuitionistic_elim_intuitionistic [BI PROP] {A A' Q : PROP} [IntoPersistently true A A'] - (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q := intuitionistic_elim_spatial h - private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (k : (B' : Q($prop)) → ProofModeM Q($P ∗ □ $B' ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do @@ -149,10 +156,6 @@ private def iCasesIntuitionistic {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' | throwError "icases: {A'} not affine and the goal not absorbing" return q(intuitionistic_elim_spatial (A := $A') $(← k B')) -theorem spatial_elim [BI PROP] {p} {A A' Q : PROP} [FromAffinely A' A p] - (h : P ∗ A' ⊢ Q) : P ∗ □?p A ⊢ Q := - (sep_mono_r <| (affinelyIf_of_intuitionisticallyIf).trans from_affinely).trans h - private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($prop)) (p : Q(Bool)) (k : (B' : Q($prop)) → ProofModeM Q($P ∗ $B' ⊢ $Q)) : ProofModeM (Q($P ∗ □?$p $A' ⊢ $Q)) := do @@ -161,8 +164,6 @@ private def iCasesSpatial {prop : Q(Type u)} (_bi : Q(BI $prop)) (P Q A' : Q($pr let _ ← ProofModeM.synthInstanceQ q(FromAffinely $B' $A' $p) return q(spatial_elim (A := $A') $(← k B')) -theorem of_emp_sep [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q := emp_sep.1.trans h - -- TODO: Why does this function require both A and A' instead of just A'? variable {u : Level} {prop : Q(Type u)} (bi : Q(BI $prop)) in partial def iCasesCore diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean index 968e85627..52e336ab4 100644 --- a/src/Iris/ProofMode/Tactics/Clear.lean +++ b/src/Iris/ProofMode/Tactics/Clear.lean @@ -9,10 +9,10 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI Iris.Std + +public section +open BI Std theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q)] (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q := @@ -21,13 +21,8 @@ theorem clear_spatial [BI PROP] {P P' A Q : PROP} [TCOr (Affine A) (Absorbing Q) theorem clear_intuitionistic [BI PROP] {P P' A Q : PROP} (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q := clear_spatial h_rem h -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Lean Elab Tactic Meta Qq def iClearCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (e e' : Q($prop)) (p : Q(Bool)) (out goal : Q($prop)) diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean index 108953e1b..47333ad30 100644 --- a/src/Iris/ProofMode/Tactics/ExFalso.lean +++ b/src/Iris/ProofMode/Tactics/ExFalso.lean @@ -8,20 +8,15 @@ module public import Iris.BI public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI -theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim +public section +open BI -end Iris.ProofMode -end +theorem exfalso [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q := h.trans false_elim public meta section - -namespace Iris.ProofMode -open Lean Elab.Tactic Meta Qq BI +open Lean Elab.Tactic Meta Qq elab "iexfalso" : tactic => do ProofModeM.runTactic λ mvar { hyps, goal, .. } => do diff --git a/src/Iris/ProofMode/Tactics/Exact.lean b/src/Iris/ProofMode/Tactics/Exact.lean index ac1378b35..a86e85246 100644 --- a/src/Iris/ProofMode/Tactics/Exact.lean +++ b/src/Iris/ProofMode/Tactics/Exact.lean @@ -8,9 +8,9 @@ module public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.Assumption -public meta section - namespace Iris.ProofMode + +public meta section open Lean Elab Tactic Meta Qq BI Std elab "iexact" colGt hyp:ident : tactic => do diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean index bb9aec1c8..86a5982df 100644 --- a/src/Iris/ProofMode/Tactics/Exists.lean +++ b/src/Iris/ProofMode/Tactics/Exists.lean @@ -9,22 +9,17 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem exists_intro' [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists P Φ] (a : α) (h : P ⊢ Q) : Φ a ⊢ Q := ((exists_intro a).trans inst.1).trans h -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI +open Lean Elab Tactic Meta Qq elab "iexists" xs:term,+ : tactic => do -- resolve existential quantifier with the given argument diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean index 16f98c538..4ab6ccc2c 100644 --- a/src/Iris/ProofMode/Tactics/Have.lean +++ b/src/Iris/ProofMode/Tactics/Have.lean @@ -10,23 +10,18 @@ public meta import Iris.ProofMode.Patterns.CasesPattern public meta import Iris.ProofMode.Tactics.HaveCore public meta import Iris.ProofMode.Tactics.Cases -public section - namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem ihave_assert [BI PROP] {A B C : PROP} (h1 : A ∗ □ (B -∗ B) ⊢ C) : A ⊢ C := (and_intro .rfl (persistently_emp_intro.trans (persistently_mono $ wand_intro emp_sep.1))).trans $ persistently_and_intuitionistically_sep_r.1.trans h1 -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Lean Elab Tactic Meta Qq macro "ihave" colGt pat:icasesPat " := " pmt:pmTerm : tactic => `(tactic | icases +keep $pmt with $pat) diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean index 5b5418b4b..7a428ff5b 100644 --- a/src/Iris/ProofMode/Tactics/HaveCore.lean +++ b/src/Iris/ProofMode/Tactics/HaveCore.lean @@ -17,22 +17,18 @@ public meta import Iris.ProofMode.Tactics.Specialize depends on `iHave` in this file. -/ -public section namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem have_asEmpValid [BI PROP] {φ} {P Q : PROP} [h1 : AsEmpValid .into φ P] (h : φ) : Q ⊢ Q ∗ □ P := sep_emp.2.trans (sep_mono_r $ intuitionistically_emp.2.trans (intuitionistically_mono (asEmpValid_1 _ h))) -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Lean Elab Tactic Meta Qq Std /-- Assert a hypothesis from either a hypothesis name or a Lean proof term `tm`. diff --git a/src/Iris/ProofMode/Tactics/Intro.lean b/src/Iris/ProofMode/Tactics/Intro.lean index 537ff197d..96afab0d4 100644 --- a/src/Iris/ProofMode/Tactics/Intro.lean +++ b/src/Iris/ProofMode/Tactics/Intro.lean @@ -9,10 +9,10 @@ public meta import Iris.ProofMode.Patterns.IntroPattern public meta import Iris.ProofMode.Tactics.Cases public meta import Iris.ProofMode.Tactics.ModIntro -public meta section - namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std + +public section +open BI Std theorem imp_intro_drop [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q := BI.imp_intro (and_elim_l' h) |>.trans inst.1 @@ -49,6 +49,9 @@ theorem imp_intro_spatial [BI PROP] {P Q A1 A2 B : PROP} theorem wand_intro_spatial [BI PROP] {P Q A1 A2 : PROP} [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q := (wand_intro h).trans from_wand +public meta section +open Lean Elab Tactic Meta Qq BI Std + private partial def iIntroCore {prop : Q(Type u)} {bi : Q(BI $prop)} {P} (hyps : Hyps bi P) (Q : Q($prop)) (pats : List (Syntax × IntroPat)) : ProofModeM (Q($P ⊢ $Q)) := do diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean index 708b2c6ba..83f16f114 100644 --- a/src/Iris/ProofMode/Tactics/LeftRight.lean +++ b/src/Iris/ProofMode/Tactics/LeftRight.lean @@ -9,10 +9,10 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem from_or_l [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A1) : P ⊢ Q := @@ -22,13 +22,8 @@ theorem from_or_r [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A2) : P ⊢ Q := (or_intro_r' h1).trans inst.1 -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab.Tactic Meta Qq BI Std +open Lean Elab.Tactic Meta Qq Std elab "ileft" : tactic => do ProofModeM.runTactic λ mvar { prop, e, hyps, goal, .. } => do diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean index 000437219..02ee92664 100644 --- a/src/Iris/ProofMode/Tactics/Mod.lean +++ b/src/Iris/ProofMode/Tactics/Mod.lean @@ -9,22 +9,17 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem mod [BI PROP] {e} {Φ} {p p'} {A A' Q Q' : PROP} [he : ElimModal Φ p p' A A' Q Q'] (h1 : e ∗ □?p' A' ⊢ Q') (hΦ : Φ) : e ∗ □?p A ⊢ Q := (sep_comm.1.trans (sep_mono_r (wand_intro h1))).trans (he.1 hΦ) -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std +open Lean Elab Tactic Meta Qq Std /-- Eliminate a modality from `A` by transforming the goal from `P ∗ □?p A ⊢ Q` to `P ∗ □?p' A' ⊢ Q'`, diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean index e195c459b..a4be000ff 100644 --- a/src/Iris/ProofMode/Tactics/ModIntro.lean +++ b/src/Iris/ProofMode/Tactics/ModIntro.lean @@ -8,10 +8,10 @@ module public meta import Iris.ProofMode.Tactics.Basic public import Iris.ProofMode.Modalities -public meta section - namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std + +public section +open Qq BI Std /-- Reified version of ModalityAction -/ inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where @@ -21,17 +21,6 @@ inductive ModalityActionQ (PROP1 : Q(Type u)) (PROP2 : Q(Type u)) : Type where | clear | id -private def parseModalityActionQ {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) : - ProofModeM (ModalityActionQ prop1 prop2) := do - let act ← whnf q($act) - match_expr act with - | ModalityAction.isEmpty _ _ => return .isEmpty - | ModalityAction.forall _ C => return .forall C - | ModalityAction.transform _ _ C => return .transform C - | ModalityAction.clear _ _ => return .clear - | ModalityAction.id _ => return .id - | _ => throwError "imodintro: unknown modality action {act}" - theorem modaction_forall [BI PROP] {p P} (M : Modality PROP PROP) {C} (h : M.action p = .forall C) (hC : C P) : □?p P ⊢ M.M iprop(□?p P) := by have hs := M.spec p @@ -59,7 +48,6 @@ theorem modaction_id [BI PROP] {p P} (M : Modality PROP PROP) (h : M.action p = rw [h] at hs apply hs - theorem modaction_sep_emp_l [BI PROP1] [bi2: BI PROP2] {elhs erhs erhs'} {M : Modality PROP1 PROP2} (h1 : elhs ⊢ M.M emp) (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(erhs') := (sep_mono h1 h2).trans $ M.sep.trans (M.mono emp_sep.1) @@ -69,6 +57,23 @@ theorem modaction_sep_emp_r [BI PROP1] [bi2: BI PROP2] {elhs elhs' erhs} {M : Mo theorem modaction_sep [BI PROP1] [bi2: BI PROP2] {elhs erhs elhs' erhs'} {M : Modality PROP1 PROP2} (h1 : elhs ⊢ M.M elhs') (h2 : erhs ⊢ M.M erhs') : elhs ∗ erhs ⊢ M.M iprop(elhs' ∗ erhs') := (sep_mono h1 h2).trans M.sep +theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q] + (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P := + (h1.trans (M.mono h2)).trans (from_modal sel hΦ) + +public meta section +open Lean Elab Tactic Meta + +private def parseModalityActionQ {prop1 prop2 : Q(Type u)} (act : Q(ModalityAction $prop1 $prop2)) : + ProofModeM (ModalityActionQ prop1 prop2) := do + let act ← whnf q($act) + match_expr act with + | ModalityAction.isEmpty _ _ => return .isEmpty + | ModalityAction.forall _ C => return .forall C + | ModalityAction.transform _ _ C => return .transform C + | ModalityAction.clear _ _ => return .clear + | ModalityAction.id _ => return .id + | _ => throwError "imodintro: unknown modality action {act}" /-- Applies modality actions to transform proof mode context. @@ -129,10 +134,6 @@ private def iModAction {prop1 : Q(Type u)} {bi1 : Q(BI $prop1)} {bi2} {e} return ⟨_, lhs', q(modaction_sep_emp_r $pflhs $pfrhs)⟩ return ⟨_, .mkSep lhs' rhs', q(modaction_sep $pflhs $pfrhs)⟩ -theorem modintro [BI PROP1] [BI PROP2] {e e'} {Φ M sel} {P : PROP2} {Q : PROP1} [FromModal Φ M sel P Q] - (h1 : e ⊢ M.M e') (h2 : e' ⊢ Q) (hΦ : Φ) : e ⊢ P := - (h1.trans (M.mono h2)).trans (from_modal sel hΦ) - /-- Introduce a modality by applying modality actions to transform hypotheses. # Parameters diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean index 56cf7fad2..936bcebdd 100644 --- a/src/Iris/ProofMode/Tactics/Pure.lean +++ b/src/Iris/ProofMode/Tactics/Pure.lean @@ -8,10 +8,10 @@ module public import Iris.ProofMode.Instances public meta import Iris.ProofMode.Tactics.Basic -public meta section - namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std + +public section +open BI Std theorem pure_elim_spatial [BI PROP] {P P' A Q : PROP} {φ : Prop} [hA : IntoPure A φ] [or : TCOr (Affine A) (Absorbing Q)] @@ -29,6 +29,10 @@ theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop} [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q := pure_elim_spatial h h' + +public meta section +open Lean Elab Tactic Meta Qq + def iPureCore {prop : Q(Type u)} (_bi : Q(BI $prop)) (P P' : Q($prop)) (p : Q(Bool)) (A Q : Q($prop)) (name : TSyntax ``binderIdent) (pf : Q($P ⊣⊢ $P' ∗ □?$p $A)) (k : (φ : Q(Prop)) → Q($φ) → ProofModeM (Q($P' ⊢ $Q))) : ProofModeM (Q($P ⊢ $Q)) := do diff --git a/src/Iris/ProofMode/Tactics/Rename.lean b/src/Iris/ProofMode/Tactics/Rename.lean index d943dafdc..ddb601ab4 100644 --- a/src/Iris/ProofMode/Tactics/Rename.lean +++ b/src/Iris/ProofMode/Tactics/Rename.lean @@ -7,9 +7,9 @@ module public meta import Iris.ProofMode.Tactics.Basic -public meta section - namespace Iris.ProofMode + +public meta section open Lean Elab Tactic Qq elab "irename" colGt nameFrom:ident " => " colGt nameTo:ident : tactic => do diff --git a/src/Iris/ProofMode/Tactics/Specialize.lean b/src/Iris/ProofMode/Tactics/Specialize.lean index 52215dc9e..6c20199d4 100644 --- a/src/Iris/ProofMode/Tactics/Specialize.lean +++ b/src/Iris/ProofMode/Tactics/Specialize.lean @@ -9,14 +9,10 @@ public meta import Iris.ProofMode.Patterns.ProofModeTerm public meta import Iris.ProofMode.Patterns.CasesPattern public meta import Iris.ProofMode.Tactics.Basic -public meta section - namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI Std -structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where - (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop)) - pf : Q($orig ⊢ $e ∗ □?$p $out) +public section +open BI theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP} (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1) @@ -41,6 +37,23 @@ theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} { [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a) := by refine h.trans <| sep_mono_r <| intuitionisticallyIf_mono <| inst.1.trans (forall_elim a) +theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B} + (h : P ∗ □?pa A ⊢ P' ∗ □?pb B) + (h2 : pa = true ∨ Affine A) + [IntoPersistently pb B B'] + : P ∗ □?pa A ⊢ P ∗ □ B' := by + apply Entails.trans _ persistently_and_intuitionistically_sep_r.1 + apply and_intro + · cases h2 <;> subst_eqs <;> apply sep_elim_l + · apply h.trans $ (sep_mono_r (persistentlyIf_of_intuitionisticallyIf.trans into_persistently)).trans sep_elim_r + +public meta section +open Lean Elab Tactic Meta Qq Std + +structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where + (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop)) + pf : Q($orig ⊢ $e ∗ □?$p $out) + private def processWand : @SpecializeState u prop bi orig → SpecPat → ProofModeM (SpecializeState bi orig) | { hyps, p, out, pf, .. }, .ident i => do @@ -91,16 +104,6 @@ def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool := | .pure _ => true | _ => false -theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B} - (h : P ∗ □?pa A ⊢ P' ∗ □?pb B) - (h2 : pa = true ∨ Affine A) - [IntoPersistently pb B B'] - : P ∗ □?pa A ⊢ P ∗ □ B' := by - apply Entails.trans _ persistently_and_intuitionistically_sep_r.1 - apply and_intro - · cases h2 <;> subst_eqs <;> apply sep_elim_l - · apply h.trans $ (sep_mono_r (persistentlyIf_of_intuitionisticallyIf.trans into_persistently)).trans sep_elim_r - /-- Specialize a proposition `A` by applying a sequence of specialization patterns. ## Parameters diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean index 3589b60da..6193f299a 100644 --- a/src/Iris/ProofMode/Tactics/Split.lean +++ b/src/Iris/ProofMode/Tactics/Split.lean @@ -9,10 +9,10 @@ public import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic -public section - namespace Iris.ProofMode -open Iris.BI + +public section +open BI theorem from_and_intro [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2] (h1 : P ⊢ A1) (h2 : P ⊢ A2) : P ⊢ Q := @@ -22,13 +22,8 @@ theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q := h.1.trans <| (sep_mono h1 h2).trans inst.1 -end Iris.ProofMode -end - public meta section - -namespace Iris.ProofMode -open Lean Elab Tactic Meta Qq BI +open Lean Elab Tactic Meta Qq elab "isplit" : tactic => do ProofModeM.runTactic λ mvar { prop, hyps, goal, .. } => do From f3e095ccbf735929b946ee486d3a518cab116382 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Mon, 2 Mar 2026 15:20:51 +0100 Subject: [PATCH 6/7] Tightening imports --- src/Iris/ProofMode/Tactics/Apply.lean | 8 ++++---- src/Iris/ProofMode/Tactics/Assumption.lean | 4 ++-- src/Iris/ProofMode/Tactics/Basic.lean | 6 +++--- src/Iris/ProofMode/Tactics/Cases.lean | 10 +++++----- src/Iris/ProofMode/Tactics/Clear.lean | 4 ++-- src/Iris/ProofMode/Tactics/ExFalso.lean | 2 +- src/Iris/ProofMode/Tactics/Exact.lean | 1 - src/Iris/ProofMode/Tactics/Exists.lean | 4 ++-- src/Iris/ProofMode/Tactics/Have.lean | 2 +- src/Iris/ProofMode/Tactics/HaveCore.lean | 4 ++-- src/Iris/ProofMode/Tactics/LeftRight.lean | 4 ++-- src/Iris/ProofMode/Tactics/Mod.lean | 2 +- src/Iris/ProofMode/Tactics/ModIntro.lean | 2 +- src/Iris/ProofMode/Tactics/Pure.lean | 1 - src/Iris/ProofMode/Tactics/Split.lean | 4 ++-- 15 files changed, 28 insertions(+), 30 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Apply.lean b/src/Iris/ProofMode/Tactics/Apply.lean index da37d0f12..bfda925bf 100644 --- a/src/Iris/ProofMode/Tactics/Apply.lean +++ b/src/Iris/ProofMode/Tactics/Apply.lean @@ -5,10 +5,10 @@ Authors: Oliver Soeser, Michael Sammler -/ module -public import Iris.BI -public import Iris.ProofMode.Classes -public meta import Iris.ProofMode.Patterns.ProofModeTerm -public meta import Iris.ProofMode.Tactics.Assumption +import Iris.BI +import Iris.ProofMode.Classes +meta import Iris.ProofMode.Patterns.ProofModeTerm +meta import Iris.ProofMode.Tactics.Assumption public meta import Iris.ProofMode.Tactics.HaveCore namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Assumption.lean b/src/Iris/ProofMode/Tactics/Assumption.lean index f7b9d7d07..55f52e51b 100644 --- a/src/Iris/ProofMode/Tactics/Assumption.lean +++ b/src/Iris/ProofMode/Tactics/Assumption.lean @@ -5,8 +5,8 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public import Iris.BI -public import Iris.ProofMode.Classes +import Iris.BI +import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Basic.lean b/src/Iris/ProofMode/Tactics/Basic.lean index 8178b95de..9c050f9a8 100644 --- a/src/Iris/ProofMode/Tactics/Basic.lean +++ b/src/Iris/ProofMode/Tactics/Basic.lean @@ -5,10 +5,10 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public meta import Iris.ProofMode.Expr -public import Iris.ProofMode.Classes +import Iris.ProofMode.Classes +meta import Iris.ProofMode.Expr +meta import Iris.ProofMode.SynthInstance public meta import Iris.ProofMode.ProofModeM -public meta import Iris.ProofMode.SynthInstance public meta section diff --git a/src/Iris/ProofMode/Tactics/Cases.lean b/src/Iris/ProofMode/Tactics/Cases.lean index 8682013e2..723d81f7a 100644 --- a/src/Iris/ProofMode/Tactics/Cases.lean +++ b/src/Iris/ProofMode/Tactics/Cases.lean @@ -5,13 +5,13 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public meta import Iris.ProofMode.Patterns.ProofModeTerm -public meta import Iris.ProofMode.Patterns.CasesPattern -public meta import Iris.ProofMode.Tactics.Basic -public meta import Iris.ProofMode.Tactics.Clear +meta import Iris.ProofMode.Patterns.ProofModeTerm +meta import Iris.ProofMode.Patterns.CasesPattern +public meta import Iris.ProofMode.Tactics.Mod public meta import Iris.ProofMode.Tactics.Pure +public meta import Iris.ProofMode.Tactics.Clear +public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.HaveCore -public meta import Iris.ProofMode.Tactics.Mod namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Clear.lean b/src/Iris/ProofMode/Tactics/Clear.lean index 52e336ab4..0afb4dd87 100644 --- a/src/Iris/ProofMode/Tactics/Clear.lean +++ b/src/Iris/ProofMode/Tactics/Clear.lean @@ -5,8 +5,8 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public import Iris.BI -public import Iris.ProofMode.Classes +import Iris.BI +import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/ExFalso.lean b/src/Iris/ProofMode/Tactics/ExFalso.lean index 47333ad30..1b819e9b8 100644 --- a/src/Iris/ProofMode/Tactics/ExFalso.lean +++ b/src/Iris/ProofMode/Tactics/ExFalso.lean @@ -5,7 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public import Iris.BI +import Iris.BI public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Exact.lean b/src/Iris/ProofMode/Tactics/Exact.lean index a86e85246..01424f5ce 100644 --- a/src/Iris/ProofMode/Tactics/Exact.lean +++ b/src/Iris/ProofMode/Tactics/Exact.lean @@ -5,7 +5,6 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.Assumption namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Exists.lean b/src/Iris/ProofMode/Tactics/Exists.lean index 86a5982df..80512ad49 100644 --- a/src/Iris/ProofMode/Tactics/Exists.lean +++ b/src/Iris/ProofMode/Tactics/Exists.lean @@ -5,8 +5,8 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public import Iris.BI -public import Iris.ProofMode.Classes +import Iris.BI +import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Have.lean b/src/Iris/ProofMode/Tactics/Have.lean index 4ab6ccc2c..ab32fdac7 100644 --- a/src/Iris/ProofMode/Tactics/Have.lean +++ b/src/Iris/ProofMode/Tactics/Have.lean @@ -5,7 +5,7 @@ Authors: Michael Sammler -/ module -public import Iris.BI +import Iris.BI public meta import Iris.ProofMode.Patterns.CasesPattern public meta import Iris.ProofMode.Tactics.HaveCore public meta import Iris.ProofMode.Tactics.Cases diff --git a/src/Iris/ProofMode/Tactics/HaveCore.lean b/src/Iris/ProofMode/Tactics/HaveCore.lean index 7a428ff5b..9527c9418 100644 --- a/src/Iris/ProofMode/Tactics/HaveCore.lean +++ b/src/Iris/ProofMode/Tactics/HaveCore.lean @@ -5,8 +5,8 @@ Authors: Michael Sammler, Zongyuan Liu -/ module -public import Iris.BI -public import Iris.ProofMode.Classes +import Iris.BI +import Iris.ProofMode.Classes public meta import Iris.ProofMode.Patterns.ProofModeTerm public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.Specialize diff --git a/src/Iris/ProofMode/Tactics/LeftRight.lean b/src/Iris/ProofMode/Tactics/LeftRight.lean index 83f16f114..f20778975 100644 --- a/src/Iris/ProofMode/Tactics/LeftRight.lean +++ b/src/Iris/ProofMode/Tactics/LeftRight.lean @@ -5,8 +5,8 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public import Iris.BI -public import Iris.ProofMode.Classes +import Iris.BI +import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Mod.lean b/src/Iris/ProofMode/Tactics/Mod.lean index 02ee92664..a0083f025 100644 --- a/src/Iris/ProofMode/Tactics/Mod.lean +++ b/src/Iris/ProofMode/Tactics/Mod.lean @@ -5,7 +5,7 @@ Authors: Michael Sammler -/ module -public import Iris.BI +import Iris.BI public import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic diff --git a/src/Iris/ProofMode/Tactics/ModIntro.lean b/src/Iris/ProofMode/Tactics/ModIntro.lean index a4be000ff..efb633874 100644 --- a/src/Iris/ProofMode/Tactics/ModIntro.lean +++ b/src/Iris/ProofMode/Tactics/ModIntro.lean @@ -5,8 +5,8 @@ Authors: Michael Sammler -/ module +import Iris.ProofMode.Modalities public meta import Iris.ProofMode.Tactics.Basic -public import Iris.ProofMode.Modalities namespace Iris.ProofMode diff --git a/src/Iris/ProofMode/Tactics/Pure.lean b/src/Iris/ProofMode/Tactics/Pure.lean index 936bcebdd..4756b76f7 100644 --- a/src/Iris/ProofMode/Tactics/Pure.lean +++ b/src/Iris/ProofMode/Tactics/Pure.lean @@ -29,7 +29,6 @@ theorem pure_elim_intuitionistic [BI PROP] {P P' A Q : PROP} {φ : Prop} [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) : P ⊢ Q := pure_elim_spatial h h' - public meta section open Lean Elab Tactic Meta Qq diff --git a/src/Iris/ProofMode/Tactics/Split.lean b/src/Iris/ProofMode/Tactics/Split.lean index 6193f299a..c7fdbf113 100644 --- a/src/Iris/ProofMode/Tactics/Split.lean +++ b/src/Iris/ProofMode/Tactics/Split.lean @@ -5,8 +5,8 @@ Authors: Lars König, Mario Carneiro, Michael Sammler -/ module -public import Iris.BI -public import Iris.ProofMode.Classes +import Iris.BI +import Iris.ProofMode.Classes public meta import Iris.ProofMode.Tactics.Basic namespace Iris.ProofMode From 0bb2be75e3c2b985f2d09c3cb9cc1be109946443 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Thu, 5 Mar 2026 15:36:31 +0100 Subject: [PATCH 7/7] Fix build --- src/Iris/Std/FromMathlib.lean | 3 +++ src/Iris/Std/PartialMap.lean | 7 +++---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Iris/Std/FromMathlib.lean b/src/Iris/Std/FromMathlib.lean index acda13174..71d5f7724 100644 --- a/src/Iris/Std/FromMathlib.lean +++ b/src/Iris/Std/FromMathlib.lean @@ -2,6 +2,9 @@ Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module + +@[expose] public section namespace FromMathlib diff --git a/src/Iris/Std/PartialMap.lean b/src/Iris/Std/PartialMap.lean index 3886c8118..4b7fe0630 100644 --- a/src/Iris/Std/PartialMap.lean +++ b/src/Iris/Std/PartialMap.lean @@ -1,6 +1,3 @@ -import Batteries.Data.List.Perm -import Iris.Std.FromMathlib - /- Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -8,6 +5,9 @@ Authors: Zongyuan Liu, Markus de Medeiros -/ module +import Iris.Std.FromMathlib +import Batteries.Data.List.Perm + /-! ## Partial Maps This file defines the base abstraction for partial maps (maps from keys to optional values). @@ -1045,5 +1045,4 @@ theorem toList_zip {m₁ : M V} {m₂ : M V'} : end LawfulFiniteMap - end Iris.Std