## Summary
The `rfl` tactic can appear to be magic as it glosses over details to quickly close a proof.
Its superpower is to find a substitution chain of definitionally equal goals that concludes with a trivial goal such as: true = true, which is true by syntactic equality.
However, when the details of each derivation step is the focus-of-attention, then `characterizing lemmas` are useful because they denote as theorems the individual constructors of definitions.
## Example: and_right_assoc
Suppose the and boolean is defined as:
![[Characterizing lemmas-1.png|298]]
Then the `characterizing lemmas`specify which match is applied to move the proof forward:
![[Characterizing lemmas-5.png|798]]
### Line-by-line description
| Lines | Description |
| ----------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| 2 - 6 | The `characterizing lemmas` are defined, one lemma for each row in the truth table. |
| 8 - 10 | `and_right_assoc` is an example of right associativity for conjunctions:<br>`(bool1 && (bool1 && bool1))` |
| 12 - 16 | This example <br>(1) Unfolds the definition of `and_right_assoc` <br>(2) Closes the proof by `rfl`, which skips justifying each reduction.<br>This is fine when the focus-of-detail is to assert that the substitution chain yields the correct result. (Only the `what` is needed, not the `how`.)<br>`and_right_assoc`, and not the details of its definition. |
| 18 - 24 | Here the focus-of-detail is the actual derivation of proposition that requires the right associativity property of the conjunction operator. <br><br>This example unfolds the definition of `and_right_assoc` and then closes the proof by applying rows in the `and` truth table. Finally in line 25 reflexivity is applied when the goal is `false = false`. |
References:
![[Appendix/Media/Icons/under-construction.png]] #TODO
## Characterizing lemmas as an interface
Characterizing lemmas can serve as an interface to one or more implementations.
![[Appendix/Media/Icons/under-construction.png]] #TODO We need an example here.