Dana: By now we have stated a good dozen Eureka lemmas.
Alfrothul: True, that.
Dana: And they pretty much all have the same structure.
After: The same structure?
Dana: Well, yes: the left-hand side contains a call to the accumulator-passing tail-recursive function.
Alfrothul: Ah, right. And the right-hand side contains a call to the accumulator-passing tail-recursive function with the accumulator reset to its initial value.
Bong-sun: And this call is combined with the accumulator used in the left-hand side to equate the right-hand side and the left-hand side.
Dana: For example, take the power function:
Fixpoint power_acc (x n a : nat) : nat :=
match n with
O =>
a
| S n' =>
power_acc x n' (x * a)
end.
Definition power_alt (x n : nat) : nat :=
power_acc x n 1.
Alfrothul: Here is its Eureka lemma:
Lemma about_power_acc :
forall x n a : nat,
power_acc x n a = power_acc x n 1 * a.
Bong-sun: In this Eureka lemma, the left-hand side contains a call to power_acc with a given accumulator.
Dana: And the right-hand side contains a call to power_acc with the accumulator reset to its initial value.
Alfrothul: And this call is combined with the given accumulator to equate the right-hand side and the left-hand side.
The Fourth Wall: What about the title of this section?
Halcyon: What is it again?
The Fourth Wall (helpfully): “A generic Eureka lemma about resetting the accumulator”.
Halcyon: Thanks, Fourth Wall.
Dana: Right. Since all the Eureka lemmas have the same structure, we should be able to abstract this structure into something generic.
Bong-sun: Let’s see. We need a type for the accumulator, an identity element for this type, and a function to combine on the right-hand side:
Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) :=
... = ...
Dana: Now for a suitable left-hand side and right-hand side...
Alfrothul: Well, once we have applied power_aux to a base and an exponent, the result has type nat -> nat. So maybe we can just quantify that. Look:
Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) :=
... = ...
Bong-sun: We also need to quantify the accumulator:
Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) (a : A):=
... = ...
Alfrothul: Right. And then the left-hand side pretty much writes itself:
Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) (a : A):=
c a = ...
Bong-sun: The right-hand side should contain a call to c with the accumulator reset:
Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) (a : A):=
c a = ... (c id_A) ...
Dana: Right. And the result should be combined with the accumulator from the left-hand side:
Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) (a : A) : Prop :=
c a = combine_A (c id_A) a.
Pablito (helpfully): This definition is type correct.
Alfrothul: Thank you, Pablito. Let us try with the power function. The type of the computation is nat:
Check (make_Eureka_lemma nat).
Pablito: The *response* window reads:
make_Eureka_lemma nat
: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat -> Prop
Alfrothul: Thanks. The initial value of the accumulator is 1:
Check (make_Eureka_lemma nat 1).
Pablito: The *response* window reads:
make_Eureka_lemma nat 1
: (nat -> nat -> nat) -> (nat -> nat) -> nat -> Prop
Alfrothul: Thanks. The combination function is multiplication:
Check (make_Eureka_lemma nat 1 Nat.mul).
Pablito: The *response* window reads:
make_Eureka_lemma nat 1 Nat.mul
: (nat -> nat) -> nat -> Prop
Alfrothul: The computation is the application of power_acc to a base and an exponent. So we need a base and an exponent.
Bong-sun: Presto:
Check (forall x n : nat, make_Eureka_lemma nat 1 Nat.mul (power_acc x n)).
Pablito: Oops. The *response* window reads:
Error: In environment
x : nat
n : nat
The term "make_Eureka_lemma nat 1 Nat.mul (power_acc x n)" has type "nat -> Prop" which should be Set, Prop or Type.
Bong-sun: Ah, right, we need to also quantify the accumulator:
Check (forall x n a : nat, make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a).
Pablito: The *response* window reads:
forall x n a : nat, make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a
: Prop
Dana: Which is the Eureka lemma for power_acc.
Big silence.
The Fourth Wall: How about we break this big silence.
Pablito: Huh, I was going to do that.
Halcyon: It feels like we should prove something.
Dana: And you are right, Halcyon. This maker of Eureka lemmas is designed to make Eureka lemmas and so we should prove them:
Lemma about_power_acc :
forall x n a : nat,
make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a.
Pablito: Let me give it a try:
Proof.
unfold make_Eureka_lemma.
Halcyon (helpfully): The *goals* window reads:
============================
forall x n a : nat, power_acc x n a = power_acc x n 1 * a
Dana: Which is the Eureka lemma that we have already proved.
Bong-sun: Ah, right, the maker yields something that we need to prove.
Dana: Yup. It’s raison d’être is to express the common pattern of this class of Eureka lemmas.
Bong-sun: And so we can complete the proof:
exact about_power_acc.
Qed.
Halcyon: Yay!
Alfrothul: Let me try something:
Fixpoint add_acc (n a : nat) : nat :=
match n with
O =>
a
| S n' =>
add_acc n' (S a)
end.
Definition add_alt (n m : nat) : nat :=
add_acc n m.
Dana: OK. The tail-recursive version of the addition function with an accumulator.
Alfrothul: Yup. So the type of the computation is nat, the initial value of the accumulator is... Ah? m? Not 0?
Dana: That seems incidental. We should go for the neutral element of the combining operation.
Alfrothul: ...which is the addition function, so, OK, 0. Here we go:
Lemma about_add_acc_generically :
forall n a : nat,
make_Eureka_lemma nat 0 Nat.add (add_acc n) a.
Pablito: Let me give it a try:
Proof.
unfold make_Eureka_lemma.
Halcyon (helpfully): The *goals* window reads:
============================
forall n a : nat, add_acc n a = add_acc n 0 + a
Dana: Which is the Eureka lemma for the accumulator-passing tail-recursive addition function.
Alfrothul: And so we can complete the proof:
exact about_add_acc.
Qed.
Pablito: Hmm...
The Fourth Wall: How about some exercises?
Revisit the accumulator-passing tail-recursive list_length_alt function from the midterm project and state its Eureka lemma generically using make_Eureka_lemma.
Revisit the accumulator-passing tail-recursive list_reverse_alt function from the midterm project and state its Eureka lemma generically using make_Eureka_lemma.
Revisit list_fold_left from the midterm project and state its Eureka lemma generically using make_Eureka_lemma.
Revisit the accumulator-passing tail-recursive factorial function and state its Eureka lemma generically using make_Eureka_lemma.
The resource file contains the declaration of binary trees of natural numbers and two implementations of a weight function that computes the sum of the leaves of any given binary tree of natural numbers.
Created [04 Apr 2024]