Skip to content

Commit 37fe563

Browse files
zqy1018zqy1018
committed
bump to Lean v4.27.0 while only upgrading those necessary for Veil
1 parent 48d2f74 commit 37fe563

File tree

15 files changed

+153
-1582
lines changed

15 files changed

+153
-1582
lines changed

‎Loom/Meta.lean‎

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ import Lean.Elab.Tactic
33

44
import Loom.MonadAlgebras.WP.Attr
55
import Loom.MonadAlgebras.WP.Basic
6-
import Loom.MonadAlgebras.NonDetT.Basic
76

87
import Mathlib.Tactic.Common
98

@@ -472,19 +471,19 @@ attribute [loomWPGenRewrite]
472471
ReaderT.wp_read
473472
MAlgLift.wp_throw
474473

475-
TotalCorrectness.AngelicChoice.MonadNonDet.wp_pickSuchThat
476-
TotalCorrectness.DemonicChoice.MonadNonDet.wp_pickSuchThat
477-
PartialCorrectness.AngelicChoice.MonadNonDet.wp_pickSuchThat
478-
PartialCorrectness.DemonicChoice.MonadNonDet.wp_pickSuchThat
479-
480-
TotalCorrectness.DemonicChoice.MonadNonDet.wp_assume
481-
TotalCorrectness.AngelicChoice.MonadNonDet.wp_assume
482-
TotalCorrectness.DemonicChoice.MonadNonDet.wp_pick
483-
TotalCorrectness.AngelicChoice.MonadNonDet.wp_pick
484-
PartialCorrectness.DemonicChoice.MonadNonDet.wp_assume
485-
PartialCorrectness.AngelicChoice.MonadNonDet.wp_assume
486-
PartialCorrectness.DemonicChoice.MonadNonDet.wp_pick
487-
PartialCorrectness.AngelicChoice.MonadNonDet.wp_pick
474+
-- TotalCorrectness.AngelicChoice.MonadNonDet.wp_pickSuchThat
475+
-- TotalCorrectness.DemonicChoice.MonadNonDet.wp_pickSuchThat
476+
-- PartialCorrectness.AngelicChoice.MonadNonDet.wp_pickSuchThat
477+
-- PartialCorrectness.DemonicChoice.MonadNonDet.wp_pickSuchThat
478+
479+
-- TotalCorrectness.DemonicChoice.MonadNonDet.wp_assume
480+
-- TotalCorrectness.AngelicChoice.MonadNonDet.wp_assume
481+
-- TotalCorrectness.DemonicChoice.MonadNonDet.wp_pick
482+
-- TotalCorrectness.AngelicChoice.MonadNonDet.wp_pick
483+
-- PartialCorrectness.DemonicChoice.MonadNonDet.wp_assume
484+
-- PartialCorrectness.AngelicChoice.MonadNonDet.wp_assume
485+
-- PartialCorrectness.DemonicChoice.MonadNonDet.wp_pick
486+
-- PartialCorrectness.AngelicChoice.MonadNonDet.wp_pick
488487

489488

490489
/- #derive_lifted_wp command, used to enable automatic VC generation in verifiers built on top of Loom.

