diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
136 files changed, 0 insertions, 4383 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1041.v b/test-suite/bugs/closed/shouldsucceed/1041.v deleted file mode 100644 index a5de82e0..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1041.v +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index 32c78b4b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1100.v +++ /dev/null @@ -1,12 +0,0 @@ -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 deleted file mode 100644 index 8c5a3885..00000000 --- a/test-suite/bugs/closed/shouldsucceed/121.v +++ /dev/null @@ -1,17 +0,0 @@ -Require Import Setoid. - -Section Setoid_Bug. - -Variable X:Type -> Type. -Variable Xeq : forall A, (X A) -> (X A) -> Prop. -Hypothesis Xst : forall A, Equivalence (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 deleted file mode 100644 index 7d6781db..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1243.v +++ /dev/null @@ -1,12 +0,0 @@ -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 deleted file mode 100644 index e94dfcfb..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1302.v +++ /dev/null @@ -1,22 +0,0 @@ -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 deleted file mode 100644 index 1ec7d452..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1322.v +++ /dev/null @@ -1,24 +0,0 @@ -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 deleted file mode 100644 index a1a7b288..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1411.v +++ /dev/null @@ -1,35 +0,0 @@ -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 deleted file mode 100644 index ee9e2504..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ /dev/null @@ -1,40 +0,0 @@ -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 u:t) - (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) - { measure (cardinal s + cardinal u) } : - {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := - match s, u 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 s - else - let (l2', r2') := split v1 u in - join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) - else - if (Z.eq_dec h1 1) - then add v1 s - else - let (l1', r1') := split v2 u in - join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _) - end. diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v deleted file mode 100644 index ee092005..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1416.v +++ /dev/null @@ -1,30 +0,0 @@ -(* In 8.1 autorewrite used to raised an anomaly here *) -(* After resolution of the bug, autorewrite succeeded *) -(* From forthcoming 8.4, autorewrite is forbidden to instantiate *) -(* evars, so the new test just checks it is not an anomaly *) - -Set Implicit Arguments. - -Record Place (Env A: Type) : Type := { - read: Env -> A ; - write: Env -> A -> Env ; - write_read: forall (e:Env), (write e (read e))=e -}. - -Hint Rewrite -> write_read: placeeq. - -Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type := - { - mkEnv: A -> B -> Env ; - mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x) - }. - -(* when the following line is commented, the bug does not appear *) -Hint Rewrite -> mkEnv2writeL: placeeq. - -Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A), - (exists e1:Env, e=(write p e1 (read p e))). -Proof. - intros Env A e p; eapply ex_intro. - autorewrite with placeeq. (* Here is the bug *) - diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/shouldsucceed/1419.v deleted file mode 100644 index d021107d..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1419.v +++ /dev/null @@ -1,8 +0,0 @@ -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 deleted file mode 100644 index 6be30174..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1425.v +++ /dev/null @@ -1,19 +0,0 @@ -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 deleted file mode 100644 index 8cb2d653..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1446.v +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index fe3b4c8b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1448.v +++ /dev/null @@ -1,28 +0,0 @@ -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 deleted file mode 100644 index dfc8c328..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1477.v +++ /dev/null @@ -1,18 +0,0 @@ -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 deleted file mode 100644 index a3d7f168..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1483.v +++ /dev/null @@ -1,10 +0,0 @@ -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 deleted file mode 100644 index f2ab9100..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1507.v +++ /dev/null @@ -1,120 +0,0 @@ -(* - Implementing reals a la Stolzenberg - - Danko Ilik, March 2007 - - 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 deleted file mode 100644 index 66bab241..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1519.v +++ /dev/null @@ -1,14 +0,0 @@ -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 deleted file mode 100644 index 3609e9c8..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1568.v +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index 3621f7a1..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1576.v +++ /dev/null @@ -1,38 +0,0 @@ -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 deleted file mode 100644 index be5d3dd2..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1582.v +++ /dev/null @@ -1,15 +0,0 @@ -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 deleted file mode 100644 index 22c3df82..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1604.v +++ /dev/null @@ -1,7 +0,0 @@ -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 deleted file mode 100644 index 6bc165d4..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1614.v +++ /dev/null @@ -1,21 +0,0 @@ -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 deleted file mode 100644 index a9b067ce..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1618.v +++ /dev/null @@ -1,23 +0,0 @@ -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 deleted file mode 100644 index 0150c250..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1634.v +++ /dev/null @@ -1,24 +0,0 @@ -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 deleted file mode 100644 index 879a65b1..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1643.v +++ /dev/null @@ -1,20 +0,0 @@ -(* 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. - 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 deleted file mode 100644 index 524c7bab..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1680.v +++ /dev/null @@ -1,9 +0,0 @@ -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 deleted file mode 100644 index 3e99694b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1683.v +++ /dev/null @@ -1,42 +0,0 @@ -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 deleted file mode 100644 index 0826428a..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1696.v +++ /dev/null @@ -1,16 +0,0 @@ -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 deleted file mode 100644 index 4b02d5f9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1704.v +++ /dev/null @@ -1,17 +0,0 @@ - -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/1711.v b/test-suite/bugs/closed/shouldsucceed/1711.v deleted file mode 100644 index e16612e3..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1711.v +++ /dev/null @@ -1,34 +0,0 @@ -(* Test for evar map consistency - was failing at some point and was *) -(* assumed to be solved from revision 10151 (but using a bad fix) *) - -Require Import List. -Set Implicit Arguments. - -Inductive rose : Set := Rose : nat -> list rose -> rose. - -Section RoseRec. -Variables (P: rose -> Set)(L: list rose -> Set). -Hypothesis - (R: forall n rs, L rs -> P (Rose n rs)) - (Lnil: L nil) - (Lcons: forall r rs, P r -> L rs -> L (cons r rs)). - -Fixpoint rose_rec2 (t:rose) {struct t} : P t := - match t as x return P x with - | Rose n rs => - R n ((fix rs_ind (l' : list rose): L l' := - match l' as x return L x with - | nil => Lnil - | cons t tl => Lcons (rose_rec2 t) (rs_ind tl) - end) - rs) - end. -End RoseRec. - -Lemma rose_map : rose -> rose. -Proof. intro H; elim H using rose_rec2 with - (L:=fun _ => list rose); (* was assumed to fail here *) -(* (L:=fun (_:list rose) => list rose); *) - clear H; simpl; intros. - exact (Rose n rs). exact nil. exact (H::H0). -Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/1718.v b/test-suite/bugs/closed/shouldsucceed/1718.v deleted file mode 100644 index 715fa941..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1718.v +++ /dev/null @@ -1,9 +0,0 @@ -(* 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 deleted file mode 100644 index c2926a2b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1738.v +++ /dev/null @@ -1,30 +0,0 @@ -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 deleted file mode 100644 index ec4a7a6b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1740.v +++ /dev/null @@ -1,23 +0,0 @@ -(* 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 deleted file mode 100644 index 06b8dce8..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1754.v +++ /dev/null @@ -1,24 +0,0 @@ -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 deleted file mode 100644 index 211af89b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1773.v +++ /dev/null @@ -1,9 +0,0 @@ -(* 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 deleted file mode 100644 index 4c24b481..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1774.v +++ /dev/null @@ -1,18 +0,0 @@ -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 deleted file mode 100644 index 932949a3..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1775.v +++ /dev/null @@ -1,39 +0,0 @@ -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 deleted file mode 100644 index 58491f9d..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1776.v +++ /dev/null @@ -1,22 +0,0 @@ -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 deleted file mode 100644 index 95bb66b9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1779.v +++ /dev/null @@ -1,25 +0,0 @@ -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 deleted file mode 100644 index fb2f0ca9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ /dev/null @@ -1,101 +0,0 @@ -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. intro H0. apply H; inversion H0; subst; trivial. Defined. -Next Obligation. intro H; inversion H. Defined. -Next Obligation. intro H; inversion H. Defined. -Next Obligation. intro H; inversion H; subst. Defined. -Next Obligation. - intro H1; contradict H. inversion H1; subst. assumption. - contradict H0; assumption. Defined. -Next Obligation. - intro H1; contradict H0. inversion H1; subst. assumption. Defined. -Next Obligation. - intro H1; contradict H. inversion H1; subst. assumption. Defined. -Next Obligation. - intro H0; contradict H. inversion H0; subst; auto. Defined. - diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v deleted file mode 100644 index be0e8ae8..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1791.v +++ /dev/null @@ -1,38 +0,0 @@ -(* simpl performs eta expansion *) - -Set Implicit Arguments. -Require Import List. - -Definition k0 := Set. -Definition k1 := k0 -> k0. - -(** iterating X n times *) -Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= - match k with 0 => fun X => X - | S k' => fun A => X (Pow X k' A) - end. - -Parameter Bush: k1. -Parameter BushToList: forall (A:k0), Bush A -> list A. - -Definition BushnToList (n:nat)(A:k0)(t:Pow Bush n A): list A. -Proof. - intros. - induction n. - exact (t::nil). - simpl in t. - exact (flat_map IHn (BushToList t)). -Defined. - -Parameter bnil : forall (A:k0), Bush A. -Axiom BushToList_bnil: forall (A:k0), BushToList (bnil A) = nil(A:=A). - -Lemma BushnToList_bnil (n:nat)(A:k0): - BushnToList (S n) A (bnil (Pow Bush n A)) = nil. -Proof. - intros. - simpl. - rewrite BushToList_bnil. - simpl. - reflexivity. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v deleted file mode 100644 index 947d15f0..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1834.v +++ /dev/null @@ -1,174 +0,0 @@ -(* This tests rather deep nesting of abstracted terms *) - -(* This used to fail before Nov 2011 because of a de Bruijn indice bug - in extract_predicate. - - Note: use of eq_ok allows shorten notations but was not in the - original example -*) - -Scheme eq_rec_dep := Induction for eq Sort Type. - -Section Teq. - -Variable P0: Type. -Variable P1: forall (y0:P0), Type. -Variable P2: forall y0 (y1:P1 y0), Type. -Variable P3: forall y0 y1 (y2:P2 y0 y1), Type. -Variable P4: forall y0 y1 y2 (y3:P3 y0 y1 y2), Type. -Variable P5: forall y0 y1 y2 y3 (y4:P4 y0 y1 y2 y3), Type. - -Variable x0:P0. - -Inductive eq0 : P0 -> Prop := - refl0: eq0 x0. - -Definition eq_0 y0 := x0 = y0. - -Variable x1:P1 x0. - -Inductive eq1 : forall y0, P1 y0 -> Prop := - refl1: eq1 x0 x1. - -Definition S0_0 y0 (e0:eq_0 y0) := - eq_rec_dep P0 x0 (fun y0 e0 => P1 y0) x1 y0 e0. - -Definition eq_ok0 y0 y1 (E: eq_0 y0) := S0_0 y0 E = y1. - -Definition eq_1 y0 y1 := - {E0:eq_0 y0 | eq_ok0 y0 y1 E0}. - -Variable x2:P2 x0 x1. - -Inductive eq2 : -forall y0 y1, P2 y0 y1 -> Prop := -refl2: eq2 x0 x1 x2. - -Definition S1_0 y0 (e0:eq_0 y0) := -eq_rec_dep P0 x0 (fun y0 e0 => P2 y0 (S0_0 y0 e0)) x2 y0 e0. - -Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := - eq_rec_dep (P1 y0) (S0_0 y0 e0) (fun y1 e1 => P2 y0 y1) - (S1_0 y0 e0) - y1 e1. - -Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) := - match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end. - -Definition eq_2 y0 y1 y2 := - {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}. - -Variable x3:P3 x0 x1 x2. - -Inductive eq3 : -forall y0 y1 y2, P3 y0 y1 y2 -> Prop := -refl3: eq3 x0 x1 x2 x3. - -Definition S2_0 y0 (e0:eq_0 y0) := -eq_rec_dep P0 x0 (fun y0 e0 => P3 y0 (S0_0 y0 e0) (S1_0 y0 e0)) x3 y0 e0. - -Definition S2_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := - eq_rec_dep (P1 y0) (S0_0 y0 e0) - (fun y1 e1 => P3 y0 y1 (S1_1 y0 y1 e0 e1)) - (S2_0 y0 e0) - y1 e1. - -Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) - (e2:S1_1 y0 y1 e0 e1 = y2) := - eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1) - (fun y2 e2 => P3 y0 y1 y2) - (S2_1 y0 y1 e0 e1) - y2 e2. - -Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop := - match E with exist (exist e0 e1) e2 => - S2_2 y0 y1 y2 e0 e1 e2 = y3 end. - -Definition eq_3 y0 y1 y2 y3 := - {E2: eq_2 y0 y1 y2 | eq_ok2 y0 y1 y2 y3 E2}. - -Variable x4:P4 x0 x1 x2 x3. - -Inductive eq4 : -forall y0 y1 y2 y3, P4 y0 y1 y2 y3 -> Prop := -refl4: eq4 x0 x1 x2 x3 x4. - -Definition S3_0 y0 (e0:eq_0 y0) := -eq_rec_dep P0 x0 (fun y0 e0 => P4 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0)) - x4 y0 e0. - -Definition S3_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := - eq_rec_dep (P1 y0) (S0_0 y0 e0) - (fun y1 e1 => P4 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1)) - (S3_0 y0 e0) - y1 e1. - -Definition S3_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) - (e2:S1_1 y0 y1 e0 e1 = y2) := - eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1) - (fun y2 e2 => P4 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2)) - (S3_1 y0 y1 e0 e1) - y2 e2. - -Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) - (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):= - eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2) - (fun y3 e3 => P4 y0 y1 y2 y3) - (S3_2 y0 y1 y2 e0 e1 e2) - y3 e3. - -Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop := - match E with exist (exist (exist e0 e1) e2) e3 => - S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end. - -Definition eq_4 y0 y1 y2 y3 y4 := - {E3: eq_3 y0 y1 y2 y3 | eq_ok3 y0 y1 y2 y3 y4 E3}. - -Variable x5:P5 x0 x1 x2 x3 x4. - -Inductive eq5 : -forall y0 y1 y2 y3 y4, P5 y0 y1 y2 y3 y4 -> Prop := -refl5: eq5 x0 x1 x2 x3 x4 x5. - -Definition S4_0 y0 (e0:eq_0 y0) := -eq_rec_dep P0 x0 -(fun y0 e0 => P5 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0) (S3_0 y0 e0)) - x5 y0 e0. - -Definition S4_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := - eq_rec_dep (P1 y0) (S0_0 y0 e0) - (fun y1 e1 => P5 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1) (S3_1 y0 y1 e0 -e1)) - (S4_0 y0 e0) - y1 e1. - -Definition S4_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) - (e2:S1_1 y0 y1 e0 e1 = y2) := - eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1) - (fun y2 e2 => P5 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2) (S3_2 y0 y1 y2 e0 e1 e2)) - (S4_1 y0 y1 e0 e1) - y2 e2. - -Definition S4_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) - (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):= - eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2) - (fun y3 e3 => P5 y0 y1 y2 y3 (S3_3 y0 y1 y2 y3 e0 e1 e2 e3)) - (S4_2 y0 y1 y2 e0 e1 e2) - y3 e3. - -Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) - (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3) - (e4:S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4) := - eq_rec_dep (P4 y0 y1 y2 y3) (S3_3 y0 y1 y2 y3 e0 e1 e2 e3) - (fun y4 e4 => P5 y0 y1 y2 y3 y4) - (S4_3 y0 y1 y2 y3 e0 e1 e2 e3) - y4 e4. - -Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop := - match E with exist (exist (exist (exist e0 e1) e2) e3) e4 => - S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end. - -Definition eq_5 y0 y1 y2 y3 y4 y5 := - {E4: eq_4 y0 y1 y2 y3 y4 | eq_ok4 y0 y1 y2 y3 y4 y5 E4 }. - -End Teq. diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v deleted file mode 100644 index 17eeb352..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1844.v +++ /dev/null @@ -1,217 +0,0 @@ -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 deleted file mode 100644 index 17c19989..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1865.v +++ /dev/null @@ -1,18 +0,0 @@ -(* 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/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v deleted file mode 100644 index 2d90a2f1..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1891.v +++ /dev/null @@ -1,13 +0,0 @@ -(* Check evar-evar unification *) - Inductive T (A: Set): Set := mkT: unit -> T A. - - Definition f (A: Set) (l: T A): unit := tt. - - Implicit Arguments f [A]. - - Lemma L (x: T unit): (unit -> T unit) -> unit. - Proof. - refine (match x return _ with mkT n => fun g => f (g _) end). - trivial. - Qed. - diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/shouldsucceed/1900.v deleted file mode 100644 index cf03efda..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1900.v +++ /dev/null @@ -1,8 +0,0 @@ -Parameter A : Type . - -Definition eq_A := @eq A. - -Goal forall x, eq_A x x. -intros. -reflexivity. -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v deleted file mode 100644 index 7d86adbf..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1901.v +++ /dev/null @@ -1,11 +0,0 @@ -Require Import Relations. - -Record Poset{A:Type}(Le : relation A) : Type := - Build_Poset - { - Le_refl : forall x : A, Le x x; - Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; - Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. - -Definition nat_Poset : Poset Peano.le. -Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v deleted file mode 100644 index 8c81d751..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1905.v +++ /dev/null @@ -1,13 +0,0 @@ - -Require Import Setoid Program. - -Axiom t : Set. -Axiom In : nat -> t -> Prop. -Axiom InE : forall (x : nat) (s:t), impl (In x s) True. - -Goal forall a s, - In a s -> False. -Proof. - intros a s Ia. - rewrite InE in Ia. -Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/shouldsucceed/1907.v deleted file mode 100644 index 55fc8231..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1907.v +++ /dev/null @@ -1,7 +0,0 @@ -(* An example of type inference *) - -Axiom A : Type. -Definition f (x y : A) := x. -Axiom g : forall x y : A, f x y = y -> Prop. -Axiom x : A. -Check (g x _ (refl_equal x)). diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v deleted file mode 100644 index 987a5417..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1912.v +++ /dev/null @@ -1,6 +0,0 @@ -Require Import ZArith. - -Goal forall x, Z.succ (Z.pred x) = x. -intros x. -omega. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v deleted file mode 100644 index 9d92fe12..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1918.v +++ /dev/null @@ -1,376 +0,0 @@ -(** Occur-check for Meta (up to delta) *) - -(** LNMItPredShort.v Version 2.0 July 2008 *) -(** does not need impredicative Set, runs under V8.2, tested with SVN 11296 *) - -(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse*) - - -Set Implicit Arguments. - -(** the universe of all monotypes *) -Definition k0 := Set. - -(** the type of all type transformations *) -Definition k1 := k0 -> k0. - -(** the type of all rank-2 type transformations *) -Definition k2 := k1 -> k1. - -(** polymorphic identity *) -Definition id : forall (A:Set), A -> A := fun A x => x. - -(** composition *) -Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x). - -Infix "o" := comp (at level 90). - -Definition sub_k1 (X Y:k1) : Type := - forall A:Set, X A -> Y A. - -Infix "c_k1" := sub_k1 (at level 60). - -(** monotonicity *) -Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B. - -(** extensionality *) -Definition ext (X:k1)(h: mon X): Prop := - forall (A B:Set)(f g:A -> B), - (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. - -(** first functor law *) -Definition fct1 (X:k1)(m: mon X) : Prop := - forall (A:Set)(x:X A), m _ _ (id(A:=A)) x = x. - -(** second functor law *) -Definition fct2 (X:k1)(m: mon X) : Prop := - forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), - m _ _ (g o f) x = m _ _ g (m _ _ f x). - -(** pack up the good properties of the approximation into - the notion of an extensional functor *) -Record EFct (X:k1) : Type := mkEFct - { m : mon X; - e : ext m; - f1 : fct1 m; - f2 : fct2 m }. - -(** preservation of extensional functors *) -Definition pEFct (F:k2) : Type := - forall (X:k1), EFct X -> EFct (F X). - - -(** we show some closure properties of pEFct, depending on such properties - for EFct *) - -Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)). -Proof. - red. - intros A B f x. - exact (mX (Y A)(Y B) (mY A B f) x). -Defined. - -(** closure under composition *) -Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)). -Proof. - intros ef1 ef2. - apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp. -(* prove ext *) - apply (e ef1). - intro. - apply (e ef2); trivial. -(* prove fct1 *) - rewrite (e ef1 (m ef2 (id (A:=A))) (id(A:=Y A))). - apply (f1 ef1). - intro. - apply (f1 ef2). -(* prove fct2 *) - rewrite (e ef1 (m ef2 (g o f))((m ef2 g)o(m ef2 f))). - apply (f2 ef1). - intro. - unfold comp at 2. - apply (f2 ef2). -Defined. - -Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> - pEFct (fun X A => F X (G X A)). -Proof. - red. - intros. - apply compEFct; auto. -Defined. - -(** closure under sums *) -Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type. -Proof. - intros ef1 ef2. - set (m12:=fun (A B:Set)(f:A->B) x => match x with - | inl y => inl _ (m ef1 f y) - | inr y => inr _ (m ef2 f y) - end). - apply (mkEFct(m:=m12)); red; intros. -(* prove ext *) - destruct r. - simpl. - apply (f_equal (fun x=>inl (A:=X B) (Y B) x)). - apply (e ef1); trivial. - simpl. - apply (f_equal (fun x=>inr (X B) (B:=Y B) x)). - apply (e ef2); trivial. -(* prove fct1 *) - destruct x. - simpl. - apply (f_equal (fun x=>inl (A:=X A) (Y A) x)). - apply (f1 ef1). - simpl. - apply (f_equal (fun x=>inr (X A) (B:=Y A) x)). - apply (f1 ef2). -(* prove fct2 *) - destruct x. - simpl. - rewrite (f2 ef1); reflexivity. - simpl. - rewrite (f2 ef2); reflexivity. -Defined. - -Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> - pEFct (fun X A => F X A + G X A)%type. -Proof. - red. - intros. - apply sumEFct; auto. -Defined. - -(** closure under products *) -Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type. -Proof. - intros ef1 ef2. - set (m12:=fun (A B:Set)(f:A->B) x => match x with - (x1,x2) => (m ef1 f x1, m ef2 f x2) end). - apply (mkEFct(m:=m12)); red; intros. -(* prove ext *) - destruct r as [x1 x2]. - simpl. - apply injective_projections; simpl. - apply (e ef1); trivial. - apply (e ef2); trivial. -(* prove fct1 *) - destruct x as [x1 x2]. - simpl. - apply injective_projections; simpl. - apply (f1 ef1). - apply (f1 ef2). -(* prove fct2 *) - destruct x as [x1 x2]. - simpl. - apply injective_projections; simpl. - apply (f2 ef1). - apply (f2 ef2). -Defined. - -Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> - pEFct (fun X A => F X A * G X A)%type. -Proof. - red. - intros. - apply prodEFct; auto. -Defined. - -(** the identity in k2 preserves extensional functors *) -Lemma idpEFct: pEFct (fun X => X). -Proof. - red. - intros. - assumption. -Defined. - -(** a variant for the eta-expanded identity *) -Lemma idpEFct_eta: pEFct (fun X A => X A). -Proof. - red. - intros X ef. - destruct ef as [m0 e0 f01 f02]. - change (mon X) with (mon (fun A => X A)) in m0. - apply (mkEFct (m:=m0) e0 f01 f02). -Defined. - -(** the identity in k1 "is" an extensional functor *) -Lemma idEFct: EFct (fun A => A). -Proof. - set (mId:=fun A B (f:A->B)(x:A) => f x). - apply (mkEFct(m:=mId)). - red. - intros. - unfold mId. - apply H. - red. - reflexivity. - red. - reflexivity. -Defined. - -(** constants in k2 *) -Lemma constpEFct (X:k1): EFct X -> pEFct (fun _ => X). -Proof. - red. - intros. - assumption. -Defined. - -(** constants in k1 *) -Lemma constEFct (C:Set): EFct (fun _ => C). -Proof. - set (mC:=fun A B (f:A->B)(x:C) => x). - apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity. -Defined. - - -(** the option type *) -Lemma optionEFct: EFct (fun (A:Set) => option A). - apply (mkEFct (X:=fun (A:Set) => option A)(m:=option_map)); red; intros. - destruct r. - simpl. - rewrite H. - reflexivity. - reflexivity. - destruct x; reflexivity. - destruct x; reflexivity. -Defined. - - -(** natural transformations from (X,mX) to (Y,mY) *) -Definition NAT(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y) : Prop := - forall (A B:Set)(f:A->B)(t:X A), j B (mX A B f t) = mY _ _ f (j A t). - - -Module Type LNMIt_Type. - -Parameter F:k2. -Parameter FpEFct: pEFct F. -Parameter mu20: k1. -Definition mu2: k1:= fun A => mu20 A. -Parameter mapmu2: mon mu2. -Definition MItType: Type := - forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. -Parameter MIt0 : MItType. -Definition MIt : MItType:= fun G s A t => MIt0 s t. -Definition InType : Type := - forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), - NAT j (m ef) mapmu2 -> F X c_k1 mu2. -Parameter In : InType. -Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2) - (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), - mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t). -Axiom MItRed : forall (G : k1) - (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2) - (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A), - MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t. -Definition mu2IndType : Prop := - forall (P : (forall A : Set, mu2 A -> Prop)), - (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2), - (forall (A : Set) (x : X A), P A (j A x)) -> - forall (A:Set)(t : F X A), P A (In ef n t)) -> - forall (A : Set) (r : mu2 A), P A r. -Axiom mu2Ind : mu2IndType. - -End LNMIt_Type. - -(** BushDepPredShort.v Version 0.2 July 2008 *) -(** does not need impredicative Set, produces stack overflow under V8.2, tested -with SVN 11296 *) - -(** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse *) - -Set Implicit Arguments. - -Require Import List. - -Definition listk1 (A:Set) : Set := list A. -Open Scope type_scope. - -Definition BushF(X:k1)(A:Set) := unit + A * X (X A). - -Definition bushpEFct : pEFct BushF. -Proof. - unfold BushF. - apply sumpEFct. - apply constpEFct. - apply constEFct. - apply prodpEFct. - apply constpEFct. - apply idEFct. - apply comppEFct. - apply idpEFct. - apply idpEFct_eta. -Defined. - -Module Type BUSH := LNMIt_Type with Definition F:=BushF - with Definition FpEFct := -bushpEFct. - -Module Bush (BushBase:BUSH). - -Definition Bush : k1 := BushBase.mu2. - -Definition bush : mon Bush := BushBase.mapmu2. - -End Bush. - - -Definition Id : k1 := fun X => X. - -Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= - match k with 0 => Id - | S k' => fun A => X (Pow X k' A) - end. - -Fixpoint POW (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) := - match k return mon (Pow X k) - with 0 => fun _ _ f => f - | S k' => fun _ _ f => m _ _ (POW k' m f) - end. - -Module Type BushkToList_Type. - -Declare Module Import BP: BUSH. -Definition F:=BushF. -Definition FpEFct:= bushpEFct. -Definition mu20 := mu20. -Definition mu2 := mu2. -Definition mapmu2 := mapmu2. -Definition MItType:= MItType. -Definition MIt0 := MIt0. -Definition MIt := MIt. -Definition InType := InType. -Definition In := In. -Definition mapmu2Red:=mapmu2Red. -Definition MItRed:=MItRed. -Definition mu2IndType:=mu2IndType. -Definition mu2Ind:=mu2Ind. - -Definition Bush:= mu2. -Module BushM := Bush BP. - -Parameter BushkToList: forall(k:nat)(A:k0)(t:Pow Bush k A), list A. -Axiom BushkToList0: forall(A:k0)(t:Pow Bush 0 A), BushkToList 0 A t = t::nil. - -End BushkToList_Type. - -Module BushDep (BushkToListM:BushkToList_Type). - -Module Bush := Bush BushkToListM. - -Import Bush. -Import BushkToListM. - - -Lemma BushkToList0NAT: NAT(Y:=listk1) (BushkToList 0) (POW 0 bush) map. -Proof. - red. - intros. - simpl. - rewrite BushkToList0. -(* stack overflow for coqc and coqtop *) - - -Abort. diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v deleted file mode 100644 index 4caee1c3..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1925.v +++ /dev/null @@ -1,22 +0,0 @@ -(* Check that the analysis of projectable rel's in an evar instance is up to - aliases *) - -Require Import List. - -Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := - fun x : A => g(f x). - -Definition map_fuse' : - forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), - (map g (map f xs)) = map (compose _ _ _ g f) xs - := - fun A B C g f => - (fix loop (ys : list A) {struct ys} := - match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys - with - | nil => refl_equal nil - | x :: xs => - match loop xs in eq _ a return eq _ ((g (f x)) :: a) with - | refl_equal => refl_equal (map g (map f (x :: xs))) - end - end). diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v deleted file mode 100644 index 930ace1d..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1931.v +++ /dev/null @@ -1,29 +0,0 @@ - - -Set Implicit Arguments. - -Inductive T (A:Set) : Set := - app : T A -> T A -> T A. - -Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B := - match t with - app t1 t2 => app (map f t1)(map f t2) - end. - -Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := - match t with - app t1 t2 => app (subst f t1)(subst f t2) - end. - -(* This is the culprit: *) -Definition k0:=Set. - -(** interaction of subst with map *) -Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): - subst g (map f t) = subst (fun x => g (f x)) t. -Proof. - intros. - generalize B C f g; clear B C f g. - induction t; intros; simpl. - f_equal. -Admitted. diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v deleted file mode 100644 index d5837619..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1935.v +++ /dev/null @@ -1,21 +0,0 @@ -Definition f (n:nat) := n = n. - -Lemma f_refl : forall n , f n. -intros. reflexivity. -Qed. - -Definition f' (x:nat) (n:nat) := n = n. - -Lemma f_refl' : forall n , f' n n. -Proof. - intros. reflexivity. -Qed. - -Require Import ZArith. - -Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt. - -Lemma f_refl'' : forall n , f'' true n n. -Proof. - intro. reflexivity. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v deleted file mode 100644 index 5e61529b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1939.v +++ /dev/null @@ -1,19 +0,0 @@ -Require Import Setoid Program.Basics. - - Parameter P : nat -> Prop. - Parameter R : nat -> nat -> Prop. - - Add Parametric Morphism : P - with signature R ++> impl as PM1. - Admitted. - - Add Parametric Morphism : P - with signature R --> impl as PM2. - Admitted. - - Goal forall x y, R x y -> P y -> P x. - Proof. - intros x y H1 H2. - rewrite H1. - auto. - Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v deleted file mode 100644 index ee2918c6..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1944.v +++ /dev/null @@ -1,9 +0,0 @@ -(* Test some uses of ? in introduction patterns *) - -Inductive J : nat -> Prop := - | K : forall p, J p -> (True /\ True) -> J (S p). - -Lemma bug : forall n, J n -> J (S n). -Proof. - intros ? H. - induction H as [? ? [? ?]]. diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v deleted file mode 100644 index 12c0ef9b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1951.v +++ /dev/null @@ -1,63 +0,0 @@ - -(* First a simplification of the bug *) - -Set Printing Universes. - -Inductive enc (A:Type (*1*)) (* : Type.1 *) := C : A -> enc A. - -Definition id (X:Type(*5*)) (x:X) := x. - -Lemma test : let S := Type(*6 : 7*) in enc S -> S. -simpl; intros. -apply enc. -apply id. -apply Prop. -Defined. - -(* Then the original bug *) - -Require Import List. - -Inductive a : Set := (* some dummy inductive *) -b : (list a) -> a. (* i don't know if this *) - (* happens for smaller *) - (* ones *) - -Inductive sg : Type := Sg. (* single *) - -Definition ipl2 (P : a -> Type) := (* in Prop, that means P is true forall *) -fold_right (fun x => prod (P x)) sg. (* the elements of a given list *) - -Definition ind - : forall S : a -> Type, - (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s := -fun (S : a -> Type) - (X : forall ls : list a, ipl2 S ls -> S (b ls)) => -fix ind2 (s : a) := -match s as a return (S a) with -| b l => - X l - (list_rect (fun l0 : list a => ipl2 S l0) Sg - (fun (a0 : a) (l0 : list a) (IHl : ipl2 S l0) => - pair (ind2 a0) IHl) l) -end. (* some induction principle *) - -Implicit Arguments ind [S]. - -Lemma k : a -> Type. (* some ininteresting lemma *) -intro;pattern H;apply ind;intros. - assert (K : Type). - induction ls. - exact sg. - exact sg. - exact (prod K sg). -Defined. - -Lemma k' : a -> Type. (* same lemma but with our bug *) -intro;pattern H;apply ind;intros. - apply prod. - induction ls. - exact sg. - exact sg. - exact sg. (* Proof complete *) -Defined. (* bug *) diff --git a/test-suite/bugs/closed/shouldsucceed/1962.v b/test-suite/bugs/closed/shouldsucceed/1962.v deleted file mode 100644 index a6b0fee5..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1962.v +++ /dev/null @@ -1,55 +0,0 @@ -(* Bug 1962.v - -Bonjour, - -J'ai un exemple de lemme que j'arrivais à prouver avec fsetdec avec la 8.2beta3 -avec la beta4 et la version svn 11447 branche 8.2 çà diverge. - -Voici l'exemple en question, l'exmple test2 marche bien dans les deux version, -test en revanche pose probleme: - -*) - -Require Export FSets. - -(** This module takes a decidable type and -build finite sets of this type, tactics and defs *) - -Module BuildFSets (DecPoints: UsualDecidableType). - -Module Export FiniteSetsOfPoints := FSetWeakList.Make DecPoints. -Module Export FiniteSetsOfPointsProperties := - WProperties FiniteSetsOfPoints. -Module Export Dec := WDecide FiniteSetsOfPoints. -Module Export FM := Dec.F. - -Definition set_of_points := t. -Definition Point := DecPoints.t. - -Definition couple(x y :Point) : set_of_points := -add x (add y empty). - -Definition triple(x y t :Point): set_of_points := -add x (add y (add t empty)). - -Lemma test : forall P A B C A' B' C', -Equal -(union (singleton P) (union (triple A B C) (triple A' B' C'))) -(union (triple P B B') (union (couple P A) (triple C A' C'))). -Proof. -intros. -unfold triple, couple. -Time fsetdec. (* works in 8.2 beta 3, not in beta 4 and final 8.2 *) - (* appears to works again in 8.3 and trunk, take 4-6 seconds *) -Qed. - -Lemma test2 : forall A B C, -Equal - (union (singleton C) (couple A B)) (triple A B C). -Proof. -intros. -unfold triple, couple. -Time fsetdec. -Qed. - -End BuildFSets.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1963.v b/test-suite/bugs/closed/shouldsucceed/1963.v deleted file mode 100644 index 11e2ee44..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1963.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Check that "dependent inversion" behaves correctly w.r.t to universes *) - -Require Import Eqdep. - -Set Implicit Arguments. - -Inductive illist(A:Type) : nat -> Type := - illistn : illist A 0 -| illistc : forall n:nat, A -> illist A n -> illist A (S n). - -Inductive isig (A:Type)(P:A -> Type) : Type := - iexists : forall x : A, P x -> isig P. - -Lemma inv : forall (A:Type)(n n':nat)(ts':illist A n'), n' = S n -> - isig (fun t => isig (fun ts => - eq_dep nat (fun n => illist A n) n' ts' (S n) (illistc t ts))). -Proof. -intros. -dependent inversion ts'. diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/shouldsucceed/1977.v deleted file mode 100644 index 28715040..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1977.v +++ /dev/null @@ -1,4 +0,0 @@ -Inductive T {A} : Prop := c : A -> T. -Goal (@T nat). -apply c. exact 0. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v deleted file mode 100644 index 99952682..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1981.v +++ /dev/null @@ -1,5 +0,0 @@ -Implicit Arguments ex_intro [A]. - -Goal exists n : nat, True. - eapply ex_intro. exact 0. exact I. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v deleted file mode 100644 index d0b3bf17..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2001.v +++ /dev/null @@ -1,22 +0,0 @@ -(* Automatic computing of guard in "Theorem with"; check that guard is not - computed when the user explicitly indicated it *) - -Unset Automatic Introduction. - -Inductive T : Set := -| v : T. - -Definition f (s:nat) (t:T) : nat. -fix 2. -intros s t. -refine - match t with - | v => s - end. -Defined. - -Lemma test : - forall s, f s v = s. -Proof. -reflexivity. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v deleted file mode 100644 index df666148..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2017.v +++ /dev/null @@ -1,15 +0,0 @@ -(* Some check of Miller's pattern inference - used to fail in 8.2 due - first to the presence of aliases, secondly due to the absence of - restriction of the potential interesting variables to the subset of - variables effectively occurring in the term to instantiate *) - -Set Implicit Arguments. - -Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool. - -Variable H : exists x : bool, True. - -Definition coef := -match Some true with - Some _ => @choose _ H |_ => true -end . diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/shouldsucceed/2021.v deleted file mode 100644 index e598e5ae..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2021.v +++ /dev/null @@ -1,23 +0,0 @@ -(* correct failure of injection/discriminate on types whose inductive - status derives from the substitution of an argument *) - -Inductive t : nat -> Type := -| M : forall n: nat, nat -> t n. - -Lemma eq_t : forall n n' m m', - existT (fun B : Type => B) (t n) (M n m) = - existT (fun B : Type => B) (t n') (M n' m') -> True. -Proof. - intros. - injection H. - intro Ht. - exact I. -Qed. - -Lemma eq_t' : forall n n' : nat, - existT (fun B : Type => B) (t n) (M n 0) = - existT (fun B : Type => B) (t n') (M n' 1) -> True. -Proof. - intros. - discriminate H || exact I. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2027.v b/test-suite/bugs/closed/shouldsucceed/2027.v deleted file mode 100644 index fb53c6ef..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2027.v +++ /dev/null @@ -1,11 +0,0 @@ - -Parameter T : Type -> Type. -Parameter f : forall {A}, T A -> T A. -Parameter P : forall {A}, T A -> Prop. -Axiom f_id : forall {A} (l : T A), f l = l. - -Goal forall A (p : T A), P p. -Proof. - intros. - rewrite <- f_id. -Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v deleted file mode 100644 index a6ce4de0..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2083.v +++ /dev/null @@ -1,27 +0,0 @@ -Require Import Program Arith. - -Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) - (H : forall (i : { i | i < n }), i < p -> P i = true) - {measure (n - p)} : - Exc (forall (p : { i | i < n}), P p = true) := - match le_lt_dec n p with - | left _ => value _ - | right cmp => - if dec (P p) then - check_n n P (S p) _ - else - error - end. - -Require Import Omega. - -Solve Obligations using program_simpl ; auto with *; try omega. - -Next Obligation. - apply H. simpl. omega. -Defined. - -Next Obligation. - case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. - revert H0. clear_subset_proofs. auto. - apply H. simpl. assumption. Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/2089.v b/test-suite/bugs/closed/shouldsucceed/2089.v deleted file mode 100644 index aebccc94..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2089.v +++ /dev/null @@ -1,17 +0,0 @@ -Inductive even (x: nat): nat -> Prop := - | even_base: even x O - | even_succ: forall n, odd x n -> even x (S n) - -with odd (x: nat): nat -> Prop := - | odd_succ: forall n, even x n -> odd x (S n). - -Scheme even_ind2 := Minimality for even Sort Prop - with odd_ind2 := Minimality for odd Sort Prop. - -Combined Scheme even_odd_ind from even_ind2, odd_ind2. - -Check (even_odd_ind :forall (x : nat) (P P0 : nat -> Prop), - P 0 -> - (forall n : nat, odd x n -> P0 n -> P (S n)) -> - (forall n : nat, even x n -> P n -> P0 (S n)) -> - (forall n : nat, even x n -> P n) /\ (forall n : nat, odd x n -> P0 n)). diff --git a/test-suite/bugs/closed/shouldsucceed/2095.v b/test-suite/bugs/closed/shouldsucceed/2095.v deleted file mode 100644 index 28ea99df..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2095.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Classes and sections *) - -Section OPT. - Variable A: Type. - - Inductive MyOption: Type := - | MyNone: MyOption - | MySome: A -> MyOption. - - Class Opt: Type := { - f_opt: A -> MyOption - }. -End OPT. - -Definition f_nat (n: nat): MyOption nat := MySome _ n. - -Instance Nat_Opt: Opt nat := { - f_opt := f_nat -}. diff --git a/test-suite/bugs/closed/shouldsucceed/2108.v b/test-suite/bugs/closed/shouldsucceed/2108.v deleted file mode 100644 index cad8baa9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2108.v +++ /dev/null @@ -1,22 +0,0 @@ -(* Declare Module in Module Type *) -Module Type A. -Record t : Set := { something : unit }. -End A. - - -Module Type B. -Declare Module BA : A. -End B. - - -Module Type C. -Declare Module CA : A. -Declare Module CB : B with Module BA := CA. -End C. - - -Module Type D. -Declare Module DA : A. -(* Next line gives: "Anomaly: uncaught exception Not_found. Please report." *) -Declare Module DC : C with Module CA := DA. -End D. diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v deleted file mode 100644 index 6377a8b7..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2117.v +++ /dev/null @@ -1,56 +0,0 @@ -(* Check pattern-unification on evars in apply unification *) - -Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'. - -Axiom copy : forall tau:Type, tau -> tau -> Prop. -Axiom copyr : forall tau:Type, tau -> tau -> Prop. -Axiom copyf : forall tau:Type, tau -> tau -> Prop. -Axiom eq : forall tau:Type, tau -> tau -> Prop. -Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop. - -Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'. -Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'), -(forall x:tau, copyr tau x x->copy tau' (t x) (t' x)) -->copy (tau->tau') t t'. - -Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'. -Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'), -copyr (tau->tau') t t' -->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)). - -Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'. -Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'), -copyr (tau->tau') t t' -->(forall x y:tau, forall z1 z2:tau', -(copy tau x y)-> -(subst tau tau' t x z1)-> -(subst tau tau' t' y z2)-> -copyf tau' z1 z2). - -Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau', -( ((subst tau tau' t q t') /\ (eq tau' t' r)) -->eq tau' (app tau tau' t q) r). - -Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau', -forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t')) -->eq tau' r (app tau tau' t q). - -Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau', -(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r)) -->subst tau tau' t q r. - -Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
-Ltac Subst := apply substcopy;intros;EtaLong. -Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A). -Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A. - -Theorem church0: forall i:Type, exists X:(i->i)->i->i, -copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)). -intros. -esplit. -EtaLong. -eapply eqappd;split. -Subst. -apply copyf_atom. -Show Existentials. -apply H1. diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/shouldsucceed/2123.v deleted file mode 100644 index 422a2c12..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2123.v +++ /dev/null @@ -1,11 +0,0 @@ -(* About the detection of non-dependent metas by the refine tactic *) - -(* The following is a simplification of bug #2123 *) - -Parameter fset : nat -> Set. -Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }. -Goal forall i, fset (S i). -intro. -refine (proj1_sig (widen i _)). - - diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v deleted file mode 100644 index 142ada26..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2127.v +++ /dev/null @@ -1,8 +0,0 @@ -(* Check that "apply eq_refl" is not exported as an interactive - tactic but as a statically globalized one *) - -(* (this is a simplification of the original bug report) *) - -Module A. -Hint Rewrite eq_sym using apply eq_refl : foo. -End A. diff --git a/test-suite/bugs/closed/shouldsucceed/2135.v b/test-suite/bugs/closed/shouldsucceed/2135.v deleted file mode 100644 index 61882176..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2135.v +++ /dev/null @@ -1,9 +0,0 @@ -(* Check that metas are whd-normalized before trying 2nd-order unification *) -Lemma test : - forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop), - (forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A)) - -> Q D (T D). -Proof. - intros D T Q H. - pattern (T D). apply H. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2136.v b/test-suite/bugs/closed/shouldsucceed/2136.v deleted file mode 100644 index d2b926f3..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2136.v +++ /dev/null @@ -1,61 +0,0 @@ -(* Bug #2136 - -The fsetdec tactic seems to get confused by hypotheses like - HeqH1 : H1 = MkEquality s0 s1 b -If I clear them then it is able to solve my goal; otherwise it is not. -I would expect it to be able to solve the goal even without this hypothesis -being cleared. A small, self-contained example is below. - -I have coq r12238. - - -Thanks -Ian -*) - - -Require Import FSets. -Require Import Arith. -Require Import FSetWeakList. - -Module DecidableNat. -Definition t := nat. -Definition eq := @eq nat. -Definition eq_refl := @refl_equal nat. -Definition eq_sym := @sym_eq nat. -Definition eq_trans := @trans_eq nat. -Definition eq_dec := eq_nat_dec. -End DecidableNat. - -Module NatSet := Make(DecidableNat). - -Module Export Dec := WDecide (NatSet). -Import FSetDecideAuxiliary. - -Parameter MkEquality : forall ( s0 s1 : NatSet.t ) - ( x : nat ), - NatSet.Equal s1 (NatSet.add x s0). - -Lemma ThisLemmaWorks : forall ( s0 s1 : NatSet.t ) - ( a b : nat ), - NatSet.In a s0 - -> NatSet.In a s1. -Proof. -intros. -remember (MkEquality s0 s1 b) as H1. -clear HeqH1. -fsetdec. -Qed. - -Lemma ThisLemmaWasFailing : forall ( s0 s1 : NatSet.t ) - ( a b : nat ), - NatSet.In a s0 - -> NatSet.In a s1. -Proof. -intros. -remember (MkEquality s0 s1 b) as H1. -fsetdec. -(* -Error: Tactic failure: because the goal is beyond the scope of this tactic. -*) -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2137.v b/test-suite/bugs/closed/shouldsucceed/2137.v deleted file mode 100644 index 6c2023ab..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2137.v +++ /dev/null @@ -1,52 +0,0 @@ -(* Bug #2137 - -The fsetdec tactic is sensitive to which way round the arguments to <> are. -In the small, self-contained example below, it is able to solve the goal -if it knows that "b <> a", but not if it knows that "a <> b". I would expect -it to be able to solve hte goal in either case. - -I have coq r12238. - - -Thanks -Ian - -*) - -Require Import Arith FSets FSetWeakList. - -Module DecidableNat. -Definition t := nat. -Definition eq := @eq nat. -Definition eq_refl := @refl_equal nat. -Definition eq_sym := @sym_eq nat. -Definition eq_trans := @trans_eq nat. -Definition eq_dec := eq_nat_dec. -End DecidableNat. - -Module NatSet := Make(DecidableNat). - -Module Export NameSetDec := WDecide (NatSet). - -Lemma ThisLemmaWorks : forall ( s0 : NatSet.t ) - ( a b : nat ), - b <> a - -> ~(NatSet.In a s0) - -> ~(NatSet.In a (NatSet.add b s0)). -Proof. -intros. -fsetdec. -Qed. - -Lemma ThisLemmaWasFailing : forall ( s0 : NatSet.t ) - ( a b : nat ), - a <> b - -> ~(NatSet.In a s0) - -> ~(NatSet.In a (NatSet.add b s0)). -Proof. -intros. -fsetdec. -(* -Error: Tactic failure: because the goal is beyond the scope of this tactic. -*) -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v deleted file mode 100644 index a7f35508..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2139.v +++ /dev/null @@ -1,24 +0,0 @@ -(* Call of apply on <-> failed because of evars in elimination predicate *) -Generalizable Variables patch. - -Class Patch (patch : Type) := { - commute : patch -> patch -> Prop -}. - -Parameter flip : forall `{patchInstance : Patch patch} - {a b : patch}, - commute a b <-> commute b a. - -Lemma Foo : forall `{patchInstance : Patch patch} - {a b : patch}, - (commute a b) - -> True. -Proof. -intros. -apply flip in H. - -(* failed in well-formed arity check because elimination predicate of - iff in (@flip _ _ _ _) had normalized evars while the ones in the - type of (@flip _ _ _ _) itself had non-normalized evars *) - -(* By the way, is the check necessary ? *) diff --git a/test-suite/bugs/closed/shouldsucceed/2141.v b/test-suite/bugs/closed/shouldsucceed/2141.v deleted file mode 100644 index 941ae530..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2141.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import FSetList. -Require Import OrderedTypeEx. - -Module NatSet := FSetList.Make (Nat_as_OT). -Recursive Extraction NatSet.fold. - -Module FSetHide (X : FSetInterface.S). - Include X. -End FSetHide. - -Module NatSet' := FSetHide NatSet. -Recursive Extraction NatSet'.fold. - -(* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v deleted file mode 100644 index 4dc0de74..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2145.v +++ /dev/null @@ -1,20 +0,0 @@ -(* Test robustness of Groebner tactic in presence of disequalities *) - -Require Export Reals. -Require Export Nsatz. - -Open Scope R_scope. - -Lemma essai : - forall yb xb m1 m2 xa ya, - xa <> xb -> - yb - 2 * m2 * xb = ya - m2 * xa -> - yb - m1 * xb = ya - m1 * xa -> - yb - ya = (2 * xb - xa) * m2 -> - yb - ya = (xb - xa) * m1. -Proof. -intros. -(* clear H. groebner used not to work when H was not cleared *) -nsatz. -Qed. - diff --git a/test-suite/bugs/closed/shouldsucceed/2181.v b/test-suite/bugs/closed/shouldsucceed/2181.v deleted file mode 100644 index 62820d86..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2181.v +++ /dev/null @@ -1,3 +0,0 @@ -Class C. -Parameter P: C -> Prop. -Fail Record R: Type := { _: C; u: P _ }. diff --git a/test-suite/bugs/closed/shouldsucceed/2193.v b/test-suite/bugs/closed/shouldsucceed/2193.v deleted file mode 100644 index fe258867..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2193.v +++ /dev/null @@ -1,31 +0,0 @@ -(* Computation of dependencies in the "match" return predicate was incomplete *) -(* Submitted by R. O'Connor, Nov 2009 *) - -Inductive Symbol : Set := - | VAR : Symbol. - -Inductive SExpression := - | atomic : Symbol -> SExpression. - -Inductive ProperExpr : SExpression -> SExpression -> Type := - | pe_3 : forall (x : Symbol) (alpha : SExpression), - ProperExpr alpha (atomic VAR) -> - ProperExpr (atomic x) alpha. - -Definition A (P : forall s : SExpression, Type) - (x alpha alpha1 : SExpression) - (t : ProperExpr (x) alpha1) : option (x = atomic VAR) := - match t as pe in ProperExpr a b return option (a = atomic VAR) with - | pe_3 x0 alpha3 tye' => - (fun (x:Symbol) (alpha : SExpression) => @None (atomic x = atomic VAR)) - x0 alpha3 - end. - -Definition B (P : forall s : SExpression, Type) - (x alpha alpha1 : SExpression) - (t : ProperExpr (x) alpha1) : option (x = atomic VAR) := - match t as pe in ProperExpr a b return option (a = atomic VAR) with - | pe_3 x0 alpha3 tye' => - (fun (x:Symbol) (alpha : SExpression) (t:ProperExpr alpha (atomic VAR)) => @None (atomic x = atomic VAR)) - x0 alpha3 tye' - end. diff --git a/test-suite/bugs/closed/shouldsucceed/2230.v b/test-suite/bugs/closed/shouldsucceed/2230.v deleted file mode 100644 index 5076fb2b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2230.v +++ /dev/null @@ -1,6 +0,0 @@ -Goal forall f, f 1 1 -> True. -intros. -match goal with - | [ H : _ ?a |- _ ] => idtac -end. -Abort. diff --git a/test-suite/bugs/closed/shouldsucceed/2231.v b/test-suite/bugs/closed/shouldsucceed/2231.v deleted file mode 100644 index 03e2c9bb..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2231.v +++ /dev/null @@ -1,3 +0,0 @@ -Inductive unit2 : Type := U : unit -> unit2. -Inductive dummy (u: unit2) : unit -> Type := - V: dummy u (let (tt) := u in tt). diff --git a/test-suite/bugs/closed/shouldsucceed/2244.v b/test-suite/bugs/closed/shouldsucceed/2244.v deleted file mode 100644 index d499e515..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2244.v +++ /dev/null @@ -1,19 +0,0 @@ -(* 1st-order unification did not work when in competition with pattern unif. *) - -Set Implicit Arguments. -Lemma test : forall - (A : Type) - (B : Type) - (f : A -> B) - (S : B -> Prop) - (EV : forall y (f':A->B), (forall x', S (f' x')) -> S (f y)) - (HS : forall x', S (f x')) - (x : A), - S (f x). -Proof. - intros. eapply EV. intros. - (* worked in v8.2 but not in v8.3beta, fixed in r12898 *) - apply HS. - - (* still not compatible with 8.2 because an evar can be solved in - two different ways and is left open *) diff --git a/test-suite/bugs/closed/shouldsucceed/2255.v b/test-suite/bugs/closed/shouldsucceed/2255.v deleted file mode 100644 index bf80ff66..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2255.v +++ /dev/null @@ -1,21 +0,0 @@ -(* Check injection in presence of dependencies hidden in applicative terms *) - -Inductive TupleT : nat -> Type := - nilT : TupleT 0 -| consT {n} A : (A -> TupleT n) -> TupleT (S n). - -Inductive Tuple : forall n, TupleT n -> Type := - nil : Tuple _ nilT -| cons {n} A (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). - -Goal forall n A F x X n0 A0 x0 F0 H0 (H : existT (fun n0 : nat => {H0 : TupleT -n0 & Tuple n0 H0}) - (S n0) - (existT (fun H0 : TupleT (S n0) => Tuple (S n0) H0) - (consT A0 F0) (cons A0 x0 F0 H0)) = - existT (fun n0 : nat => {H0 : TupleT n0 & Tuple n0 H0}) - (S n) - (existT (fun H0 : TupleT (S n) => Tuple (S n) H0) - (consT A F) (cons A x F X))), False. -intros. -injection H. diff --git a/test-suite/bugs/closed/shouldsucceed/2262.v b/test-suite/bugs/closed/shouldsucceed/2262.v deleted file mode 100644 index b61f18b8..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2262.v +++ /dev/null @@ -1,11 +0,0 @@ - - -Generalizable Variables A. -Class Test A := { test : A }. - -Lemma mylemma : forall `{Test A}, test = test. -Admitted. (* works fine *) - -Definition mylemma' := forall `{Test A}, test = test. -About mylemma'. - diff --git a/test-suite/bugs/closed/shouldsucceed/2281.v b/test-suite/bugs/closed/shouldsucceed/2281.v deleted file mode 100644 index 40948d90..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2281.v +++ /dev/null @@ -1,50 +0,0 @@ -(** Bug #2281 - -In the code below, coq is confused by an equality unless it is first 'subst'ed -away, yet http://coq.inria.fr/stdlib/Coq.FSets.FSetDecide.html says - - fsetdec will first perform any necessary zeta and beta reductions and will -invoke subst to eliminate any Coq equalities between finite sets or their -elements. - -I have coq r12851. - -*) - -Require Import Arith. -Require Import FSets. -Require Import FSetWeakList. - -Module DecidableNat. -Definition t := nat. -Definition eq := @eq nat. -Definition eq_refl := @refl_equal nat. -Definition eq_sym := @sym_eq nat. -Definition eq_trans := @trans_eq nat. -Definition eq_dec := eq_nat_dec. -End DecidableNat. - -Module NatSet := Make(DecidableNat). - -Module Export NameSetDec := WDecide (NatSet). - -Lemma ThisLemmaWorks : forall ( s1 s2 : NatSet.t ) - ( H : s1 = s2 ), - NatSet.Equal s1 s2. -Proof. -intros. -subst. -fsetdec. -Qed. - -Import FSetDecideAuxiliary. - -Lemma ThisLemmaWasFailing : forall ( s1 s2 : NatSet.t ) - ( H : s1 = s2 ), - NatSet.Equal s1 s2. -Proof. -intros. -fsetdec. -(* Error: Tactic failure: because the goal is beyond the scope of this tactic. -*) -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2295.v b/test-suite/bugs/closed/shouldsucceed/2295.v deleted file mode 100644 index f5ca28dc..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2295.v +++ /dev/null @@ -1,11 +0,0 @@ -(* Check if omission of "as" in return clause works w/ section variables too *) - -Section sec. - -Variable b: bool. - -Definition d' := - (match b return b = true \/ b = false with - | true => or_introl _ (refl_equal true) - | false => or_intror _ (refl_equal false) - end). diff --git a/test-suite/bugs/closed/shouldsucceed/2299.v b/test-suite/bugs/closed/shouldsucceed/2299.v deleted file mode 100644 index c0552ca7..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2299.v +++ /dev/null @@ -1,13 +0,0 @@ -(* Check that destruct refreshes universes in what it generalizes *) - -Section test. - -Variable A: Type. - -Inductive T: unit -> Type := C: A -> unit -> T tt. - -Let unused := T tt. - -Goal T tt -> False. - intro X. - destruct X. diff --git a/test-suite/bugs/closed/shouldsucceed/2300.v b/test-suite/bugs/closed/shouldsucceed/2300.v deleted file mode 100644 index 4e587cbb..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2300.v +++ /dev/null @@ -1,15 +0,0 @@ -(* Check some behavior of Ltac pattern-matching wrt universe levels *) - -Section contents. - -Variables (A: Type) (B: (unit -> Type) -> Type). - -Inductive C := c: A -> unit -> C. - -Let unused2 (x: unit) := C. - -Goal True. -intuition. -Qed. - -End contents. diff --git a/test-suite/bugs/closed/shouldsucceed/2303.v b/test-suite/bugs/closed/shouldsucceed/2303.v deleted file mode 100644 index e614b9b5..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2303.v +++ /dev/null @@ -1,4 +0,0 @@ -Class A := a: unit. -Class B (x: unit). -Axiom H: forall x: A, @B x -> x = x -> unit. -Definition Field (z: A) (m: @B z) x := (@H _ _ x) = z. diff --git a/test-suite/bugs/closed/shouldsucceed/2304.v b/test-suite/bugs/closed/shouldsucceed/2304.v deleted file mode 100644 index 1ac2702b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2304.v +++ /dev/null @@ -1,4 +0,0 @@ -(* This used to fail with an anomaly NotASort at some time *) -Class A (O: Type): Type := a: O -> Type. -Fail Goal forall (x: a tt), @a x = @a x. - diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v deleted file mode 100644 index 7c049495..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2307.v +++ /dev/null @@ -1,3 +0,0 @@ -Inductive V: nat -> Type := VS n: V (S n). -Definition f (e: V 1): nat := match e with VS 0 => 3 end. - diff --git a/test-suite/bugs/closed/shouldsucceed/2320.v b/test-suite/bugs/closed/shouldsucceed/2320.v deleted file mode 100644 index facb9ecf..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2320.v +++ /dev/null @@ -1,14 +0,0 @@ -(* Managing metavariables in the return clause of a match *) - -(* This was working in 8.1 but is failing in 8.2 and 8.3. It works in - trunk thanks to the new proof engine. It could probably made to work in - 8.2 and 8.3 if a return predicate of the form "dummy 0" instead of - (or in addition to) a sophisticated predicate of the form - "as x in dummy y return match y with 0 => ?P | _ => ID end" *) - -Inductive dummy : nat -> Prop := constr : dummy 0. - -Lemma failure : forall (x : dummy 0), x = constr. -Proof. -intros x. -refine (match x with constr => _ end). diff --git a/test-suite/bugs/closed/shouldsucceed/2342.v b/test-suite/bugs/closed/shouldsucceed/2342.v deleted file mode 100644 index 094e5466..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2342.v +++ /dev/null @@ -1,8 +0,0 @@ -(* Checking that the type inference algoithme does not commit to an - equality over sorts when only a subtyping constraint is around *) - -Parameter A : Set. -Parameter B : A -> Set. -Parameter F : Set -> Prop. -Check (F (forall x, B x)). - diff --git a/test-suite/bugs/closed/shouldsucceed/2347.v b/test-suite/bugs/closed/shouldsucceed/2347.v deleted file mode 100644 index e433f158..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2347.v +++ /dev/null @@ -1,10 +0,0 @@ -Require Import EquivDec List. -Generalizable All Variables. - -Program Definition list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := - (fun (x y : list A) => _). -Admit Obligations of list_eqdec. - -Program Definition list_eqdec' `(eqa : EqDec A eq) : EqDec (list A) eq := - (fun _ : nat => (fun (x y : list A) => _)) 0. -Admit Obligations of list_eqdec'. diff --git a/test-suite/bugs/closed/shouldsucceed/2350.v b/test-suite/bugs/closed/shouldsucceed/2350.v deleted file mode 100644 index e91f22e2..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2350.v +++ /dev/null @@ -1,6 +0,0 @@ -(* Check that the fix tactic, when called from refine, reduces enough - to see the products *) - -Definition foo := forall n:nat, n=n. -Definition bar : foo. -refine (fix aux (n:nat) := _). diff --git a/test-suite/bugs/closed/shouldsucceed/2353.v b/test-suite/bugs/closed/shouldsucceed/2353.v deleted file mode 100644 index b5c45c28..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2353.v +++ /dev/null @@ -1,12 +0,0 @@ -(* Are recursively non-uniform params correctly treated? *) -Inductive list (A:nat -> Type) n := cons : A n -> list A (S n) -> list A n. -Inductive term n := app (l : list term n). -Definition term_list := - fix term_size n (t : term n) (acc : nat) {struct t} : nat := - match t with - | app l => - (fix term_list_size n (l : list term n) (acc : nat) {struct l} : nat := - match l with - | cons t q => term_list_size (S n) q (term_size n t acc) - end) n l (S acc) - end. diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v deleted file mode 100644 index 4ae97c97..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2360.v +++ /dev/null @@ -1,13 +0,0 @@ -(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *) -Definition interp (etyp : nat -> Type) (p: nat) := etyp p. - -Record Value (etyp : nat -> Type) := Mk { - typ : nat; - value : interp etyp typ -}. - -Definition some_value (etyp : nat -> Type) : (Value etyp). -Proof. - intros. - Fail apply Mk. (* Check that it does not raise an anomaly *) - diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v deleted file mode 100644 index febb9c7b..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2362.v +++ /dev/null @@ -1,38 +0,0 @@ -Set Implicit Arguments. - -Class Pointed (M:Type -> Type) := -{ - creturn: forall {A: Type}, A -> M A -}. - -Unset Implicit Arguments. -Inductive FPair (A B:Type) (neutral: B) : Type:= - fpair : forall (a:A) (b:B), FPair A B neutral. -Implicit Arguments fpair [[A] [B] [neutral]]. - -Set Implicit Arguments. - -Notation "( x ,> y )" := (fpair x y) (at level 0). - -Instance Pointed_FPair B neutral: - Pointed (fun A => FPair A B neutral) := - { creturn := fun A (a:A) => (a,> neutral) }. -Definition blah_fail (x:bool) : FPair bool nat O := - creturn x. -Set Printing All. Print blah_fail. - -Definition blah_explicit (x:bool) : FPair bool nat O := - @creturn _ (Pointed_FPair _ ) _ x. - -Print blah_explicit. - - -Instance Pointed_FPair_mono: - Pointed (fun A => FPair A nat 0) := - { creturn := fun A (a:A) => (a,> 0) }. - - -Definition blah (x:bool) : FPair bool nat O := - creturn x. - - diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/shouldsucceed/2375.v deleted file mode 100644 index c17c426c..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2375.v +++ /dev/null @@ -1,18 +0,0 @@ -(* In the following code, the (superfluous) lemma [lem] is responsible -for the failure of congruence. *) - -Definition f : nat -> Prop := fun x => True. - -Lemma lem : forall x, (True -> True) = ( True -> f x). -Proof. - intros. reflexivity. -Qed. - -Goal forall (x:nat), x = x. -Proof. - intros. - assert (lem := lem). - (*clear ax.*) - congruence. -Qed. - diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v deleted file mode 100644 index 7deec64d..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2378.v +++ /dev/null @@ -1,608 +0,0 @@ -(* test with Coq 8.3rc1 *) - -Require Import Program. - -Inductive Unit: Set := unit: Unit. - -Definition eq_dec T := forall x y:T, {x=y}+{x<>y}. - -Section TTS_TASM. - -Variable Time: Set. -Variable Zero: Time. -Variable tle: Time -> Time -> Prop. -Variable tlt: Time -> Time -> Prop. -Variable tadd: Time -> Time -> Time. -Variable tsub: Time -> Time -> Time. -Variable tmin: Time -> Time -> Time. -Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity). -Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity). -Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity). -Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity). -Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level). -Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level). - -Variable tzerop: forall n, (n = Zero) + {Zero @< n}. -Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}. -Variable tle_plus_l: forall n m, n @<= n @+ m. -Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}. - -Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (@eq_refl _ Zero). -Variable tplus_n_O: forall n, n @+ Zero = n. -Variable tlt_le_weak: forall n m, n @< m -> n @<= m. -Variable tlt_irrefl: forall n, ~ n @< n. -Variable tplus_nlt: forall n m, ~n @+ m @< n. -Variable tle_n: forall n, n @<= n. -Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m. -Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p. -Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p. -Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p. -Variable tle_refl: forall n, n @<= n. -Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero. -Variable Time_eq_dec: eq_dec Time. - -(*************************************************************) - -Section PropLogic. -Variable Predicate: Type. - -Inductive LP: Type := - LPPred: Predicate -> LP -| LPAnd: LP -> LP -> LP -| LPNot: LP -> LP. - -Variable State: Type. -Variable Sat: State -> Predicate -> Prop. - -Fixpoint lpSat st f: Prop := - match f with - LPPred p => Sat st p - | LPAnd f1 f2 => lpSat st f1 /\ lpSat st f2 - | LPNot f1 => ~lpSat st f1 - end. -End PropLogic. - -Implicit Arguments lpSat. - -Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := - match f with - LPPred p => p2lp p - | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) - | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) - end. -Implicit Arguments LPTransfo. - -Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := - LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f. - -Section TTS. - -Variable State: Type. - -Record TTS: Type := mkTTS { - Init: State -> Prop; - Delay: State -> Time -> State -> Prop; - Next: State -> State -> Prop; - Predicate: Type; - Satisfy: State -> Predicate -> Prop -}. - -Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := mkTTS - (fun st => forall i, Init (tts i) st) - (fun st d st' => forall i, Delay (tts i) st d st') - (fun st st' => forall i, Next (tts i) st st') - { i: Ind & Predicate (tts i) } - (fun st p => Satisfy (tts (projT1 p)) st (projT2 p)). - -End TTS. - -Section SIMU_F. - -Variables StateA StateC: Type. - -Record mapping: Type := mkMapping { - mState: Type; - mInit: StateC -> mState; - mNext: mState -> StateC -> mState; - mDelay: mState -> StateC -> Time -> mState; - mabs: mState -> StateC -> StateA -}. - -Variable m: mapping. - -Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuPrf { - inv: (mState m) -> StateC -> Prop; - invInit: forall st, Init _ c st -> inv (mInit m st) st; - invDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> inv (mDelay m ex1 st1 d) st2; - invNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> inv (mNext m ex1 st1) st2; - simuInit: forall st, Init _ c st -> Init _ a (mabs m (mInit m st) st); - simuDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> - Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2); - simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> - Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2); - simuPred: forall ext st, inv ext st -> - (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) -}. - -Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)), - lpSat (Sat i) st f - <-> - lpSat - (fun (st : State) (p : {i : Ind & Pred i}) => Sat (projT1 p) st (projT2 p)) st - (addIndex Ind _ i f). -Proof. - induction f; simpl; intros; split; intros; intuition. -Qed. - -Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))): - {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) := - fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)). - -Implicit Arguments trProd. -Require Import Setoid. - -Theorem satTrProd: - forall State Ind Pred (tts: Ind -> TTS State) - (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}), - lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p)) - <-> - lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p). -Proof. - unfold trProd, TTSIndexedProduct; simpl; intros. - rewrite (satProd State Ind (fun i => Predicate State (tts i)) - (fun i => Satisfy _ (tts i))); tauto. -Qed. - -Theorem simuProd: - forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) - (tra: forall i, (Pred i) -> LP (Predicate _ (tta i))) - (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))), - (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> - simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc) - (trProd Pred tta tra) (trProd Pred ttc trc). -Proof. - intros. - apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto. - eapply invInit; eauto. - eapply invDelay; eauto. - eapply invNext; eauto. - eapply simuInit; eauto. - eapply simuDelay; eauto. - eapply simuNext; eauto. - split; simpl; intros. - generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro. - rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1. - rewrite (satTrProd StateC Ind Pred ttc trc); apply H0. - - generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro. - rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1. - rewrite (satTrProd StateA Ind Pred tta tra); apply H0. -Qed. - -End SIMU_F. - -Section TRANSFO. - -Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf { - simuLR: simu StateA StateC m1 Pred a c tra trc; - simuRL: simu StateC StateA m2 Pred c a trc tra -}. - -Theorem simu_equivProd: - forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) - (tra: forall i, (Pred i) -> LP (Predicate _ (tta i))) - (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))), - (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> - simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc) - (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc). -Proof. - intros; split; intros. - apply simuProd; intro. - elim (X i); auto. - apply simuProd; intro. - elim (X i); auto. -Qed. - -Record RTLanguage: Type := mkRTLanguage { - Syntax: Type; - DynamicState: Syntax -> Type; - Semantic: forall (mdl:Syntax), TTS (DynamicState mdl); - MdlPredicate: Syntax -> Type; - MdlPredicateDefinition: forall mdl, MdlPredicate mdl -> LP (Predicate _ (Semantic mdl)) -}. - -Record Transformation (l1 l2: RTLanguage): Type := mkTransformation { - Tmodel: Syntax l1 -> Syntax l2; - Tl1l2: forall mdl, mapping (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)); - Tl2l1: forall mdl, mapping (DynamicState l2 (Tmodel mdl)) (DynamicState l1 mdl); - Tpred: forall mdl, MdlPredicate l1 mdl -> LP (MdlPredicate l2 (Tmodel mdl)); - Tsim: forall mdl, simu_equiv (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)) (Tl1l2 mdl) (Tl2l1 mdl) - (MdlPredicate l1 mdl) (Semantic l1 mdl) (Semantic l2 (Tmodel mdl)) - (MdlPredicateDefinition l1 mdl) - (fun p => LPTransfo (MdlPredicateDefinition l2 (Tmodel mdl)) (Tpred mdl p)) -}. - -Section Product. - -Record PSyntax (L: RTLanguage): Type := mkPSyntax { - pIndex: Type; - pIsEmpty: pIndex + {pIndex -> False}; - pState: Type; - pComponents: pIndex -> Syntax L; - pIsShared: forall i, DynamicState L (pComponents i) = pState -}. - -Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & MdlPredicate L (pComponents L sys i)}. - -(* product with shared state *) - -Definition PLanguage (L: RTLanguage): RTLanguage := - mkRTLanguage - (PSyntax L) - (pState L) - (fun mdl => TTSIndexedProduct (pState L mdl) (pIndex L mdl) - (fun i => match pIsShared L mdl i in (_ = y) return TTS y with - eq_refl => Semantic L (pComponents L mdl i) - end)) - (pPredicate L) - (fun mdl => trProd _ _ _ _ - (fun i pi => match pIsShared L mdl i as e in (_ = y) return - (LP (Predicate y - match e in (_ = y0) return (TTS y0) with - | eq_refl => Semantic L (pComponents L mdl i) - end)) - with - | eq_refl => MdlPredicateDefinition L (pComponents L mdl i) pi - end)). - -Inductive Empty: Type :=. - -Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf { -sameState: forall mdl i j, - DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) = - DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j)); -sameMState: forall mdl i j, - mState _ _ (Tl1l2 _ _ tr (pComponents l1 mdl i)) = - mState _ _ (Tl1l2 _ _ tr (pComponents l1 mdl j)); -sameM12: forall mdl i j, - Tl1l2 _ _ tr (pComponents l1 mdl i) = - match sym_eq (sameState mdl i j) in _=y return mapping _ y with - eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with - eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with - eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j) - end - end - end; -sameM21: forall mdl i j, - Tl2l1 l1 l2 tr (pComponents l1 mdl i) = - match - sym_eq (sameState mdl i j) in (_ = y) - return (mapping y (DynamicState l1 (pComponents l1 mdl i))) - with eq_refl => - match - sym_eq (pIsShared l1 mdl i) in (_ = y) - return - (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y) - with - | eq_refl => - match - pIsShared l1 mdl j in (_ = y) - return - (mapping - (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y) - with - | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl j) - end - end -end -}. - -Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl := - mkPSyntax l2 (pIndex l1 mdl) - (pIsEmpty l1 mdl) - (match pIsEmpty l1 mdl return Type with - inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) - |inright h => pState l1 mdl - end) - (fun i => Tmodel l1 l2 tr (pComponents l1 mdl i)) - (fun i => match pIsEmpty l1 mdl as y return - (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) = - match y with - | inleft i0 => - DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i0)) - | inright _ => pState l1 mdl - end) - with - inleft j => sameState l1 l2 tr h mdl i j - | inright h => match h i with end - end). - -Definition compSemantic l mdl i := - match pIsShared l mdl i in (_=y) return TTS y with - eq_refl => Semantic l (pComponents l mdl i) - end. - -Definition compSemanticEq l mdl i s (e: DynamicState l (pComponents l mdl i) = s) := - match e in (_=y) return TTS y with - eq_refl => Semantic l (pComponents l mdl i) - end. - -Definition Pmap12 l1 l2 tr (h: isSharedTransfo l1 l2 tr) (mdl : PSyntax l1) := -match - pIsEmpty l1 mdl as s - return - (mapping (pState l1 mdl) - match s with - | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) - | inright _ => pState l1 mdl - end) -with -| inleft p => - match - pIsShared l1 mdl p in (_ = y) - return - (mapping y (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p)))) - with - | eq_refl => Tl1l2 l1 l2 tr (pComponents l1 mdl p) - end -| inright _ => - mkMapping (pState l1 mdl) (pState l1 mdl) Unit - (fun _ : pState l1 mdl => unit) - (fun (_ : Unit) (_ : pState l1 mdl) => unit) - (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit) - (fun (_ : Unit) (X : pState l1 mdl) => X) -end. - -Definition Pmap21 l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl := -match - pIsEmpty l1 mdl as s - return - (mapping - match s with - | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) - | inright _ => pState l1 mdl - end (pState l1 mdl)) -with -| inleft p => - match - pIsShared l1 mdl p in (_ = y) - return - (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) y) - with - | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl p) - end -| inright _ => - mkMapping (pState l1 mdl) (pState l1 mdl) Unit - (fun _ : pState l1 mdl => unit) - (fun (_ : Unit) (_ : pState l1 mdl) => unit) - (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit) - (fun (_ : Unit) (X : pState l1 mdl) => X) -end. - -Definition PTpred l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl (pp : pPredicate l1 mdl): - LP (MdlPredicate (PLanguage l2) (PTransfoSyntax l1 l2 tr h mdl)) := -match pIsEmpty l1 mdl with -| inleft _ => - let (x, p) := pp in - addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x - (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x)) - (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p)) -| inright f => match f (projS1 pp) with end -end. - -Lemma simu_eqA: - forall A1 A2 C m P sa sc tta ttc (h: A2=A1), - simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) - P (match h in (_=y) return TTS y with eq_refl => sa end) - sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end) - ttc -> - simu A2 C m P sa sc tta ttc. -admit. -Qed. - -Lemma simu_eqC: - forall A C1 C2 m P sa sc tta ttc (h: C2=C1), - simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) - P sa (match h in (_=y) return TTS y with eq_refl => sc end) - tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end) - -> - simu A C2 m P sa sc tta ttc. -admit. -Qed. - -Lemma simu_eqA1: - forall A1 A2 C m P sa sc tta ttc (h: A1=A2), - simu A1 C m - P - (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc - (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc - -> - simu A2 C (match h in (_=y) return mapping _ C with eq_refl => m end) P sa sc tta ttc. -admit. -Qed. - -Lemma simu_eqA2: - forall A1 A2 C m P sa sc tta ttc (h: A1=A2), - simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end) - P - sa sc tta ttc - -> - simu A2 C m P - (match h in (_=y) return TTS y with eq_refl => sa end) sc - (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end) - ttc. -admit. -Qed. - -Lemma simu_eqC2: - forall A C1 C2 m P sa sc tta ttc (h: C1=C2), - simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end) - P - sa sc tta ttc - -> - simu A C2 m P - sa (match h in (_=y) return TTS y with eq_refl => sc end) - tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end). -admit. -Qed. - -Lemma simu_eqM: - forall A C m1 m2 P sa sc tta ttc (h: m1=m2), - simu A C m1 P sa sc tta ttc - -> - simu A C m2 P sa sc tta ttc. -admit. -Qed. - -Lemma LPTransfo_trans: - forall Pred1 Pred2 Pred3 (tr1: Pred1 -> LP Pred2) (tr2: Pred2 -> LP Pred3) f, - LPTransfo tr2 (LPTransfo tr1 f) = LPTransfo (fun x => LPTransfo tr2 (tr1 x)) f. -Proof. - admit. -Qed. - -Lemma LPTransfo_addIndex: - forall Ind Pred tr1 x (tr2: forall i, Pred i -> LP (tr1 i)) (p: LP (Pred x)), - addIndex Ind tr1 x (LPTransfo (tr2 x) p) = - LPTransfo - (fun p0 : {i : Ind & Pred i} => - addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))) - (addIndex Ind Pred x p). -Proof. - unfold addIndex; intros. - rewrite LPTransfo_trans. - rewrite LPTransfo_trans. - simpl. - auto. -Qed. - -Record tr_compat I0 I1 tr := compatPrf { - and_compat: forall p1 p2, tr (LPAnd I0 p1 p2) = LPAnd I1 (tr p1) (tr p2); - not_compat: forall p, tr (LPNot I0 p) = LPNot I1 (tr p) -}. - -Lemma LPTransfo_addIndex_tr: - forall Ind Pred tr0 tr1 x (tr2: forall i, Pred i -> LP (tr0 i)) (tr3: forall i, LP (tr0 i) -> LP (tr1 i)) (p: LP (Pred x)), - (forall x, tr_compat (tr0 x) (tr1 x) (tr3 x)) -> - addIndex Ind tr1 x (tr3 x (LPTransfo (tr2 x) p)) = - LPTransfo - (fun p0 : {i : Ind & Pred i} => - addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))) - (addIndex Ind Pred x p). -Proof. - unfold addIndex; simpl; intros. - rewrite LPTransfo_trans; simpl. - rewrite <- LPTransfo_trans. - f_equal. - induction p; simpl; intros; auto. - rewrite (and_compat _ _ _ (H x)). - rewrite <- IHp1, <- IHp2; auto. - rewrite <- IHp. - rewrite (not_compat _ _ _ (H x)); auto. -Qed. - -Require Export Coq.Logic.FunctionalExtensionality. -Print PLanguage. -Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): -Transformation (PLanguage l1) (PLanguage l2) := - mkTransformation (PLanguage l1) (PLanguage l2) - (PTransfoSyntax l1 l2 tr h) - (Pmap12 l1 l2 tr h) - (Pmap21 l1 l2 tr h) - (PTpred l1 l2 tr h) - (fun mdl => simu_equivProd - (pState l1 mdl) - (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) - (Pmap12 l1 l2 tr h mdl) - (Pmap21 l1 l2 tr h mdl) - (pIndex l1 mdl) - (fun i => MdlPredicate l1 (pComponents l1 mdl i)) - (compSemantic l1 mdl) - (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl)) - _ - _ - _ - ). - -Next Obligation. - unfold compSemantic, PTransfoSyntax; simpl. - case (pIsEmpty l1 mdl); simpl; intros. - unfold pPredicate; simpl. - unfold pPredicate in X; simpl in X. - case (sameState l1 l2 tr h mdl i p). - apply (LPTransfo (MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))). - apply (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl i))). - apply (LPPred _ X). - - apply False_rect; apply (f i). -Defined. - -Next Obligation. - split; intros. - unfold Pmap12; simpl. - unfold PTransfo_obligation_1; simpl. - unfold compSemantic; simpl. - unfold eq_ind, eq_rect, f_equal; simpl. - case (pIsEmpty l1 mdl); intros. - apply simu_eqA2. - apply simu_eqC2. - apply simu_eqM with (Tl1l2 l1 l2 tr (pComponents l1 mdl i)). - apply sameM12. - apply (simuLR _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro. - - apply False_rect; apply (f i). - - unfold Pmap21; simpl. - unfold PTransfo_obligation_1; simpl. - unfold compSemantic; simpl. - unfold eq_ind, eq_rect, f_equal; simpl. - case (pIsEmpty l1 mdl); intros. - apply simu_eqC2. - apply simu_eqA2. - apply simu_eqM with (Tl2l1 l1 l2 tr (pComponents l1 mdl i)). - apply sameM21. - apply (simuRL _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro. - - apply False_rect; apply (f i). -Qed. - -Next Obligation. - unfold trProd; simpl. - unfold PTransfo_obligation_1; simpl. - unfold compSemantic; simpl. - unfold eq_ind, eq_rect, f_equal; simpl. - apply functional_extensionality; intro. - case x; clear x; intros. - unfold PTpred; simpl. - case (pIsEmpty l1 mdl); simpl; intros. - set (tr0 i := - Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) - (Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))). - set (tr1 i := - Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) - match sameState l1 l2 tr h mdl i p in (_ = y) return (TTS y) with - | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) - end). - set (tr2 x := MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))). - set (Pred x := MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))). - set (tr3 x f := match - sameState l1 l2 tr h mdl x p as e in (_ = y) - return - (LP - (Predicate y - match e in (_ = y0) return (TTS y0) with - | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl x)) - end)) - with - | eq_refl => f - end). - apply (LPTransfo_addIndex_tr _ Pred tr0 tr1 x tr2 tr3 - (Tpred l1 l2 tr (pComponents l1 mdl x) m)). - unfold tr0, tr1, tr3; intros; split; simpl; intros; auto. - case (sameState l1 l2 tr h mdl x0 p); auto. - case (sameState l1 l2 tr h mdl x0 p); auto. - - apply False_rect; apply (f x). -Qed. - -End Product. diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v deleted file mode 100644 index c7926711..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2388.v +++ /dev/null @@ -1,10 +0,0 @@ -(* Error message was not printed in the correct environment *) - -Fail Parameters (A:Prop) (a:A A). - -(* This is a variant (reported as part of bug #2347) *) - -Require Import EquivDec. -Fail Program Instance bool_eq_eqdec : EqDec bool eq := - {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}. - diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v deleted file mode 100644 index fb4f9261..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2393.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Program. - -Inductive T := MkT. - -Definition sizeOf (t : T) : nat - := match t with - | MkT => 1 - end. -Variable vect : nat -> Type. -Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T - := match t with - | MkT => MkT - end. diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v deleted file mode 100644 index fe8eba54..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2404.v +++ /dev/null @@ -1,46 +0,0 @@ -(* Check that dependencies in the indices of the type of the terms to - match are taken into account and correctly generalized *) - -Require Import Relations.Relation_Definitions. -Require Import Basics. - -Record Base := mkBase - {(* Primitives *) - World : Set - (* Names are real, links are theoretical *) - ; Name : World -> Set - - ; wweak : World -> World -> Prop - - ; exportw : forall a b : World, (wweak a b) -> (Name b) -> option (Name a) -}. - -Section Derived. - Variable base : Base. - Definition bWorld := World base. - Definition bName := Name base. - Definition bexportw := exportw base. - Definition bwweak := wweak base. - - Implicit Arguments bexportw [a b]. - -Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type := - starReflS : forall a, RstarSetProof T a a -| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k. - -Implicit Arguments starTransS [I T i j k]. - -Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))). - -Definition bwweakFlip (b a : bWorld) : Prop := (bwweak a b). -Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak. - -Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) := - match aRWb,y with - | starReflS a, y' => Some y' - | starTransS i j k jWk jRWi, y' => - match (bexportw jWk y) with - | Some x => exportRweak jRWi x - | None => None - end - end. diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v deleted file mode 100644 index 56f046c4..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2456.v +++ /dev/null @@ -1,53 +0,0 @@ - -Require Import Equality. - -Parameter Patch : nat -> nat -> Set. - -Inductive Catch (from to : nat) : Type - := MkCatch : forall (p : Patch from to), - Catch from to. -Implicit Arguments MkCatch [from to]. - -Inductive CatchCommute5 - : forall {from mid1 mid2 to : nat}, - Catch from mid1 - -> Catch mid1 to - -> Catch from mid2 - -> Catch mid2 to - -> Prop - := MkCatchCommute5 : - forall {from mid1 mid2 to : nat} - (p : Patch from mid1) - (q : Patch mid1 to) - (q' : Patch from mid2) - (p' : Patch mid2 to), - CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p'). - -Inductive CatchCommute {from mid1 mid2 to : nat} - (p : Catch from mid1) - (q : Catch mid1 to) - (q' : Catch from mid2) - (p' : Catch mid2 to) - : Prop - := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'), - CatchCommute p q q' p'. -Notation "<< p , q >> <~> << q' , p' >>" - := (CatchCommute p q q' p') - (at level 60, no associativity). - -Lemma CatchCommuteUnique2 : - forall {from mid mid' to : nat} - {p : Catch from mid} {q : Catch mid to} - {q' : Catch from mid'} {p' : Catch mid' to} - {q'' : Catch from mid'} {p'' : Catch mid' to} - (commute1 : <<p, q>> <~> <<q', p'>>) - (commute2 : <<p, q>> <~> <<q'', p''>>), - (p' = p'') /\ (q' = q''). -Proof with auto. -intros. -set (X := commute2). -dependent destruction commute1; -dependent destruction catchCommuteDetails; -dependent destruction commute2; -dependent destruction catchCommuteDetails generalizing X. -Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2464.v b/test-suite/bugs/closed/shouldsucceed/2464.v deleted file mode 100644 index af708587..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2464.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import FSetWeakList. -Require Import FSetDecide. - -Parameter Name : Set. -Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}. - -Module DecidableName. -Definition t := Name. -Definition eq := @eq Name. -Definition eq_refl := @refl_equal Name. -Definition eq_sym := @sym_eq Name. -Definition eq_trans := @trans_eq Name. -Definition eq_dec := eq_Name_dec. -End DecidableName. - -Module NameSetMod := Make(DecidableName). - -Module NameSetDec := WDecide (NameSetMod). - -Class PartPatchUniverse (pu_type1 pu_type2 : Type) - : Type := mkPartPatchUniverse { -}. -Class PatchUniverse {pu_type : Type} - (ppu : PartPatchUniverse pu_type pu_type) - : Type := mkPatchUniverse { - pu_nameOf : pu_type -> Name -}. - -Lemma foo : forall (pu_type : Type) - (ppu : PartPatchUniverse pu_type pu_type) - (patchUniverse : PatchUniverse ppu) - (ns ns1 ns2 : NameSetMod.t) - (containsOK : NameSetMod.Equal ns1 ns2) - (p : pu_type) - (HX1 : NameSetMod.Equal ns1 (NameSetMod.add (pu_nameOf p) ns)), - NameSetMod.Equal ns2 (NameSetMod.add (pu_nameOf p) ns). -Proof. -NameSetDec.fsetdec. -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/shouldsucceed/2467.v deleted file mode 100644 index ad17814a..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2467.v +++ /dev/null @@ -1,49 +0,0 @@ -(* -In the code below, I would expect the - NameSetDec.fsetdec. -to solve the Lemma, but I need to do it in steps instead. - -This is a regression relative to FSet, - -I have v8.3 (13702). -*) - -Require Import Coq.MSets.MSets. - -Parameter Name : Set. -Parameter Name_compare : Name -> Name -> comparison. -Parameter Name_compare_sym : forall {x y : Name}, - Name_compare y x = CompOpp (Name_compare x y). -Parameter Name_compare_trans : forall {c : comparison} - {x y z : Name}, - Name_compare x y = c - -> Name_compare y z = c - -> Name_compare x z = c. -Parameter Name_eq_leibniz : forall {s s' : Name}, - Name_compare s s' = Eq - -> s = s'. - -Module NameOrderedTypeAlt. -Definition t := Name. -Definition compare := Name_compare. -Definition compare_sym := @Name_compare_sym. -Definition compare_trans := @Name_compare_trans. -End NameOrderedTypeAlt. - -Module NameOrderedType := OT_from_Alt(NameOrderedTypeAlt). - -Module NameOrderedTypeWithLeibniz. -Include NameOrderedType. -Definition eq_leibniz := @Name_eq_leibniz. -End NameOrderedTypeWithLeibniz. - -Module NameSetMod := MSetList.MakeWithLeibniz(NameOrderedTypeWithLeibniz). -Module NameSetDec := WDecide (NameSetMod). - -Lemma foo : forall (xs ys : NameSetMod.t) - (n : Name) - (H1 : NameSetMod.Equal xs (NameSetMod.add n ys)), - NameSetMod.In n xs. -Proof. -NameSetDec.fsetdec. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v deleted file mode 100644 index 4c302512..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2473.v +++ /dev/null @@ -1,39 +0,0 @@ - -Require Import Relations Program Setoid Morphisms. - -Section S1. - Variable R: nat -> relation bool. - Instance HR1: forall n, Transitive (R n). Admitted. - Instance HR2: forall n, Symmetric (R n). Admitted. - Hypothesis H: forall n a, R n (andb a a) a. - Goal forall n a b, R n b a. - intros. - (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *) - (* idem with setoid_rewrite *) -(* assert (HR2' := HR2 n). *) - rewrite <- H. (* ok *) - admit. - Qed. -End S1. - -Section S2. - Variable R: nat -> relation bool. - Instance HR: forall n, Equivalence (R n). Admitted. - Hypothesis H: forall n a, R n (andb a a) a. - Goal forall n a b, R n a b. - intros. rewrite <- H. admit. - Qed. -End S2. - -(* the parametrised relation is required to get the problem *) -Section S3. - Variable R: relation bool. - Instance HR1': Transitive R. Admitted. - Instance HR2': Symmetric R. Admitted. - Hypothesis H: forall a, R (andb a a) a. - Goal forall a b, R b a. - intros. - rewrite <- H. (* ok *) - admit. - Qed. -End S3.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v deleted file mode 100644 index 371bfdc5..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2603.v +++ /dev/null @@ -1,33 +0,0 @@ -(** Namespace of module vs. namescope of definitions/constructors/... - -As noticed by A. Appel in bug #2603, module names and definition -names used to be in the same namespace. But conflict with names -of constructors (or 2nd mutual inductive...) used to not be checked -enough, leading to stange situations. - -- In 8.3pl3 we introduced checks that forbid uniformly the following - situations. - -- For 8.4 we finally managed to make module names and other names - live in two separate namespace, hence allowing all of the following - situations. -*) - -Module Type T. -End T. - -Declare Module K : T. - -Module Type L. -Declare Module E : T. -End L. - -Module M1 : L with Module E:=K. -Module E := K. -Inductive t := E. (* Used to be accepted, but End M1 below was failing *) -End M1. - -Module M2 : L with Module E:=K. -Inductive t := E. -Module E := K. (* Used to be accepted *) -End M2. (* Used to be accepted *) diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v deleted file mode 100644 index a4c95ff9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2608.v +++ /dev/null @@ -1,34 +0,0 @@ - -Module Type T. - Parameter Inline t : Type. -End T. - -Module M. - Definition t := nat. -End M. - -Module Make (X:T). - Include X. - - (* here t is : (Top.Make.t,Top.X.t) *) - - (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t) - which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]} - which gives : EvalConstRef (Top.Make.t,Top.X.t) *) - -End Make. - -Module P := Make M. - - (* resolver returned by add_module : Top.P.t=>inline *) - (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *) - - (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t) - given to subst = {<X#1> |-> Top.M [, Top.M.t=>inline]} - which used to give : EvalConstRef (Top.Make.t,Top.M.t) - given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]} - which used to give : EvalConstRef (Top.P.t,Top.M.t) *) - -Definition u := P.t. - (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t) - and not of (Top.P.t,Top.P.t) *) diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v deleted file mode 100644 index 4f0470b1..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2613.v +++ /dev/null @@ -1,17 +0,0 @@ -(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *) - -Require Import ZArith. -Require Recdef. - -Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}. - -Locate eq_sym. (* Constant Coq.Init.Logic.eq_sym *) - -Function loop (n: nat) {measure (fun x => x) n} : bool := - if nat_eq_dec n 0 then false else loop (pred n). -Proof. - admit. -Defined. - -Check eq_sym eq_refl : 0=0. - diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v deleted file mode 100644 index 54e1a07c..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2615.v +++ /dev/null @@ -1,14 +0,0 @@ -(* This failed with an anomaly in pre-8.4 because of let-in not - properly taken into account in the test for unification pattern *) - -Inductive foo : forall A, A -> Prop := -| foo_intro : forall A x, foo A x. -Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x). -Fail induction 1. - -(* Whether these examples should succeed with a non-dependent return predicate - or fail because there is well-typed return predicate dependent in f - is questionable. As of 25 oct 2011, they succeed *) -refine (fun p => match p with _ => _ end). -Undo. -refine (fun p => match p with foo_intro _ _ => _ end). diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/shouldsucceed/2616.v deleted file mode 100644 index 8758e32d..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2616.v +++ /dev/null @@ -1,7 +0,0 @@ -(* Testing ill-typed rewrite which used to succeed in 8.3 *) -Goal - forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), - N 0 -> False. -Proof. -intros. -Fail rewrite IN in H. diff --git a/test-suite/bugs/closed/shouldsucceed/2629.v b/test-suite/bugs/closed/shouldsucceed/2629.v deleted file mode 100644 index 759cd3dd..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2629.v +++ /dev/null @@ -1,22 +0,0 @@ -Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}. - -Class sepalg (t: Type) {JOIN: Join t} : Type := - SepAlg { - join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z'; - join_assoc: forall {a b c d e}, join a b d -> join d c e -> - {f : t & join b c f /\ join a f e}; - join_com: forall {a b c}, join a b c -> join b a c; - join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2; - - unit_for : t -> t -> Prop := fun e a => join e a a; - join_ex_units: forall a, {e : t & unit_for e a} -}. - -Definition joins {A} `{Join A} (a b : A) : Prop := - exists c, join a b c. - -Lemma join_joins {A} `{sepalg A}: forall {a b c}, - join a b c -> joins a b. -Proof. - firstorder. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v deleted file mode 100644 index da0cc68a..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2640.v +++ /dev/null @@ -1,17 +0,0 @@ -(* Testing consistency of globalization and interpretation in some - extreme cases *) - -Section sect. - - (* Simplification of the initial example *) - Hypothesis Other: True. - - Lemma C2 : True. - proof. - Fail have True using Other. - Abort. - - (* Variant of the same problem *) - Lemma C2 : True. - Fail clear; Other. - Abort. diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v deleted file mode 100644 index 74c8fa34..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2668.v +++ /dev/null @@ -1,6 +0,0 @@ -Require Import MSetPositive. -Require Import MSetProperties. - -Module Pos := MSetPositive.PositiveSet. -Module PPPP := MSetProperties.WPropertiesOn(Pos). -Print Module PPPP.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/shouldsucceed/2732.v deleted file mode 100644 index f22a8ccc..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2732.v +++ /dev/null @@ -1,19 +0,0 @@ -(* Check correct behavior of add_primitive_tactic in TACEXTEND *) - -(* Added also the case of eauto and congruence *) - -Ltac thus H := solve [H]. - -Lemma test: forall n : nat, n <= n. -Proof. - intro. - thus firstorder. - Undo. - thus eauto. -Qed. - -Lemma test2: false = true -> False. -Proof. - intro. - thus congruence. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v deleted file mode 100644 index fd7bd3bd..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2733.v +++ /dev/null @@ -1,26 +0,0 @@ -Definition goodid : forall {A} (x: A), A := fun A x => x. -Definition wrongid : forall A (x: A), A := fun {A} x => x. - -Inductive ty := N | B. - -Inductive alt_list : ty -> ty -> Type := - | nil {k} : alt_list k k - | Ncons {k} : nat -> alt_list B k -> alt_list N k - | Bcons {k} : bool -> alt_list N k -> alt_list B k. - -Definition trullynul k {k'} (l : alt_list k k') := -match k,l with - |N,l' => Ncons 0 (Bcons true l') - |B,l' => Bcons true (Ncons 0 l') -end. - -Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 -> -alt_list t1 t3 := - match l with - | nil _ => fun _ l2 => P l2 - | Ncons _ n l1 => fun _ l2 => Ncons n (app (@P) l1 l2) - | Bcons _ b l1 => fun _ l2 => Bcons b (app (@P) l1 l2) - end. - -Check (fun {t t'} (l: alt_list t t') => - app trullynul (goodid l) (wrongid _ nil)). diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/shouldsucceed/2734.v deleted file mode 100644 index 826361be..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2734.v +++ /dev/null @@ -1,15 +0,0 @@ -Require Import Arith List. -Require Import OrderedTypeEx. - -Module Adr. - Include Nat_as_OT. - Definition nat2t (i: nat) : t := i. -End Adr. - -Inductive expr := Const: Adr.t -> expr. - -Inductive control := Go: expr -> control. - -Definition program := (Adr.t * (control))%type. - -Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ).
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/shouldsucceed/2750.v deleted file mode 100644 index fc580f10..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2750.v +++ /dev/null @@ -1,23 +0,0 @@ - -Module Type ModWithRecord. - - Record foo : Type := - { A : nat - ; B : nat - }. -End ModWithRecord. - -Module Test_ModWithRecord (M : ModWithRecord). - - Definition test1 : M.foo := - {| M.A := 0 - ; M.B := 2 - |}. - - Module B := M. - - Definition test2 : M.foo := - {| M.A := 0 - ; M.B := 2 - |}. -End Test_ModWithRecord.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v deleted file mode 100644 index 08dff992..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2817.v +++ /dev/null @@ -1,9 +0,0 @@ -(** Occur-check for Meta (up to application of already known instances) *) - -Goal forall (f: nat -> nat -> Prop) (x:bool) - (H: forall (u: nat), f u u -> True) - (H0: forall x0, f (if x then x0 else x0) x0), -False. - -intros. -Fail apply H in H0. (* should fail without exhausting the stack *) diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v deleted file mode 100644 index a948b75e..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2836.v +++ /dev/null @@ -1,39 +0,0 @@ -(* Check that possible instantiation made during evar materialization - are taken into account and do not raise Not_found *) - -Set Implicit Arguments. - -Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := { - Object :> _ := obj; - - Identity' : forall o, Morphism o o; - Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' -}. - -Section SpecializedCategoryInterface. - Variable obj : Type. - Variable mor : obj -> obj -> Type. - Variable C : @SpecializedCategory obj mor. - - Definition Morphism (s d : C) := mor s d. - Definition Identity (o : C) : Morphism o o := C.(Identity') o. - Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) : -Morphism s d' := C.(Compose') s d d' m m0. -End SpecializedCategoryInterface. - -Section ProductCategory. - Variable objC : Type. - Variable morC : objC -> objC -> Type. - Variable objD : Type. - Variable morD : objD -> objD -> Type. - Variable C : SpecializedCategory morC. - Variable D : SpecializedCategory morD. - -(* Should fail nicely *) -Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d -=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type). -Fail refine {| - Identity' := (fun o => (Identity (fst o), Identity (snd o))); - Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd -m2) (snd m1))) - |}. diff --git a/test-suite/bugs/closed/shouldsucceed/2837.v b/test-suite/bugs/closed/shouldsucceed/2837.v deleted file mode 100644 index 5d984463..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2837.v +++ /dev/null @@ -1,15 +0,0 @@ -Require Import JMeq. - -Axiom test : forall n m : nat, JMeq n m. - -Goal forall n m : nat, JMeq n m. - -(* I) with no intros nor variable hints, this should produce a regular error - instead of Uncaught exception Failure("nth"). *) -Fail rewrite test. - -(* II) with intros but indication of variables, still an error *) -Fail (intros; rewrite test). - -(* III) a working variant: *) -intros; rewrite (test n m).
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v deleted file mode 100644 index 21e92ae2..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2928.v +++ /dev/null @@ -1,11 +0,0 @@ -Class Equiv A := equiv: A -> A -> Prop. -Infix "=" := equiv : type_scope. - -Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z. - -Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }. - -Class SemiLattice A op `{Equiv A} := - { semilattice_sg :>> SemiGroup A op - ; redundant : Associative op - }. diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v deleted file mode 100644 index 15598352..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2983.v +++ /dev/null @@ -1,8 +0,0 @@ -Module Type ModA. -End ModA. -Module Type ModB(A : ModA). -End ModB. -Module Foo(A : ModA)(B : ModB A). -End Foo. - -Print Module Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v deleted file mode 100644 index ba3acd08..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2995.v +++ /dev/null @@ -1,9 +0,0 @@ -Module Type Interface. - Parameter error: nat. -End Interface. - -Module Implementation <: Interface. - Definition t := bool. - Definition error: t := false. -Fail End Implementation. -(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v deleted file mode 100644 index 27de34ed..00000000 --- a/test-suite/bugs/closed/shouldsucceed/3000.v +++ /dev/null @@ -1,2 +0,0 @@ -Inductive t (t':Type) : Type := A | B. -Definition d := match t with _ => 1 end. (* used to fail on list_chop *) diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/shouldsucceed/3004.v deleted file mode 100644 index 896b1958..00000000 --- a/test-suite/bugs/closed/shouldsucceed/3004.v +++ /dev/null @@ -1,7 +0,0 @@ -Set Implicit Arguments. -Unset Strict Implicit. -Parameter (M : nat -> Type). -Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2). - -Definition foo (s : list {n : nat & M n}) := - let exT := existT in mp (fun x => projT1 x) s. diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v deleted file mode 100644 index 3f3a979a..00000000 --- a/test-suite/bugs/closed/shouldsucceed/3008.v +++ /dev/null @@ -1,29 +0,0 @@ -Module Type Intf1. -Parameter T : Type. -Inductive a := A. -End Intf1. - -Module Impl1 <: Intf1. -Definition T := unit. -Inductive a := A. -End Impl1. - -Module Type Intf2 - (Impl1 : Intf1). -Parameter x : Impl1.A=Impl1.A -> Impl1.T. -End Intf2. - -Module Type Intf3 - (Impl1 : Intf1) - (Impl2 : Intf2(Impl1)). -End Intf3. - -Fail Module Toto - (Impl1' : Intf1) - (Impl2 : Intf2(Impl1')) - (Impl3 : Intf3(Impl1)(Impl2)). -(* A UserError is expected here, not an uncaught Not_found *) - -(* NB : the Inductive above and the A=A weren't in the initial test, - they are here only to force an access to the environment - (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/335.v b/test-suite/bugs/closed/shouldsucceed/335.v deleted file mode 100644 index 166fa7a9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/335.v +++ /dev/null @@ -1,5 +0,0 @@ -(* Compatibility of Require with backtracking at interactive module end *) - -Module A. -Require List. -End A. diff --git a/test-suite/bugs/closed/shouldsucceed/348.v b/test-suite/bugs/closed/shouldsucceed/348.v deleted file mode 100644 index 28cc5cb1..00000000 --- a/test-suite/bugs/closed/shouldsucceed/348.v +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index 4fc8d7c9..00000000 --- a/test-suite/bugs/closed/shouldsucceed/38.v +++ /dev/null @@ -1,22 +0,0 @@ -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 deleted file mode 100644 index 926af7dd..00000000 --- a/test-suite/bugs/closed/shouldsucceed/545.v +++ /dev/null @@ -1,5 +0,0 @@ -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/808_2411.v b/test-suite/bugs/closed/shouldsucceed/808_2411.v deleted file mode 100644 index 1c13e745..00000000 --- a/test-suite/bugs/closed/shouldsucceed/808_2411.v +++ /dev/null @@ -1,27 +0,0 @@ -Section test. -Variable n:nat. -Lemma foo: 0 <= n. -Proof. -(* declaring an Axiom during a proof makes it immediatly - usable, juste as a full Definition. *) -Axiom bar : n = 1. -rewrite bar. -now apply le_S. -Qed. - -Lemma foo' : 0 <= n. -Proof. -(* Declaring an Hypothesis during a proof is ok, - but this hypothesis won't be usable by the current proof(s), - only by later ones. *) -Hypothesis bar' : n = 1. -Fail rewrite bar'. -Abort. - -Lemma foo'' : 0 <= n. -Proof. -rewrite bar'. -now apply le_S. -Qed. - -End test.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v deleted file mode 100644 index ee5ec1fa..00000000 --- a/test-suite/bugs/closed/shouldsucceed/846.v +++ /dev/null @@ -1,213 +0,0 @@ -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 deleted file mode 100644 index 21f15e72..00000000 --- a/test-suite/bugs/closed/shouldsucceed/931.v +++ /dev/null @@ -1,7 +0,0 @@ -Parameter P : forall n : nat, n=n -> Prop. - -Goal Prop. - refine (P _ _). - instantiate (1:=0). - trivial. -Qed. |