Add monad laws #1485
Add monad laws #1485
Conversation
I will take a look. |
|
Fixed the io_monad |
I investigated some of your proofs. I can see it was not a smooth ride. |
…s used see leanprover#1485 @Kha We need this commit to be able to execute commands such as: ```lean #check @monad.mk ```
| cases x, | ||
| { dsimp [option_t_bind._match_1, return, pure], | ||
| rw [monad.pure_bind], apply rfl }, | ||
| { apply rfl } |
There was a problem hiding this comment.
We have tactic.interactive.refl.
…ctics see leanprover#1485 @Kha I added by_auto_param and by_opt_param
…ctics see leanprover#1485 @Kha I added by_auto_param and by_opt_param
… given fields as soon as possible, too. Also make sure not to elaborate fields before other fields their type depends on. Makes inline tactic proofs in structure instances possible.
…s used see leanprover#1485 @Kha We need this commit to be able to execute commands such as: ```lean #check @monad.mk ```
| @@ -29,7 +29,7 @@ class unfold_untrusted_macros_fn : public replace_visitor_with_tc { | |||
| expr r = update_macro(e, new_args.size(), new_args.data()); | |||
| if (!m_trust_lvl || def.trust_level() >= *m_trust_lvl) { | |||
| if (optional<expr> new_r = m_ctx.expand_macro(r)) { | |||
| return *new_r; | |||
| return visit(*new_r); | |||
| } else { | |||
There was a problem hiding this comment.
BTW, this module will need to be re-implemented. It was already a performance bottleneck before this change.
Thanks! There is a last trust0 issue with macros in intro rules not being expanded, but I'm not sure where to best place a fix. |
Did the change at |
|
Sorry, I should have been more specific. I was looking for a catch-all location to place the call at, but I don't think there is one in library/. I'll add one just in structure_cmd for now. |
|
@Kha I have been trying to implement the "abstract nested proofs" feature. It was much harder than expected. I found many problems. I can list them if you are interested. Here is the compromise I implemented. Proofs are abstracted in
#check @vector.append.equations._eqn_1produces ∀ {α} {n m} l₁ h₁ l₂ h₂, append ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ = ⟨l₁ ++ l₂, append._main._proof_1 l₁ h₁ l₂ h₂⟩Before this change, we would get ∀ {α} {n m} l₁ h₁ l₂ h₂, append ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ = ⟨l₁ ++ l₂, ... huge mess ...⟩ |
|
In terms of design, is there a reason to have the functor, applicative and monad methods provided in the same classes as the laws? I find the layering of orders (i.e. has_le, weak_order, linear_weak_order, strict_order, etc) and arithmetic (has_add, add_semigroup, add_monoid, etc) very appealing and it makes them easier to use. |
|
@cipher1024 Are you suggesting we start with simple classes such as BTW, we are planning to revise the algebraic hierarchy. If you have time, it would be great to have your feedback. The proposal is here: https://github.com/leanprover/lean/wiki/Refactoring-structures |
|
@leodemoura I was mostly referring to the separation that exists in the Lean library between the type classes with functions and the type classes with laws. I find it especially useful because, typically, when you define functions in terms of monads, what you really need is to have access to the bind operator, regardless of how it behaves. Later, when you prove something about the function, then you should assume that bind is associative, etc. This being said, I like the idea of having the basic I'm thinking that the classes with laws could follow the hierarchy of the semigroupoids Haskell library with respect to Functor, Apply, Applicative, Bind and Monad. BTW, thanks for linking me to the refactoring project. It looks exciting :) I'll contribute whatever feedback I can. |
…em correct for non-meta instances
…s used see leanprover#1485 @Kha We need this commit to be able to execute commands such as: ```lean #check @monad.mk ```
…ition name on eval_expr type error
Nice, that sounds good enough. For default proofs in class decls, the |
Sure, we can always add those (note that we already have
Feel free to insert the missing classes into the hierarchy. I also haven't added laws to |
|
@Kha:
I think you meant |
Oh, right :) . |
|
@Kha it looks like we need a hierarchy of |
@Kha Yes, this is correct. |
…s used see leanprover#1485 @Kha We need this commit to be able to execute commands such as: ```lean #check @monad.mk ```
functor,applicative, andmonadpureandbind, the proof obligations break down to just 1 functor law and 2 monad lawsundefinedfor meta onesstructurea bit to make things easierThe instance proofs aren't exactly pretty - I wildly switched between
dsimp,simp, andrwdepending on what worked in a given context.I tried to fix
ioby constructing an unsafemonadinstance in C++ via Lean, but there's still some VM error left. There are also a few other tests I have broken somehow.