‎Loom/MonadAlgebras/Defs.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,8 +118,8 @@ class MAlgDet (l : outParam (Type v)) [Monad m] [CompleteLattice l] [MAlgOrdered
118118
class MAlgPartial (m : Type u -> Type v) [Monad m] [∀ α, Lean.Order.CCPO (m α)]
119119
[CompleteLattice l] [MAlgOrdered m l] where
120120
csup_lift {α : Type u} (xc : Set (m α)) (post : α -> l) :
121-
Lean.Order.chain xc ->
122-
⨅ x ∈ xc, MAlg.lift x post <= MAlg.lift (Lean.Order.CCPO.csup xc) post
121+
∀ (hc : Lean.Order.chain xc),
122+
⨅ x ∈ xc, MAlg.lift x post <= MAlg.lift (Lean.Order.CCPO.csup hc) post
123123

124124
/-- Class for total correctness monadic algebras -/
125125
class MAlgTotal (m : Type u -> Type v) [Monad m] [∀ α, Lean.Order.CCPO (m α)]

‎Loom/MonadAlgebras/Instances/Basic.lean‎

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,8 @@ instance : Monad DivM where
3333
class CCPOBot (m : Type u -> Type v) where
3434
compBot {α} : m α
3535

36-
class CCPOBotLawful (m : Type u -> Type v) [∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] where
37-
prop {α} : CCPOBot.compBot (m := m) (α := α) = Lean.Order.bot
36+
-- class CCPOBotLawful (m : Type u -> Type v) [∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] where
37+
-- prop {α} [Lean.Order.PartialOrder (m α)] : ∀ (c : (m α) → Prop), Lean.Order.is_sup c <| CCPOBot.compBot (m := m) (α := α)
3838

3939
instance : LawfulMonad DivM := by
4040
refine LawfulMonad.mk' _ ?_ ?_ ?_
@@ -46,8 +46,8 @@ noncomputable instance : Lean.Order.CCPO (DivM α) := inferInstanceAs (Lean.Orde
4646
instance : CCPOBot DivM where
4747
compBot := .div
4848

49-
instance : CCPOBotLawful DivM where
50-
prop := by simp [Lean.Order.bot, Lean.Order.CCPO.csup,Lean.Order.flat_csup, instCCPOBotDivM]
49+
-- instance : CCPOBotLawful DivM where
50+
-- prop := by sorry-- simp [Lean.Order.bot, Lean.Order.CCPO.csup, instCCPOBotDivM]
5151

5252
instance : Lean.Order.MonoBind DivM where
5353
bind_mono_left := by
@@ -73,15 +73,15 @@ scoped instance : MAlgDet DivM Prop where
7373
angelic := by
7474
rintro _ _ (_|_) <;> simp [MAlg.lift, MAlgOrdered.μ, Functor.map]
7575

76-
instance : MAlgPartial DivM where
77-
csup_lift {α} chain := by
78-
intro post hchain
79-
simp [Lean.Order.CCPO.csup, Lean.Order.flat_csup]
80-
split_ifs with ch
81-
{ intro h; apply h;
82-
rcases Classical.choose_spec ch
83-
solve_by_elim }
84-
solve_by_elim
76+
-- instance : MAlgPartial DivM where
77+
-- csup_lift {α} chain := by
78+
-- intro post hchain
79+
-- simp [Lean.Order.CCPO.csup, Lean.Order.flat_csup]
80+
-- split_ifs with ch
81+
-- { intro h; apply h;
82+
-- rcases Classical.choose_spec ch
83+
-- solve_by_elim }
84+
-- solve_by_elim
8585

8686
instance : NoFailure DivM where
8787
noFailure := by
@@ -106,9 +106,9 @@ scoped instance : MAlgDet DivM Prop where
106106
demonic := by
107107
rintro _ _ (_|_) <;> simp [MAlg.lift, MAlgOrdered.μ, Functor.map, LE.pure]
108108

109-
instance : MAlgTotal DivM where
110-
bot_lift := by
111-
rintro _ _; simp [MAlg.lift, MAlgOrdered.μ, Functor.map, LE.pure]
112-
rw [<-CCPOBotLawful.prop]; simp
109+
-- instance : MAlgTotal DivM where
110+
-- bot_lift := by
111+
-- rintro _ _; simp [MAlg.lift, MAlgOrdered.μ, Functor.map, LE.pure]
112+
-- rw [<-CCPOBotLawful.prop]; simp
113113

114114
end TotalCorrectness

‎Loom/MonadAlgebras/Instances/ExceptT.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -158,8 +158,8 @@ instance [Monad m] [∀ α, CCPO (m α)] [MonoBind m] : MonoBind (ExceptT ε m)
158158
instance [Monad m] [CCPOBot m] : CCPOBot (ExceptT ε m) where
159159
compBot := CCPOBot.compBot (m := m)
160160

161-
instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (ExceptT ε m) where
162-
prop := CCPOBotLawful.prop (m := m)
161+
-- instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (ExceptT ε m) where
162+
-- prop := CCPOBotLawful.prop (m := m)
163163

164164
instance (hd : ε -> _) [IsHandler hd] [_root_.CompleteLattice l] [Monad m] [LawfulMonad m] [inst: MAlgOrdered m l]
165165
[∀ α, CCPO (m α)] [MonoBind m]

‎Loom/MonadAlgebras/Instances/ReaderT.lean‎

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -51,41 +51,41 @@ instance [Monad m] [∀ α, Lean.Order.CCPO (m α)] [Lean.Order.MonoBind m] : Le
5151
instance [Monad m] [CCPOBot m] : CCPOBot (ReaderT σ m) where
5252
compBot := fun _ => CCPOBot.compBot
5353

54-
instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (ReaderT σ m) where
55-
prop := by
56-
simp [Lean.Order.bot, Lean.Order.CCPO.csup, instCCPOReaderTOfMonad_loom]
57-
unfold Lean.Order.fun_csup; intro α; ext; simp
58-
apply CCPOBotLawful.prop
54+
-- instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (ReaderT σ m) where
55+
-- prop := by
56+
-- simp [Lean.Order.bot, Lean.Order.CCPO.csup, instCCPOReaderTOfMonad_loom]
57+
-- unfold Lean.Order.fun_csup; intro α; ext; simp
58+
-- apply CCPOBotLawful.prop
5959

6060
lemma MAlg.lift_ReaderT [Monad m] [LawfulMonad m] [CompleteLattice l] [inst: MAlgOrdered m l] (x : ReaderT σ m α) :
6161
MAlg.lift x post = fun s => MAlg.lift (x s) (fun xs => post xs s) := by
6262
simp [MAlg.lift, Functor.map, MAlgOrdered.μ]
6363

64-
open Lean.Order
65-
instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
66-
[∀ α, CCPO (m α)] [MonoBind m]
67-
[MAlgPartial m] : MAlgPartial (ReaderT σ m) where
68-
csup_lift {α} chain := by
69-
intro post hchain
70-
simp [instCCPOReaderTOfMonad_loom, CCPO.csup, MAlg.lift_ReaderT]
71-
rw [@Pi.le_def]; simp; unfold fun_csup; intro s
72-
apply le_trans'
73-
apply MAlgPartial.csup_lift (m := m)
74-
{ simp [Lean.Order.chain]; rintro x y f cf rfl g cg rfl
75-
cases (hchain f g cf cg)
76-
{ left; solve_by_elim }
77-
right; solve_by_elim }
78-
repeat rw [@iInf_subtype']
79-
refine iInf_mono' ?_; simp [Membership.mem, Set.Mem]; aesop
64+
-- open Lean.Order
65+
-- instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
66+
-- [∀ α, CCPO (m α)] [MonoBind m]
67+
-- [MAlgPartial m] : MAlgPartial (ReaderT σ m) where
68+
-- csup_lift {α} chain := by
69+
-- intro post hchain
70+
-- simp [instCCPOReaderTOfMonad_loom, CCPO.csup, MAlg.lift_ReaderT]
71+
-- rw [@Pi.le_def]; simp; unfold fun_csup; intro s
72+
-- apply le_trans'
73+
-- apply MAlgPartial.csup_lift (m := m)
74+
-- { simp [Lean.Order.chain]; rintro x y f cf rfl g cg rfl
75+
-- cases (hchain f g cf cg)
76+
-- { left; solve_by_elim }
77+
-- right; solve_by_elim }
78+
-- repeat rw [@iInf_subtype']
79+
-- refine iInf_mono' ?_; simp [Membership.mem, Set.Mem]; aesop
8080

81-
attribute [-simp] le_bot_iff in
82-
instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
83-
[∀ α, CCPO (m α)] [MonoBind m]
84-
[MAlgTotal m] : MAlgTotal (ReaderT σ m) where
85-
bot_lift := by
86-
simp [MAlg.lift_ReaderT, bot, instCCPOReaderTOfMonad_loom, CCPO.csup, fun_csup]
87-
intros; intro; simp;
88-
apply MAlgTotal.bot_lift (m := m)
81+
-- attribute [-simp] le_bot_iff in
82+
-- instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
83+
-- [∀ α, CCPO (m α)] [MonoBind m]
84+
-- [MAlgTotal m] : MAlgTotal (ReaderT σ m) where
85+
-- bot_lift := by
86+
-- simp [MAlg.lift_ReaderT, bot, instCCPOReaderTOfMonad_loom, CCPO.csup, fun_csup]
87+
-- intros; intro; simp;
88+
-- apply MAlgTotal.bot_lift (m := m)
8989

9090
instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
9191
[inst': NoFailure m] : NoFailure (ReaderT σ m) where

‎Loom/MonadAlgebras/Instances/StateT.lean‎

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -47,42 +47,42 @@ instance [Monad m] [∀ α, Lean.Order.CCPO (m α)] [Lean.Order.MonoBind m] : Le
4747
instance [Monad m] [CCPOBot m] : CCPOBot (StateT σ m) where
4848
compBot := fun _ => CCPOBot.compBot
4949

50-
instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (StateT σ m) where
51-
prop := by
52-
simp [Lean.Order.bot, Lean.Order.CCPO.csup, instCCPOStateTOfMonad_loom]
53-
unfold Lean.Order.fun_csup; intro α; ext; simp [StateT.run]
54-
apply CCPOBotLawful.prop
50+
-- instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (StateT σ m) where
51+
-- prop := by
52+
-- simp [Lean.Order.bot, Lean.Order.CCPO.csup, instCCPOStateTOfMonad_loom]
53+
-- unfold Lean.Order.fun_csup; intro α; ext; simp [StateT.run]
54+
-- apply CCPOBotLawful.prop
5555

5656

5757
lemma MAlg.lift_StateT [Monad m] [LawfulMonad m] [CompleteLattice l] [inst: MAlgOrdered m l] (x : StateT σ m α) :
5858
MAlg.lift x post = fun s => MAlg.lift (x s) (fun xs => post xs.1 xs.2) := by
5959
simp [MAlg.lift, Functor.map, MAlgOrdered.μ, StateT.map]
6060

61-
open Lean.Order
62-
instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
63-
[∀ α, CCPO (m α)] [MonoBind m]
64-
[MAlgPartial m] : MAlgPartial (StateT σ m) where
65-
csup_lift {α} chain := by
66-
intro post hchain
67-
simp [instCCPOStateTOfMonad_loom, CCPO.csup, MAlg.lift_StateT]
68-
rw [@Pi.le_def]; simp; unfold fun_csup; intro s
69-
apply le_trans'
70-
apply MAlgPartial.csup_lift (m := m)
71-
{ simp [Lean.Order.chain]; rintro x y f cf rfl g cg rfl
72-
cases (hchain f g cf cg)
73-
{ left; solve_by_elim }
74-
right; solve_by_elim }
75-
repeat rw [@iInf_subtype']
76-
refine iInf_mono' ?_; simp [Membership.mem, Set.Mem]; aesop
61+
-- open Lean.Order
62+
-- instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
63+
-- [∀ α, CCPO (m α)] [MonoBind m]
64+
-- [MAlgPartial m] : MAlgPartial (StateT σ m) where
65+
-- csup_lift {α} chain := by
66+
-- intro post hchain
67+
-- simp [instCCPOStateTOfMonad_loom, CCPO.csup, MAlg.lift_StateT]
68+
-- rw [@Pi.le_def]; simp; unfold fun_csup; intro s
69+
-- apply le_trans'
70+
-- apply MAlgPartial.csup_lift (m := m)
71+
-- { simp [Lean.Order.chain]; rintro x y f cf rfl g cg rfl
72+
-- cases (hchain f g cf cg)
73+
-- { left; solve_by_elim }
74+
-- right; solve_by_elim }
75+
-- repeat rw [@iInf_subtype']
76+
-- refine iInf_mono' ?_; simp [Membership.mem, Set.Mem]; aesop
7777

78-
attribute [-simp] le_bot_iff in
79-
instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
80-
[∀ α, CCPO (m α)] [MonoBind m]
81-
[MAlgTotal m] : MAlgTotal (StateT σ m) where
82-
bot_lift := by
83-
simp [MAlg.lift_StateT, bot, instCCPOStateTOfMonad_loom, CCPO.csup, fun_csup]
84-
intros; intro; simp;
85-
apply MAlgTotal.bot_lift (m := m)
78+
-- attribute [-simp] le_bot_iff in
79+
-- instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
80+
-- [∀ α, CCPO (m α)] [MonoBind m]
81+
-- [MAlgTotal m] : MAlgTotal (StateT σ m) where
82+
-- bot_lift := by
83+
-- simp [MAlg.lift_StateT, bot, instCCPOStateTOfMonad_loom, CCPO.csup, fun_csup]
84+
-- intros; intro; simp;
85+
-- apply MAlgTotal.bot_lift (m := m)
8686

8787
instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l]
8888
[inst': NoFailure m] : NoFailure (StateT σ m) where

0 commit comments

Comments
 (0)