diff options
Diffstat (limited to 'test-suite/bugs/closed')
49 files changed, 1508 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/1519.v b/test-suite/bugs/closed/1519.v new file mode 100644 index 00000000..98e3e214 --- /dev/null +++ b/test-suite/bugs/closed/1519.v @@ -0,0 +1,23 @@ +Section S. + + Variable A:Prop. + Variable W:A. + + Remark T: A -> A. + intro Z. + rename W into Z_. + rename Z into W. + rename Z_ into Z. + exact Z. + Qed. + + (* bug : + Error: + Unbound reference: In environment + A : Prop + W : A + Z : A + The reference 2 is free + *) + +End S. diff --git a/test-suite/bugs/closed/1780.v b/test-suite/bugs/closed/1780.v new file mode 100644 index 00000000..3929fbae --- /dev/null +++ b/test-suite/bugs/closed/1780.v @@ -0,0 +1,12 @@ + +Definition bug := Eval vm_compute in eq_rect. +(* bug: +Error: Illegal application (Type Error): +The term "eq" of type "forall A : Type, A -> A -> Prop" +cannot be applied to the terms + "x" : "A" + "P" : "A -> Type" + "x0" : "A" +The 1st term has type "A" which should be coercible to +"Type". +*) diff --git a/test-suite/bugs/closed/1787.v b/test-suite/bugs/closed/1787.v new file mode 100644 index 00000000..8e1024e6 --- /dev/null +++ b/test-suite/bugs/closed/1787.v @@ -0,0 +1,11 @@ +Parameter P : nat -> nat -> Prop. +Parameter Q : nat -> nat -> Prop. +Axiom A : forall x x' x'', P x x' -> Q x'' x' -> P x x''. + +Goal (P 1 3) -> (Q 1 3) -> (P 1 1). +intros H H'. +refine ((fun H1 : P 1 _ => let H2 := (_:Q 1 _) in A _ _ _ H1 H2) _). +clear. +Admitted. + + diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v new file mode 100644 index 00000000..6b5198cc --- /dev/null +++ b/test-suite/bugs/closed/shouldfail/1703.v @@ -0,0 +1,7 @@ +(* Check correct binding of intros until used in Ltac *) + +Ltac intros_until n := intros until n. + +Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0. +intro i. +intros until i. diff --git a/test-suite/bugs/closed/shouldsucceed/1041.v b/test-suite/bugs/closed/shouldsucceed/1041.v new file mode 100644 index 00000000..a5de82e0 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1041.v @@ -0,0 +1,13 @@ +Goal Prop. + +pose (P:=(fun x y :Prop => y)). +evar (Q: (forall X Y,P X Y -> Prop)) . + +instantiate (1:= fun _ => _ ) in (Value of Q). +instantiate (1:= fun _ => _ ) in (Value of Q). +instantiate (1:= fun _ => _ ) in (Value of Q). + +instantiate (1:=H) in (Value of Q). + +Admitted. + diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v new file mode 100644 index 00000000..6d619c74 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1100.v @@ -0,0 +1,12 @@ +Require Import Setoid. + +Parameter P : nat -> Prop. +Parameter Q : nat -> Prop. +Parameter PQ : forall n, P n <-> Q n. + +Lemma PQ2 : forall n, P n -> Q n. + intros. + rewrite PQ in H. + trivial. +Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v new file mode 100644 index 00000000..d193aa73 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/121.v @@ -0,0 +1,17 @@ +Require Import Setoid. + +Section Setoid_Bug. + +Variable X:Type -> Type. +Variable Xeq : forall A, (X A) -> (X A) -> Prop. +Hypothesis Xst : forall A, Equivalence (X A) (Xeq A). + +Variable map : forall A B, (A -> B) -> X A -> X B. + +Implicit Arguments map [A B]. + +Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c). +intros A B a b c f Hab Hbc. +rewrite Hab. +assumption. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1243.v b/test-suite/bugs/closed/shouldsucceed/1243.v new file mode 100644 index 00000000..7d6781db --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1243.v @@ -0,0 +1,12 @@ +Require Import ZArith. +Require Import Arith. +Open Scope Z_scope. + +Theorem r_ex : (forall x y:nat, x + y = x + y)%nat. +Admitted. + +Theorem r_ex' : forall x y:nat, (x + y = x + y)%nat. +Admitted. + + + diff --git a/test-suite/bugs/closed/shouldsucceed/1302.v b/test-suite/bugs/closed/shouldsucceed/1302.v new file mode 100644 index 00000000..e94dfcfb --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1302.v @@ -0,0 +1,22 @@ +Module Type T. + +Parameter A : Type. + +Inductive L : Type := +| L0 : L (* without this constructor, it works right *) +| L1 : A -> L. + +End T. + +Axiom Tp : Type. + +Module TT : T. + +Definition A : Type := Tp. + +Inductive L : Type := +| L0 : L +| L1 : A -> L. + +End TT. + diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v new file mode 100644 index 00000000..7e21aa7c --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1322.v @@ -0,0 +1,24 @@ +Require Import Setoid. + +Section transition_gen. + +Variable I : Type. +Variable I_eq :I -> I -> Prop. +Variable I_eq_equiv : Setoid_Theory I I_eq. + +(* Add Relation I I_eq + reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) + symmetry proved by I_eq_equiv.(Seq_sym I I_eq) + transitivity proved by I_eq_equiv.(Seq_trans I I_eq) +as I_eq_relation. *) + +Add Setoid I I_eq I_eq_equiv as I_with_eq. + +Variable F : I -> Type. +Variable F_morphism : forall i j, I_eq i j -> F i = F j. + + +Add Morphism F with signature I_eq ==> (@eq _) as F_morphism2. +Admitted. + +End transition_gen. diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v new file mode 100644 index 00000000..e330d46f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1411.v @@ -0,0 +1,35 @@ +Require Import List. +Require Import Program. + +Inductive Tree : Set := +| Br : Tree -> Tree -> Tree +| No : nat -> Tree +. + +(* given a tree, we want to know which lists can + be used to navigate exactly to a node *) +Inductive Exact : Tree -> list bool -> Prop := +| exDone n : Exact (No n) nil +| exLeft l r p: Exact l p -> Exact (Br l r) (true::p) +| exRight l r p: Exact r p -> Exact (Br l r) (false::p) +. + +Definition unreachable A : False -> A. +intros. +destruct H. +Defined. + +Program Fixpoint fetch t p (x:Exact t p) {struct t} := + match t, p with + | No p' , nil => p' + | No p' , _::_ => unreachable nat _ + | Br l r, nil => unreachable nat _ + | Br l r, true::t => fetch l t _ + | Br l r, false::t => fetch r t _ + end. + +Next Obligation. inversion x. Qed. +Next Obligation. inversion x. Qed. +Next Obligation. inversion x; trivial. Qed. +Next Obligation. inversion x; trivial. Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v new file mode 100644 index 00000000..d3c00808 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -0,0 +1,41 @@ +Require Import ZArith Coq.Program.Wf Coq.Program.Utils. + +Parameter data:Set. + +Inductive t : Set := + | Leaf : t + | Node : t -> data -> t -> Z -> t. + +Parameter avl : t -> Prop. +Parameter bst : t -> Prop. +Parameter In : data -> t -> Prop. +Parameter cardinal : t -> nat. +Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2. + +Parameter split : data -> t -> t*(bool*t). +Parameter join : t -> data -> t -> t. +Parameter add : data -> t -> t. + +Program Fixpoint union + (s:t*t) + (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) + { measure card2 s } : + {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd +s)} := + match s with + | (Leaf,t2) => t2 + | (t1,Leaf) => t1 + | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) => + if (Z_ge_lt_dec h1 h2) then + if (Z_eq_dec h2 1) + then add v2 (fst s) + else + let (l2', r2') := split v1 (snd s) in + join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _) + else + if (Z_eq_dec h1 1) + then add v1 (snd s) + else + let (l1', r1') := split v2 (fst s) in + join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _) + end. diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/shouldsucceed/1419.v new file mode 100644 index 00000000..d021107d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1419.v @@ -0,0 +1,8 @@ +Goal True. + set(a := 0). + set(b := a). + unfold a in b. + clear a. + Eval vm_compute in b. + trivial. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v new file mode 100644 index 00000000..8e26209a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1425.v @@ -0,0 +1,19 @@ +Require Import Setoid. + +Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A. + +Axiom recursion_S : + forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A) (n : nat), + EA (recursion A a f (S n)) (f n (recursion A a f n)). + +Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1. +intro n. +rewrite recursion_S. +reflexivity. +Qed. + +Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1. +intro n. +setoid_rewrite recursion_S. +reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v new file mode 100644 index 00000000..d4e7cea8 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1446.v @@ -0,0 +1,20 @@ +Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false. +Proof. + destruct b;intros;trivial. + elim H. + exact (refl_equal true). +Qed. + +Section BUG. + + Variable b : bool. + Hypothesis H : b <> true. + Hypothesis H0 : b = true. + Hypothesis H1 : b <> true. + + Goal False. + rewrite (not_true_eq_false _ H) in * |-. + contradiction. + Qed. + +End BUG. diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v new file mode 100644 index 00000000..fe3b4c8b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1448.v @@ -0,0 +1,28 @@ +Require Import Relations. +Require Import Setoid. +Require Import Ring_theory. +Require Import Ring_base. + + +Variable R : Type. +Variable Rone Rzero : R. +Variable Rplus Rmult Rminus : R -> R -> R. +Variable Rneg : R -> R. + +Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq +R). +Admitted. + +Variable Req : R -> R -> Prop. + +Hypothesis Req_refl : reflexive _ Req. +Hypothesis Req_sym : symmetric _ Req. +Hypothesis Req_trans : transitive _ Req. + +Add Relation R Req + reflexivity proved by Req_refl + symmetry proved by Req_sym + transitivity proved by Req_trans + as Req_rel. + +Add Ring my_ring : my_ring_theory (abstract). diff --git a/test-suite/bugs/closed/shouldsucceed/1477.v b/test-suite/bugs/closed/shouldsucceed/1477.v new file mode 100644 index 00000000..dfc8c328 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1477.v @@ -0,0 +1,18 @@ +Inductive I : Set := + | A : nat -> nat -> I + | B : nat -> nat -> I. + +Definition foo1 (x:I) : nat := + match x with + | A a b | B a b => S b + end. + +Definition foo2 (x:I) : nat := + match x with + | A _ b | B b _ => S b + end. + +Definition foo (x:I) : nat := + match x with + | A a b | B b a => S b + end. diff --git a/test-suite/bugs/closed/shouldsucceed/1483.v b/test-suite/bugs/closed/shouldsucceed/1483.v new file mode 100644 index 00000000..a3d7f168 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1483.v @@ -0,0 +1,10 @@ +Require Import BinPos. + +Definition P := (fun x : positive => x = xH). + +Goal forall (p q : positive), P q -> q = p -> P p. +intros; congruence. +Qed. + + + diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v new file mode 100644 index 00000000..b484c7dc --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1507.v @@ -0,0 +1,121 @@ +(* + Implementing reals a la Stolzenberg + + Danko Ilik, March 2007 + svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $ + + XField.v -- (unfinished) axiomatisation of the theories of real and + rational intervals. +*) + +Definition associative (A:Type)(op:A->A->A) := + forall x y z:A, op (op x y) z = op x (op y z). + +Definition commutative (A:Type)(op:A->A->A) := + forall x y:A, op x y = op y x. + +Definition trichotomous (A:Type)(R:A->A->Prop) := + forall x y:A, R x y \/ x=y \/ R y x. + +Definition relation (A:Type) := A -> A -> Prop. +Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x. +Definition transitive (A:Type)(R:relation A) := + forall x y z:A, R x y -> R y z -> R x z. +Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x. + +Record interval (X:Set)(le:X->X->Prop) : Set := + interval_make { + interval_left : X; + interval_right : X; + interval_nonempty : le interval_left interval_right + }. + +Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake { + Icar := interval grnd le; + Iplus : Icar -> Icar -> Icar; + Imult : Icar -> Icar -> Icar; + Izero : Icar; + Ione : Icar; + Iopp : Icar -> Icar; + Iinv : Icar -> Icar; + Ic : Icar -> Icar -> Prop; (* consistency *) + (* monoids *) + Iplus_assoc : associative Icar Iplus; + Imult_assoc : associative Icar Imult; + (* abelian groups *) + Iplus_comm : commutative Icar Iplus; + Imult_comm : commutative Icar Imult; + Iplus_0_l : forall x:Icar, Ic (Iplus Izero x) x; + Iplus_0_r : forall x:Icar, Ic (Iplus x Izero) x; + Imult_0_l : forall x:Icar, Ic (Imult Ione x) x; + Imult_0_r : forall x:Icar, Ic (Imult x Ione) x; + Iplus_opp_r : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero); + Imult_inv_r : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione; + (* distributive laws *) + Imult_plus_distr_l : forall x x' y y' z z' z'', + Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' -> + Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z'')); + (* order and lattice structure *) + Ilt : Icar -> Icar -> Prop; + Ilc := fun (x y:Icar) => Ilt x y \/ Ic x y; + Isup : Icar -> Icar -> Icar; + Iinf : Icar -> Icar -> Icar; + Ilt_trans : transitive _ lt; + Ilt_trich : forall x y:Icar, Ilt x y \/ Ic x y \/ Ilt y x; + Isup_lub : forall x y z:Icar, Ilc x z -> Ilc y z -> Ilc (Isup x y) z; + Iinf_glb : forall x y z:Icar, Ilc x y -> Ilc x z -> Ilc x (Iinf y z); + (* order preserves operations? *) + (* properties of Ic *) + Ic_refl : reflexive _ Ic; + Ic_sym : symmetric _ Ic +}. + +Definition interval_set (X:Set)(le:X->X->Prop) := + (interval X le) -> Prop. (* can be Set as well *) +Check interval_set. +Check Ic. +Definition consistent (X:Set)(le:X->X->Prop)(TI:I X le)(p:interval_set X le) := + forall I J:interval X le, p I -> p J -> (Ic X le TI) I J. +Check consistent. +(* define 'fine' *) + +Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake { + Ncar := interval_set grnd le; + Nplus : Ncar -> Ncar -> Ncar; + Nmult : Ncar -> Ncar -> Ncar; + Nzero : Ncar; + None : Ncar; + Nopp : Ncar -> Ncar; + Ninv : Ncar -> Ncar; + Nc : Ncar -> Ncar -> Prop; (* Ncistency *) + (* monoids *) + Nplus_assoc : associative Ncar Nplus; + Nmult_assoc : associative Ncar Nmult; + (* abelian groups *) + Nplus_comm : commutative Ncar Nplus; + Nmult_comm : commutative Ncar Nmult; + Nplus_0_l : forall x:Ncar, Nc (Nplus Nzero x) x; + Nplus_0_r : forall x:Ncar, Nc (Nplus x Nzero) x; + Nmult_0_l : forall x:Ncar, Nc (Nmult None x) x; + Nmult_0_r : forall x:Ncar, Nc (Nmult x None) x; + Nplus_opp_r : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero); + Nmult_inv_r : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None; + (* distributive laws *) + Nmult_plus_distr_l : forall x x' y y' z z' z'', + Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' -> + Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z'')); + (* order and lattice structure *) + Nlt : Ncar -> Ncar -> Prop; + Nlc := fun (x y:Ncar) => Nlt x y \/ Nc x y; + Nsup : Ncar -> Ncar -> Ncar; + Ninf : Ncar -> Ncar -> Ncar; + Nlt_trans : transitive _ lt; + Nlt_trich : forall x y:Ncar, Nlt x y \/ Nc x y \/ Nlt y x; + Nsup_lub : forall x y z:Ncar, Nlc x z -> Nlc y z -> Nlc (Nsup x y) z; + Ninf_glb : forall x y z:Ncar, Nlc x y -> Nlc x z -> Nlc x (Ninf y z); + (* order preserves operations? *) + (* properties of Nc *) + Nc_refl : reflexive _ Nc; + Nc_sym : symmetric _ Nc +}. + diff --git a/test-suite/bugs/closed/shouldsucceed/1519.v b/test-suite/bugs/closed/shouldsucceed/1519.v new file mode 100644 index 00000000..66bab241 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1519.v @@ -0,0 +1,14 @@ +Section S. + + Variable A:Prop. + Variable W:A. + + Remark T: A -> A. + intro Z. + rename W into Z_. + rename Z into W. + rename Z_ into Z. + exact Z. + Qed. + +End S. diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v new file mode 100644 index 00000000..9f10f749 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1568.v @@ -0,0 +1,13 @@ +CoInductive A: Set := + mk_A: B -> A +with B: Set := + mk_B: A -> B. + +CoFixpoint a:A := mk_A b +with b:B := mk_B a. + +Goal b = match a with mk_A a1 => a1 end. + simpl. reflexivity. +Qed. + + diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v new file mode 100644 index 00000000..c9ebbd14 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1576.v @@ -0,0 +1,38 @@ +Module Type TA. +Parameter t : Set. +End TA. + +Module Type TB. +Declare Module A: TA. +End TB. + +Module Type TC. +Declare Module B : TB. +End TC. + +Module Type TD. + +Declare Module B: TB . +Declare Module C: TC + with Module B := B . +End TD. + +Module Type TE. +Declare Module D : TD. +End TE. + +Module Type TF. +Declare Module E: TE. +End TF. + +Module G (D: TD). +Module B' := D.C.B. +End G. + +Module H (F: TF). +Module I := G(F.E.D). +End H. + +Declare Module F: TF. +Module K := H(F). + diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v new file mode 100644 index 00000000..47953a66 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1582.v @@ -0,0 +1,15 @@ +Require Import Peano_dec. + +Definition fact_F : + forall (n:nat), + (forall m, m<n -> nat) -> + nat. +refine + (fun n fact_rec => + if eq_nat_dec n 0 then + 1 + else + let fn := fact_rec (n-1) _ in + n * fn). +Admitted. + diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v new file mode 100644 index 00000000..22c3df82 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1604.v @@ -0,0 +1,7 @@ +Require Import Setoid. + +Parameter F : nat -> nat. +Axiom F_id : forall n : nat, n = F n. +Goal forall n : nat, F n = n. +intro n. setoid_rewrite F_id at 3. reflexivity. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1614.v b/test-suite/bugs/closed/shouldsucceed/1614.v new file mode 100644 index 00000000..6bc165d4 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1614.v @@ -0,0 +1,21 @@ +Require Import Ring. +Require Import ArithRing. + +Fixpoint eq_nat_bool (x y : nat) {struct x} : bool := +match x, y with +| 0, 0 => true +| S x', S y' => eq_nat_bool x' y' +| _, _ => false +end. + +Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y = true -> x = y. +Proof. +induction x; destruct y; simpl; intro H; try (reflexivity || inversion H). +apply IHx in H; rewrite H; reflexivity. +Qed. + +Add Ring MyNatSRing : natSRth (decidable eq_nat_bool_implies_eq). + +Goal 0 = 0. + ring. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v new file mode 100644 index 00000000..a90290bf --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1618.v @@ -0,0 +1,23 @@ +Inductive A: Set := +| A1: nat -> A. + +Definition A_size (a: A) : nat := + match a with + | A1 n => 0 + end. + +Require Import Recdef. + +Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a := + match a return (P a) with + | A1 n => f n + end. + + +Function n1 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {measure A_size a} : +P +a := + match a return (P a) with + | A1 n => f n + end. + diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v new file mode 100644 index 00000000..e0c540f3 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1634.v @@ -0,0 +1,24 @@ +Require Export Relation_Definitions. +Require Export Setoid. + +Variable A : Type. +Variable S : A -> Type. +Variable Seq : forall {a:A}, relation (S a). + +Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x. +Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x. +Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z -> +Seq x z. + +Add Parametric Relation a : (S a) Seq + reflexivity proved by Seq_refl + symmetry proved by Seq_sym + transitivity proved by Seq_trans + as S_Setoid. + +Goal forall (a : A) (x y : S a), Seq x y -> Seq x y. + intros a x y H. + setoid_replace x with y. + reflexivity. + trivial. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v new file mode 100644 index 00000000..4114987d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1643.v @@ -0,0 +1,21 @@ +(* Check some aspects of that the algorithm used to possibly reuse a + global name in the recursive calls (coinductive case) *) + +CoInductive Str : Set := Cons (h:nat) (t:Str). + +Definition decomp_func (s:Str) := + match s with + | Cons h t => Cons h t + end. + +Theorem decomp s: s = decomp_func s. +Proof. + intros s. + case s; simpl; reflexivity. +Qed. + +Definition zeros := (cofix z : Str := Cons 0 z). +Lemma zeros_rw : zeros = Cons 0 zeros. + rewrite (decomp zeros). + simpl. +Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1680.v b/test-suite/bugs/closed/shouldsucceed/1680.v new file mode 100644 index 00000000..524c7bab --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1680.v @@ -0,0 +1,9 @@ +Ltac int1 := let h := fresh in intro h. + +Goal nat -> nat -> True. + let h' := fresh in (let h := fresh in intro h); intro h'. + Restart. let h' := fresh in int1; intro h'. + trivial. +Qed. + + diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v new file mode 100644 index 00000000..1571ee20 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1683.v @@ -0,0 +1,42 @@ +Require Import Setoid. + +Section SetoidBug. + +Variable ms : Type. +Variable ms_type : ms -> Type. +Variable ms_eq : forall (A:ms), relation (ms_type A). + +Variable CR : ms. + +Record Ring : Type := +{Ring_type : Type}. + +Variable foo : forall (A:Ring), nat -> Ring_type A. +Variable IR : Ring. +Variable IRasCR : Ring_type IR -> ms_type CR. + +Definition CRasCRing : Ring := Build_Ring (ms_type CR). + +Hypothesis ms_refl : forall A x, ms_eq A x x. +Hypothesis ms_sym : forall A x y, ms_eq A x y -> ms_eq A y x. +Hypothesis ms_trans : forall A x y z, ms_eq A x y -> ms_eq A y z -> ms_eq A x z. + +Add Parametric Relation A : (ms_type A) (ms_eq A) + reflexivity proved by (ms_refl A) + symmetry proved by (ms_sym A) + transitivity proved by (ms_trans A) + as ms_Setoid. + +Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n). + +Goal forall (b:ms_type CR), + ms_eq CR (IRasCR (foo IR O)) b -> + ms_eq CR (IRasCR (foo IR O)) b. +intros b H. +rewrite foobar. +rewrite foobar in H. +assumption. +Qed. + + + diff --git a/test-suite/bugs/closed/shouldsucceed/1696.v b/test-suite/bugs/closed/shouldsucceed/1696.v new file mode 100644 index 00000000..0826428a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1696.v @@ -0,0 +1,16 @@ +Require Import Setoid. + +Inductive mynat := z : mynat | s : mynat -> mynat. + +Parameter E : mynat -> mynat -> Prop. +Axiom E_equiv : equiv mynat E. + +Add Relation mynat E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. + +Notation "x == y" := (E x y) (at level 70). + +Goal z == s z -> s z == z. intros H. setoid_rewrite H at 2. reflexivity. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/shouldsucceed/1704.v new file mode 100644 index 00000000..4b02d5f9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1704.v @@ -0,0 +1,17 @@ + +Require Import Setoid. +Parameter E : nat -> nat -> Prop. +Axiom E_equiv : equiv nat E. +Add Relation nat E +reflexivity proved by (proj1 E_equiv) +symmetry proved by (proj2 (proj2 E_equiv)) +transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. +Notation "x == y" := (E x y) (at level 70, no associativity). +Axiom r : False -> 0 == 1. +Goal 0 == 0. +Proof. +rewrite r. +reflexivity. +admit. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1718.v b/test-suite/bugs/closed/shouldsucceed/1718.v new file mode 100644 index 00000000..715fa941 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1718.v @@ -0,0 +1,9 @@ +(* lazy delta unfolding used to miss delta on rels and vars (fixed in 10172) *) + +Check + let g := fun _ => 0 in + fix f (n : nat) := + match n with + | 0 => g f + | S n' => 0 + end. diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v new file mode 100644 index 00000000..0deed366 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1738.v @@ -0,0 +1,30 @@ +Require Import FSets. + +Module SomeSetoids (Import M:FSetInterface.S). + +Lemma Equal_refl : forall s, s[=]s. +Proof. red; split; auto. Qed. + +Add Relation t Equal + reflexivity proved by Equal_refl + symmetry proved by eq_sym + transitivity proved by eq_trans + as EqualSetoid. + +Add Morphism Empty with signature Equal ==> iff as Empty_m. +Proof. +unfold Equal, Empty; firstorder. +Qed. + +End SomeSetoids. + +Module Test (Import M:FSetInterface.S). + Module A:=SomeSetoids M. + Module B:=SomeSetoids M. (* lots of warning *) + + Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'. + intros. + rewrite H in H0. + assumption. +Qed. +End Test.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v new file mode 100644 index 00000000..d9ce546a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1740.v @@ -0,0 +1,23 @@ +(* Check that expansion of alias in pattern-matching compilation is no + longer dependent of whether the pattern-matching problem occurs in a + typed context or at toplevel (solved from revision 10883) *) + +Definition f := + fun n m : nat => + match n, m with + | O, _ => O + | n, O => n + | _, _ => O + end. + +Goal f = + fun n m : nat => + match n, m with + | O, _ => O + | n, O => n + | _, _ => O + end. + unfold f. + reflexivity. +Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/1754.v b/test-suite/bugs/closed/shouldsucceed/1754.v new file mode 100644 index 00000000..06b8dce8 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1754.v @@ -0,0 +1,24 @@ +Axiom hp : Set. +Axiom cont : nat -> hp -> Prop. +Axiom sconj : (hp -> Prop) -> (hp -> Prop) -> hp -> Prop. +Axiom sconjImpl : forall h A B, + (sconj A B) h -> forall (A' B': hp -> Prop), + (forall h', A h' -> A' h') -> + (forall h', B h' -> B' h') -> + (sconj A' B') h. + +Definition cont' (h:hp) := exists y, cont y h. + +Lemma foo : forall h x y A, + (sconj (cont x) (sconj (cont y) A)) h -> + (sconj cont' (sconj cont' A)) h. +Proof. + intros h x y A H. + eapply sconjImpl. + 2:intros h' Hp'; econstructor; apply Hp'. + 2:intros h' Hp'; eapply sconjImpl. + 3:intros h'' Hp''; econstructor; apply Hp''. + 3:intros h'' Hp''; apply Hp''. + 2:apply Hp'. + clear H. +Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1773.v b/test-suite/bugs/closed/shouldsucceed/1773.v new file mode 100644 index 00000000..211af89b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1773.v @@ -0,0 +1,9 @@ +(* An occur-check test was done too early *) + +Goal forall B C : nat -> nat -> Prop, forall k, + (exists A, (forall k', C A k' -> B A k') -> B A k). +Proof. + intros B C k. + econstructor. + intros X. + apply X. (* used to fail here *) diff --git a/test-suite/bugs/closed/shouldsucceed/1774.v b/test-suite/bugs/closed/shouldsucceed/1774.v new file mode 100644 index 00000000..4c24b481 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1774.v @@ -0,0 +1,18 @@ +Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop). +Axiom plImp : forall k P Q, + pl P Q k -> forall (P':nat -> Prop), + (forall k', P k' -> P' k') -> forall (Q':nat -> Prop), + (forall k', Q k' -> Q' k') -> + pl P' Q' k. + +Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := + fun k' => exists k, P k k'. + +Goal forall k (A:nat -> nat -> Prop) (B:nat -> Prop), + pl (nexists A) B k. +intros. +eapply plImp. +2:intros m' M'; econstructor; apply M'. +2:intros m' M'; apply M'. +simpl. +Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v new file mode 100644 index 00000000..dab4120b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1775.v @@ -0,0 +1,39 @@ +Axiom pair : nat -> nat -> nat -> Prop. +Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop). +Axiom plImp : forall k P Q, + pl P Q k -> forall (P':nat -> Prop), + (forall k', P k' -> P' k') -> forall (Q':nat -> Prop), + (forall k', Q k' -> Q' k') -> + pl P' Q' k. + +Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := + fun k' => exists k, P k k'. + +Goal forall s k k' m, + (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w) + (pl (pair s b) + (nexists (fun w0 => (nexists (fun a => pl (pair b w0) + (nexists (fun w1 => (nexists (fun c => pl + (pair a w1) (pl (pair a c) k))))))))))))))) m. +intros. +eapply plImp; [ | eauto | intros ]. +2:econstructor. +2:econstructor. +2:eapply plImp; [ | eauto | intros ]. +3:eapply plImp; [ | eauto | intros ]. +4:econstructor. +4:econstructor. +4:eapply plImp; [ | eauto | intros ]. +5:econstructor. +5:econstructor. +5:eauto. +4:eauto. +3:eauto. +2:eauto. + +assert (X := 1). +clear X. (* very slow! *) + +simpl. (* exception Not_found *) + +Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v new file mode 100644 index 00000000..abf85455 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1776.v @@ -0,0 +1,22 @@ +Axiom pair : nat -> nat -> nat -> Prop. +Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop). +Axiom plImpR : forall k P Q, + pl P Q k -> forall (Q':nat -> Prop), + (forall k', Q k' -> Q' k') -> + pl P Q' k. + +Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := + fun k' => exists k, P k k'. + +Goal forall a A m, + True -> + (pl A (nexists (fun x => (nexists + (fun y => pl (pair a (S x)) (pair a (S y))))))) m. +Proof. + intros. + eapply plImpR; [ | intros; econstructor; econstructor; eauto]. + clear H; + match goal with + | |- (pl _ (pl (pair _ ?x) _)) _ => replace x with 0 + end. +Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1779.v b/test-suite/bugs/closed/shouldsucceed/1779.v new file mode 100644 index 00000000..95bb66b9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1779.v @@ -0,0 +1,25 @@ +Require Import Div2. + +Lemma double_div2: forall n, div2 (double n) = n. +exact (fun n => let _subcase := + let _cofact := fun _ : 0 = 0 => refl_equal 0 in + _cofact (let _fact := refl_equal 0 in _fact) in + let _subcase0 := + fun (m : nat) (Hrec : div2 (double m) = m) => + let _fact := f_equal div2 (double_S m) in + let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in + let _eq0 := + trans_eq _eq + (trans_eq + (f_equal (fun f : nat -> nat => f (div2 (double m))) + (refl_equal S)) (f_equal S Hrec)) in + _eq0 in + (fix _fix (__ : nat) : div2 (double __) = __ := + match __ as n return (div2 (double n) = n) with + | 0 => _subcase + | S __0 => + (fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec) + (_fix __0) + end) n). +Guarded. +Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v new file mode 100644 index 00000000..616dd26f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -0,0 +1,101 @@ +Require Import List. +Require Import ZArith. +Require String. Open Scope string_scope. +Ltac Case s := let c := fresh "case" in set (c := s). + +Set Implicit Arguments. +Unset Strict Implicit. + +Inductive sv : Set := +| I : Z -> sv +| S : list sv -> sv. + +Section sv_induction. + +Variables + (VP: sv -> Prop) + (LP: list sv -> Prop) + + (VPint: forall n, VP (I n)) + (VPset: forall vs, LP vs -> VP (S vs)) + (lpcons: forall v vs, VP v -> LP vs -> LP (v::vs)) + (lpnil: LP nil). + +Fixpoint setl_value_indp (x:sv) {struct x}: VP x := + match x as x return VP x with + | I n => VPint n + | S vs => + VPset + ((fix values_indp (vs:list sv) {struct vs}: (LP vs) := + match vs as vs return LP vs with + | nil => lpnil + | v::vs => lpcons (setl_value_indp v) (values_indp vs) + end) vs) + end. +End sv_induction. + +Inductive slt : sv -> sv -> Prop := +| IC : forall z, slt (I z) (I z) +| IS : forall vs vs', slist_in vs vs' -> slt (S vs) (S vs') + +with sin : sv -> list sv -> Prop := +| Ihd : forall s s' sv', slt s s' -> sin s (s'::sv') +| Itl : forall s s' sv', sin s sv' -> sin s (s'::sv') + +with slist_in : list sv -> list sv -> Prop := +| Inil : forall sv', + slist_in nil sv' +| Icons : forall s sv sv', + sin s sv' -> + slist_in sv sv' -> + slist_in (s::sv) sv'. + +Hint Constructors sin slt slist_in. + +Require Import Program. + +Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := + match x with + | I x => + match y with + | I y => if (Z_eq_dec x y) then in_left else in_right + | S ys => in_right + end + | S xs => + match y with + | I y => in_right + | S ys => + let fix list_in (xs ys:list sv) {struct xs} : + {slist_in xs ys} + {~slist_in xs ys} := + match xs with + | nil => in_left + | x::xs => + let fix elem_in (ys:list sv) : {sin x ys}+{~sin x ys} := + match ys with + | nil => in_right + | y::ys => if lt_dec x y then in_left else if elem_in + ys then in_left else in_right + end + in + if elem_in ys then + if list_in xs ys then in_left else in_right + else in_right + end + in if list_in xs ys then in_left else in_right + end + end. + +Next Obligation. apply H; inversion H0; subst; trivial. Defined. +Next Obligation. inversion H. Defined. +Next Obligation. inversion H. Defined. +Next Obligation. inversion H; subst. Defined. +Next Obligation. + contradict H. inversion H1; subst. assumption. + contradict H0; assumption. Defined. +Next Obligation. + contradict H0. inversion H1; subst. assumption. Defined. +Next Obligation. + contradict H. inversion H0; subst. assumption. Defined. +Next Obligation. + contradict H. inversion H0; subst; auto. Defined. + diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v new file mode 100644 index 00000000..545f2615 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1844.v @@ -0,0 +1,217 @@ +Require Import ZArith. + +Definition zeq := Z_eq_dec. + +Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := + fun y => if zeq x y then v else s y. + +Implicit Arguments update [A]. + +Definition ident := Z. +Parameter operator: Set. +Parameter value: Set. +Parameter is_true: value -> Prop. +Definition label := Z. + +Inductive expr : Set := + | Evar: ident -> expr + | Econst: value -> expr + | Eop: operator -> expr -> expr -> expr. + +Inductive stmt : Set := + | Sskip: stmt + | Sassign: ident -> expr -> stmt + | Scall: ident -> ident -> expr -> stmt (* x := f(e) *) + | Sreturn: expr -> stmt + | Sseq: stmt -> stmt -> stmt + | Sifthenelse: expr -> stmt -> stmt -> stmt + | Sloop: stmt -> stmt + | Sblock: stmt -> stmt + | Sexit: nat -> stmt + | Slabel: label -> stmt -> stmt + | Sgoto: label -> stmt. + +Record function : Set := mkfunction { + fn_param: ident; + fn_body: stmt +}. + +Parameter program: ident -> option function. + +Parameter main_function: ident. + +Definition store := ident -> value. + +Parameter empty_store : store. + +Parameter eval_op: operator -> value -> value -> option value. + +Fixpoint eval_expr (st: store) (e: expr) {struct e} : option value := + match e with + | Evar v => Some (st v) + | Econst v => Some v + | Eop op e1 e2 => + match eval_expr st e1, eval_expr st e2 with + | Some v1, Some v2 => eval_op op v1 v2 + | _, _ => None + end + end. + +Inductive outcome: Set := + | Onormal: outcome + | Oexit: nat -> outcome + | Ogoto: label -> outcome + | Oreturn: value -> outcome. + +Definition outcome_block (out: outcome) : outcome := + match out with + | Onormal => Onormal + | Oexit O => Onormal + | Oexit (S m) => Oexit m + | Ogoto lbl => Ogoto lbl + | Oreturn v => Oreturn v + end. + +Fixpoint label_defined (lbl: label) (s: stmt) {struct s}: Prop := + match s with + | Sskip => False + | Sassign id e => False + | Scall id fn e => False + | Sreturn e => False + | Sseq s1 s2 => label_defined lbl s1 \/ label_defined lbl s2 + | Sifthenelse e s1 s2 => label_defined lbl s1 \/ label_defined lbl s2 + | Sloop s1 => label_defined lbl s1 + | Sblock s1 => label_defined lbl s1 + | Sexit n => False + | Slabel lbl1 s1 => lbl1 = lbl \/ label_defined lbl s1 + | Sgoto lbl => False + end. + +Inductive exec : stmt -> store -> outcome -> store -> Prop := + | exec_skip: forall st, + exec Sskip st Onormal st + | exec_assign: forall id e st v, + eval_expr st e = Some v -> + exec (Sassign id e) st Onormal (update id v st) + | exec_call: forall id fn e st v1 f v2 st', + eval_expr st e = Some v1 -> + program fn = Some f -> + exec_function f (update f.(fn_param) v1 empty_store) v2 st' -> + exec (Scall id fn e) st Onormal (update id v2 st) + | exec_return: forall e st v, + eval_expr st e = Some v -> + exec (Sreturn e) st (Oreturn v) st + | exec_seq_2: forall s1 s2 st st1 out' st', + exec s1 st Onormal st1 -> exec s2 st1 out' st' -> + exec (Sseq s1 s2) st out' st' + | exec_seq_1: forall s1 s2 st out st', + exec s1 st out st' -> out <> Onormal -> + exec (Sseq s1 s2) st out st' + | exec_ifthenelse_true: forall e s1 s2 st out st' v, + eval_expr st e = Some v -> is_true v -> exec s1 st out st' -> + exec (Sifthenelse e s1 s2) st out st' + | exec_ifthenelse_false: forall e s1 s2 st out st' v, + eval_expr st e = Some v -> ~is_true v -> exec s2 st out st' -> + exec (Sifthenelse e s1 s2) st out st' + | exec_loop_loop: forall s st st1 out' st', + exec s st Onormal st1 -> + exec (Sloop s) st1 out' st' -> + exec (Sloop s) st out' st' + | exec_loop_stop: forall s st st' out, + exec s st out st' -> out <> Onormal -> + exec (Sloop s) st out st' + | exec_block: forall s st out st', + exec s st out st' -> + exec (Sblock s) st (outcome_block out) st' + | exec_exit: forall n st, + exec (Sexit n) st (Oexit n) st + | exec_label: forall s lbl st st' out, + exec s st out st' -> + exec (Slabel lbl s) st out st' + | exec_goto: forall st lbl, + exec (Sgoto lbl) st (Ogoto lbl) st + +(** [execg lbl stmt st out st'] starts executing at label [lbl] within [s], + in initial store [st]. The result of the execution is the outcome + [out] with final store [st']. *) + +with execg: label -> stmt -> store -> outcome -> store -> Prop := + | execg_left_seq_2: forall lbl s1 s2 st st1 out' st', + execg lbl s1 st Onormal st1 -> exec s2 st1 out' st' -> + execg lbl (Sseq s1 s2) st out' st' + | execg_left_seq_1: forall lbl s1 s2 st out st', + execg lbl s1 st out st' -> out <> Onormal -> + execg lbl (Sseq s1 s2) st out st' + | execg_right_seq: forall lbl s1 s2 st out st', + ~(label_defined lbl s1) -> + execg lbl s2 st out st' -> + execg lbl (Sseq s1 s2) st out st' + | execg_ifthenelse_left: forall lbl e s1 s2 st out st', + execg lbl s1 st out st' -> + execg lbl (Sifthenelse e s1 s2) st out st' + | execg_ifthenelse_right: forall lbl e s1 s2 st out st', + ~(label_defined lbl s1) -> + execg lbl s2 st out st' -> + execg lbl (Sifthenelse e s1 s2) st out st' + | execg_loop_loop: forall lbl s st st1 out' st', + execg lbl s st Onormal st1 -> + exec (Sloop s) st1 out' st' -> + execg lbl (Sloop s) st out' st' + | execg_loop_stop: forall lbl s st st' out, + execg lbl s st out st' -> out <> Onormal -> + execg lbl (Sloop s) st out st' + | execg_block: forall lbl s st out st', + execg lbl s st out st' -> + execg lbl (Sblock s) st (outcome_block out) st' + | execg_label_found: forall lbl s st st' out, + exec s st out st' -> + execg lbl (Slabel lbl s) st out st' + | execg_label_notfound: forall lbl s lbl' st st' out, + lbl' <> lbl -> + execg lbl s st out st' -> + execg lbl (Slabel lbl' s) st out st' + +(** [exec_finish out st st'] takes the outcome [out] and the store [st] + at the end of the evaluation of the program. If [out] is a [goto], + execute again the program starting at the corresponding label. + Iterate this way until [out] is [Onormal]. *) + +with exec_finish: function -> outcome -> store -> value -> store -> Prop := + | exec_finish_normal: forall f st v, + exec_finish f (Oreturn v) st v st + | exec_finish_goto: forall f lbl st out v st1 st', + execg lbl f.(fn_body) st out st1 -> + exec_finish f out st1 v st' -> + exec_finish f (Ogoto lbl) st v st' + +(** Execution of a function *) + +with exec_function: function -> store -> value -> store -> Prop := + | exec_function_intro: forall f st out st1 v st', + exec f.(fn_body) st out st1 -> + exec_finish f out st1 v st' -> + exec_function f st v st'. + +Scheme exec_ind4:= Minimality for exec Sort Prop + with execg_ind4:= Minimality for execg Sort Prop + with exec_finish_ind4 := Minimality for exec_finish Sort Prop + with exec_function_ind4 := Minimality for exec_function Sort Prop. + +Scheme exec_dind4:= Induction for exec Sort Prop + with execg_dind4:= Minimality for execg Sort Prop + with exec_finish_dind4 := Induction for exec_finish Sort Prop + with exec_function_dind4 := Induction for exec_function Sort Prop. + +Combined Scheme exec_inductiond from exec_dind4, execg_dind4, exec_finish_dind4, + exec_function_dind4. + +Scheme exec_dind4' := Induction for exec Sort Prop + with execg_dind4' := Induction for execg Sort Prop + with exec_finish_dind4' := Induction for exec_finish Sort Prop + with exec_function_dind4' := Induction for exec_function Sort Prop. + +Combined Scheme exec_induction from exec_ind4, execg_ind4, exec_finish_ind4, + exec_function_ind4. + +Combined Scheme exec_inductiond' from exec_dind4', execg_dind4', exec_finish_dind4', + exec_function_dind4'. diff --git a/test-suite/bugs/closed/shouldsucceed/1865.v b/test-suite/bugs/closed/shouldsucceed/1865.v new file mode 100644 index 00000000..17c19989 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1865.v @@ -0,0 +1,18 @@ +(* Check that tactics (here dependent inversion) do not generate + conversion problems T <= U with sup's of universes in U *) + +(* Submitted by David Nowak *) + +Inductive list (A:Set) : nat -> Set := +| nil : list A O +| cons : forall n, A -> list A n -> list A (S n). + +Definition f (n:nat) : Type := + match n with + | O => bool + | _ => unit + end. + +Goal forall A n, list A n -> f n. +intros A n. +dependent inversion n. diff --git a/test-suite/bugs/closed/shouldsucceed/348.v b/test-suite/bugs/closed/shouldsucceed/348.v new file mode 100644 index 00000000..28cc5cb1 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/348.v @@ -0,0 +1,13 @@ +Module Type S. + Parameter empty: Set. +End S. + +Module D (M:S). + Import M. + Definition empty:=nat. +End D. + +Module D' (M:S). + Import M. + Definition empty:Set. exact nat. Save. +End D'. diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v new file mode 100644 index 00000000..7bc04b1f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/38.v @@ -0,0 +1,22 @@ +Require Import Setoid. + +Variable A : Set. + +Inductive liste : Set := +| vide : liste +| c : A -> liste -> liste. + +Inductive e : A -> liste -> Prop := +| ec : forall (x : A) (l : liste), e x (c x l) +| ee : forall (x y : A) (l : liste), e x l -> e x (c y l). + +Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m. + +Definition same_refl (x:liste) : (same x x). + unfold same; split; intros; trivial. +Save. + +Goal forall (x:liste), (same x x). + intro. + apply (same_refl x). +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/545.v b/test-suite/bugs/closed/shouldsucceed/545.v new file mode 100644 index 00000000..926af7dd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/545.v @@ -0,0 +1,5 @@ +Require Export Reals. + +Parameter toto : nat -> nat -> nat. + +Notation " e # f " := (toto e f) (at level 30, f at level 0). diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v new file mode 100644 index 00000000..a963b225 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/846.v @@ -0,0 +1,213 @@ +Set Implicit Arguments. + +Open Scope type_scope. + +Inductive One : Set := inOne: One. + +Definition maybe: forall A B:Set,(A -> B) -> One + A -> One + B. +Proof. + intros A B f c. + case c. + left; assumption. + right; apply f; assumption. +Defined. + +Definition id (A:Set)(a:A):=a. + +Definition LamF (X: Set -> Set)(A:Set) :Set := + A + (X A)*(X A) + X(One + A). + +Definition LamF' (X: Set -> Set)(A:Set) :Set := + LamF X A. + +Require Import List. +Require Import Bool. + +Definition index := list bool. + +Inductive L (A:Set) : index -> Set := + initL: A -> L A nil + | pluslL: forall l:index, One -> L A (false::l) + | plusrL: forall l:index, L A l -> L A (false::l) + | varL: forall l:index, L A l -> L A (true::l) + | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l) + | absL: forall l:index, L A (true::false::l) -> L A (true::l). + +Scheme L_rec_simp := Minimality for L Sort Set. + +Definition Lam' (A:Set) := L A (true::nil). + +Definition aczelapp: forall (l1 l2: index)(A:Set), L (L A l2) l1 -> L A + (l1++l2). +Proof. + intros l1 l2 A. + generalize l1. + clear l1. + (* Check (fun i:index => L A (i++l2)). *) + apply (L_rec_simp (A:=L A l2) (fun i:index => L A (i++l2))). + trivial. + intros l o. + simpl app. + apply pluslL; assumption. + intros l _ t. + simpl app. + apply plusrL; assumption. + intros l _ t. + simpl app. + apply varL; assumption. + intros l _ t1 _ t2. + simpl app in *|-*. + Check 0. + apply appL; [exact t1| exact t2]. + intros l _ t. + simpl app in *|-*. + Check 0. + apply absL; assumption. +Defined. + +Definition monL: forall (l:index)(A:Set)(B:Set), (A->B) -> L A l -> L B l. +Proof. + intros l A B f. + intro t. + elim t. + intro a. + exact (initL (f a)). + intros i u. + exact (pluslL _ _ u). + intros i _ r. + exact (plusrL r). + intros i _ r. + exact (varL r). + intros i _ r1 _ r2. + exact (appL r1 r2). + intros i _ r. + exact (absL r). +Defined. + +Definition lam': forall (A B:Set), (A -> B) -> Lam' A -> Lam' B. +Proof. + intros A B f t. + unfold Lam' in *|-*. + Check 0. + exact (monL f t). +Defined. + +Definition inLam': forall A:Set, LamF' Lam' A -> Lam' A. +Proof. + intros A [[a|[t1 t2]]|r]. + unfold Lam'. + exact (varL (initL a)). + exact (appL t1 t2). + unfold Lam' in * |- *. + Check 0. + apply absL. + change (L A ((true::nil) ++ (false::nil))). + apply aczelapp. + (* Check (fun x:One + A => (match (maybe (fun a:A => initL a) x) with + | inl u => pluslL _ _ u + | inr t' => plusrL t' end)). *) + exact (monL (fun x:One + A => + (match (maybe (fun a:A => initL a) x) with + | inl u => pluslL _ _ u + | inr t' => plusrL t' end)) r). +Defined. + +Section minimal. + +Definition sub1 (F G: Set -> Set):= forall A:Set, F A->G A. +Hypothesis G: Set -> Set. +Hypothesis step: sub1 (LamF' G) G. + +Fixpoint L'(A:Set)(i:index){struct i} : Set := + match i with + nil => A + | false::l => One + L' A l + | true::l => G (L' A l) + end. + +Definition LinL': forall (A:Set)(i:index), L A i -> L' A i. +Proof. + intros A i t. + elim t. + intro a. + unfold L'. + assumption. + intros l u. + left; assumption. + intros l _ r. + right; assumption. + intros l _ r. + apply (step (A:=L' A l)). + exact (inl _ (inl _ r)). + intros l _ r1 _ r2. + apply (step (A:=L' A l)). + (* unfold L' in * |- *. + Check 0. *) + exact (inl _ (inr _ (pair r1 r2))). + intros l _ r. + apply (step (A:=L' A l)). + exact (inr _ r). +Defined. + +Definition L'inG: forall A: Set, L' A (true::nil) -> G A. +Proof. + intros A t. + unfold L' in t. + assumption. +Defined. + +Definition Itbasic: sub1 Lam' G. +Proof. + intros A t. + apply L'inG. + unfold Lam' in t. + exact (LinL' t). +Defined. + +End minimal. + +Definition recid := Itbasic inLam'. + +Definition L'Lam'inL: forall (i:index)(A:Set), L' Lam' A i -> L A i. +Proof. + intros i A t. + induction i. + unfold L' in t. + apply initL. + assumption. + induction a. + simpl L' in t. + apply (aczelapp (l1:=true::nil) (l2:=i)). + exact (lam' IHi t). + simpl L' in t. + induction t. + exact (pluslL _ _ a). + exact (plusrL (IHi b)). +Defined. + + +Lemma recidgen: forall(A:Set)(i:index)(t:L A i), L'Lam'inL i A (LinL' inLam' t) + = t. +Proof. + intros A i t. + induction t. + trivial. + trivial. + simpl. + rewrite IHt. + trivial. + simpl L'Lam'inL. + rewrite IHt. + trivial. + simpl L'Lam'inL. + simpl L'Lam'inL in IHt1. + unfold lam' in IHt1. + simpl L'Lam'inL in IHt2. + unfold lam' in IHt2. + + (* going on. This fails for the original solution. *) + rewrite IHt1. + rewrite IHt2. + trivial. +Abort. (* one goal still left *) + diff --git a/test-suite/bugs/closed/shouldsucceed/931.v b/test-suite/bugs/closed/shouldsucceed/931.v new file mode 100644 index 00000000..21f15e72 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/931.v @@ -0,0 +1,7 @@ +Parameter P : forall n : nat, n=n -> Prop. + +Goal Prop. + refine (P _ _). + instantiate (1:=0). + trivial. +Qed. |