1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
(* Was raising stack overflow in 8.4 and assertion failed in future 8.5 *)
Set Implicit Arguments.
Require Import List.
Require Import Coq.Program.Equality.
(** Reflexive-transitive closure ( R* ) *)
Inductive rtclosure (A : Type) (R : A-> A->Prop) : A->A->Prop :=
| rtclosure_refl : forall x,
rtclosure R x x
| rtclosure_step : forall y x z,
R x y -> rtclosure R y z -> rtclosure R x z.
(* bug goes away if rtclosure_step is commented out *)
(** The closure of the trivial binary relation [eq] *)
Definition tr (A:Type) := rtclosure (@eq A).
(** The bug *)
Lemma bug : forall A B (l t:list A) (r s:list B),
length l = length r ->
tr (combine l r) (combine t s) -> tr l t.
Proof.
intros * E Hp.
(* bug goes away if [revert E] is called explicitly *)
dependent induction Hp.
Abort.
|
