Strongly Connected Components #
This file defines tactics to construct proofs of equivalences between a set of mutually equivalent propositions. The tactics use implications transitively to find sets of equivalent propositions.
Implementation notes #
The tactics use a strongly connected components algorithm on a graph where propositions are vertices and edges are proofs that the source implies the target. The strongly connected components are therefore sets of propositions that are pairwise equivalent to each other.
The resulting strongly connected components are encoded in a disjoint set data structure to facilitate the construction of equivalence proofs between two arbitrary members of an equivalence class.
Possible generalizations #
Instead of reasoning about implications and equivalence, we could generalize the machinery to reason about arbitrary partial orders.
- Tarjan, R. E. (1972), "Depth-first search and linear graph algorithms", SIAM Journal on Computing, 1 (2): 146–160, doi:10.1137/0201010
- Dijkstra, Edsger (1976), A Discipline of Programming, NJ: Prentice Hall, Ch. 25.
graphs, tactic, strongly connected components, disjoint sets
scc uses the available equivalences and implications to prove
a goal of the form
p ↔ q.
example (p q r : Prop) (hpq : p → q) (hqr : q ↔ r) (hrp : r → p) : p ↔ r := by scc
scc' populates the local context with all equivalences that
scc is able to prove.
This is mostly useful for testing purposes.