From edbd6a211c934778d9721c36463836ef902b4fdd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 3 Nov 2014 20:16:48 +0100 Subject: New bugs revealed fixed: #3408 by (probably) Maxime's commits on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459. --- test-suite/bugs/closed/3068.v | 60 ++++++++++++++++ test-suite/bugs/closed/3408.v | 163 ++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/3068.v | 60 ---------------- test-suite/bugs/opened/3408.v | 163 ------------------------------------------ test-suite/bugs/opened/3459.v | 4 +- 5 files changed, 225 insertions(+), 225 deletions(-) create mode 100644 test-suite/bugs/closed/3068.v create mode 100644 test-suite/bugs/closed/3408.v delete mode 100644 test-suite/bugs/opened/3068.v delete mode 100644 test-suite/bugs/opened/3408.v diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v new file mode 100644 index 0000000000..7cdd4ea17e --- /dev/null +++ b/test-suite/bugs/closed/3068.v @@ -0,0 +1,60 @@ +Section Counted_list. + + Variable A : Type. + + Inductive counted_list : nat -> Type := + | counted_nil : counted_list 0 + | counted_cons : forall(n : nat), + A -> counted_list n -> counted_list (S n). + + + Fixpoint counted_def_nth{n : nat}(l : counted_list n) + (i : nat)(def : A) : A := + match i with + | 0 => match l with + | counted_nil => def + | counted_cons _ a _ => a + end + | S i => match l with + | counted_nil => def + | counted_cons _ _ tl => counted_def_nth tl i def + end + end. + + + Lemma counted_list_equal_nth_char : + forall(n : nat)(l1 l2 : counted_list n)(def : A), + (forall(i : nat), counted_def_nth l1 i def = counted_def_nth l2 i def) -> + l1 = l2. + Proof. + admit. + Qed. + +End Counted_list. + +Implicit Arguments counted_def_nth [A n]. + +Section Finite_nat_set. + + Variable set_size : nat. + + Definition fnat_subset : Type := counted_list bool set_size. + + Definition fnat_member(fs : fnat_subset)(n : nat) : Prop := + is_true (counted_def_nth fs n false). + + + Lemma fnat_subset_member_eq : forall(fs1 fs2 : fnat_subset), + fs1 = fs2 <-> + forall(n : nat), fnat_member fs1 n <-> fnat_member fs2 n. + + Proof. + intros fs1 fs2. + split. + intros H n. + subst fs1. + apply iff_refl. + intros H. + eapply counted_list_equal_nth_char. + intros i. + destruct (counted_def_nth fs1 i _ ) eqn:H0. diff --git a/test-suite/bugs/closed/3408.v b/test-suite/bugs/closed/3408.v new file mode 100644 index 0000000000..b12b8c1afb --- /dev/null +++ b/test-suite/bugs/closed/3408.v @@ -0,0 +1,163 @@ +Require Import BinPos. + +Inductive expr : Type := + Var : nat -> expr +| App : expr -> expr -> expr +| Abs : unit -> expr -> expr. + +Inductive expr_acc +: expr -> expr -> Prop := + acc_App_l : forall f a : expr, + expr_acc f (App f a) +| acc_App_r : forall f a : expr, + expr_acc a (App f a) +| acc_Abs : forall (t : unit) (e : expr), + expr_acc e (Abs t e). + +Theorem wf_expr_acc : well_founded expr_acc. +Proof. + red. + refine (fix rec a : Acc expr_acc a := + match a as a return Acc expr_acc a with + | Var v => Acc_intro _ (fun y (_H : expr_acc y (Var v)) => + match _H in expr_acc z Z + return match Z return Prop with + | Var _ => Acc _ y + | _ => True + end + with + | acc_App_l _ _ => I + | _ => I + end) + | App f x => Acc_intro _ (fun y (pf : expr_acc y (App f x)) => + match pf in expr_acc z Z + return match Z return Prop with + | App a b => f = a -> x = b -> Acc expr_acc z + | _ => True + end + with + | acc_App_l f' x' => fun pf _ => match pf in _ = z return + Acc expr_acc z + with + | eq_refl => rec f + end + | acc_App_r f' x' => fun _ pf => match pf in _ = z return + Acc expr_acc z + with + | eq_refl => rec x + end + | _ => I + end eq_refl eq_refl) + | Abs t e => Acc_intro _ (fun y (pf : expr_acc y (Abs t e)) => + match pf in expr_acc z Z + return match Z return Prop with + | Abs a b => e = b -> Acc expr_acc z + | _ => True + end + with + | acc_Abs f x => fun pf => match pf in _ = z return + Acc expr_acc z + with + | eq_refl => rec e + end + | _ => I + end eq_refl) + end). +Defined. + +Theorem wf_expr_acc_delay : well_founded expr_acc. +Proof. + red. + refine (fix rec a : Acc expr_acc a := + match a as a return Acc expr_acc a with + | Var v => Acc_intro _ (fun y (_H : expr_acc y (Var v)) => + match _H in expr_acc z Z + return match Z return Prop with + | Var _ => Acc _ y + | _ => True + end + with + | acc_App_l _ _ => I + | _ => I + end) + | App f x => Acc_intro _ (fun y (pf : expr_acc y (App f x)) => + match pf in expr_acc z Z + return match Z return Prop with + | App a b => (unit -> Acc expr_acc a) -> (unit -> Acc expr_acc b) -> Acc expr_acc z + | _ => True + end + with + | acc_App_l f' x' => fun pf _ => pf tt + | acc_App_r f' x' => fun _ pf => pf tt + | _ => I + end (fun _ => rec f) (fun _ => rec x)) + | Abs t e => Acc_intro _ (fun y (pf : expr_acc y (Abs t e)) => + match pf in expr_acc z Z + return match Z return Prop with + | Abs a b => (unit -> Acc expr_acc b) -> Acc expr_acc z + | _ => True + end + with + | acc_Abs f x => fun pf => pf tt + | _ => I + end (fun _ => rec e)) + end); + try solve [ inversion _H ]. +Defined. + +Fixpoint build_large (n : nat) : expr := + match n with + | 0 => Var 0 + | S n => + let e := build_large n in + App e e + end. + +Section guard. + Context {A : Type} {R : A -> A -> Prop}. + + Fixpoint guard (n : nat) (wfR : well_founded R) : well_founded R := + match n with + | 0 => wfR + | S n0 => + fun x : A => + Acc_intro x + (fun (y : A) (_ : R y x) => guard n0 (guard n0 wfR) y) + end. +End guard. + + +Definition sizeF_delay : expr -> positive. +refine + (@Fix expr (expr_acc) + (wf_expr_acc_delay) + (fun _ => positive) + (fun e => + match e as e return (forall l, expr_acc l e -> positive) -> positive with + | Var _ => fun _ => 1 + | App l r => fun rec => @rec l _ + @rec r _ + | Abs _ e => fun rec => 1 + @rec e _ + end%positive)). +eapply acc_App_l. +eapply acc_App_r. +eapply acc_Abs. +Defined. + +Definition sizeF_guard : expr -> positive. +refine + (@Fix expr (expr_acc) + (guard 5 wf_expr_acc) + (fun _ => positive) + (fun e => + match e as e return (forall l, expr_acc l e -> positive) -> positive with + | Var _ => fun _ => 1 + | App l r => fun rec => @rec l _ + @rec r _ + | Abs _ e => fun rec => 1 + @rec e _ + end%positive)). +eapply acc_App_l. +eapply acc_App_r. +eapply acc_Abs. +Defined. + +Time Eval native_compute in sizeF_delay (build_large 2). +Time Eval native_compute in sizeF_guard (build_large 2). diff --git a/test-suite/bugs/opened/3068.v b/test-suite/bugs/opened/3068.v deleted file mode 100644 index 5d3bc0cbc6..0000000000 --- a/test-suite/bugs/opened/3068.v +++ /dev/null @@ -1,60 +0,0 @@ -Section Counted_list. - - Variable A : Type. - - Inductive counted_list : nat -> Type := - | counted_nil : counted_list 0 - | counted_cons : forall(n : nat), - A -> counted_list n -> counted_list (S n). - - - Fixpoint counted_def_nth{n : nat}(l : counted_list n) - (i : nat)(def : A) : A := - match i with - | 0 => match l with - | counted_nil => def - | counted_cons _ a _ => a - end - | S i => match l with - | counted_nil => def - | counted_cons _ _ tl => counted_def_nth tl i def - end - end. - - - Lemma counted_list_equal_nth_char : - forall(n : nat)(l1 l2 : counted_list n)(def : A), - (forall(i : nat), counted_def_nth l1 i def = counted_def_nth l2 i def) -> - l1 = l2. - Proof. - admit. - Qed. - -End Counted_list. - -Implicit Arguments counted_def_nth [A n]. - -Section Finite_nat_set. - - Variable set_size : nat. - - Definition fnat_subset : Type := counted_list bool set_size. - - Definition fnat_member(fs : fnat_subset)(n : nat) : Prop := - is_true (counted_def_nth fs n false). - - - Lemma fnat_subset_member_eq : forall(fs1 fs2 : fnat_subset), - fs1 = fs2 <-> - forall(n : nat), fnat_member fs1 n <-> fnat_member fs2 n. - - Proof. - intros fs1 fs2. - split. - intros H n. - subst fs1. - apply iff_refl. - intros H. - eapply counted_list_equal_nth_char. - intros i. - Fail destruct (counted_def_nth fs1 i _ ) eqn:H0. diff --git a/test-suite/bugs/opened/3408.v b/test-suite/bugs/opened/3408.v deleted file mode 100644 index 921f641558..0000000000 --- a/test-suite/bugs/opened/3408.v +++ /dev/null @@ -1,163 +0,0 @@ -Require Import BinPos. - -Inductive expr : Type := - Var : nat -> expr -| App : expr -> expr -> expr -| Abs : unit -> expr -> expr. - -Inductive expr_acc -: expr -> expr -> Prop := - acc_App_l : forall f a : expr, - expr_acc f (App f a) -| acc_App_r : forall f a : expr, - expr_acc a (App f a) -| acc_Abs : forall (t : unit) (e : expr), - expr_acc e (Abs t e). - -Theorem wf_expr_acc : well_founded expr_acc. -Proof. - red. - refine (fix rec a : Acc expr_acc a := - match a as a return Acc expr_acc a with - | Var v => Acc_intro _ (fun y (_H : expr_acc y (Var v)) => - match _H in expr_acc z Z - return match Z return Prop with - | Var _ => Acc _ y - | _ => True - end - with - | acc_App_l _ _ => I - | _ => I - end) - | App f x => Acc_intro _ (fun y (pf : expr_acc y (App f x)) => - match pf in expr_acc z Z - return match Z return Prop with - | App a b => f = a -> x = b -> Acc expr_acc z - | _ => True - end - with - | acc_App_l f' x' => fun pf _ => match pf in _ = z return - Acc expr_acc z - with - | eq_refl => rec f - end - | acc_App_r f' x' => fun _ pf => match pf in _ = z return - Acc expr_acc z - with - | eq_refl => rec x - end - | _ => I - end eq_refl eq_refl) - | Abs t e => Acc_intro _ (fun y (pf : expr_acc y (Abs t e)) => - match pf in expr_acc z Z - return match Z return Prop with - | Abs a b => e = b -> Acc expr_acc z - | _ => True - end - with - | acc_Abs f x => fun pf => match pf in _ = z return - Acc expr_acc z - with - | eq_refl => rec e - end - | _ => I - end eq_refl) - end). -Defined. - -Theorem wf_expr_acc_delay : well_founded expr_acc. -Proof. - red. - refine (fix rec a : Acc expr_acc a := - match a as a return Acc expr_acc a with - | Var v => Acc_intro _ (fun y (_H : expr_acc y (Var v)) => - match _H in expr_acc z Z - return match Z return Prop with - | Var _ => Acc _ y - | _ => True - end - with - | acc_App_l _ _ => I - | _ => I - end) - | App f x => Acc_intro _ (fun y (pf : expr_acc y (App f x)) => - match pf in expr_acc z Z - return match Z return Prop with - | App a b => (unit -> Acc expr_acc a) -> (unit -> Acc expr_acc b) -> Acc expr_acc z - | _ => True - end - with - | acc_App_l f' x' => fun pf _ => pf tt - | acc_App_r f' x' => fun _ pf => pf tt - | _ => I - end (fun _ => rec f) (fun _ => rec x)) - | Abs t e => Acc_intro _ (fun y (pf : expr_acc y (Abs t e)) => - match pf in expr_acc z Z - return match Z return Prop with - | Abs a b => (unit -> Acc expr_acc b) -> Acc expr_acc z - | _ => True - end - with - | acc_Abs f x => fun pf => pf tt - | _ => I - end (fun _ => rec e)) - end); - try solve [ inversion _H ]. -Defined. - -Fixpoint build_large (n : nat) : expr := - match n with - | 0 => Var 0 - | S n => - let e := build_large n in - App e e - end. - -Section guard. - Context {A : Type} {R : A -> A -> Prop}. - - Fixpoint guard (n : nat) (wfR : well_founded R) : well_founded R := - match n with - | 0 => wfR - | S n0 => - fun x : A => - Acc_intro x - (fun (y : A) (_ : R y x) => guard n0 (guard n0 wfR) y) - end. -End guard. - - -Definition sizeF_delay : expr -> positive. -refine - (@Fix expr (expr_acc) - (wf_expr_acc_delay) - (fun _ => positive) - (fun e => - match e as e return (forall l, expr_acc l e -> positive) -> positive with - | Var _ => fun _ => 1 - | App l r => fun rec => @rec l _ + @rec r _ - | Abs _ e => fun rec => 1 + @rec e _ - end%positive)). -eapply acc_App_l. -eapply acc_App_r. -eapply acc_Abs. -Defined. - -Definition sizeF_guard : expr -> positive. -refine - (@Fix expr (expr_acc) - (guard 5 wf_expr_acc) - (fun _ => positive) - (fun e => - match e as e return (forall l, expr_acc l e -> positive) -> positive with - | Var _ => fun _ => 1 - | App l r => fun rec => @rec l _ + @rec r _ - | Abs _ e => fun rec => 1 + @rec e _ - end%positive)). -eapply acc_App_l. -eapply acc_App_r. -eapply acc_Abs. -Defined. - -Time Eval native_compute in sizeF_delay (build_large 2). -Fail Time Eval native_compute in sizeF_guard (build_large 2). diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v index 949cace1dc..7c01330990 100644 --- a/test-suite/bugs/opened/3459.v +++ b/test-suite/bugs/opened/3459.v @@ -12,8 +12,8 @@ match goal with exact r)$) in pose y end. -(* Add extra test for typability *) -match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end. +(* Add extra test for typability (should not fail when bug closed) *) +Fail match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end. Abort. (* Second report raising a Not_found at the time of 21 Oct 2014 *) -- cgit v1.2.3