diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 12:36:30 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 16:17:09 +0100 |
commit | 4f2bbf0c82f8ea4ba26990770fb1f103a6ca1668 (patch) | |
tree | 155b33821acfd18702fcd5daffa0802b2d2b4fe9 /test-suite/success/induct.v | |
parent | 34d52eb3577fa329e4637409e8d602fd23ac126d (diff) |
Compatibility with 8.4 in the heuristic used to build the induction
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
Diffstat (limited to 'test-suite/success/induct.v')
-rw-r--r-- | test-suite/success/induct.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4b0b5d01c..0d0466cb5 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -113,3 +113,30 @@ induction x as [|n IHn]. 2:change (n = 0) in IHn. (* We don't want a generalization over cond *) Abort. End S3. + +(* These examples show somehow arbitrary choices of generalization wrt + to indices, when those indices are not linear. We check here 8.4 + compatibility: when an index is a subterm of a parameter of the + inductive type, it is not generalized. *) + +Inductive repr (x:nat) : nat -> Prop := reprc z : repr x z -> repr x z. + +Goal forall x, 0 = x -> repr x x -> True. +intros x H1 H. +induction H. +change True in IHrepr. +Abort. + +Goal forall x, 0 = S x -> repr (S x) (S x) -> True. +intros x H1 H. +induction H. +change True in IHrepr. +Abort. + +Inductive repr' (x:nat) : nat -> Prop := reprc' z : repr' x (S z) -> repr' x z. + +Goal forall x, 0 = x -> repr' x x -> True. +intros x H1 H. +induction H. +change True in IHrepr'. +Abort. |