From 643d44e524e9b566fc82fef22b9767908b6c7e97 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 15 Feb 2017 10:01:49 -0500 Subject: [PATCH] Polymorphism: add a comment about the infamous quantifier-ordering issue with induction --- Polymorphism.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Polymorphism.v b/Polymorphism.v index 49fea50..b458dce 100644 --- a/Polymorphism.v +++ b/Polymorphism.v @@ -189,6 +189,13 @@ Proof. equality. Qed. +(* IMPORTANT NOTE: the proof above would *not* have worked with the orders of + * variables [ls] and [acc] swapped in the lemma statement! Try the proof that + * way to see what goes wrong. The problem is that the induction hypothesis + * would be too weak. A single [acc] value would be fixed for the whole proof, + * while we need [acc] to *vary* throughout the induction, by retaining a + * universal quantifier for it in the IH. *) + (* Concatenating the empty list has no effect. *) Lemma app_nil : forall A (ls : list A), ls ++ [] = ls.