Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and the symmetry induced by the list reversal mapping. The method is implemented as an attribute and its result is based on user-declared symmetry rules. Besides general rules, we provide rules that are aimed to be applied in the domain of Combinatorics on Words.
While formalizing a piece of mathematical knowledge, one probably hopes that some part of
the tedious work will be done by the machine. One such mechanical tasks are proofs that follow
“by symmetry” which can be seen as a variation of “without loss of generality” [
In this article, we exhibit a partial, yet quite useful, solution to “by symmetry” in the case of
lists and the reversal mapping in the proof assistant Isabelle/HOL [
First, we give a short overview of mathematical context along with examples of the symmetry
in question. In Section 3, we shortly describe possible approaches to the solution and then we
describe our solution which is part of the ongoing project of formalization of Combinatorics
on Words [
We work with words, which are finite sequences ()=0 with ∈ with usually being a ifnite set. The set of all words over is denoted * (where * is the Kleene star). The reversal mapping, denoted rev, is a mapping * → * which maps the word = ()=0 to the word rev () = (− )=0, or simply put, it reads the letters of the word in the reverse order. The reversal mapping is an involutive antimorphism with respect to the operation of concatenation of two words, that is, rev ∘ rev = id and rev ( · ) = rev () · rev () where · is the binary operation of concatenation. It follows that rev is also a bijection.
In our ongoing project [
Lemma 1. If is a prefix of , then a prefix of · .
Proof. If is a prefix of , there exists a word such that = · . Hence, · = · · , and is a prefix of · .
By the symmetrical counterpart of Lemma 1 we mean the following claim.
Lemma 2. If is sufix of , then is a sufix of · .
Its proof can be done as the presented proof of Lemma 1, however, stating in follows “by symmetry” from Lemma 1 would be no exception in literature.
In order to formally exploit the symmetry in a full proof, we have to make the intended symmetry between a prefix and a sufix explicit: Lemma 3. The word is a prefix of if and only if rev () is a sufix of rev ().
A full proof of Lemma 2, by symmetry, is as follows.
Proof of Lemma 2. Fix and assume that is a sufix of . Let ′, ′, and ′ be the words such that As the reversal is an involution, it follows that ′ = rev (), ′ = rev () = rev (︀ ′)︀ , = rev (︀ ′)︀ and and ′ = rev (). = rev (︀ ′)︀ .
As is a sufix of , the word rev (′) is a sufix of rev (′). By Lemma 3, ′ is a prefix of ′. Using Lemma 1, ′ is a prefix of ′ · ′. Again, by Lemma 3, rev (′) is a sufix of rev (′ · ′). Since
rev (︀ ′ · ′)︀ = rev (︀ ′)︀ · rev (︀ ′)︀ = · , we conclude that is a sufix of · . 2.2. Example 2 Since the next examples are in the framework of Isabelle/HOL, we first recall our setting. A word is represented by the datatype of list, which is is specified via 2 constructors: Nil (denoted []), the empty list/word, and Cons (denoted #), the recursive constructor allowing to add an element to the list at its beginning. The reversal mapping is represented by the function rev: primrec rev :: ′a list ⇒ ′a list where rev [] = [] | rev (x # xs) = rev xs @ [x] with @ being the notation for list append, i.e., concatenation of two words.
The predicates for prefix and sufix are already part of the Isabelle distribution in the theory HOL-Library.Sublist: definition prefix :: ′a list ⇒ ′a list ⇒ bool where prefix xs ys →← definition sufix :: ′a list ⇒ ′a list ⇒ bool where sufix xs ys
The second example is constituted by the pair of symmetric definitions of the first and the last letter of a word, i.e., element of a list. In Isabelle/HOL, the first element of a list is its head, realized as one of two selectors, named hd, of the list constructor Cons. The last letter is the recursive function last: primrec (nonexhaustive) last :: ′a list ⇒ ′a where
last (x # xs) = (if xs = [] then x else last xs) given in the main theory List. To obtain a simple enough symmetry rule for hd and last, it sufices to notice that they behave the same way on the empty list.
lemma hd_last_Nil: hd [] = last [] unfolding hd_def last_def by simp lemma hd_rev_last: hd(rev xs) = last xs by (induct xs, simp add: hd_last_Nil, simp)
lemma example2: u ̸= [] =⇒ prefix u v =⇒ hd u = hd v lemma example2_sym: u ̸= [] =⇒ sufix u v
=⇒ last u = last v
The goal is to obtain example2_sym from example2 by symmetry. We proceed analogously to the proof of Lemma 2 above using standard methods in Isabelle/HOL: example2[of rev u rev v, unfolded rev_is_Nil_conv sufix_to_prefix [symmetric] hd_rev_last] where rev_is_Nil_conv is (rev xs = []) = (xs = []) and suffix_to_prefix[symmetric] is prefix (rev xs) (rev ys) = suffix xs ys. That is, we instantiate every variable of example2 by its reversal to obtain rev u ̸= [] =⇒ prefix (rev u) (rev v) =⇒ hd (rev u) = hd (rev v), and then rewrite the terms using appropriate symmetry rules, via the unfolded attribute (which is analogous to what was done in the proof of Lemma 2 above). We end up with example2_sym and the proof by symmetry is done. 2.3. Example 3 The next example is the following pair of symmetric facts. Applying the same strategy as for example2 fails, since trying to obtain example3_sym from example3[of rev u rev p rev w rev q, unfolded symmetry_rules], where symmetry_rules is a list of appropriate symmetry rules, leaves us with which is not yet in the form of example3_sym. This is not unexpected, the claim contains a bound variable r. To finish the conversion, it sufices to realize that (∃. ()) ↔ (∃. (rev )) holds. Thus, we may replace the last two occurrences of r with rev r, and apply appropriate symmetric rules.
The next section addresses our realization of automatic production of symmetric rules, preceded by a discussion on the use of existing tools.
Before describing our solution to the automation of producing symmetrical claims, we discuss if and how might our task be achieved using tools for theorem reuse available in Isabelle/HOL. We have not found any ready made tool in Isabelle/HOL that could achieve our objectives. We shall briefly discuss two existing tools that achieve a similar task, namely reusing of a theory in a homomorphic setting.
The first tool are locales. Locale is a mechanism for abstraction via interpretation and locale
expressions [
The second tool is the infrastructure of transfer [
Since it seems from the above discussion that there is no direct way how to achieve the desired automation of the symmetry, we propose a “lightweight” solution which closely mimics the simple reproving of each individual claim “on the fly” as indicated by the examples in Section 2. Our solution is very simple but at the same time it proves to be very practical and suficiently versatile.
It is created as a single attribute called “reversed”. The symmetry rules are collected as a list of theorems called “reversal_rule”, i.e., a user can add and remove them any time. By default, rules are required to eliminate reversal images, thus the reversal images are supposed to be on the left side of the equalities serving as rules. For instance, the symmetry rule Lemma 3 is stored in this form sufix (rev p) (rev w) = prefix p w.
The execution follows examples of Sections 2.2 and 2.3: first, all schematic variables of type list of the fact being reversed are instantiated by their reversals. Before the application of the symmetry rules, bound variables need to be treated. Let us indicate this procedure on example3 of Section 2.3 which contains one bound variable. As indicated above, the idea is to use the equivalence (∃. ()) ↔ (∃. (rev )). We introduce a helper (private) definition and 2 claims as follows: definition Ex_rev_wrap :: ( ′a list ⇒ bool) ⇒ bool
where Ex_rev_wrap P = (∃ x. P (rev x)) lemma Ex_rev_wrapI: ∃ x. P x ≡ Ex_rev_wrap P lemma Ex_rev_wrapE: Ex_rev_wrap ( x. P x) ≡ ∃ x. P (rev x)
example3[of rev u rev p rev w rev q,unfolded Ex_rev_wrapI], which yields The next step is resulting in example3[of rev u rev p rev w rev q,unfolded Ex_rev_wrapI, unfolded Ex_rev_wrapE] prefix (rev u) (rev p @ rev w @ rev q) =⇒ length (rev p) ≤ length (rev u) =⇒ length (rev u) ≤ length (rev p @ rev w) =⇒ ∃ r. rev u = rev p @ rev r ∧ prefix (rev r) (rev w).
Note that the name of the bound variable is preserved in this step. It is due to ( x. P x) being present in Ex_rev_wrapE rather than just P.
This two step rewriting using the definition Ex_rev_wrap in the intermediate step is to prevent an infinite loop of rewriting while trying to go directly from ∃ x. P x to ∃ x. P (rev x).
The last form is ready for the application of symmetry rules, and we almost obtain our goal, example3_sym. The remaining diference is the order of application of @, i.e., the arrangement of parentheses. The operation @ is associative and this final adjustment is left to be done manually, if desirable.
The implementation deals with other types of bound variables in a similar manner using a
definition analogous to Ex_rev_wrap and its two associated wrapping and unwrapping rules.
In a similar spirit, a special care for the constructors Nil and Cons is also part of the reversing
process. The described implementation is available at [
To show the current limits, consider the following pair of symmetric claims: lemma example4: prefix ps ws =⇒ prefix (concat ps) (concat ws) lemma example4_sym: sufix ps ws
=⇒ sufix (concat ps) (concat ws)
sufix ps ws
=⇒ prefix (concat (rev ps)) (concat (rev ws))
The problem here is that we are dealing with variables of type ′a list list, representing factorizations or decomposition of words. As they are of type ′b list, the reversing happens only on this level, whereas to produce example4_sym one would need the reversing to act on ′a list = ′b. Namely, the additional required action of the symmetry on ps and ws is the application of map rev. The reason that this represents a current limit is that the choice of correct reversal rules for variables of type ′a list list becomes crucial and it is no more clear what are the correct reversal rules.
Although the implemented attribute seems to be very simple, together with many delicately
selected reversal rules it is very useful in our current project of formalization of Combinatorics
on Words [
As the attribute is a part of a living project, and the time period between the acceptance and publication of this article was noticeable, the obstacle exhibited in the previous section has been already surmounted in a way to suit the needs of the project. However, the goal to properly deal with variables of any type remains. In order to do that, our tentative model of the symmetry in question needs to be generalized and validated.
Acknowledgements The authors acknowledge support by the Czech Science Foundation grant GAČR 20-20621S.