git.iko.soy/Idris-dev
on master help sign in
add symmetry, symmetryIn and applyIn
3ef0740Alex Gryzlov
libs/pruviloj/Pruviloj/Core.idr+41−1
compare with master
unifiedsplit
@@ -225,13 +225,19 @@ refine tm =
225 countPi (RBind _ (Pi _ _) body) = S (countPi body)
225 countPi (RBind _ (Pi _ _) body) = S (countPi body)
226 countPi _ = Z
226 countPi _ = Z
227
227
228+||| A helper to extract the type representation for term.
229+getTTType : Raw -> Elab TT
230+getTTType r = do
231+ env <- getEnv
232+ rty <- check env r
233+ pure $ snd rty
228
234
229||| Split a pair into its projections, binding them in the context
235||| Split a pair into its projections, binding them in the context
230||| with the supplied names. A special case of Coq's `inversion`.
236||| with the supplied names. A special case of Coq's `inversion`.
231both : Raw -> TTName -> TTName -> Elab ()
237both : Raw -> TTName -> TTName -> Elab ()
232both tm n1 n2 =
238both tm n1 n2 =
233 do -- We don't know that the term is canonical, so let-bind projections applied to it
239 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))
240+ (A, B) <- isPairTy !(getTTType tm)
235 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
241 remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
236 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
242 remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
237 where
243 where
@@ -268,3 +274,37 @@ reflexivity =
268 , NamePart `{reflexivity}
274 , NamePart `{reflexivity}
269 , TextPart "is not applicable."
275 , TextPart "is not applicable."
270 ]
276 ]
277+
278+||| Attempt to swap the sides of equality in a goal.
279+symmetry : Elab ()
280+symmetry = do
281+ [_,_,_,_,_] <- apply (Var `{{sym}}) [True, True, True, True, False]
282+ | _ => fail [TextPart "Failed while applying", NamePart `{symmetry} ]
283+ solve
284+ attack
285+
286+||| Swap the sides of an equality and bind the result to supplied name.
287+symmetryIn : Raw -> TTName -> Elab ()
288+symmetryIn t n = do
289+ tt <- getTTType t
290+ case tt of
291+ `((=) {A=~A} {B=~B} ~l ~r) => do
292+ 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+ tsty <- forget !(getTTType ts)
298+ letbind n tsty ts
299+ _ => fail [TermPart tt, TextPart "is not an equality"]
300+
301+||| Apply argument term to a function term and bind the result to supplied name.
302+applyIn : Raw -> Raw -> TTName -> Elab ()
303+applyIn f x n = do
304+ ftt <- getTTType f
305+ case ftt of
306+ `(~xty -> ~yty) => do
307+ let fx = RApp f x
308+ fxty <- forget !(getTTType fx)
309+ letbind n fxty fx
310+ _ => fail [TermPart ftt, TextPart "is not a function"]