Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
I want to define a translation function g from another function f.
Definition trans (f g : Q -> Q) (t : Q) :=
forall q : Q, f (q + t) == g q.
In the above code, I implicitly define a translation g.
However, I'm unsatisfied with this definition.
In the case that a function f is declared, I want to define a translation function explicitly with a fixed distance (for example, 1).
Do you mean a functional like below ?
Definition trans (t:nat){A: Type}(f: nat-> A) := fun n => f (t+n).
Definition g := trans 3 (fun n => 2 * n).
Compute g 10.
