From ff712dd78d10d790c7a42a84416aff9ff343205d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Jul 2016 20:00:30 -0400 Subject: [PATCH] test(tests/lean/run/unfold_crash): add Jared's repro --- tests/lean/run/unfold_crash.lean | 37 ++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/lean/run/unfold_crash.lean diff --git a/tests/lean/run/unfold_crash.lean b/tests/lean/run/unfold_crash.lean new file mode 100644 index 0000000000..e76b798106 --- /dev/null +++ b/tests/lean/run/unfold_crash.lean @@ -0,0 +1,37 @@ +import data.nat +open tactic + +inductive vector (A : Type) : nat → Type := + | nil {} : vector A 0 + | cons : Π {n}, A -> vector A n -> vector A (nat.succ n) + +definition vmap {A B : Type} (f : A -> B) : Π {n}, vector A n -> vector B n +| vmap vector.nil := vector.nil +| vmap (vector.cons x xs) := vector.cons (f x) (vmap xs) + +definition vappend {A} : Π {n m}, vector A n -> vector A m -> vector A (m + n) +| vappend vector.nil vector.nil := vector.nil +| vappend vector.nil (vector.cons x xs) := vector.cons x xs +| vappend (vector.cons x xs) vector.nil := vector.cons x (vappend xs vector.nil) +| vappend (vector.cons x xs) (vector.cons y ys) := vector.cons x (vappend xs (vector.cons y ys)) + +axiom Sorry : ∀ A, A + +theorem vappend_assoc : + Π {A : Type} {n m k : nat} (v1 : vector A n) (v2 : vector A m) (v3 : vector A k), + vappend (vappend v1 v2) v3 == vappend v1 (vappend v2 v3) := +by do + intros, + v <- get_local "v1", + induction_core semireducible v ("vector" <.> "rec_on") [], + v2 ← get_local "v2", + cases_using v2 ["m", "h2", "t2"], + trace_state, trace "------", + -- unfold only the first occurrence (i.e., the one of the form (vappend nil nil) + unfold_occs_of [1] "vappend", + trace_state, trace "------", + mk_const "Sorry" >>= apply, + -- unfold only the first occurrence (i.e., the one of the form (vappend nil (cons ...)) + unfold_occs_of [1] "vappend", + trace_state, trace "------", + repeat $ mk_const "Sorry" >>= apply