diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/bugs/closed/4069.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/bugs/closed/4069.v')
-rw-r--r-- | test-suite/bugs/closed/4069.v | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v new file mode 100644 index 00000000..21b03ce5 --- /dev/null +++ b/test-suite/bugs/closed/4069.v @@ -0,0 +1,51 @@ + +Lemma test1 : +forall (v : nat) (f g : nat -> nat), +f v = g v. +intros. f_equal. +(* +Goal in v8.5: f v = g v +Goal in v8.4: v = v -> f v = g v +Expected: f = g +*) +Admitted. + +Lemma test2 : +forall (v u : nat) (f g : nat -> nat), +f v = g u. +intros. f_equal. +(* +In both v8.4 And v8.5 +Goal 1: v = u -> f v = g u +Goal 2: v = u + +Expected Goal 1: f = g +Expected Goal 2: v = u +*) +Admitted. + +Lemma test3 : +forall (v : nat) (u : list nat) (f : nat -> nat) (g : list nat -> nat), +f v = g u. +intros. f_equal. +(* +In both v8.4 And v8.5, the goal is unchanged. +*) +Admitted. + +Require Import List. +Lemma foo n (l k : list nat) : k ++ skipn n l = skipn n l. +Proof. f_equal. +(* + 8.4: leaves the goal unchanged, i.e. k ++ skipn n l = skipn n l + 8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l + and skipn n l = l +*) +Require Import List. +Fixpoint replicate {A} (n : nat) (x : A) : list A := + match n with 0 => nil | S n => x :: replicate n x end. +Lemma bar {A} n m (x : A) : + skipn n (replicate m x) = replicate (m - n) x -> + skipn n (replicate m x) = replicate (m - n) x. +Proof. intros. f_equal. +(* 8.5: one goal, n = m - n *) |