NOTE - I abandoned this repository and contributed to the standard library's cong! tactic instead.

Kong

Kong provides one thing, kong, which is a version of cong that automatically figures out its first argument, i.e., where in a goal to apply the equality given by its second argument.

It looks at the left-hand side of a goal, finds all occurrences of the equality's left-hand side in it, and constructs a function that applies the equality to all of them.

This is more naive than what the standard library's cong! tactic does, which compares the goal's left-hand and right-hand sides, figures out the differences, and constructs a function that applies the equality exactly where the differences are.

In my use cases, Kong's more naive approach seems a little more robust. It handles, for example, turning x + y into y + x.

Note that the equality must not have any implicit or instance arguments left. For example, to use m*n%n≡0 you need to explicitly provide the NonZero argument:

... ≡⟨ kong (m*n%n≡0 x d ⦃ d≢0 ⦄) ⟩