Stlc.CalcNotationsRecursive
Notation for reasoning using several transitive steps (recursive)
Inspired by this: https://gist.github.com/gallais/f046bcc2c348c5fed5e9
This notation is similar to
CalcNotations.v, but works for any number of transitive steps. However, it fails when one needs to use rewrites or, say ring, because we want to avoid writing the "middle points" when we use the notation. E.g. we write
_ = b by p for all the steps excluding the first one. They can be ommitted because we know that the previous equation "end" coincudes with the "start" of the current one, since we build a chain of transitive steps. Usually, these "middle points" can be inferred by Coq, but if we use
ltac:() to build terms witnessing the transitivity steps, the "middle points" might be not resolved yet and the tactics in the
ltac:() call might fail.
Notation "'calc' p" :=
p (
at level 70,
right associativity) :
calc_scope.
Notation "a = b 'by' p ; pr" := (@
eq_trans _ a b _ p pr) (
at level 70,
b at next level,
right associativity) :
calc_scope.
Notation "a = b 'by' p 'end'" := (@
eq_trans _ _ b b p (@
eq_refl _ b)) (
b at next level,
at level 70):
calc_scope.