From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/bugs/closed/4745.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test-suite/bugs/closed/4745.v (limited to 'test-suite/bugs/closed/4745.v') diff --git a/test-suite/bugs/closed/4745.v b/test-suite/bugs/closed/4745.v new file mode 100644 index 00000000..c090125e --- /dev/null +++ b/test-suite/bugs/closed/4745.v @@ -0,0 +1,35 @@ +(*I get an Anomaly in the following code. + +```*) +Require Vector. + +Module M. + Lemma Vector_map_map : + forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n), + Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v. + Proof. + induction v; simpl; auto using f_equal. + Qed. + + Lemma Vector_map_map_transparent : + forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n), + Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v. + Proof. + induction v; simpl; auto using f_equal. + Defined. + (* Anomaly: constant not found in kind_of_head: Coq.Vectors.Vector.t_ind. Please report. *) + + (* strangely, explicitly passing the principle to induction works *) + Lemma Vector_map_map_transparent' : + forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n), + Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v. + Proof. + induction v using Vector.t_ind; simpl; auto using f_equal. + Defined. +End M. +(*``` + +Changing any of the following things eliminates the Anomaly + * moving the lemma out of the module M to the top level + * proving the lemma as a Fixpoint instead of using induction + * proving the analogous lemma on lists instead of vectors*) -- cgit v1.2.3