@@ -195,3 +195,31 @@ refine tm =
195195 where countPi : Raw -> Nat
196196 countPi (RBind _ (Pi _ _) body) = S (countPi body)
197197 countPi _ = Z
198+
199+
200+||| Split a pair into its projections, binding them in the context
201+||| with the supplied names. A special case of Coq's `inversion`.
202+both : Raw -> TTName -> TTName -> Elab ()
203+both tm n1 n2 =
204+ do -- We don't know that the term is canonical, so let-bind projections applied to it
205+ (A, B) <- isPairTy (snd !(check tm))
206+ remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
207+ remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
208+ where
209+ isPairTy : TT -> Elab (Raw, Raw)
210+ isPairTy `((~A, ~B) : Type) = [| MkPair (forgetTypes A) (forgetTypes B) |]
211+ isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]
212+
213+||| Let-bind all results of completely destructuring nested tuples.
214+|||
215+||| This makes them available to the `hypothesis` tactic, among others.
216+|||
217+||| @ tm the nested tuple to destructure
218+covering
219+unproduct : (tm : Raw) -> Elab ()
220+unproduct tm =
221+ do n1 <- gensym "left"
222+ n2 <- gensym "right"
223+ both tm n1 n2
224+ try (unproduct (Var n1))
225+ try (unproduct (Var n2))