Environment Extensions and Attributes: Example
In the recipe Environment Extensions and Attributes, we defined an environment extension to store lemmas tagged with the @[distribute] attribute, and we defined the @[distribute] attribute to add lemmas to this environment extension, and implemented the distribute tactic that retrieves the lemmas from the environment extension and applies them.
In this recipe, we show how to use the @[distribute] attribute and the distribute tactic. We cannot tag or use attributes in the same file where they are initialized, so we had to split the code into two files. In this file, we tag some lemmas with the @[distribute] attribute, and then we use the distribute tactic to apply these lemmas.
open Distribute
@[distribute]
theorem distributeAnd (a b c : Prop) :
(a ∧ (b ∨ c)) ↔ (a ∧ b) ∨ (a ∧ c) := a:Propb:Propc:Prop⊢ a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c
All goals completed! 🐙
example : (1 = 1) ∧ (2 = 3 ∨ 3 = 3) := ⊢ 1 = 1 ∧ (2 = 3 ∨ 3 = 3)
⊢ 1 = 1 ∧ 2 = 3 ∨ 1 = 1 ∧ 3 = 3
All goals completed! 🐙
We can also tag definitions or theorems from imported modules with the @[distribute] attribute, and they will be added to the environment extension and used by the distribute tactic.
attribute [distribute] Nat.mul_add
example (a b c : Nat) : a * (b + c) = a * b + a * c := a:Natb:Natc:Nat⊢ a * (b + c) = a * b + a * c
All goals completed! 🐙