You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The scalar_tac tactic is heavily used as there are a lot of arithmetic proof obligations in the proofs. It can be dramatically improved, both in terms of performance and features.
For instance:
scalar_tac splits all the "cases" (the if ... then ... else ..., the match ... with but not the \/- maybe it should for the latter ones; for now it is handled afterwards by the omega tactic which scalar_tac delegates the end of the proof to) which appear in the context before calling simp_all. To be more precise and because it is expensive: it first attempts the proof without splitting, then retries after splitting. As progress tries scalar_tac on all arithmetic preconditions, the cost of failing on goals for which we split can be expensive. We should add an option to deactivate this behavior globally (and have some syntax to reactivate it on a per-case basis, like scalar_tac split).
scalar_tac applies some simplification lemmas during its preprocessing phase. For now, those lemmas are hardcoded in the tactic, but they should not: we should introduce attributes to add such lemmas in an extensible manner. Also, there are two simplification phases: one before the "saturation" phase, and one after, so we should have two sets of lemmas. For some context: the saturation phase introduces useful facts in the context, and the system is extensible (see this PR - note that since then we reimplemented our own saturation mechanism which doesn't use aesop: see here). For instance, if we have the lemma:
@[simp, scalar_tac replicate l x]theoremreplicate_length {α : Type u} (l : Nat) (x : α) :
(replicate l x).length = l := by
induction l <;> simp_all
Then whenever scalar_tac sees something of the shape replicate l x in the context, it will introduce the assumption (replicate l x).length = l in the preprocessing phase.
The two simplification phases (before saturation/after saturation) can be found here and there.
the lemmas introduced during the saturation phase can be improved. For instance, whenever scalar_tac sees Scalar.toNat x it introduces the fact (x.toNat : Int) = x.val \/ (x.toNat : Int) = - x.val. If the scalar is an unsigned scalar it is always positive, so the second case can not happen (omega performs a case split on all the disjunctions, so this has a cost). We could fix the issue if we added lemmas of the shape : (x.toNat : Int) = x.val \/ (x.toNat : Int) = - x.val <-> (x.toNat : Int) = x.val in the simplification lemmas (for after the saturation phase) for all the unsigned scalar types.
The text was updated successfully, but these errors were encountered:
The
scalar_tac
tactic is heavily used as there are a lot of arithmetic proof obligations in the proofs. It can be dramatically improved, both in terms of performance and features.For instance:
scalar_tac
splits all the "cases" (theif ... then ... else ...
, thematch ... with
but not the\/
- maybe it should for the latter ones; for now it is handled afterwards by theomega
tactic whichscalar_tac
delegates the end of the proof to) which appear in the context before callingsimp_all
. To be more precise and because it is expensive: it first attempts the proof without splitting, then retries after splitting. Asprogress
triesscalar_tac
on all arithmetic preconditions, the cost of failing on goals for which we split can be expensive. We should add an option to deactivate this behavior globally (and have some syntax to reactivate it on a per-case basis, likescalar_tac split
).scalar_tac
applies some simplification lemmas during its preprocessing phase. For now, those lemmas are hardcoded in the tactic, but they should not: we should introduce attributes to add such lemmas in an extensible manner. Also, there are two simplification phases: one before the "saturation" phase, and one after, so we should have two sets of lemmas. For some context: the saturation phase introduces useful facts in the context, and the system is extensible (see this PR - note that since then we reimplemented our own saturation mechanism which doesn't use aesop: see here). For instance, if we have the lemma:Then whenever
scalar_tac
sees something of the shapereplicate l x
in the context, it will introduce the assumption(replicate l x).length = l
in the preprocessing phase.The two simplification phases (before saturation/after saturation) can be found here and there.
scalar_tac
seesScalar.toNat x
it introduces the fact(x.toNat : Int) = x.val \/ (x.toNat : Int) = - x.val
. If the scalar is an unsigned scalar it is always positive, so the second case can not happen (omega
performs a case split on all the disjunctions, so this has a cost). We could fix the issue if we added lemmas of the shape :(x.toNat : Int) = x.val \/ (x.toNat : Int) = - x.val <-> (x.toNat : Int) = x.val
in the simplification lemmas (for after the saturation phase) for all the unsigned scalar types.The text was updated successfully, but these errors were encountered: