diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-26 10:55:15 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-26 11:01:28 +0200 |
commit | 4ae315f92e4a9849a56d3d9b0da33027f362d6e8 (patch) | |
tree | f1a41706cd8de59b5ce215ff66f8107299fc791f /test-suite/bugs/closed/4725.v | |
parent | 62fa31d219dcf2129c55b3c46b8cc25be60edcab (diff) |
Univs/Program/Function: Fix bug #4725
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
Diffstat (limited to 'test-suite/bugs/closed/4725.v')
-rw-r--r-- | test-suite/bugs/closed/4725.v | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 000000000..fd5e0fb60 --- /dev/null +++ b/test-suite/bugs/closed/4725.v @@ -0,0 +1,38 @@ +Require Import EquivDec Equivalence List Program. +Require Import Relation_Definitions. +Import ListNotations. +Generalizable All Variables. + +Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V +:= + match l with + | nil => nil + | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl) + end. + +Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (xs : list V) (x : V) : + length (removeV x xs) < length (x :: xs). + Proof. Admitted. + +(* Function version *) +Set Printing Universes. + +Require Import Recdef. + +Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (l : list V) { measure length l} := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) + end. +Proof. intros. apply remove_le. Qed. + +(* Program version *) + +Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V) + { measure (@length V l) lt } := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _ + end. |