Say I have a proved lemma "obvious", which states every Type is also a Solvable.
obvious : ∀ {A : Type} → Solvable A
obvious = one-proof
And I have a lemma "trivial", which somehow requires a Type A and Solvable p (depends on A),
trivial : ∀ {A : Type} {p : Solvable A} → A <: Top
trivial = another-proof
Everytime I want to use this "trivial" lemma, I probably need to write explicitly arguments A and p
trivial {A} {obvious A}
It's rather boring to write those proof because A can be inferred, but p cannot because type -checker doesn't know my "obvious" lemma so that I need to write it again and again.
How to avoid this situation?
In fact I've taken two attempts:
Attempt 1
Drop arguments p and use with-abstraction to create immediate one.
trivial : ∀ {A : Type} → A <: Top
trivial {A} with obvious A
... | branch = another-proof
It didn't solve my case because in reality I need to do some induction on p and then recursive call "trivial" function with sub-structures of p. Agda termination checker will complain about it.
Attempt 2
As suggested by Agda docs, use @tactic. But I cannot find more information on its usage, can someone illustrate on this?
Aha, I was hinted by an answer via function composition
trivial : ∀ {A : Type} → A <: Top
trivial {A} = trivial-verbose {A} {obvious A}
where
trivial-verbose : ∀ {A : Type} {p : Solvable A} → A <: Top
trivial-verbose = another-proof
then we can always use "trivial" without explicitly writing arguments.