diff options
Diffstat (limited to 'test-suite/success')
76 files changed, 2360 insertions, 370 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index 97cf316c..d819dc47 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -47,6 +47,24 @@ Goal forall a1 a2, eqA (plusA a1 zeroA) a2. change (eqB (plusB (phi a1) zeroB) (phi a2)). Admitted. +Variable foo : A -> Type. + +Definition local0 := fun (a1 : A) (a2 : A) (a3 : A) => + (eq_refl : plusA a1 (plusA zeroA a2) = ia _). +Definition local1 := + fun (a1 : A) (a2 : A) (f : A -> A) => + (eq_refl : plusA a1 (plusA zeroA (f a2)) = ia _). + +Definition local2 := + fun (a1 : A) (f : A -> A) => + (eq_refl : (f a1) = ia _). + +Goal forall a1 a2, eqA (plusA a1 zeroA) a2. + intros a1 a2. + refine (eq_img _ _ _). +change (eqB (plusB (phi a1) zeroB) (phi a2)). +Admitted. + End group_morphism. Open Scope type_scope. @@ -129,13 +147,3 @@ Admitted. Check L : abs _ . End type_reification. - - - - - - - - - - diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v index fd5d139c..445ffac8 100644 --- a/test-suite/success/Case11.v +++ b/test-suite/success/Case11.v @@ -1,5 +1,5 @@ -(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *) -(* Problème rapporté par Solange Coupet *) +(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *) +(* Problème rapporté par Solange Coupet *) Section A. @@ -7,7 +7,7 @@ Variables (Alpha : Set) (Beta : Set). Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) : Alpha * Beta := match c with - | existS a b => (a, b) + | existS _ a b => (a, b) end. End A. diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v index 729ab824..55e17fac 100644 --- a/test-suite/success/Case12.v +++ b/test-suite/success/Case12.v @@ -68,6 +68,6 @@ Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set := Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) {struct l} : nat := match l with - | nil''' => 0 - | cons''' _ m l0 => S (length''' A a m l0) + | nil''' _ _ => 0 + | @cons''' _ _ _ _ m l0 => S (length''' A a m l0) end. diff --git a/test-suite/success/Case16.v b/test-suite/success/Case16.v index 77016bbf..ce9a0ecb 100644 --- a/test-suite/success/Case16.v +++ b/test-suite/success/Case16.v @@ -5,6 +5,6 @@ Check (fun x : {b : bool | if b then True else False} => match x return (let (b, _) := x in if b then True else False) with - | exist true y => y - | exist false z => z + | exist _ true y => y + | exist _ false z => z end). diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v index 66af9e0d..861d0466 100644 --- a/test-suite/success/Case17.v +++ b/test-suite/success/Case17.v @@ -19,10 +19,10 @@ Axiom HHH : forall A : Prop, A. Check (match rec l0 (HHH _) with - | inleft (existS (false :: l1) _) => inright _ (HHH _) - | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) => + | inleft (existS _ (false :: l1) _) => inright _ (HHH _) + | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) => inright _ (HHH _) - | inleft (existS _ _) => inright _ (HHH _) + | inleft (existS _ _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end :{l'' : list bool & @@ -39,10 +39,10 @@ Check {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) => match rec l0 (HHH _) with - | inleft (existS (false :: l1) _) => inright _ (HHH _) - | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) => + | inleft (existS _ (false :: l1) _) => inright _ (HHH _) + | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) => inright _ (HHH _) - | inleft (existS _ _) => inright _ (HHH _) + | inleft (existS _ _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end :{l'' : list bool & diff --git a/test-suite/success/Case20.v b/test-suite/success/Case20.v new file mode 100644 index 00000000..67eebf72 --- /dev/null +++ b/test-suite/success/Case20.v @@ -0,0 +1,35 @@ +(* Example taken from RelationAlgebra *) +(* Was failing from r16205 up to now *) + +Require Import BinNums. + +Section A. + +Context (A:Type) {X: A} (tst:A->Type) (top:forall X, X). + +Inductive v: (positive -> A) -> Type := +| v_L: forall f', v f' +| v_N: forall f', + v (fun n => f' (xO n)) -> + (positive -> tst (f' xH)) -> + v (fun n => f' (xI n)) -> v f'. + +Fixpoint v_add f' (t: v f') n: (positive -> tst (f' n)) -> v f' := + match t in (v o) return ((positive -> (tst (o n))) -> v o) with + | v_L f' => + match n return ((positive -> (tst (f' n))) -> v f') with + | xH => fun x => v_N _ (v_L _) x (v_L _) + | xO n => fun x => v_N _ + (v_add (fun n => f' (xO n)) (v_L _) n x) (fun _ => top _) (v_L _) + | xI n => fun x => v_N _ + (v_L _) (fun _ => top _) (v_add (fun n => f' (xI n)) (v_L _) n x) + end + | v_N f' l y r => + match n with + | xH => fun x => v_N _ l x r + | xO n => fun x => v_N _ (v_add (fun n => f' (xO n)) l n x) y r + | xI n => fun x => v_N _ l y (v_add (fun n => f' (xI n)) r n x) + end + end. + +End A. diff --git a/test-suite/success/Case21.v b/test-suite/success/Case21.v new file mode 100644 index 00000000..db91eb40 --- /dev/null +++ b/test-suite/success/Case21.v @@ -0,0 +1,15 @@ +(* Check insertion of impossible case when there is no branch at all *) + +Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. + +Check fun H:eq_true false => match H with end : False. + +Inductive I : bool -> bool -> Prop := C : I true true. + +Check fun x (H:I x false) => match H with end : False. + +Check fun x (H:I false x) => match H with end : False. + +Inductive I' : bool -> Type := C1 : I' true | C2 : I' true. + +Check fun x : I' false => match x with end : False. diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v new file mode 100644 index 00000000..4eb2dbe9 --- /dev/null +++ b/test-suite/success/Case22.v @@ -0,0 +1,7 @@ +(* Check typing in the presence of let-in in inductive arity *) + +Inductive I : let a := 1 in a=a -> let b := 2 in Type := C : I (eq_refl). +Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl end = eq_refl. +intro. +match goal with |- ?c => let x := eval cbv in c in change x end. +Abort. diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v index 6e4b2003..f95598aa 100644 --- a/test-suite/success/Case7.v +++ b/test-suite/success/Case7.v @@ -12,6 +12,6 @@ Parameter Type (fun (A : Set) (l : List A) => match l return (Empty A l \/ ~ Empty A l) with - | Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A) - | Cons a y as b => or_intror (Empty A b) (inv_Empty A a y) + | Nil _ => or_introl (~ Empty A (Nil A)) (intro_Empty A) + | Cons _ a y as b => or_intror (Empty A b) (inv_Empty A a y) end). diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v index a8534a0b..e34e5b9b 100644 --- a/test-suite/success/Case9.v +++ b/test-suite/success/Case9.v @@ -36,10 +36,10 @@ Parameter Fixpoint eqlongdec (x y : List nat) {struct x} : eqlong x y \/ ~ eqlong x y := match x, y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil - | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) - | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) - | Cons a x as L1, Cons b y as L2 => + | Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons _ a x as L1, Cons _ b y as L2 => match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) @@ -49,10 +49,10 @@ Fixpoint eqlongdec (x y : List nat) {struct x} : Type match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil - | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) - | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) - | Cons a x as L1, Cons b y as L2 => + | Nil _, Nil _ => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil _, Cons _ a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons _ a x as L, Nil _ => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons _ a x as L1, Cons _ b y as L2 => match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v new file mode 100644 index 00000000..3679eead --- /dev/null +++ b/test-suite/success/CaseInClause.v @@ -0,0 +1,22 @@ +(* in clause pattern *) +Require Vector. +Check (fun n (x: Vector.t True (S n)) => + match x in Vector.t _ (S m) return True with + |Vector.cons _ h _ _ => h + end). + +(* Notation *) +Import Vector.VectorNotations. +Notation "A \dots n" := (Vector.t A n) (at level 200). +Check (fun m (x: Vector.t nat m) => + match x in _ \dots k return Vector.t nat (S k) with + | Vector.nil _ => 0 :: [] + | Vector.cons _ h _ t => h :: h :: t + end). + +(* N should be a variable and not the inductiveRef *) +Require Import NArith. +Theorem foo : forall (n m : nat) (pf : n = m), + match pf in _ = N with + | eq_refl => unit + end. diff --git a/test-suite/success/Cases-bug1834.v b/test-suite/success/Cases-bug1834.v index 543ca0c9..cf102486 100644 --- a/test-suite/success/Cases-bug1834.v +++ b/test-suite/success/Cases-bug1834.v @@ -7,7 +7,7 @@ Definition T := sig P. Parameter Q : T -> Prop. Definition U := sig Q. Parameter a : U. -Check (match a with exist (exist tt e2) e3 => e3=e3 end). +Check (match a with exist _ (exist _ tt e2) e3 => e3=e3 end). (* There is still a form submitted by Pierre Corbineau (#1834) which fails *) diff --git a/test-suite/success/Cases-bug3758.v b/test-suite/success/Cases-bug3758.v new file mode 100644 index 00000000..e48f4523 --- /dev/null +++ b/test-suite/success/Cases-bug3758.v @@ -0,0 +1,17 @@ +(* There used to be an evar leak in the to_nat example *) + +Require Import Coq.Lists.List. +Import ListNotations. + +Fixpoint Idx {A:Type} (l:list A) : Type := + match l with + | [] => False + | _::l => True + Idx l + end. + +Fixpoint to_nat {A:Type} (l:list A) (i:Idx l) : nat := + match l,i with + | [] , i => match i with end + | _::_, inl _ => 0 + | _::l, inr i => S (to_nat l i) + end. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index c9a3c08e..e4266350 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -2,21 +2,21 @@ (* Pattern-matching when non inductive terms occur *) (* Dependent form of annotation *) -Type match 0 as n, eq return nat with +Type match 0 as n, @eq return nat with | O, x => 0 | S x, y => x end. -Type match 0, eq, 0 return nat with +Type match 0, 0, @eq return nat with | O, x, y => 0 | S x, y, z => x end. -Type match 0, eq, 0 return _ with +Type match 0, @eq, 0 return _ with | O, x, y => 0 | S x, y, z => x end. (* Non dependent form of annotation *) -Type match 0, eq return nat with +Type match 0, @eq return nat with | O, x => 0 | S x, y => x end. @@ -309,43 +309,43 @@ Type Type (fun l : List nat => match l return (List nat) with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end). Type (fun l : List nat => match l with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end). Type match Nil nat return nat with - | Nil => 0 - | Cons a l => S a + | Nil _ => 0 + | Cons _ a l => S a end. Type match Nil nat with - | Nil => 0 - | Cons a l => S a + | Nil _ => 0 + | Cons _ a l => S a end. Type match Nil nat return (List nat) with - | Cons a l => l + | Cons _ a l => l | x => x end. Type match Nil nat with - | Cons a l => l + | Cons _ a l => l | x => x end. Type match Nil nat return (List nat) with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end. Type match Nil nat with - | Nil => Nil nat - | Cons a l => l + | Nil _ => Nil nat + | Cons _ a l => l end. @@ -353,8 +353,8 @@ Type match 0 return nat with | O => 0 | S x => match Nil nat return nat with - | Nil => x - | Cons a l => x + a + | Nil _ => x + | Cons _ a l => x + a end end. @@ -362,8 +362,8 @@ Type match 0 with | O => 0 | S x => match Nil nat with - | Nil => x - | Cons a l => x + a + | Nil _ => x + | Cons _ a l => x + a end end. @@ -372,8 +372,8 @@ Type match y with | O => 0 | S x => match Nil nat with - | Nil => x - | Cons a l => x + a + | Nil _ => x + | Cons _ a l => x + a end end). @@ -381,8 +381,8 @@ Type Type match 0, Nil nat return nat with | O, x => 0 - | S x, Nil => x - | S x, Cons a l => x + a + | S x, Nil _ => x + | S x, Cons _ a l => x + a end. @@ -597,71 +597,60 @@ Type Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return nat with - | Niln => 0 - | Consn n a Niln => 0 - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _) => 0 + | Consn _ n a (Consn _ m b l) => n + m end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln => 0 - | Consn n a Niln => 0 - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _) => 0 + | Consn _ n a (Consn _ m b l) => n + m end). -(* This example was deactivated in Cristina's code - Type (fun (A:Set) (n:nat) (l:Listn A n) => match l return Listn A O with - | Niln as b => b - | Consn n a (Niln as b) => (Niln A) - | Consn n a (Consn m b l) => (Niln A) + | Niln _ as b => b + | Consn _ n a (Niln _ as b) => (Niln A) + | Consn _ n a (Consn _ m b l) => (Niln A) end). -*) - -(* This one is (still) failing: too weak unification +(* Type (fun (A:Set) (n:nat) (l:Listn A n) => match l with - | Niln as b => b - | Consn n a (Niln as b) => (Niln A) - | Consn n a (Consn m b l) => (Niln A) + | Niln _ as b => b + | Consn _ n a (Niln _ as b) => (Niln A) + | Consn _ n a (Consn _ m b l) => (Niln A) end). *) -(* This one is failing: alias L not chosen of the right type - Type (fun (A:Set) (n:nat) (l:Listn A n) => match l return Listn A (S 0) with - | Niln as b => Consn A O O b - | Consn n a Niln as L => L - | Consn n a _ => Consn A O O (Niln A) + | Niln _ as b => Consn A O O b + | Consn _ n a (Niln _) as L => L + | Consn _ n a _ => Consn A O O (Niln A) end). -*) - -(******** This example (still) failed Type (fun (A:Set) (n:nat) (l:Listn A n) => match l return Listn A (S 0) with - | Niln as b => Consn A O O b - | Consn n a Niln as L => L - | Consn n a _ => Consn A O O (Niln A) + | Niln _ as b => Consn A O O b + | Consn _ n a (Niln _) as L => L + | Consn _ n a _ => Consn A O O (Niln A) end). -**********) - (* To test treatment of as-patterns in depth *) Type (fun (A : Set) (l : List A) => match l with - | Nil as b => Nil A - | Cons a Nil as L => L - | Cons a (Cons b m) as L => L + | Nil _ as b => Nil A + | Cons _ a (Nil _) as L => L + | Cons _ a (Cons _ b m) as L => L end). @@ -704,40 +693,40 @@ Type Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln as b => l + | Niln _ as b => l | _ => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return (Listn A n) with - | Niln => l - | Consn n a Niln => l - | Consn n a (Consn m b c) => l + | Niln _ => l + | Consn _ n a (Niln _) => l + | Consn _ n a (Consn _ m b c) => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln => l - | Consn n a Niln => l - | Consn n a (Consn m b c) => l + | Niln _ => l + | Consn _ n a (Niln _) => l + | Consn _ n a (Consn _ m b c) => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return (Listn A n) with - | Niln as b => l - | Consn n a (Niln as b) => l - | Consn n a (Consn m b _) => l + | Niln _ as b => l + | Consn _ n a (Niln _ as b) => l + | Consn _ n a (Consn _ m b _) => l end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln as b => l - | Consn n a (Niln as b) => l - | Consn n a (Consn m b _) => l + | Niln _ as b => l + | Consn _ n a (Niln _ as b) => l + | Consn _ n a (Consn _ m b _) => l end). @@ -770,40 +759,40 @@ Type match LeO 0 with Type (fun (n : nat) (l : Listn nat n) => match l return nat with - | Niln => 0 - | Consn n a l => 0 + | Niln _ => 0 + | Consn _ n a l => 0 end). Type (fun (n : nat) (l : Listn nat n) => match l with - | Niln => 0 - | Consn n a l => 0 + | Niln _ => 0 + | Consn _ n a l => 0 end). Type match Niln nat with - | Niln => 0 - | Consn n a l => 0 + | Niln _ => 0 + | Consn _ n a l => 0 end. Type match LE_n 0 return nat with - | LE_n => 0 - | LE_S m h => 0 + | LE_n _ => 0 + | LE_S _ m h => 0 end. Type match LE_n 0 with - | LE_n => 0 - | LE_S m h => 0 + | LE_n _ => 0 + | LE_S _ m h => 0 end. Type match LE_n 0 with - | LE_n => 0 - | LE_S m h => 0 + | LE_n _ => 0 + | LE_S _ m h => 0 end. @@ -825,16 +814,17 @@ Type Type match Niln nat return nat with - | Niln => 0 - | Consn n a Niln => n - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _ +) => n + | Consn _ n a (Consn _ m b l) => n + m end. Type match Niln nat with - | Niln => 0 - | Consn n a Niln => n - | Consn n a (Consn m b l) => n + m + | Niln _ => 0 + | Consn _ n a (Niln _) => n + | Consn _ n a (Consn _ m b l) => n + m end. @@ -1027,17 +1017,17 @@ Type Type match LE_n 0 return nat with - | LE_n => 0 - | LE_S m LE_n => 0 + m - | LE_S m (LE_S y h) => 0 + m + | LE_n _ => 0 + | LE_S _ m (LE_n _) => 0 + m + | LE_S _ m (LE_S _ y h) => 0 + m end. Type match LE_n 0 with - | LE_n => 0 - | LE_S m LE_n => 0 + m - | LE_S m (LE_S y h) => 0 + m + | LE_n _ => 0 + | LE_S _ m (LE_n _) => 0 + m + | LE_S _ m (LE_S _ y h) => 0 + m end. @@ -1077,25 +1067,25 @@ Type Type (fun (A : Set) (n : nat) (l : Listn A n) => match l return (nat -> nat) with - | Niln => fun _ : nat => 0 - | Consn n a Niln => fun _ : nat => n - | Consn n a (Consn m b l) => fun _ : nat => n + m + | Niln _ => fun _ : nat => 0 + | Consn _ n a (Niln _) => fun _ : nat => n + | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m end). Type (fun (A : Set) (n : nat) (l : Listn A n) => match l with - | Niln => fun _ : nat => 0 - | Consn n a Niln => fun _ : nat => n - | Consn n a (Consn m b l) => fun _ : nat => n + m + | Niln _ => fun _ : nat => 0 + | Consn _ n a (Niln _) => fun _ : nat => n + | Consn _ n a (Consn _ m b l) => fun _ : nat => n + m end). (* Also tests for multiple _ patterns *) Type (fun (A : Set) (n : nat) (l : Listn A n) => match l in (Listn _ n) return (Listn A n) with - | Niln as b => b - | Consn _ _ _ as b => b + | Niln _ as b => b + | Consn _ _ _ _ as b => b end). (** This one was said to raised once an "Horrible error message!" *) @@ -1103,8 +1093,8 @@ Type Type (fun (A:Set) (n:nat) (l:Listn A n) => match l with - | Niln as b => b - | Consn _ _ _ as b => b + | Niln _ as b => b + | Consn _ _ _ _ as b => b end). Type @@ -1123,26 +1113,26 @@ Type Type (fun (n m : nat) (h : LE n m) => match h return (nat -> nat) with - | LE_n => fun _ : nat => n - | LE_S m LE_n => fun _ : nat => n + m - | LE_S m (LE_S y h) => fun _ : nat => m + y + | LE_n _ => fun _ : nat => n + | LE_S _ m (LE_n _) => fun _ : nat => n + m + | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y end). Type (fun (n m : nat) (h : LE n m) => match h with - | LE_n => fun _ : nat => n - | LE_S m LE_n => fun _ : nat => n + m - | LE_S m (LE_S y h) => fun _ : nat => m + y + | LE_n _ => fun _ : nat => n + | LE_S _ m (LE_n _) => fun _ : nat => n + m + | LE_S _ m (LE_S _ y h) => fun _ : nat => m + y end). Type (fun (n m : nat) (h : LE n m) => match h return nat with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y LE_n) => n + m + y - | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y') + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y + | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y') end). @@ -1150,28 +1140,28 @@ Type Type (fun (n m : nat) (h : LE n m) => match h with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y LE_n) => n + m + y - | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y') + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y (LE_n _)) => n + m + y + | LE_S _ m (LE_S _ y (LE_S _ y' h)) => n + m + (y + y') end). Type (fun (n m : nat) (h : LE n m) => match h return nat with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y h) => n + m + y + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y h) => n + m + y end). Type (fun (n m : nat) (h : LE n m) => match h with - | LE_n => n - | LE_S m LE_n => n + m - | LE_S m (LE_S y h) => n + m + y + | LE_n _ => n + | LE_S _ m (LE_n _) => n + m + | LE_S _ m (LE_S _ y h) => n + m + y end). Type @@ -1231,14 +1221,14 @@ Parameter B : Set. Type (fun (P : nat -> B -> Prop) (x : SStream B P) => match x return B with - | scons _ a _ _ => a + | scons _ _ a _ _ => a end). Type (fun (P : nat -> B -> Prop) (x : SStream B P) => match x with - | scons _ a _ _ => a + | scons _ _ a _ _ => a end). Type match (0, 0) return (nat * nat) with @@ -1267,14 +1257,14 @@ Parameter concat : forall A : Set, List A -> List A -> List A. Type match Nil nat, Nil nat return (List nat) with - | Nil as b, x => concat nat b x - | Cons _ _ as d, Nil as c => concat nat d c + | Nil _ as b, x => concat nat b x + | Cons _ _ _ as d, Nil _ as c => concat nat d c | _, _ => Nil nat end. Type match Nil nat, Nil nat with - | Nil as b, x => concat nat b x - | Cons _ _ as d, Nil as c => concat nat d c + | Nil _ as b, x => concat nat b x + | Cons _ _ _ as d, Nil _ as c => concat nat d c | _, _ => Nil nat end. @@ -1415,7 +1405,7 @@ Parameter p : eq_prf. Type match p with - | ex_intro c eqc => + | ex_intro _ c eqc => match eq_nat_dec c n with | right _ => refl_equal n | left y => (* c=n*) refl_equal n @@ -1438,7 +1428,7 @@ Type (fun N : nat => match N_cla N with | inright H => match exist_U2 N H with - | exist a b => a + | exist _ a b => a end | _ => 0 end). @@ -1636,8 +1626,8 @@ Parameter Type match Nil nat as l return (Empty nat l \/ ~ Empty nat l) with - | Nil => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat) - | Cons a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y) + | Nil _ => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat) + | Cons _ a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y) end. @@ -1687,20 +1677,20 @@ Parameter Type match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => V1 - | Nil, Cons a x => V2 a x - | Cons a x, Nil => V3 a x - | Cons a x, Cons b y => V4 a x b y + | Nil _, Nil _ => V1 + | Nil _, Cons _ a x => V2 a x + | Cons _ a x, Nil _ => V3 a x + | Cons _ a x, Cons _ b y => V4 a x b y end. Type (fun x y : List nat => match x, y return (eqlong x y \/ ~ eqlong x y) with - | Nil, Nil => V1 - | Nil, Cons a x => V2 a x - | Cons a x, Nil => V3 a x - | Cons a x, Cons b y => V4 a x b y + | Nil _, Nil _ => V1 + | Nil _, Cons _ a x => V2 a x + | Cons _ a x, Nil _ => V3 a x + | Cons _ a x, Cons _ b y => V4 a x b y end). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index bfead53c..8d9edbd6 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -4,8 +4,8 @@ Check (fun (P : nat -> Prop) Q (A : P 0 -> Q) (B : forall n : nat, P (S n) -> Q) x => match x return Q with - | exist O H => A H - | exist (S n) H => B n H + | exist _ O H => A H + | exist _ (S n) H => B n H end). (* Check dependencies in anonymous arguments (from FTA/listn.v) *) @@ -21,30 +21,30 @@ Variable c : C. Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C := match bs with - | niln => c - | consn b _ tl => g b (foldrn _ tl) + | niln _ => c + | consn _ b _ tl => g b (foldrn _ tl) end. End Folding. (** Testing post-processing of nested dependencies *) Check fun x:{x|x=0}*nat+nat => match x with - | inl ((exist 0 eq_refl),0) => None + | inl ((exist _ 0 eq_refl),0) => None | _ => Some 0 end. Check fun x:{_:{x|x=0}|True}+nat => match x with - | inl (exist (exist 0 eq_refl) I) => None + | inl (exist _ (exist _ 0 eq_refl) I) => None | _ => Some 0 end. Check fun x:{_:{x|x=0}|True}+nat => match x with - | inl (exist (exist 0 eq_refl) I) => None + | inl (exist _ (exist _ 0 eq_refl) I) => None | _ => Some 0 end. Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with - | inl (exist (exist 0 eq_refl) I) => None + | inl (exist _ (exist _ 0 eq_refl) I) => None | _ => Some 0 end. @@ -52,11 +52,11 @@ Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with (* due to a bug in dependencies postprocessing (revealed by CoLoR) *) Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with - | exist2 (x,y) eq_refl I => None + | exist2 _ _ (x,y) eq_refl I => None end. Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with - | inl (exist (exist2 (x,y) eq_refl I) I) => None + | inl (exist _ (exist2 _ _ (x,y) eq_refl I) I) => None | _ => Some 0 end. @@ -521,8 +521,8 @@ end. Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) := match v with - | niln => w - | consn a n' v' => consn _ a _ (app v' w) + | niln _ => w + | consn _ a n' v' => consn _ a _ (app v' w) end. (* Testing regression of bug 2106 *) @@ -547,7 +547,7 @@ n'. Definition test (s:step E E) := match s with - | Step nil _ (cons E nil) _ Plus l l' => true + | @Step nil _ (cons E nil) _ Plus l l' => true | _ => false end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 49c54916..87c38cfa 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Compiling the theories allows to test parsing and typing but not printing *) +(* Compiling the theories allows testing parsing and typing but not printing *) (* This file tests that pretty-printing does not fail *) (* Test of exact output is not specified *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index cdf9d6da..8db08b6d 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 3a4f8899..5fc703cf 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -42,8 +42,8 @@ Variables (B C : Set) (g : B -> C -> C) (c : C). Fixpoint foldrn n bs := match bs with - | Vnil => c - | Vcons b _ tl => g b (foldrn _ tl) + | Vnil _ => c + | Vcons _ b _ tl => g b (foldrn _ tl) end. End folding. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index ccce3bbe..3bf97c13 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -23,6 +23,7 @@ Function ftest (n m : nat) : nat := end | S p => 0 end. +(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *) Lemma test1 : forall n m : nat, ftest n m <= 2. intros n m. @@ -150,7 +151,7 @@ Function nat_equal_bool (n m : nat) {struct n} : bool := Require Export Div2. - +Require Import Nat. Functional Scheme div2_ind := Induction for div2 Sort Prop. Lemma div2_inf : forall n : nat, div2 n <= n. intros n. @@ -233,11 +234,11 @@ Qed. Inductive istrue : bool -> Prop := istrue0 : istrue true. -Functional Scheme plus_ind := Induction for plus Sort Prop. +Functional Scheme add_ind := Induction for add Sort Prop. Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. intros n m. - functional induction plus n m; intros. + functional induction add n m; intros. auto with arith. auto with arith. Qed. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index 84ec298d..f702aa62 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -9,11 +9,15 @@ Require Import Coq.Program.Program. Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n := match v with | vnil => ! - | vcons a n' v' => v' + | vcons a v' => v' end. Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) := match v in vector _ n return vector A (n + m) with | vnil => w - | vcons a n' v' => vcons a (app v' w) + | vcons a v' => vcons a (app v' w) end. + +(* Test sharing information between different hypotheses *) + +Parameters (a:_) (b:a=0). diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index da5dd5e4..3d425754 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -17,7 +17,7 @@ Check fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => let B := A in fun (a : A) (e : eq1 A a) => - match e in (eq1 A0 B0 a0) return (P A0 a0) with + match e in (@eq1 A0 B0 a0) return (P A0 a0) with | refl1 => f end. @@ -37,8 +37,8 @@ Check fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type) (f : forall z : C, P z (I C D x y z)) (y0 : C) (a : A C D x y y0) => - match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with - | I x0 => f x0 + match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with + | I _ _ _ _ x0 => f x0 end). Record B (C D : Set) (E:=C) (F:=D) (x y : E -> F) : Set := {p : C; q : E}. @@ -51,7 +51,7 @@ Check (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) (b : B C D x y) => match b as b0 return (P b0) with - | Build_B x0 x1 => f x0 x1 + | Build_B _ _ _ _ x0 x1 => f x0 x1 end). (* Check inductive types with local definitions (constructors) *) @@ -107,3 +107,17 @@ Set Implicit Arguments. Inductive I A : A->Prop := C a : (forall A, A) -> I a. *) + +(* Test recursively non-uniform parameters (was formerly in params_ind.v) *) + +Inductive list (A : Set) : Set := + | nil : list A + | cons : A -> list (A -> A) -> list A. + +(* Check inference of evars in arity using information from constructors *) + +Inductive foo1 : forall p, Prop := cc1 : foo1 0. + +(* Check cross inference of evars from constructors *) + +Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index c5cd7380..6a488244 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -39,7 +39,7 @@ Qed. (* Test injection as *) Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z. -intros; injection H as Hyt Hxz. +intros; injection H as Hxz Hyt. exact Hxz. Qed. @@ -66,6 +66,56 @@ einjection (H O). instantiate (1:=O). Abort. +(* Test the injection intropattern *) + +Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b. +intros * [= H1 H2]. +exact H1. +Qed. + +(* Test injection using K, knowing that an equality is decidable *) +(* Basic case, using sigT *) + +Scheme Equality for nat. +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + existT P n H1 = existT P n H2 -> H1 = H2. +intros. +injection H. +intro H0. exact H0. +Abort. + +(* Test injection using K, knowing that an equality is decidable *) +(* Basic case, using sigT, with "as" clause *) + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + existT P n H1 = existT P n H2 -> H1 = H2. +intros. +injection H as H. +exact H. +Abort. + +(* Test injection using K, knowing that an equality is decidable *) +(* Dependent case not directly exposing sigT *) + +Inductive my_sig (A : Type) (P : A -> Type) : Type := + my_exist : forall x : A, P x -> my_sig A P. + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + my_exist _ _ n H1 = my_exist _ _ n H2 -> H1 = H2. +intros. +injection H as H. +exact H. +Abort. + +(* Test injection using K, knowing that an equality is decidable *) +(* Dependent case not directly exposing sigT deeply nested *) + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + (my_exist _ _ n H1,0) = (my_exist _ _ n H2,0) -> H1 = H2. +intros * [= H]. +exact H. +Abort. + (* Injection does not projects at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index b068f729..850f0943 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -136,3 +136,56 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. + +(* Was failing at some time between 7 and 10 September 2014 *) +(* even though, it is not clear that the resulting context is interesting *) + +Parameter P:nat*nat->Prop. +Inductive IND : nat * nat -> { x : nat * nat | P x } * nat -> Prop := +CONSTR a b (H:P (a,b)) c : IND (a,b) (exist _ (a,b) H, c). + +Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z. +intros * Hyp. +inversion Hyp. + (* By the way, why is "H" removed even in non-clear mode ? *) +reflexivity. +Qed. + +Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z. +intros * Hyp. +inversion Hyp as (a,b,H,c,(H1_1,H1_2),(H2_1,H2_2,H2_3)). +reflexivity. +Qed. + +(* Up to September 2014, Mapp below was called MApp0 because of a bug + in intro_replacing (short version of bug 2164.v) + (example taken from CoLoR) *) + +Parameter Term : Type. +Parameter isApp : Term -> Prop. +Parameter appBodyL : forall M, isApp M -> Prop. +Parameter lower : forall M Mapp, appBodyL M Mapp -> Term. + +Inductive BetaStep : Term -> Term -> Prop := + Beta M Mapp Mabs : BetaStep M (lower M Mapp Mabs). + +Goal forall M N, BetaStep M N -> True. +intros M N H. +inversion H as (P,Mapp,Mabs,H0,H1). +clear Mapp Mabs H0 H1. +exact Logic.I. +Qed. + +(* Up to September 2014, H0 below was renamed called H1 because of a collision + with the automaticallly generated names for equations. + (example taken from CoLoR) *) + +Inductive term := Var | Fun : term -> term -> term. +Inductive lt : term -> term -> Prop := + mpo f g ss ts : lt Var (Fun f ts) -> lt (Fun f ss) (Fun g ts). + +Goal forall f g ss ts, lt (Fun f ss) (Fun g ts) -> lt Var (Fun f ts). +intros. +inversion H as (f',g',ss',ts',H0). +exact H0. +Qed. diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v deleted file mode 100644 index 9b2a2c6a..00000000 --- a/test-suite/success/LegacyField.v +++ /dev/null @@ -1,76 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(**** Tests of Field with real numbers ****) - -Require Import Reals LegacyRfield. - -(* Example 1 *) -Goal -forall eps : R, -(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 2 *) -Goal -forall (f g : R -> R) (x0 x1 : R), -((f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)))%R = -((f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)))%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 3 *) -Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 4 *) -Goal -forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 5 *) -Goal forall a : R, 1%R = (1 * (1 / a) * a)%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 6 *) -Goal forall a b : R, b = (b * / a * a)%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 7 *) -Goal forall a b : R, b = (b * (1 / a) * a)%R. -Proof. - intros. - legacy field. -Abort. - -(* Example 8 *) -Goal -forall x y : R, -(x * (1 / x + x / (x + y)))%R = -(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R. -Proof. - intros. - legacy field. -Abort. diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v index 4c790680..0e557aee 100644 --- a/test-suite/success/LetPat.v +++ b/test-suite/success/LetPat.v @@ -9,22 +9,22 @@ Print l3. Record someT (A : Type) := mkT { a : nat; b: A }. -Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x. +Definition l4 A (t : someT A) : nat := let 'mkT _ x y := t in x. Print l4. Print sigT. Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) := - let 'existT x y := t return B (projT1 t) in y. + let 'existT _ x y := t return B (projT1 t) in y. Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) := - let 'existT x y as t' := t return B (projT1 t') in y. + let 'existT _ x y as t' := t return B (projT1 t') in y. Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) := - let 'existT x y as t' in sigT _ := t return B (projT1 t') in y. + let 'existT _ x y as t' in sigT _ := t return B (projT1 t') in y. Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := match t with - existT x y => y + existT _ x y => y end. (** An example from algebra, using let' and inference of return clauses diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index c2d87a44..7069bba4 100644 --- a/test-suite/success/MatchFail.v +++ b/test-suite/success/MatchFail.v @@ -4,7 +4,7 @@ Require Export ZArithRing. (* Cette tactique a pour objectif de remplacer toute instance de (POS (xI e)) ou de (POS (xO e)) par 2*(POS e)+1 ou 2*(POS e), pour rendre les expressions plus - à même d'être utilisées par Ring, lorsque ces expressions contiennent + à même d'être utilisées par Ring, lorsque ces expressions contiennent des variables de type positive. *) Ltac compute_POS := match goal with diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v new file mode 100644 index 00000000..6d787210 --- /dev/null +++ b/test-suite/success/NumberScopes.v @@ -0,0 +1,62 @@ + +(* We check that various definitions or lemmas have the correct + argument scopes, especially the ones created via functor application. *) + +Close Scope nat_scope. + +Require Import PArith. +Check (Pos.add 1 2). +Check (Pos.add_comm 1 2). +Check (Pos.min_comm 1 2). +Definition f_pos (x:positive) := x. +Definition f_pos' (x:Pos.t) := x. +Check (f_pos 1). +Check (f_pos' 1). + +Require Import ZArith. +Check (Z.add 1 2). +Check (Z.add_comm 1 2). +Check (Z.min_comm 1 2). +Definition f_Z (x:Z) := x. +Definition f_Z' (x:Z.t) := x. +Check (f_Z 1). +Check (f_Z' 1). + +Require Import NArith. +Check (N.add 1 2). +Check (N.add_comm 1 2). +Check (N.min_comm 1 2). +Definition f_N (x:N) := x. +Definition f_N' (x:N.t) := x. +Check (f_N 1). +Check (f_N' 1). + +Require Import Arith. +Check (Nat.add 1 2). +Check (Nat.add_comm 1 2). +Check (Nat.min_comm 1 2). +Definition f_nat (x:nat) := x. +Definition f_nat' (x:Nat.t) := x. +Check (f_nat 1). +Check (f_nat' 1). + +Require Import BigN. +Check (BigN.add 1 2). +Check (BigN.add_comm 1 2). +Check (BigN.min_comm 1 2). +Definition f_bigN (x:bigN) := x. +Check (f_bigN 1). + +Require Import BigZ. +Check (BigZ.add 1 2). +Check (BigZ.add_comm 1 2). +Check (BigZ.min_comm 1 2). +Definition f_bigZ (x:bigZ) := x. +Check (f_bigZ 1). + +Require Import BigQ. +Check (BigQ.add 1 2). +Check (BigQ.add_comm 1 2). +Check (BigQ.min_comm 1 2). +Definition f_bigQ (x:bigQ) := x. +Check (f_bigQ 1).
\ No newline at end of file diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 3b7f0d84..681c4716 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -100,6 +100,6 @@ Next Obligation. simpl in *; intros. apply H. simpl. omega. Qed. -Program Fixpoint check_n' (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p) +Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) {measure (p - n) p} : nat := - _. + _.
\ No newline at end of file diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v index d8faa88a..3ffd41ea 100644 --- a/test-suite/success/Projection.v +++ b/test-suite/success/Projection.v @@ -1,3 +1,9 @@ +Record foo (A : Type) := { B :> Type }. + +Lemma bar (f : foo nat) (x : f) : x = x. + destruct f. simpl B. simpl B in x. +Abort. + Structure S : Type := {Dom : Type; Op : Dom -> Dom -> Dom}. Check (fun s : S => Dom s). diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 459645f6..11fbf24d 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -301,8 +301,8 @@ Section Le_case_analysis. (HS : forall m, n <= m -> Q (S m)). Check ( match H in (_ <= q) return (Q q) with - | le_n => H0 - | le_S m Hm => HS m Hm + | le_n _ => H0 + | le_S _ m Hm => HS m Hm end ). @@ -320,8 +320,8 @@ Qed. Definition Vtail_total (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):= match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with -| Vector.nil => Vector.nil A -| Vector.cons _ n0 v0 => v0 +| Vector.nil _ => Vector.nil A +| Vector.cons _ _ n0 v0 => v0 end. Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n). @@ -520,8 +520,7 @@ Inductive typ : Type := Definition typ_inject: typ. split. -exact typ. -Fail Defined. +Fail exact typ. (* Error: Universe Inconsistency. *) @@ -1060,8 +1059,8 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with _ , Vector.nil => None - | 0 , Vector.cons b _ _ => Some b - | S n', Vector.cons _ p' v' => vector_nth A n' p' v' + | 0 , Vector.cons b _ => Some b + | S n', Vector.cons _ v' => vector_nth A n' _ v' end. Implicit Arguments vector_nth [A p]. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index a79d28fa..43e3493c 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -6,3 +6,17 @@ Module A. Definition opp := Z.opp. End A. Check (A.opp 3). + +(* Test extra scopes to be used in the presence of coercions *) + +Record B := { f :> Z -> Z }. +Variable a:B. +Arguments Scope a [Z_scope]. +Check a 0. + +(* Check that casts activate scopes if ever possible *) + +Inductive U := A. +Bind Scope u with U. +Notation "'ε'" := A : u. +Definition c := ε : U. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index ed445c63..01d9afb4 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index aecc9ed0..3090f40c 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -53,7 +53,7 @@ Abort. Lemma essai2 : forall x : nat, x = x. - refine (fix f (x : nat) : x = x := _). +Fail refine (fix f (x : nat) : x = x := _). Restart. @@ -119,7 +119,7 @@ Lemma essai : {x : nat | x = 1}. Restart. (* mais si on contraint par le but alors ca marche : *) -(* Remarque : on peut toujours faire ça *) +(* Remarque : on peut toujours faire ça *) refine (exist _ 1 _:{x : nat | x = 1}). Restart. @@ -176,7 +176,7 @@ Restart. end). exists 1. trivial. -elim (f0 p). +elim (f p). refine (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _). rewrite h. auto. @@ -184,7 +184,7 @@ Qed. -(* Quelques essais de recurrence bien fondée *) +(* Quelques essais de recurrence bien fondée *) Require Import Wf. Require Import Wf_nat. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 0d8bf556..21b829aa 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -164,8 +164,8 @@ intros. apply H with (y:=y). (* [x] had two possible instances: [S 0], coming from unifying the type of [y] with [I ?n] and [succ 0] coming from the unification with - the goal; only the first one allows to make the next apply (which - does not work modulo delta) working *) + the goal; only the first one allows the next apply (which + does not work modulo delta) work *) apply H0. Qed. @@ -336,25 +336,43 @@ Qed. (* From 12612, descent in conjunctions is more powerful *) (* The following, which was failing badly in bug 1980, is now properly rejected, as descend in conjunctions builds an - ill-formed elimination from Prop to Type. *) + ill-formed elimination from Prop to Type. + + Added Aug 2014: why it fails is now that trivial unification ?x = goal is + rejected by the descent in conjunctions to avoid surprising results. *) Goal True. Fail eapply ex_intro. exact I. Qed. -(* The following, which were not accepted, are now accepted as - expected by descent in conjunctions *) +Goal True. +Fail eapply (ex_intro _). +exact I. +Qed. + +(* Note: the following succeed directly (i.e. w/o "exact I") since + Aug 2014 since the descent in conjunction does not use a "cut" + anymore: the iota-redex is contracted and we get rid of the + uninstantiated evars + + Is it good or not? Maybe it does not matter so much. Goal True. eapply (ex_intro (fun _ => True) I). -exact I. +exact I. (* Not needed since Aug 2014 *) +Qed. + +Goal True. +eapply (ex_intro (fun _ => True) I _). +exact I. (* Not needed since Aug 2014 *) Qed. Goal True. eapply (fun (A:Prop) (x:A) => conj I x). -exact I. +exact I. (* Not needed since Aug 2014 *) Qed. +*) (* The following was not accepted from r12612 to r12657 *) @@ -430,3 +448,91 @@ Undo. (* H' is displayed as (forall n0, n=n0) *) apply H' with (n0:=0). Qed. + +(* Check that evars originally present in goal do not prevent apply in to work*) + +Goal (forall x, x <= 0 -> x = 0) -> exists x, x <= 0 -> 0 = 0. +intros. +eexists. +intros. +apply H in H0. +Abort. + +(* Check correct failure of apply in when hypothesis is dependent *) + +Goal forall H:0=0, H = H. +intros. +Fail apply eq_sym in H. + +(* Check that unresolved evars not originally present in goal prevent + apply in to work*) + +Goal (forall x y, x <= 0 -> x + y = 0) -> exists x, x <= 0 -> 0 = 0. +intros. +eexists. +intros. +Fail apply H in H0. +Abort. + +(* Check naming pattern in apply in *) + +Goal ((False /\ (True -> True))) -> True -> True. +intros F H. +apply F in H as H0. (* Check that H0 is not used internally *) +exact H0. +Qed. + +Goal ((False /\ (True -> True/\True))) -> True -> True/\True. +intros F H. +apply F in H as (?,?). +split. +exact H. (* Check that generated names are H and H0 *) +exact H0. +Qed. + +(* This failed at some time in between 18 August 2014 and 2 September 2014 *) + +Goal forall A B C: Prop, (True -> A -> B /\ C) -> A -> B. +intros * H. +apply H. +Abort. + +(* This failed between 2 and 3 September 2014 *) + +Goal forall A B C D:Prop, (A<->B)/\(C<->D) -> A -> B. +intros. +apply H in H0. +pose proof I as H1. (* Test that H1 does not exist *) +Abort. + +Goal forall A B C D:Prop, (A<->B)/\(C<->D) -> A. +intros. +apply H. +pose proof I as H0. (* Test that H0 does not exist *) +Abort. + +(* The first example below failed at some time in between 18 August + 2014 and 2 September 2014 *) + +Goal forall x, 2=0 -> x+1=2 -> (forall x, S x = 0) -> True. +intros x H H0 H1. +eapply eq_trans in H. 2:apply H0. +rewrite H1 in H. +change (x+0=0) in H. (* Check the result in H1 *) +Abort. + +Goal forall x, 2=x+1 -> (forall x, S x = 0) -> 2 = 0. +intros x H H0. +eapply eq_trans. apply H. +rewrite H0. +change (x+0=0). +Abort. + +(* 2nd order apply used to have delta on local definitions even though + it does not have delta on global definitions; keep it by + compatibility while finding a more uniform way to proceed. *) + +Goal forall f:nat->nat, (forall P x, P (f x)) -> let x:=f 0 in x = 0. +intros f H x. +apply H. +Qed. diff --git a/test-suite/success/applyTC.v b/test-suite/success/applyTC.v new file mode 100644 index 00000000..c2debdec --- /dev/null +++ b/test-suite/success/applyTC.v @@ -0,0 +1,15 @@ +Axiom P : nat -> Prop. + +Class class (A : Type) := { val : A }. + +Lemma usetc {t : class nat} : P (@val nat t). +Admitted. + +Notation "{val:= v }" := (@val _ v). + +Instance zero : class nat := {| val := 0 |}. + +Lemma test : P 0. +Fail apply usetc. +pose (tmp := usetc); apply tmp; clear tmp. +Qed. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 9b691e25..db3b19af 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -14,7 +14,7 @@ Hint Resolve L. Goal G unit Q -> F (Q tt). intro. - auto. + eauto. Qed. (* Test implicit arguments in "using" clause *) @@ -24,3 +24,24 @@ auto using (pair O). Undo. eauto using (pair O). Qed. + +Create HintDb test discriminated. + +Parameter foo : forall x, x = x + 0. +Hint Resolve foo : test. + +Variable C : nat -> Type -> Prop. + +Variable c_inst : C 0 nat. + +Hint Resolve c_inst : test. + +Hint Mode C - + : test. +Hint Resolve c_inst : test2. +Hint Mode C + + : test2. + +Goal exists n, C n nat. +Proof. + eexists. Fail progress debug eauto with test2. + progress eauto with test. +Qed. diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index b565183b..a70d9196 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -102,5 +102,32 @@ Proof. auto. Qed. +(* bug 2447 is now closed (PC, 2014) *) + +Section bug_2447. + +Variable T:Type. + +Record R := mkR {x:T;y:T;z:T}. + +Variables a a' b b' c c':T. + + + +Lemma bug_2447: mkR a b c = mkR a' b c -> a = a'. +congruence. +Qed. + +Lemma bug_2447_variant1: mkR a b c = mkR a b' c -> b = b'. +congruence. +Qed. + +Lemma bug_2447_variant2: mkR a b c = mkR a b c' -> c = c'. +congruence. +Qed. + + +End bug_2447. + diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 7bed7ecb..1f0b7d38 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -38,3 +38,24 @@ Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x). Fail change True with match ex_intro _ True (eq_refl True) with ex_intro x _ => x end. Abort. + +(* Check absence of loop in identity substitution (was failing up to + Sep 2014, see #3641) *) + +Goal True. +change ?x with x. +Abort. + +(* Check typability after change of type subterms *) +Goal nat = nat :> Set. +Fail change nat with (@id Type nat). (* would otherwise be ill-typed *) +Abort. + +(* Check typing env for rhs is the correct one *) + +Goal forall n, let x := n in id (fun n => n + x) 0 = 0. +intros. +unfold x. +(* check that n in 0+n is not interpreted as the n from "fun n" *) +change n with (0+n). +Abort. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 4292ecb6..b538d2ed 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -96,13 +96,13 @@ Inductive list (A : Type) : Type := nil : list A | cons : A -> list A -> list A. Inductive vect (A : Type) : nat -> Type := vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n). -Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end. +Fixpoint size A (l : list A) : nat := match l with nil _ => 0 | cons _ _ tl => 1+size _ tl end. Section test_non_unif_but_complete. Fixpoint l2v A (l : list A) : vect A (size A l) := match l as l return vect A (size A l) with - | nil => vnil A - | cons x xs => vcons A (size A xs) x (l2v A xs) + | nil _ => vnil A + | cons _ x xs => vcons A (size A xs) x (l2v A xs) end. Local Coercion l2v : list >-> vect. @@ -121,8 +121,8 @@ Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := match l as l return vect B (size A l) with - | nil => vnil B - | cons x xs => vcons _ _ (c x) (l2v2 xs) end. + | nil _ => vnil B + | cons _ x xs => vcons _ _ (c x) (l2v2 xs) end. Local Coercion l2v2 : list >-> vect. diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v index 52575eca..58f79d45 100644 --- a/test-suite/success/decl_mode.v +++ b/test-suite/success/decl_mode.v @@ -67,7 +67,7 @@ proof. end proof. Qed. -Require Omega. +Require Import Omega. Lemma even_double_n: (forall m, even (double m)). proof. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index fc40ea96..83a33f75 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -37,7 +37,6 @@ Goal True. case Refl || ecase Refl. Abort. - (* Submitted by B. Baydemir (bug #1882) *) Require Import List. @@ -93,3 +92,339 @@ Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0. intros. destruct (g _). (* This was failing in at least r14571 *) Abort. + +(* Check that subterm selection does not solve existing evars *) + +Goal exists x, S x = S 0. +eexists. +destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) +change (0 = S 0). +Abort. + +Goal exists x, S 0 = S x. +eexists. +destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) +change (0 = S ?x). +Abort. + +Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. +do 2 eexists. +destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *) +change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n). +Abort. + +(* An example with incompatible but convertible occurrences *) + +Goal id (id 0) = 0. +Fail destruct (id _) at 1 2. +Abort. + +(* Avoid unnatural selection of a subterm larger than expected *) + +Goal let g := fun x:nat => x in g (S 0) = 0. +intro. +destruct S. +(* Check that it is not the larger subterm "g (S 0)" which is + selected, as it was the case in 8.4 *) +unfold g at 1. +Abort. + +(* Some tricky examples convenient to support *) + +Goal forall x, nat_rect (fun _ => nat) O (fun x y => S x) x = nat_rect (fun _ => nat) O (fun x y => S x) x. +intros. +destruct (nat_rect _ _ _ _). +Abort. +(* Check compatibility in selecting what is open or "shelved" *) + +Goal (forall x, x=0 -> nat) -> True. +intros. +Fail destruct H. +edestruct H. +- reflexivity. +- exact Logic.I. +- exact Logic.I. +Qed. + +(* Check an example which was working with case/elim in 8.4 but not with + destruct/induction *) + +Goal forall x, (True -> x = 0) -> 0=0. +intros. +destruct H. +- trivial. +- apply (eq_refl x). +Qed. + +(* Check an example which was working with case/elim in 8.4 but not with + destruct/induction (not the different order between induction/destruct) *) + +Goal forall x, (True -> x = 0) -> 0=0. +intros. +induction H. +- apply (eq_refl x). +- trivial. +Qed. + +(* This test assumes that destruct/induction on non-dependent hypotheses behave the same + when using holes or not + +Goal forall x, (True -> x = 0) -> 0=0. +intros. +destruct (H _). +- apply I. +- apply (eq_refl x). +Qed. +*) + +(* Check destruct vs edestruct *) + +Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0. +intros. +Fail destruct H. +edestruct H. +- trivial. +- apply (eq_refl x). +Qed. + +Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0. +intros. +Fail destruct (H _ _). +(* Now a test which assumes that edestruct on non-dependent + hypotheses accept unresolved subterms in the induction argument. +edestruct (H _ _). +- trivial. +- apply (eq_refl x). +Qed. +*) +Abort. + +(* Test selection when not in an inductive type *) +Parameter T:Type. +Axiom elim: forall P, T -> P. +Goal forall a:T, a = a. +induction a using elim. +Qed. + +Goal forall a:nat -> T, a 0 = a 1. +intro a. +induction (a 0) using elim. +Qed. + +(* From Oct 2014, a subterm is found, as if without "using"; in 8.4, + it did not find a subterm *) + +Goal forall a:nat -> T, a 0 = a 1. +intro a. +induction a using elim. +Qed. + +Goal forall a:nat -> T, forall b, a 0 = b. +intros a b. +induction a using elim. +Qed. + +(* From Oct 2014, first subterm is found; in 8.4, it failed because it + found "a 0" and wanted to clear a *) + +Goal forall a:nat -> nat, a 0 = a 1. +intro a. +destruct a. +change (0 = a 1). +Abort. + +(* This example of a variable not fully applied in the goal was working in 8.4*) + +Goal forall H : 0<>0, H = H. +destruct H. +reflexivity. +Qed. + +(* Check that variables not fully applied in the goal are not erased + (this example was failing in 8.4 because of a forbidden "clear H" in + the code of "destruct H" *) + +Goal forall H : True -> True, H = H. +destruct H. +- exact I. +- reflexivity. +Qed. + +(* Check destruct on idents with maximal implicit arguments - which did + not work in 8.4 *) + +Parameter g : forall {n:nat}, n=n -> nat. +Goal g (eq_refl 0) = 0. +destruct g. +Abort. + +(* This one was working in 8.4 (because of full conv on closed arguments) *) + +Class E. +Instance a:E. +Goal forall h : E -> nat -> nat, h (id a) 0 = h a 0. +intros. +destruct (h _). +change (0=0). +Abort. + +(* This one was not working in 8.4 because an occurrence of f was + remaining, blocking the "clear f" *) + +Goal forall h : E -> nat -> nat, h a 0 = h a 1. +intros. +destruct h. +Abort. + +(* This was not working in 8.4 *) + +Section S1. +Variables x y : Type. +Variable H : x = y. +Goal True. +destruct H. (* Was not working in 8.4 *) +(* Now check that H statement has itself be subject of the rewriting *) +change (x=x) in H. +Abort. +End S1. + +(* This was not working in 8.4 because of untracked dependencies *) +Goal forall y, forall h:forall x, x = y, h 0 = h 0. +intros. +destruct (h 0). +Abort. + +(* Check absence of useless local definitions *) + +Section S2. +Variable H : 1=1. +Goal 0=1. +destruct H. +Fail clear n. (* Check that there is no n as it was in Coq <= 8.4 *) +Abort. +End S2. + +Goal forall x:nat, x=x->x=1. +intros x H. +destruct H. +Fail clear n. (* Check that there is no n as it was in Coq <= 8.4 *) +Fail clear H. (* Check that H has been removed *) +Abort. + +(* Check support for induction arguments which do not expose an inductive + type rightaway *) + +Definition U := nat -> nat. +Definition S' := S : U. +Goal forall n, S' n = 0. +intro. +destruct S'. +Abort. + +(* This was working by chance in 8.4 thanks to "accidental" use of select + subterms _syntactically_ equal to the first matching one. + +Parameter f2:bool -> unit. +Parameter r2:f2 true=f2 true. +Goal forall (P: forall b, b=b -> Prop), f2 (id true) = tt -> P (f2 true) r2. +intros. +destruct f2. +Abort. +*) + +(* This did not work in 8.4, because of a clear failing *) + +Inductive IND : forall x y:nat, x=y -> Type := CONSTR : IND 0 0 eq_refl. +Goal forall x y e (h:x=y -> y=x) (z:IND y x (h e)), e = e /\ z = z. +intros. +destruct z. +Abort. + +(* The two following examples show how the variables occurring in the + term being destruct affects the generalization; don't know if these + behaviors are "good". None of them was working in 8.4. *) + +Goal forall x y e (t:x=y) (z:x=y -> IND y x e), e = e. +intros. +destruct (z t). +change (0=0) in t. (* Generalization made *) +Abort. + +Goal forall x y e (t:x=y) (z:x=y -> IND y x e), e = e /\ z t = z t. +intros. +destruct (z t). +change (0=0) in t. (* Generalization made *) +Abort. + +(* Check that destruct on a scheme with a functional argument works *) + +Goal (forall P:Prop, (nat->nat) -> P) -> forall h:nat->nat, h 0 = h 0. +intros. +destruct h using H. +Qed. + +Goal (forall P:Prop, (nat->nat) -> P) -> forall h:nat->nat->nat, h 0 0 = h 1 0. +intros. +induction (h 1) using H. +Qed. + +(* Check blocking generalization is not too strong (failed at some time) *) + +Goal (E -> 0=1) -> 1=0 -> True. +intros. +destruct (H _). +change (0=0) in H0. (* Check generalization on H0 was made *) +Abort. + +(* Check absence of anomaly (failed at some time) *) + +Goal forall A (a:A) (P Q:A->Prop), (forall a, P a -> Q a) -> True. +intros. +Fail destruct H. +Abort. + +(* Check keep option (bug #3791) *) + +Goal forall b:bool, True. +intro b. +destruct !b. +clear b. (* b has to be here *) +Abort. + +(* Check clearing of names *) + +Inductive IND2 : nat -> Prop := CONSTR2 : forall y, y = y -> IND2 y. +Goal forall x y z:nat, y = z -> x = y -> y = x -> x = y. +intros * Heq H Heq'. +destruct H. +Abort. + +Goal 2=1 -> 1=0. +intro H. destruct H. +Fail (match goal with n:nat |- _ => unfold n end). (* Check that no let-in remains *) +Abort. + +(* Check clearing of names *) + +Inductive eqnat (x : nat) : nat -> Prop := + reflnat : forall y, x = y -> eqnat x y. + +Goal forall x z:nat, x = z -> eqnat x z -> True. +intros * H1 H. +destruct H. +Fail clear z. (* Should not be here *) +Abort. + +(* Check ok in the presence of an equation *) + +Goal forall b:bool, b = b. +intros. +destruct b eqn:H. + +(* Check natural instantiation behavior when the goal has already an evar *) + +Goal exists x, S x = x. +eexists. +destruct (S _). +change (0 = ?x). +Abort. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index b7b0f7fd..9e57801e 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 044b41d3..1b5c7f18 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index e6088091..4e2bf451 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -1,3 +1,4 @@ + (* The "?" of cons and eq should be inferred *) Variable list : Set -> Set. Variable cons : forall T : Set, T -> list T -> list T. @@ -44,13 +45,13 @@ Fixpoint build (nl : list nat) : (* Checks that disjoint contexts are correctly set by restrict_hyp *) -(* Bug de 1999 corrigé en déc 2004 *) +(* Bug de 1999 corrigé en déc 2004 *) Check (let p := fun (m : nat) f (n : nat) => match f m n with - | exist a b => exist _ a b + | exist _ a b => exist _ a b end in p :forall x : nat, @@ -61,7 +62,7 @@ Check Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). -(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *) +(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *) Theorem contradiction : forall p, ~ p -> p -> False. Proof. trivial. Qed. @@ -177,9 +178,9 @@ refine | left _ => _ | right _ => match le_step s _ _ with - | exist s' h' => + | exist _ s' h' => match hr s' _ _ with - | exist s'' _ => exist _ s'' _ + | exist _ s'' _ => exist _ s'' _ end end end)). @@ -203,7 +204,7 @@ Abort. Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := match l with | nil => nil - | (existT k v)::l' => (existT _ k v):: (filter A l') + | (existT _ k v)::l' => (existT _ k v):: (filter A l') end. (* Bug #2000: used to raise Out of memory in 8.2 while it should fail by @@ -379,3 +380,38 @@ Section evar_evar_occur. (* Still evars in the resulting type, but constraints should be solved *) Check match g _ with conj a b => f _ a b end. End evar_evar_occur. + +(* Eta expansion (bug #2936) *) +Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. +Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { + tri0 : forall a b c, R a b -> S a c -> T b c +}. +Implicit Arguments mkTri [R S T]. +Definition tri_iffT : tri iffT iffT iffT := + (mkTri + (fun X0 X1 X2 E01 E02 => + (mkIff _ _ (fun x1 => iffLR _ _ E02 (iffRL _ _ E01 x1)) + (fun x2 => iffLR _ _ E01 (iffRL _ _ E02 x2))))). + +(* Check that local defs names are preserved if possible during unification *) + +Goal forall x (x':=x) (f:forall y, y=y:>nat -> Prop), f _ (eq_refl x'). +intros. +unfold x' at 2. (* A way to check that there are indeed 2 occurrences of x' *) +Abort. + +(* A simple example we would like not to fail (it used to fail because of + not strict enough evar restriction) *) + +Check match Some _ with None => _ | _ => _ end. + +(* Used to fail for a couple of days in Nov 2014 *) + +Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2. + +(* Check use of candidates *) + +Import EqNotations. +Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a. + + diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index eaed9616..57f3775d 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v new file mode 100644 index 00000000..11bb25fd --- /dev/null +++ b/test-suite/success/extraction_dep.v @@ -0,0 +1,46 @@ + +(** Examples of code elimination inside modules during extraction *) + +(** NB: we should someday check the produced code instead of + simply running the commands. *) + +(** 1) Without signature ... *) + +Module A. + Definition u := 0. + Definition v := 1. + Module B. + Definition w := 2. + Definition x := 3. + End B. +End A. + +Definition testA := A.u + A.B.x. + +Recursive Extraction testA. (* without: v w *) + +(** 1b) Same with an Include *) + +Module Abis. + Include A. + Definition y := 4. +End Abis. + +Definition testAbis := Abis.u + Abis.y. + +Recursive Extraction testAbis. (* without: A B v w x *) + +(** 2) With signature, we only keep elements mentionned in signature. *) + +Module Type SIG. + Parameter u : nat. + Parameter v : nat. +End SIG. + +Module Ater : SIG. + Include A. +End Ater. + +Definition testAter := Ater.u. + +Recursive Extraction testAter. (* with only: u v *) diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index 8623f718..ff34840d 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -9,12 +9,13 @@ Inductive rBoolOp : Set := | rAnd : rBoolOp | rEq : rBoolOp. -Definition rlt (a b : rNat) : Prop := Pos.compare_cont a b Eq = Lt. +Definition rlt (a b : rNat) : Prop := Pos.compare_cont Eq a b = Lt. Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}. +Proof. intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m); generalize (nat_of_P_gt_Gt_compare_morphism n m); - generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq). + generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont Eq n m). intros H' H'0 H'1; right; right; auto. intros H' H'0 H'1; left; unfold rlt. apply nat_of_P_lt_Lt_compare_complement_morphism; auto. @@ -25,6 +26,7 @@ Defined. Definition rmax : rNat -> rNat -> rNat. +Proof. intros n m; case (rltDec n m); intros Rlt0. exact m. exact n. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index e8019a90..a0981311 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -61,7 +61,7 @@ Check (eq1 0 0). Check (eq2 0 0). Check (eq3 nat 0 0). -(* Example submitted by Frédéric (interesting in v8 syntax) *) +(* Example submitted by Frédéric (interesting in v8 syntax) *) Parameter f : nat -> nat * nat. Notation lhs := fst. diff --git a/test-suite/success/indelim.v b/test-suite/success/indelim.v new file mode 100644 index 00000000..91b6dee2 --- /dev/null +++ b/test-suite/success/indelim.v @@ -0,0 +1,61 @@ +Inductive boolP : Prop := +| trueP : boolP +| falseP : boolP. + +Fail Check boolP_rect. + + +Inductive True : Prop := I : True. + +Inductive False : Prop :=. + +Inductive Empty_set : Set :=. + +Fail Inductive Large_set : Set := + large_constr : forall A : Set, A -> Large_set. + +Inductive smallunitProp : Prop := +| onlyProps : True -> smallunitProp. + +Check smallunitProp_rect. + +Inductive nonsmallunitProp : Prop := +| notonlyProps : nat -> nonsmallunitProp. + +Fail Check nonsmallunitProp_rect. +Set Printing Universes. +Inductive inferProp := +| hasonlyProps : True -> nonsmallunitProp -> inferProp. + +Check (inferProp : Prop). + +Inductive inferSet := +| hasaset : nat -> True -> nonsmallunitProp -> inferSet. + +Fail Check (inferSet : Prop). + +Check (inferSet : Set). + +Inductive inferLargeSet := +| hasalargeset : Set -> True -> nonsmallunitProp -> inferLargeSet. + +Fail Check (inferLargeSet : Set). + +Inductive largeProp : Prop := somelargeprop : Set -> largeProp. + + +Inductive comparison : Set := + | Eq : comparison + | Lt : comparison + | Gt : comparison. + +Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := + | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq + | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt + | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. + +Inductive color := Red | Black. + +Inductive option (A : Type) : Type := +| None : option A +| Some : A -> option A.
\ No newline at end of file diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 83c90929..b733aef6 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 75643d9d..7ae60d98 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -25,7 +25,7 @@ Check fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => let B := A in fun (a : A) (e : eq1 A a) => - match e in (eq1 A0 B0 a0) return (P A0 a0) with + match e in (eq1 A0 a0) return (P A0 a0) with | refl1 => f end. @@ -64,3 +64,90 @@ Undo 2. Fail induction (S _) in |- * at 4. Abort. +(* Check use of "as" clause *) + +Inductive I := C : forall x, x<0 -> I -> I. + +Goal forall x:I, x=x. +intros. +induction x as [y * IHx]. +change (x = x) in IHx. (* We should have IHx:x=x *) +Abort. + +(* This was not working in 8.4 *) + +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros. +induction h. +2:change (n = h 1 -> n = h 2) in IHn. +Abort. + +(* This was not working in 8.4 *) + +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros h H H0. +induction h in H |- *. +Abort. + +(* "at" was not granted in 8.4 in the next two examples *) + +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros h H H0. +induction h in H at 2, H0 at 1. +change (h 0 = 0) in H. +Abort. + +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros h H H0. +Fail induction h in H at 2 |- *. (* Incompatible occurrences *) +Abort. + +(* Check generalization with dependencies in section variables *) + +Section S3. +Variables x : nat. +Definition cond := x = x. +Goal cond -> x = 0. +intros H. +induction x as [|n IHn]. +2:change (n = 0) in IHn. (* We don't want a generalization over cond *) +Abort. +End S3. + +(* These examples show somehow arbitrary choices of generalization wrt + to indices, when those indices are not linear. We check here 8.4 + compatibility: when an index is a subterm of a parameter of the + inductive type, it is not generalized. *) + +Inductive repr (x:nat) : nat -> Prop := reprc z : repr x z -> repr x z. + +Goal forall x, 0 = x -> repr x x -> True. +intros x H1 H. +induction H. +change True in IHrepr. +Abort. + +Goal forall x, 0 = S x -> repr (S x) (S x) -> True. +intros x H1 H. +induction H. +change True in IHrepr. +Abort. + +Inductive repr' (x:nat) : nat -> Prop := reprc' z : repr' x (S z) -> repr' x z. + +Goal forall x, 0 = x -> repr' x x -> True. +intros x H1 H. +induction H. +change True in IHrepr'. +Abort. + +(* In this case, generalization was done in 8.4 and we preserve it; this + is arbitrary choice *) + +Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z. + +Goal forall x, 0 = x -> repr'' x x -> True. +intros x H1 H. +induction H. +change (0 = z -> True) in IHrepr''. +Abort. diff --git a/test-suite/success/instantiate.v b/test-suite/success/instantiate.v deleted file mode 100644 index 4224405d..00000000 --- a/test-suite/success/instantiate.v +++ /dev/null @@ -1,11 +0,0 @@ -(* Test régression bug #1041 *) - -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). diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 3599da4d..9443d01e 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -3,5 +3,33 @@ Goal forall A, A -> True. intros _ _. +Abort. +(* This did not work until March 2013, because of underlying "red" *) +Goal (fun x => True -> True) 0. +intro H. +Abort. +(* This should still work, with "intro" calling "hnf" *) +Goal (fun f => True -> f 0 = f 0) (fun x => x). +intro H. +match goal with [ |- 0 = 0 ] => reflexivity end. +Abort. + +(* Somewhat related: This did not work until March 2013 *) +Goal (fun f => f 0 = f 0) (fun x => x). +hnf. +match goal with [ |- 0 = 0 ] => reflexivity end. +Abort. + +(* Fixing behavior of "*" and "**" in branches, so that they do not + introduce more than what the branch expects them to introduce at most *) +Goal forall n p, n + p = 0. +intros [|*]; intro p. +Abort. + +(* Check non-interference of "_" with name generation *) +Goal True -> True -> True. +intros _ ?. +exact H. +Qed. diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v new file mode 100644 index 00000000..bbe9d4bf --- /dev/null +++ b/test-suite/success/keyedrewrite.v @@ -0,0 +1,24 @@ +Set Keyed Unification. + +Section foo. +Variable f : nat -> nat. + +Definition g := f. + +Variable lem : g 0 = 0. + +Goal f 0 = 0. +Proof. + Fail rewrite lem. +Abort. + +Declare Equivalent Keys @g @f. +(** Now f and g are considered equivalent heads for subterm selection *) +Goal f 0 = 0. +Proof. + rewrite lem. + reflexivity. +Qed. + +Print Equivalent Keys. +End foo. diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v new file mode 100644 index 00000000..a183be62 --- /dev/null +++ b/test-suite/success/letproj.v @@ -0,0 +1,9 @@ +Set Primitive Projections. +Set Record Elimination Schemes. +Record Foo (A : Type) := { bar : A -> A; baz : A }. + +Definition test (A : Type) (f : Foo A) := + let (x, y) := f in x. + +Scheme foo_case := Case for Foo Sort Type. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index c2eb8bd7..badce063 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -1,6 +1,6 @@ (* The tactic language *) -(* Submitted by Pierre Crégut *) +(* Submitted by Pierre Crégut *) (* Checks substitution of x *) Ltac f x := unfold x; idtac. @@ -9,7 +9,7 @@ f plus. reflexivity. Qed. -(* Submitted by Pierre Crégut *) +(* Submitted by Pierre Crégut *) (* Check syntactic correctness *) Ltac F x := idtac; G x with G y := idtac; F y. @@ -143,7 +143,7 @@ Qed. Ltac check_binding y := cut ((fun y => y) = S). Goal True. -check_binding true. +check_binding ipattern:H. Abort. (* Check that variables explicitly parsed as ltac variables are not @@ -211,7 +211,7 @@ is. exact I. Abort. -(* Interférence entre espaces des noms *) +(* Interférence entre espaces des noms *) Ltac O := intro. Ltac Z1 t := set (x:=t). @@ -298,7 +298,3 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. - -(* Check that this returns an error and not an anomaly (see r13667) *) - -Fail Local Tactic Notation "myintro" := intro. diff --git a/test-suite/success/ltac_plus.v b/test-suite/success/ltac_plus.v new file mode 100644 index 00000000..8a08d646 --- /dev/null +++ b/test-suite/success/ltac_plus.v @@ -0,0 +1,12 @@ +(** Checks that Ltac's '+' tactical works as intended. *) + +Goal forall (A B C D:Prop), (A->C) -> (B->C) -> (D->C) -> B -> C. +Proof. + intros A B C D h0 h1 h2 h3. + (* backtracking *) + (apply h0 + apply h1);apply h3. + Undo. + Fail ((apply h0+apply h2) || apply h1); apply h3. + (* interaction with || *) + ((apply h0+apply h1) || apply h2); apply h3. +Qed.
\ No newline at end of file diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 05303f37..54cfa658 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v new file mode 100644 index 00000000..059462fa --- /dev/null +++ b/test-suite/success/namedunivs.v @@ -0,0 +1,102 @@ +(* Inductive paths {A} (x : A) : A -> Type := idpath : paths x x where "x = y" := (@paths _ x y) : type_scope. *) +(* Goal forall A B : Set, @paths Type A B -> @paths Set A B. *) +(* intros A B H. *) +(* Fail exact H. *) +(* Section . *) + +Section lift_strict. +Polymorphic Definition liftlt := + let t := Type@{i} : Type@{k} in + fun A : Type@{i} => A : Type@{k}. + +Polymorphic Definition liftle := + fun A : Type@{i} => A : Type@{k}. +End lift_strict. + + +Set Universe Polymorphism. + +(* Inductive option (A : Type) : Type := *) +(* | None : option A *) +(* | Some : A -> option A. *) + +Inductive option (A : Type@{i}) : Type@{i} := + | None : option A + | Some : A -> option A. + +Definition foo' {A : Type@{i}} (o : option@{i} A) : option@{i} A := + o. + +Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A := + o. + + +Definition testm (A : Type@{i}) : Type@{max(i,j)} := A. + +(* Inductive prod (A : Type@{i}) (B : Type@{j}) := *) +(* | pair : A -> B -> prod A B. *) + +(* Definition snd {A : Type@{i}} (B : Type@{j}) (p : prod A B) : B := *) +(* match p with *) +(* | pair _ _ a b => b *) +(* end. *) + +(* Definition snd' {A : Type@{i}} (B : Type@{i}) (p : prod A B) : B := *) +(* match p with *) +(* | pair _ _ a b => b *) +(* end. *) + +(* Inductive paths {A : Type} : A -> A -> Type := *) +(* | idpath (a : A) : paths a a. *) + +Inductive paths {A : Type@{i}} : A -> A -> Type@{i} := +| idpath (a : A) : paths a a. + +Definition Funext := + forall (A : Type) (B : A -> Type), + forall f g : (forall a, B a), (forall x : A, paths (f x) (g x)) -> paths f g. + +Definition paths_lift_closed (A : Type@{i}) (x y : A) : + paths x y -> @paths (liftle@{j Type} A) x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_lift (A : Type@{i}) (x y : A) : + paths x y -> paths@{j} x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_lift_closed_strict (A : Type@{i}) (x y : A) : + paths x y -> @paths (liftlt@{j Type} A) x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_downward_closed_le (A : Type@{i}) (x y : A) : + paths@{j} (A:=liftle@{i j} A) x y -> paths@{i} x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_downward_closed_lt (A : Type@{i}) (x y : A) : + @paths (liftlt@{j i} A) x y -> paths x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_downward_closed_lt_nolift (A : Type@{i}) (x y : A) : + paths@{j} x y -> paths x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition funext_downward_closed (F : Funext@{i' j' k'}) : + Funext@{i j k}. +Proof. + intros A B f g H. red in F. + pose (F A B f g (fun x => paths_lift _ _ _ (H x))). + apply paths_downward_closed_lt_nolift. apply p. +Defined. + diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v new file mode 100644 index 00000000..94ff96ef --- /dev/null +++ b/test-suite/success/paralleltac.v @@ -0,0 +1,46 @@ +Fixpoint fib n := match n with + | O => 1 + | S m => match m with + | O => 1 + | S o => fib o + fib m end end. +Ltac sleep n := + try (assert (fib n = S (fib n)) by reflexivity). +(* Tune that depending on your PC *) +Let time := 18. + +Axiom P : nat -> Prop. +Axiom P_triv : Type -> forall x, P x. +Ltac solve_P := + match goal with |- P (S ?X) => + sleep time; exact (P_triv Type _) + end. + +Lemma test_old x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T1: linear". +Time all: solve_P. +Qed. + +Lemma test_ok x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T2: parallel". +Time par: solve_P. +Qed. + +Lemma test_fail x : P (S x) /\ P x /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T3: linear failure". +Fail Time all: solve_P. +all: apply (P_triv Type). +Qed. + +Lemma test_fail2 x : P (S x) /\ P x /\ P (S x) /\ P (S x). +Proof. +repeat split. +idtac "T4: parallel failure". +Fail Time par: solve_P. +all: apply (P_triv Type). +Qed. diff --git a/test-suite/success/params_ind.v b/test-suite/success/params_ind.v deleted file mode 100644 index 1bee31c8..00000000 --- a/test-suite/success/params_ind.v +++ /dev/null @@ -1,4 +0,0 @@ -Inductive list (A : Set) : Set := - | nil : list A - | cons : A -> list (A -> A) -> list A. - diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 56cab0f6..9167c9fc 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -1,12 +1,294 @@ +Module withoutpoly. + +Inductive empty :=. + +Inductive emptyt : Type :=. +Inductive singleton : Type := + single. +Inductive singletoninfo : Type := + singleinfo : unit -> singletoninfo. +Inductive singletonset : Set := + singleset. + +Inductive singletonnoninfo : Type := + singlenoninfo : empty -> singletonnoninfo. + +Inductive singletoninfononinfo : Prop := + singleinfononinfo : unit -> singletoninfononinfo. + +Inductive bool : Type := + | true | false. + +Inductive smashedbool : Prop := + | trueP | falseP. +End withoutpoly. + +Set Universe Polymorphism. + +Inductive empty :=. +Inductive emptyt : Type :=. +Inductive singleton : Type := + single. +Inductive singletoninfo : Type := + singleinfo : unit -> singletoninfo. +Inductive singletonset : Set := + singleset. + +Inductive singletonnoninfo : Type := + singlenoninfo : empty -> singletonnoninfo. + +Inductive singletoninfononinfo : Prop := + singleinfononinfo : unit -> singletoninfononinfo. + +Inductive bool : Type := + | true | false. + +Inductive smashedbool : Prop := + | trueP | falseP. + +Section foo. + Let T := Type. + Inductive polybool : T := + | trueT | falseT. +End foo. + +Inductive list (A: Type) : Type := +| nil : list A +| cons : A -> list A -> list A. + +Module ftypSetSet. +Inductive ftyp : Type := + | Funit : ftyp + | Ffun : list ftyp -> ftyp + | Fref : area -> ftyp +with area : Type := + | Stored : ftyp -> area +. +End ftypSetSet. + + +Module ftypSetProp. +Inductive ftyp : Type := + | Funit : ftyp + | Ffun : list ftyp -> ftyp + | Fref : area -> ftyp +with area : Type := + | Stored : (* ftyp -> *)area +. +End ftypSetProp. + +Module ftypSetSetForced. +Inductive ftyp : Type := + | Funit : ftyp + | Ffun : list ftyp -> ftyp + | Fref : area -> ftyp +with area : Set (* Type *) := + | Stored : (* ftyp -> *)area +. +End ftypSetSetForced. + +Unset Universe Polymorphism. + +Set Printing Universes. +Module Easy. + + Polymorphic Inductive prod (A : Type) (B : Type) : Type := + pair : A -> B -> prod A B. + + Check prod nat nat. + Print Universes. + + + Polymorphic Inductive sum (A B:Type) : Type := + | inl : A -> sum A B + | inr : B -> sum A B. + Print sum. + Check (sum nat nat). + +End Easy. + +Section Hierarchy. + +Definition Type3 := Type. +Definition Type2 := Type : Type3. +Definition Type1 := Type : Type2. + +Definition id1 := ((forall A : Type1, A) : Type2). +Definition id2 := ((forall A : Type2, A) : Type3). +Definition id1' := ((forall A : Type1, A) : Type3). +Fail Definition id1impred := ((forall A : Type1, A) : Type1). + +End Hierarchy. + +Section structures. + +Record hypo : Type := mkhypo { + hypo_type : Type; + hypo_proof : hypo_type + }. + +Definition typehypo (A : Type) : hypo := {| hypo_proof := A |}. + +Polymorphic Record dyn : Type := + mkdyn { + dyn_type : Type; + dyn_proof : dyn_type + }. + +Definition monotypedyn (A : Type) : dyn := {| dyn_proof := A |}. +Polymorphic Definition typedyn (A : Type) : dyn := {| dyn_proof := A |}. + +Definition atypedyn : dyn := typedyn Type. + +Definition projdyn := dyn_type atypedyn. + +Definition nested := {| dyn_type := dyn; dyn_proof := atypedyn |}. + +Definition nested2 := {| dyn_type := dyn; dyn_proof := nested |}. + +Definition projnested2 := dyn_type nested2. + +Polymorphic Definition nest (d : dyn) := {| dyn_proof := d |}. + +Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d. + +End structures. + +Section cats. + Local Set Universe Polymorphism. + Require Import Utf8. + Definition fibration (A : Type) := A -> Type. + Definition Hom (A : Type) := A -> A -> Type. + + Record sigma (A : Type) (P : fibration A) := + { proj1 : A; proj2 : P proj1} . + + Class Identity {A} (M : Hom A) := + identity : ∀ x, M x x. + + Class Inverse {A} (M : Hom A) := + inverse : ∀ x y:A, M x y -> M y x. + + Class Composition {A} (M : Hom A) := + composition : ∀ {x y z:A}, M x y -> M y z -> M x z. + + Notation "g ° f" := (composition f g) (at level 50). + + Class Equivalence T (Eq : Hom T):= + { + Equivalence_Identity :> Identity Eq ; + Equivalence_Inverse :> Inverse Eq ; + Equivalence_Composition :> Composition Eq + }. + + Class EquivalenceType (T : Type) : Type := + { + m2: Hom T; + equiv_struct :> Equivalence T m2 }. + + Polymorphic Record cat (T : Type) := + { cat_hom : Hom T; + cat_equiv : forall x y, EquivalenceType (cat_hom x y) }. + + Definition catType := sigma Type cat. + + Notation "[ T ]" := (proj1 T). + + Require Import Program. + + Program Definition small_cat : cat Empty_set := + {| cat_hom x y := unit |}. + Next Obligation. + refine ({|m2:=fun x y => True|}). + constructor; red; intros; trivial. + Defined. + + Record iso (T U : Set) := + { f : T -> U; + g : U -> T }. + + Program Definition Set_cat : cat Set := + {| cat_hom := iso |}. + Next Obligation. + refine ({|m2:=fun x y => True|}). + constructor; red; intros; trivial. + Defined. + + Record isoT (T U : Type) := + { isoT_f : T -> U; + isoT_g : U -> T }. + + Program Definition Type_cat : cat Type := + {| cat_hom := isoT |}. + Next Obligation. + refine ({|m2:=fun x y => True|}). + constructor; red; intros; trivial. + Defined. + + Polymorphic Record cat1 (T : Type) := + { cat1_car : Type; + cat1_hom : Hom cat1_car; + cat1_hom_cat : forall x y, cat (cat1_hom x y) }. +End cats. + +Polymorphic Definition id {A : Type} (a : A) : A := a. + +Definition typeid := (@id Type). + + +Fail Check (Prop : Set). +Fail Check (Set : Set). +Check (Set : Type). +Check (Prop : Type). +Definition setType := $(let t := type of Set in exact t)$. + +Definition foo (A : Prop) := A. + +Fail Check foo Set. +Check fun A => foo A. +Fail Check fun A : Type => foo A. +Check fun A : Prop => foo A. +Fail Definition bar := fun A : Set => foo A. + +Fail Check (let A := Type in foo (id A)). + +Definition fooS (A : Set) := A. + +Check (let A := nat in fooS (id A)). +Fail Check (let A := Set in fooS (id A)). +Fail Check (let A := Prop in fooS (id A)). + (* Some tests of sort-polymorphisme *) Section S. -Variable A:Type. +Polymorphic Variable A:Type. (* Definition f (B:Type) := (A * B)%type. *) -Inductive I (B:Type) : Type := prod : A->B->I B. +Polymorphic Inductive I (B:Type) : Type := prod : A->B->I B. + +Check I nat. + End S. (* Check f nat nat : Set. *) -Check I nat nat : Set.
\ No newline at end of file +Definition foo' := I nat nat. +Print Universes. Print foo. Set Printing Universes. Print foo. + +(* Polymorphic axioms: *) +Polymorphic Axiom funext : forall (A B : Type) (f g : A -> B), + (forall x, f x = g x) -> f = g. + +(* Check @funext. *) +(* Check funext. *) + +Polymorphic Definition fun_ext (A B : Type) := + forall (f g : A -> B), + (forall x, f x = g x) -> f = g. + +Polymorphic Class Funext A B := extensional : fun_ext A B. + +Section foo2. + Context `{forall A B, Funext A B}. + Print Universes. +End foo2. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v new file mode 100644 index 00000000..068f8ac3 --- /dev/null +++ b/test-suite/success/primitiveproj.v @@ -0,0 +1,190 @@ +Set Primitive Projections. +Set Record Elimination Schemes. +Module Prim. + +Record F := { a : nat; b : a = a }. +Record G (A : Type) := { c : A; d : F }. + +Check c. +End Prim. +Module Univ. +Set Universe Polymorphism. +Set Implicit Arguments. +Record Foo (A : Type) := { foo : A }. + +Record G (A : Type) := { c : A; d : c = c; e : Foo A }. + +Definition Foon : Foo nat := {| foo := 0 |}. + +Definition Foonp : nat := Foon.(foo). + +Definition Gt : G nat := {| c:= 0; d:=eq_refl; e:= Foon |}. + +Check (Gt.(e)). + +Section bla. + + Record bar := { baz : nat; def := 0; baz' : forall x, x = baz \/ x = def }. +End bla. + +End Univ. + +Set Primitive Projections. +Unset Elimination Schemes. +Set Implicit Arguments. + +Check nat. + +(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *) +(* Parameter x : X nat. *) +(* Check x.(k). *) + +Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }. + +Parameter x:X nat. +Check (a x : forall _ : @eq nat (k x) (k x), X nat). +Check (b x : X nat). + +Inductive Y := { next : option Y }. + +Check _.(next) : option Y. +Lemma eta_ind (y : Y) : y = Build_Y y.(next). +Proof. reflexivity. Defined. + +Variable t : Y. + +Fixpoint yn (n : nat) (y : Y) : Y := + match n with + | 0 => t + | S n => {| next := Some (yn n y) |} + end. + +Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. +Proof. reflexivity. Defined. + + +(* + Rules for parsing and printing of primitive projections and their eta expansions. + If r : R A where R is a primitive record with implicit parameter A. + If p : forall {A} (r : R A) {A : Set}, list (A * B). +*) + +Record R {A : Type} := { p : forall {X : Set}, A * X }. +Arguments R : clear implicits. + +Record R' {A : Type} := { p' : forall X : Set, A * X }. +Arguments R' : clear implicits. + +Unset Printing All. + +Parameter r : R nat. + +Check (r.(p)). +Set Printing Projections. +Check (r.(p)). +Unset Printing Projections. +Set Printing All. +Check (r.(p)). +Unset Printing All. + +(* Check (r.(p)). + Elaborates to a primitive application, X arg implicit. + Of type nat * ?ex + No Printing All: p r + Set Printing Projections.: r.(p) + Printing All: r.(@p) ?ex + *) + +Check p r. +Set Printing Projections. +Check p r. +Unset Printing Projections. +Set Printing All. +Check p r. +Unset Printing All. + +Check p r (X:=nat). +Set Printing Projections. +Check p r (X:=nat). +Unset Printing Projections. +Set Printing All. +Check p r (X:=nat). +Unset Printing All. + +(* Same elaboration, printing for p r *) + +(** Explicit version of the primitive projection, under applied w.r.t implicit arguments + can be printed only using projection notation. r.(@p) *) +Check r.(@p _). +Set Printing Projections. +Check r.(@p _). +Unset Printing Projections. +Set Printing All. +Check r.(@p _). +Unset Printing All. + +(** Explicit version of the primitive projection, applied to its implicit arguments + can be printed using application notation r.(p), r.(@p) in fully explicit form *) +Check r.(@p _) nat. +Set Printing Projections. +Check r.(@p _) nat. +Unset Printing Projections. +Set Printing All. +Check r.(@p _) nat. +Unset Printing All. + +Parameter r' : R' nat. + +Check (r'.(p')). +Set Printing Projections. +Check (r'.(p')). +Unset Printing Projections. +Set Printing All. +Check (r'.(p')). +Unset Printing All. + +(* Check (r'.(p')). + Elaborates to a primitive application, X arg explicit. + Of type forall X : Set, nat * X + No Printing All: p' r' + Set Printing Projections.: r'.(p') + Printing All: r'.(@p') + *) + +Check p' r'. +Set Printing Projections. +Check p' r'. +Unset Printing Projections. +Set Printing All. +Check p' r'. +Unset Printing All. + +(* Same elaboration, printing for p r *) + +(** Explicit version of the primitive projection, under applied w.r.t implicit arguments + can be printed only using projection notation. r.(@p) *) +Check r'.(@p' _). +Set Printing Projections. +Check r'.(@p' _). +Unset Printing Projections. +Set Printing All. +Check r'.(@p' _). +Unset Printing All. + +(** Explicit version of the primitive projection, applied to its implicit arguments + can be printed only using projection notation r.(p), r.(@p) in fully explicit form *) +Check p' r' nat. +Set Printing Projections. +Check p' r' nat. +Unset Printing Projections. +Set Printing All. +Check p' r' nat. +Unset Printing All. + +Check (@p' nat). +Check p'. +Set Printing All. + +Check (@p' nat). +Check p'. +Unset Printing All. diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index bf302df4..dbbd57ae 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -65,3 +65,56 @@ End S1. Check (deep 3 4 : 3 = 4). Check (deep2 3 4 : 3 = 4). + +Section P1. + +Variable x : nat. +Variable y : nat. +Variable z : nat. + + +Collection TOTO := x y. + +Collection TITI := TOTO - x. + +Lemma t1 : True. Proof using TOTO. trivial. Qed. +Lemma t2 : True. Proof using TITI. trivial. Qed. + + Section P2. + Collection TOTO := x. + Lemma t3 : True. Proof using TOTO. trivial. Qed. + End P2. + +Lemma t4 : True. Proof using TOTO. trivial. Qed. + +End P1. + +Lemma t5 : True. Fail Proof using TOTO. trivial. Qed. + +Check (t1 1 2 : True). +Check (t2 1 : True). +Check (t3 1 : True). +Check (t4 1 2 : True). + + +Section T1. + +Variable x : nat. +Hypothesis px : 1 = x. +Let w := x + 1. + +Set Suggest Proof Using. + +Set Default Proof Using "Type". + +Lemma bla : 2 = w. +Proof. +admit. +Qed. + +End T1. + +Check (bla 7 : 2 = 8). + + + diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 4d743a6d..1e667884 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -62,14 +62,14 @@ Abort. Goal (forall n : nat, n = 0 -> Prop) -> Prop. intro P. refine (P _ _). -reflexivity. +2:reflexivity. Abort. (* Submitted by Jacek Chrzaszcz (bug #1102) *) -(* le problème a été résolu ici par normalisation des evars présentes - dans les types d'evars, mais le problème reste a priori ouvert dans - le cas plus général d'evars non instanciées dans les types d'autres +(* le problème a été résolu ici par normalisation des evars présentes + dans les types d'evars, mais le problème reste a priori ouvert dans + le cas plus général d'evars non instanciées dans les types d'autres evars *) Goal exists n:nat, n=n. @@ -84,7 +84,7 @@ Definition div : refine (fun m div_rec n => match div_rec m n with - | exist _ _ => _ + | exist _ _ _ => _ end). Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 08c406be..6dcd6592 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -129,3 +129,22 @@ intros. Fail rewrite H in H0. Abort. +(* Test subst in the presence of a dependent let-in *) +(* Was not working prior to May 2014 *) + +Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x. +intros. +subst x. (* was failing *) +subst z. +rewrite H0. +auto with arith. +Qed. + +(* Check that evars are instantiated when the term to rewrite is + closed, like in the case it is open *) + +Goal exists x, S 0 = 0 -> S x = 0. +eexists. intro H. +rewrite H. +reflexivity. +Abort. diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v new file mode 100644 index 00000000..fe250ae8 --- /dev/null +++ b/test-suite/success/rewrite_dep.v @@ -0,0 +1,33 @@ +Require Import Setoid. +Require Import Morphisms. +Require Vector. +Notation vector := Vector.t. +Notation Vcons n t := (@Vector.cons _ n _ t). + +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Instance vecequiv A `{Equiv A} n : Equiv (vector A n). +admit. +Qed. + +Global Instance vcons_proper A `{Equiv A} `{!Setoid A} : + Proper (equiv ==> forall_relation (fun k => equiv ==> equiv)) + (@Vector.cons A). +Proof. Admitted. + +Instance vecseotid A `{Setoid A} n : Setoid (vector A n). +Proof. Admitted. + +(* Instance equiv_setoid A {e : Equiv A} {s : @Setoid A e} : Equivalence e. *) +(* apply setoid_equiv. *) +(* Qed. *) +(* Typeclasses Transparent Equiv. *) + +Goal forall A `{Equiv A} `{!Setoid A} (f : A -> A) (a b : A) (H : equiv a b) n (v : vector A n), + equiv (Vcons a v) (Vcons b v). +Proof. + intros. + rewrite H0. + reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v new file mode 100644 index 00000000..04c67556 --- /dev/null +++ b/test-suite/success/rewrite_strat.v @@ -0,0 +1,53 @@ +Require Import Setoid. + +Variable X : Set. + +Variable f : X -> X. +Variable g : X -> X -> X. +Variable h : nat -> X -> X. + +Variable lem0 : forall x, f (f x) = f x. +Variable lem1 : forall x, g x x = f x. +Variable lem2 : forall n x, h (S n) x = g (h n x) (h n x). +Variable lem3 : forall x, h 0 x = x. + +Hint Rewrite lem0 lem1 lem2 lem3 : rew. + +Goal forall x, h 10 x = f x. +Proof. + intros. + Time autorewrite with rew. (* 0.586 *) + reflexivity. +Time Qed. (* 0.53 *) + +Goal forall x, h 6 x = f x. +intros. + Time rewrite_strat topdown lem2. + Time rewrite_strat topdown lem1. + Time rewrite_strat topdown lem0. + Time rewrite_strat topdown lem3. + reflexivity. +Undo 5. + Time rewrite_strat topdown (choice lem2 lem1). + Time rewrite_strat topdown (choice lem0 lem3). + reflexivity. +Undo 3. + Time rewrite_strat (topdown (choice lem2 lem1); topdown (choice lem0 lem3)). + reflexivity. +Undo 2. + Time rewrite_strat (topdown (choice lem2 (choice lem1 (choice lem0 lem3)))). + reflexivity. +Undo 2. + Time rewrite_strat (topdown (choice lem2 (choice lem1 (choice lem0 lem3)))). + reflexivity. +Qed. + +Goal forall x, h 10 x = f x. +Proof. + intros. + Time rewrite_strat topdown (hints rew). (* 0.38 *) + reflexivity. +Time Qed. (* 0.06 s *) + +Set Printing All. +Set Printing Depth 100000.
\ No newline at end of file diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 653b5bf9..be0d49e0 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -153,7 +153,7 @@ End mult. does not fix the instance at the first unification, use [at], or simply rewrite for this semantics. *) -Require Import Arith. +Parameter beq_nat : forall x y : nat, bool. Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}. Instance: Foo nat. admit. Defined. diff --git a/test-suite/success/setoid_unif.v b/test-suite/success/setoid_unif.v new file mode 100644 index 00000000..912596b4 --- /dev/null +++ b/test-suite/success/setoid_unif.v @@ -0,0 +1,27 @@ +(* An example of unification in rewrite which uses eager substitution + of metas (provided by Pierre-Marie). + + Put in the test suite as an indication of what the use metas + eagerly flag provides, even though the concrete cases that use it + are seldom. Today supported thanks to a new flag for using evars + eagerly, after this variant of setoid rewrite started to use clause + environments based on evars (fbbe491cfa157da627) *) + +Require Import Setoid. + +Parameter elt : Type. +Parameter T : Type -> Type. +Parameter empty : forall A, T A. +Parameter MapsTo : forall A : Type, elt -> A -> T A -> Prop. + +(* Definition In A x t := exists e, MapsTo A x e t. *) +Axiom In : forall A, A -> T A -> Prop. +Axiom foo : forall A x, In A x (empty A) <-> False. + +Record R := { t : T unit; s : unit }. +Definition Empty := {| t := empty unit; s := tt |}. + +Goal forall x, ~ In _ x (t Empty). +Proof. +intros x. +rewrite foo. diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 271e6ef7..b5330779 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -45,3 +45,55 @@ Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i. simpl. admit. Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *) + +(* Check that maximally inserted arguments do not break interpretation + of references in simpl, vm_compute etc. *) + +Arguments fst {A} {B} p. + +Goal fst (0,0) = 0. +simpl fst. +Fail set (fst _). +Abort. + +Goal fst (0,0) = 0. +vm_compute fst. +Fail set (fst _). +Abort. + +Goal let f x := x + 0 in f 0 = 0. +intro. +vm_compute f. +Fail set (f _). +Abort. + +(* This is a change wrt 8.4 (waiting to know if it breaks script a lot or not)*) + +Goal 0+0=0. +Fail simpl @eq. +Abort. + +(* Check reference by notation in simpl *) + +Goal 0+0 = 0. +simpl "+". +Fail set (_ + _). +Abort. + +(* Check occurrences *) + +Record box A := Box { unbox : A }. + +Goal unbox _ (unbox _ (unbox _ (Box _ (Box _ (Box _ True))))) = + unbox _ (unbox _ (unbox _ (Box _ (Box _ (Box _ True))))). +simpl (unbox _ (unbox _ _)) at 1. +match goal with |- True = unbox _ (unbox _ (unbox _ (Box _ (Box _ (Box _ True))))) => idtac end. +Undo 2. +Fail simpl (unbox _ (unbox _ _)) at 5. +simpl (unbox _ (unbox _ _)) at 1 4. +match goal with |- True = unbox _ (Box _ True) => idtac end. +Undo 2. +Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *) +simpl (unbox _ (unbox _ _)) at 2 4. +match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end. +Abort. diff --git a/test-suite/success/somatching.v b/test-suite/success/somatching.v new file mode 100644 index 00000000..5ed833ec --- /dev/null +++ b/test-suite/success/somatching.v @@ -0,0 +1,64 @@ +Goal forall A B C (p : forall (x : A) (y : B), C x y) (x : A) (y : B), True. +Proof. + intros A B C p x y. + match type of p with + | forall x y, @?F x y => pose F as C1 + end. + match type of p with + | forall x y, @?F y x => pose F as C2 + end. + assert (C1 x y) as ?. + assert (C2 y x) as ?. +Abort. + +Goal forall A B C D (p : forall (x : A) (y : B) (z : C), D x y) (x : A) (y : B), True. +Proof. + intros A B C D p x y. + match type of p with + | forall x y z, @?F x y => pose F as C1 + end. + assert (C1 x y) as ?. +Abort. + +Goal forall A B C D (p : forall (z : C) (x : A) (y : B), D x y) (x : A) (y : B), True. +Proof. + intros A B C D p x y. + match type of p with + | forall z x y, @?F x y => pose F as C1 + end. + assert (C1 x y) as ?. +Abort. + +(** Those should fail *) + +Goal forall A B C (p : forall (x : A) (y : B), C x y) (x : A) (y : B), True. +Proof. + intros A B C p x y. + Fail match type of p with + | forall x, @?F x y => pose F as C1 + end. + Fail match type of p with + | forall x y, @?F x x y => pose F as C1 + end. + Fail match type of p with + | forall x y, @?F x => pose F as C1 + end. +Abort. + +(** This one is badly typed *) + +Goal forall A (B : A -> Type) (C : forall x, B x -> Type), (forall x y, C x y) -> True. +Proof. +intros A B C p. +Fail match type of p with +| forall x y, @?F y x => idtac +end. +Abort. + +Goal forall A (B : A -> Type) (C : Type) (D : forall x, B x -> Type), (forall x (z : C) y, D x y) -> True. +Proof. +intros A B C D p. +match type of p with +| forall x z y, @?F x y => idtac +end. +Abort. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index c067eb81..2954e255 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index 42e32ccc..50a65310 100644 --- a/test-suite/success/unicode_utf8.v +++ b/test-suite/success/unicode_utf8.v @@ -11,11 +11,12 @@ Parameter Ï€ : â„. (** Check indices *) Definition test_indices : nat -> nat := fun xâ‚ => xâ‚. -Definition π₂ := snd. +Definition π₂ := @snd. (** More unicode in identifiers *) Definition αβ_áà _×ב := 0. +Notation "C 'áµ’áµ–'" := C (at level 30). (** UNICODE IN STRINGS *) diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 997dceb4..296686e1 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -1,3 +1,7 @@ +Let test_stack_unification_interaction_with_delta A + : (if negb _ then true else false) = if orb false (negb A) then true else false + := eq_refl. + (* Test patterns unification *) Lemma l1 : (forall P, (exists x:nat, P x) -> False) @@ -97,7 +101,7 @@ apply H. Qed. (* Feature deactivated in commit 14189 (see commit log) -(* Test instanciation of evars by unification *) +(* Test instantiation of evars by unification *) Goal (forall x, 0 + x = 0 -> True) -> True. intros; eapply H. diff --git a/test-suite/success/univscompute.v b/test-suite/success/univscompute.v new file mode 100644 index 00000000..1d60ab36 --- /dev/null +++ b/test-suite/success/univscompute.v @@ -0,0 +1,32 @@ +Set Universe Polymorphism. + +Polymorphic Definition id {A : Type} (a : A) := a. + +Eval vm_compute in id 1. + +Polymorphic Inductive ind (A : Type) := cons : A -> ind A. + +Eval vm_compute in ind unit. + +Check ind unit. + +Eval vm_compute in ind unit. + +Definition bar := Eval vm_compute in ind unit. +Definition bar' := Eval vm_compute in id (cons _ tt). + +Definition bar'' := Eval native_compute in id 1. +Definition bar''' := Eval native_compute in id (cons _ tt). + +Definition barty := Eval native_compute in id (cons _ Set). + +Definition one := @id. + +Monomorphic Definition sec := one. + +Eval native_compute in sec. +Definition sec' := Eval native_compute in sec. +Eval vm_compute in sec. +Definition sec'' := Eval vm_compute in sec. + + |