@@ -225,13 +225,16 @@ refine tm =
225225 countPi (RBind _ (Pi _ _) body) = S (countPi body)
226226 countPi _ = Z
227227
228+||| A helper to extract the type representation for term.
229+getTTType : Raw -> Elab TT
230+getTTType r = snd <$> check !getEnv r
228231
229232||| Split a pair into its projections, binding them in the context
230233||| with the supplied names. A special case of Coq's `inversion`.
231234both : Raw -> TTName -> TTName -> Elab ()
232235both tm n1 n2 =
233236 do -- We don't know that the term is canonical, so let-bind projections applied to it
234− (A, B) <- isPairTy (snd !(check !getEnv tm))
237+ (A, B) <- isPairTy !(getTTType tm)
235238 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
236239 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
237240 where
@@ -253,7 +256,6 @@ unproduct tm =
253256 try (unproduct (Var n1))
254257 try (unproduct (Var n2))
255258
256−
257259||| A special-purpose tactic that attempts to solve a goal using
258260||| `Refl`. This is useful for ensuring that goals in fact are trivial
259261||| when developing or testing other tactics; otherwise, consider
@@ -268,3 +270,47 @@ reflexivity =
268270 , NamePart `{reflexivity}
269271 , TextPart "is not applicable."
270272 ]
273+
274+||| Attempt to swap the sides of equality in a goal. If the goal is `x = y`,
275+||| after the invocation the focus will be on a hole of type `y = x`.
276+symmetry : Elab ()
277+symmetry =
278+ do [_,_,_,_,res] <- apply (Var `{{sym}}) [True, True, True, True, False]
279+ | _ => fail [TextPart "Failed while applying", NamePart `{symmetry}]
280+ solve
281+ focus res
282+
283+||| Swap the sides of an equality, saving the result in a `let`-binding.
284+||| Returns the generated name.
285+|||
286+||| @ t the equality proof to swap
287+||| @ hint a hint to use for generating the variable name for the result
288+symmetryAs : (t : Raw) -> (hint : String) -> Elab TTName
289+symmetryAs t hint =
290+ case !(getTTType t) of
291+ `((=) {A=~A} {B=~B} ~l ~r) =>
292+ do af <- forget A
293+ bf <- forget B
294+ lf <- forget l
295+ rf <- forget r
296+ let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)
297+ n <- gensym hint
298+ letbind n !(forget !(getTTType ts)) ts
299+ pure n
300+ tt => fail [TermPart tt, TextPart "is not an equality"]
301+
302+||| Apply a function term to an argument term, saving the result in a
303+||| `let`-binding. Returns the generated name.
304+|||
305+||| @ f the function to apply
306+||| @ x the term to apply to
307+||| @ hint a hint to use for generating the variable name for the result
308+applyAs : (f : Raw) -> (x : Raw) -> (hint : String) -> Elab TTName
309+applyAs f x hint =
310+ case !(getTTType f) of
311+ `(~xty -> ~yty) =>
312+ do let fx = RApp f x
313+ n <- gensym hint
314+ letbind n !(forget !(getTTType fx)) fx
315+ pure n
316+ ftt => fail [TermPart ftt, TextPart "is not a function"]