diff options
Diffstat (limited to 'test-suite/output')
175 files changed, 7512 insertions, 0 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out new file mode 100644 index 0000000000..7074ad2d41 --- /dev/null +++ b/test-suite/output/Arguments.out @@ -0,0 +1,117 @@ +Nat.sub : nat -> nat -> nat + +Nat.sub is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +The reduction tactics unfold Nat.sub but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat + +Nat.sub is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +The reduction tactics unfold Nat.sub when applied to 1 argument + but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat + +Nat.sub is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +The reduction tactics unfold Nat.sub + when the 1st argument evaluates to a constructor and + when applied to 1 argument but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat + +Nat.sub is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor and when applied to 2 arguments +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat + +Nat.sub is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +pf : +forall D1 C1 : Type, +(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 + +pf is not universe polymorphic +Arguments D2, C2 are implicit +Arguments D1, C1 are implicit and maximally inserted +Argument scopes are [foo_scope type_scope _ _ _ _ _] +The reduction tactics never unfold pf +pf is transparent +Expands to: Constant Arguments.pf +fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C + +fcomp is not universe polymorphic +Arguments A, B, C are implicit and maximally inserted +Argument scopes are [type_scope type_scope type_scope _ _ _] +The reduction tactics unfold fcomp when applied to 6 arguments +fcomp is transparent +Expands to: Constant Arguments.fcomp +volatile : nat -> nat + +volatile is not universe polymorphic +Argument scope is [nat_scope] +The reduction tactics always unfold volatile +volatile is transparent +Expands to: Constant Arguments.volatile +f : T1 -> T2 -> nat -> unit -> nat -> nat + +f is not universe polymorphic +Argument scopes are [_ _ nat_scope _ nat_scope] +f is transparent +Expands to: Constant Arguments.S1.S2.f +f : T1 -> T2 -> nat -> unit -> nat -> nat + +f is not universe polymorphic +Argument scopes are [_ _ nat_scope _ nat_scope] +The reduction tactics unfold f when the 3rd, 4th and + 5th arguments evaluate to a constructor +f is transparent +Expands to: Constant Arguments.S1.S2.f +f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat + +f is not universe polymorphic +Argument T2 is implicit +Argument scopes are [type_scope _ _ nat_scope _ nat_scope] +The reduction tactics unfold f when the 4th, 5th and + 6th arguments evaluate to a constructor +f is transparent +Expands to: Constant Arguments.S1.f +f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat + +f is not universe polymorphic +Arguments T1, T2 are implicit +Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor +f is transparent +Expands to: Constant Arguments.f + = forall v : unit, f 0 0 5 v 3 = 2 + : Prop + = 2 = 2 + : Prop +f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat + +f is not universe polymorphic +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor +f is transparent +Expands to: Constant Arguments.f +forall w : r, w 3 true = tt + : Prop +The command has indeed failed with message: +Unknown interpretation for notation "$". +w 3 true = tt + : Prop +The command has indeed failed with message: +Extra arguments: _, _. diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v new file mode 100644 index 0000000000..844f96aaa1 --- /dev/null +++ b/test-suite/output/Arguments.v @@ -0,0 +1,57 @@ +(* coq-prog-args: ("-top" "Arguments") *) +Arguments Nat.sub n m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub n / m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub !n / m : simpl nomatch. +About Nat.sub. +Arguments Nat.sub !n !m /. +About Nat.sub. +Arguments Nat.sub !n !m. +About Nat.sub. +Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := + fun x => (f (fst x), g (snd x)). +Declare Scope foo_scope. +Declare Scope bar_scope. +Delimit Scope foo_scope with F. +Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. +About pf. +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). +Arguments fcomp {_ _ _}%type_scope f g x /. +About fcomp. +Definition volatile := fun x : nat => x. +Arguments volatile / _. +About volatile. +Set Implicit Arguments. +Section S1. +Variable T1 : Type. +Section S2. +Variable T2 : Type. +Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat := + match n, m with + | 0,_ => 0 + | S _, 0 => n + | S n', S m' => f x y n' v m' end. +About f. +Global Arguments f x y !n !v !m. +About f. +End S2. +About f. +End S1. +About f. +Eval cbn in forall v, f 0 0 5 v 3 = 2. +Eval cbn in f 0 0 5 tt 3 = 2. +Arguments f : clear implicits and scopes. +About f. +Record r := { pi :> nat -> bool -> unit }. +Notation "$" := 3 (only parsing) : foo_scope. +Notation "$" := true (only parsing) : bar_scope. +Delimit Scope bar_scope with B. +Arguments pi _ _%F _%B. +Check (forall w : r, pi w $ $ = tt). +Fail Check (forall w : r, w $ $ = tt). +Axiom w : r. +Arguments w x%F y%B : extra scopes. +Check (w $ $ = tt). +Fail Arguments w _%F _%B. + diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out new file mode 100644 index 0000000000..69ba329ff1 --- /dev/null +++ b/test-suite/output/ArgumentsScope.out @@ -0,0 +1,70 @@ +a : bool -> bool + +a is not universe polymorphic +Argument scope is [bool_scope] +Expands to: Variable a +b : bool -> bool + +b is not universe polymorphic +Argument scope is [bool_scope] +Expands to: Variable b +negb'' : bool -> bool + +negb'' is not universe polymorphic +Argument scope is [bool_scope] +negb'' is transparent +Expands to: Constant ArgumentsScope.A.B.negb'' +negb' : bool -> bool + +negb' is not universe polymorphic +Argument scope is [bool_scope] +negb' is transparent +Expands to: Constant ArgumentsScope.A.negb' +negb : bool -> bool + +negb is not universe polymorphic +Argument scope is [bool_scope] +negb is transparent +Expands to: Constant Coq.Init.Datatypes.negb +a : bool -> bool + +a is not universe polymorphic +Expands to: Variable a +b : bool -> bool + +b is not universe polymorphic +Expands to: Variable b +negb : bool -> bool + +negb is not universe polymorphic +negb is transparent +Expands to: Constant Coq.Init.Datatypes.negb +negb' : bool -> bool + +negb' is not universe polymorphic +negb' is transparent +Expands to: Constant ArgumentsScope.A.negb' +negb'' : bool -> bool + +negb'' is not universe polymorphic +negb'' is transparent +Expands to: Constant ArgumentsScope.A.B.negb'' +a : bool -> bool + +a is not universe polymorphic +Expands to: Variable a +negb : bool -> bool + +negb is not universe polymorphic +negb is transparent +Expands to: Constant Coq.Init.Datatypes.negb +negb' : bool -> bool + +negb' is not universe polymorphic +negb' is transparent +Expands to: Constant ArgumentsScope.negb' +negb'' : bool -> bool + +negb'' is not universe polymorphic +negb'' is transparent +Expands to: Constant ArgumentsScope.negb'' diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v new file mode 100644 index 0000000000..ec49d85161 --- /dev/null +++ b/test-suite/output/ArgumentsScope.v @@ -0,0 +1,30 @@ +(* coq-prog-args: ("-top" "ArgumentsScope") *) +(* A few tests to check Global Argument Scope command *) + +Section A. +Variable a : bool -> bool. +Definition negb' := negb. +Section B. +Variable b : bool -> bool. +Definition negb'' := negb. +About a. +About b. +About negb''. +About negb'. +About negb. +Global Arguments negb'' _ : clear scopes. +Global Arguments negb' _ : clear scopes. +Global Arguments negb _ : clear scopes. +Global Arguments a _ : clear scopes. +Global Arguments b _ : clear scopes. +About a. +About b. +About negb. +About negb'. +About negb''. +End B. +About a. +End A. +About negb. +About negb'. +About negb''. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out new file mode 100644 index 0000000000..583ea0cb43 --- /dev/null +++ b/test-suite/output/Arguments_renaming.out @@ -0,0 +1,122 @@ +The command has indeed failed with message: +Flag "rename" expected to rename A into B. +File "stdin", line 3, characters 0-25: +Warning: This command is just asserting the names of arguments of identity. +If this is what you want add ': assert' to silence the warning. If you want +to clear implicit arguments add ': clear implicits'. If you want to clear +notation scopes add ': clear scopes' [arguments-assert,vernacular] +@eq_refl + : forall (B : Type) (y : B), y = y +eq_refl + : ?y = ?y +where +?y : [ |- nat] +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq_refl: Arguments are renamed to B, y +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments B, y are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument B is implicit +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] +eq_refl : forall (A : Type) (x : A), x = x + +eq_refl is not universe polymorphic +Arguments are renamed to B, y +When applied to no arguments: + Arguments B, y are implicit and maximally inserted +When applied to 1 argument: + Argument B is implicit +Argument scopes are [type_scope _] +Expands to: Constructor Coq.Init.Logic.eq_refl +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x + +For myrefl: Arguments are renamed to C, x, _ +For myrefl: Argument C is implicit and maximally inserted +For myEq: Argument scopes are [type_scope _ _] +For myrefl: Argument scopes are [type_scope _ _] +myrefl : forall (B : Type) (x : A), B -> myEq B x x + +myrefl is not universe polymorphic +Arguments are renamed to C, x, _ +Argument C is implicit and maximally inserted +Argument scopes are [type_scope _ _] +Expands to: Constructor Arguments_renaming.Test1.myrefl +myplus = +fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S n' => S (myplus T t n' m) + end + : forall T : Type, T -> nat -> nat -> nat + +myplus is not universe polymorphic +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +myplus : forall T : Type, T -> nat -> nat -> nat + +myplus is not universe polymorphic +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor +myplus is transparent +Expands to: Constant Arguments_renaming.Test1.myplus +@myplus + : forall Z : Type, Z -> nat -> nat -> nat +Inductive myEq (A B : Type) (x : A) : A -> Prop := + myrefl : B -> myEq A B x x + +For myrefl: Arguments are renamed to A, C, x, _ +For myrefl: Argument C is implicit and maximally inserted +For myEq: Argument scopes are [type_scope type_scope _ _] +For myrefl: Argument scopes are [type_scope type_scope _ _] +myrefl : forall (A B : Type) (x : A), B -> myEq A B x x + +myrefl is not universe polymorphic +Arguments are renamed to A, C, x, _ +Argument C is implicit and maximally inserted +Argument scopes are [type_scope type_scope _ _] +Expands to: Constructor Arguments_renaming.myrefl +myrefl + : forall (A C : Type) (x : A), C -> myEq A C x x +myplus = +fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S n' => S (myplus T t n' m) + end + : forall T : Type, T -> nat -> nat -> nat + +myplus is not universe polymorphic +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +myplus : forall T : Type, T -> nat -> nat -> nat + +myplus is not universe polymorphic +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor +myplus is transparent +Expands to: Constant Arguments_renaming.myplus +@myplus + : forall Z : Type, Z -> nat -> nat -> nat +The command has indeed failed with message: +Argument lists should agree on the names they provide. +The command has indeed failed with message: +Sequences of implicit arguments must be of different lengths. +The command has indeed failed with message: +Some argument names are duplicated: F +The command has indeed failed with message: +Argument z cannot be declared implicit. +The command has indeed failed with message: +Extra arguments: y. +The command has indeed failed with message: +Flag "rename" expected to rename A into R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v new file mode 100644 index 0000000000..9713a9dbbe --- /dev/null +++ b/test-suite/output/Arguments_renaming.v @@ -0,0 +1,55 @@ +(* coq-prog-args: ("-top" "Arguments_renaming") *) +Fail Arguments eq_refl {B y}, [B] y. +Arguments identity A _ _. +Arguments eq_refl A x : assert. +Arguments eq_refl {B y}, [B] y : rename. + +Check @eq_refl. +Check (eq_refl (B := nat)). +Print eq_refl. +About eq_refl. + +Goal 3 = 3. +apply @eq_refl with (B := nat). +Undo. +apply @eq_refl with (y := 3). +Undo. +pose (y := nat). +apply (@eq_refl y) with (y0 := 3). +Qed. + +Section Test1. + +Variable A : Type. + +Inductive myEq B (x : A) : A -> Prop := myrefl : B -> myEq B x x. + +Global Arguments myrefl {C} x _ : rename. +Print myrefl. +About myrefl. + +Fixpoint myplus T (t : T) (n m : nat) {struct n} := + match n with O => m | S n' => S (myplus T t n' m) end. + +Global Arguments myplus {Z} !t !n m : rename. + +Print myplus. +About myplus. +Check @myplus. + +End Test1. +Print myrefl. +About myrefl. +Check myrefl. + +Print myplus. +About myplus. +Check @myplus. + +Fail Arguments eq_refl {F g}, [H] k. +Fail Arguments eq_refl {F}, [F] : rename. +Fail Arguments eq_refl {F F}, [F] F : rename. +Fail Arguments eq {F} x [z] : rename. +Fail Arguments eq {F} x z y. +Fail Arguments eq {R} s t. + diff --git a/test-suite/output/BadOptionValueType.out b/test-suite/output/BadOptionValueType.out new file mode 100644 index 0000000000..34d8518a75 --- /dev/null +++ b/test-suite/output/BadOptionValueType.out @@ -0,0 +1,8 @@ +The command has indeed failed with message: +Bad type of value for this option: expected int, got string. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got string. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got int. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got int. diff --git a/test-suite/output/BadOptionValueType.v b/test-suite/output/BadOptionValueType.v new file mode 100644 index 0000000000..b61c3757ba --- /dev/null +++ b/test-suite/output/BadOptionValueType.v @@ -0,0 +1,4 @@ +Fail Set Default Timeout "2". +Fail Set Debug Eauto "yes". +Fail Set Debug Eauto 1. +Fail Set Implicit Arguments 1. diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out new file mode 100644 index 0000000000..6e27837b26 --- /dev/null +++ b/test-suite/output/Binder.out @@ -0,0 +1,12 @@ +foo = fun '(x, y) => x + y + : nat * nat -> nat + +foo is not universe polymorphic +forall '(a, b), a /\ b + : Prop +foo = λ '(x, y), x + y + : nat * nat → nat + +foo is not universe polymorphic +∀ '(a, b), a ∧ b + : Prop diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v new file mode 100644 index 0000000000..9aced9f665 --- /dev/null +++ b/test-suite/output/Binder.v @@ -0,0 +1,7 @@ +Definition foo '(x,y) := x + y. +Print foo. +Check forall '(a,b), a /\ b. + +Require Import Utf8. +Print foo. +Check forall '(a,b), a /\ b. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out new file mode 100644 index 0000000000..efcc299e82 --- /dev/null +++ b/test-suite/output/Cases.out @@ -0,0 +1,181 @@ +t_rect = +fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => +fix F (t : t) : P t := + match t as t0 return (P t0) with + | k _ x0 => f x0 (F x0) + end + : forall P : t -> Type, + (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t + +t_rect is not universe polymorphic +Argument scopes are [function_scope function_scope _] + = fun d : TT => match d with + | {| f3 := b |} => b + end + : TT -> 0 = 0 + = fun d : TT => match d with + | {| f3 := b |} => b + end + : TT -> 0 = 0 +proj = +fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => +match Nat.eq_dec x y with +| left eqprf => match eqprf in (_ = z) return (P z) with + | eq_refl => def + end +| right _ => prf +end + : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y + +proj is not universe polymorphic +Argument scopes are [nat_scope nat_scope function_scope _ _] +foo = +fix foo (A : Type) (l : list A) {struct l} : option A := + match l with + | nil => None + | x0 :: nil => Some x0 + | x0 :: (_ :: _) as l0 => foo A l0 + end + : forall A : Type, list A -> option A + +foo is not universe polymorphic +Argument scopes are [type_scope list_scope] +uncast = +fun (A : Type) (x : I A) => match x with + | x0 <: _ => x0 + end + : forall A : Type, I A -> A + +uncast is not universe polymorphic +Argument scopes are [type_scope _] +foo' = if A 0 then true else false + : bool + +foo' is not universe polymorphic +f = +fun H : B => +match H with +| AC x => + let b0 := b in + (if b0 as b return (P b -> True) + then fun _ : P true => Logic.I + else fun _ : P false => Logic.I) x +end + : B -> True + +f is not universe polymorphic +The command has indeed failed with message: +Non exhaustive pattern-matching: no clause found for pattern +gadtTy _ _ +The command has indeed failed with message: +In environment +texpDenote : forall t : type, texp t -> typeDenote t +t : type +e : texp t +n : nat +The term "n" has type "nat" while it is expected to have type + "typeDenote ?t@{t1:=Nat}". +fun '{{n, m, _}} => n + m + : J -> nat +fun '{{n, m, p}} => n + m + p + : J -> nat +fun '(D n m p q) => n + m + p + q + : J -> nat +The command has indeed failed with message: +The constructor D (in type J) expects 3 arguments. +lem1 = +fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl + : forall k : nat * nat, k = k + +lem1 is not universe polymorphic +lem2 = +fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl + : forall k : bool, k = k + +lem2 is not universe polymorphic +Argument scope is [bool_scope] +lem3 = +fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl + : forall k : nat * nat, k = k + +lem3 is not universe polymorphic +1 subgoal + + x : nat + n, n0 := match x + 0 with + | 0 | S _ => 0 + end : nat + e, + e0 := match x + 0 as y return (y = y) with + | 0 => eq_refl + | S n => eq_refl + end : x + 0 = x + 0 + n1, n2 := match x with + | 0 | S _ => 0 + end : nat + e1, e2 := match x return (x = x) with + | 0 => eq_refl + | S n => eq_refl + end : x = x + ============================ + x + 0 = 0 +1 subgoal + + p : nat + a, + a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with + | eq_refl => conj eq_refl eq_refl + end : eq_refl = eq_refl /\ p = p + a1, + a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with + | eq_refl => conj eq_refl eq_refl + end : p = p /\ p = p + ============================ + eq_refl = eq_refl +fun x : comparison => match x with + | Eq => 1 + | _ => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt => 0 + | Gt => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt | Gt => 0 + end + : comparison -> nat +fun x : comparison => +match x return nat with +| Eq => S O +| Lt => O +| Gt => O +end + : forall _ : comparison, nat +fun x : K => match x with + | a3 | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a3 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a3 | a4 => 3 + | _ => 2 + end + : K -> nat +The command has indeed failed with message: +Pattern "S _, _" is redundant in this clause. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v new file mode 100644 index 0000000000..4e949dcb04 --- /dev/null +++ b/test-suite/output/Cases.v @@ -0,0 +1,225 @@ +(* Cases with let-in in constructors types *) + +Unset Printing Allow Match Default Clause. + +Inductive t : Set := + k : let x := t in x -> x. + +Print t_rect. + +Record TT : Type := CTT { f1 := 0 : nat; f2: nat; f3 : f1=f1 }. + +Eval cbv in fun d:TT => match d return 0 = 0 with CTT a _ b => b end. +Eval lazy in fun d:TT => match d return 0 = 0 with CTT a _ b => b end. + +(* Do not contract nested patterns with dependent return type *) +(* see bug #1699 *) + +Require Import Arith. + +Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y := + match eq_nat_dec x y return P y with + | left eqprf => + match eqprf in (_ = z) return (P z) with + | refl_equal => def + end + | _ => prf + end. + +Print proj. + +(* Use notations even below aliases *) + +Require Import List. + +Fixpoint foo (A:Type) (l:list A) : option A := + match l with + | nil => None + | x0 :: nil => Some x0 + | x0 :: (x1 :: xs) as l0 => foo A l0 + end. + +Print foo. + +(* Accept and use notation with binded parameters *) + +#[universes(template)] +Inductive I (A: Type) : Type := C : A -> I A. +Notation "x <: T" := (C T x) (at level 38). + +Definition uncast A (x : I A) := +match x with + | x <: _ => x +end. + +Print uncast. + +(* Do not duplicate the matched term *) + +Axiom A : nat -> bool. + +Definition foo' := + match A 0 with + | true => true + | x => x + end. + +Print foo'. + +(* Was bug #3293 (eta-expansion at "match" printing time was failing because + of let-in's interpreted as being part of the expansion) *) + +Axiom b : bool. +Axiom P : bool -> Prop. +Inductive B : Prop := AC : P b -> B. +Definition f : B -> True. + +Proof. +intros [x]. +destruct b as [|] ; exact Logic.I. +Defined. + +Print f. + +(* Was enhancement request #5142 (error message reported on the most + general return clause heuristic) *) + +#[universes(template)] +Inductive gadt : Type -> Type := +| gadtNat : nat -> gadt nat +| gadtTy : forall T, T -> gadt T. + +Fail Definition gadt_id T (x: gadt T) : gadt T := + match x with + | gadtNat n => gadtNat n + end. + +(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *) + +Inductive type:Set:=Nat. +Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat. +Inductive texp:type->Set:= + |TNConst:nat->texp Nat + |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t. +Definition typeDenote(t:type):Set:= match t with Nat => nat end. + +(* We expect a failure on TBinop *) +Fail Fixpoint texpDenote t (e:texp t):typeDenote t:= + match e with + | TNConst n => n + | TBinop t1 t2 _ b e1 e2 => O + end. + +(* Test notations with local definitions in constructors *) + +Inductive J := D : forall n m, let p := n+m in nat -> J. +Notation "{{ n , m , q }}" := (D n m q). + +Check fun x : J => let '{{n, m, _}} := x in n + m. +Check fun x : J => let '{{n, m, p}} := x in n + m + p. + +(* Cannot use the notation because of the dependency in p *) + +Check fun x => let '(D n m p q) := x in n+m+p+q. + +(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *) + +Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. + +(* Test use of idents bound to ltac names in a "match" *) + +Lemma lem1 : forall k, k=k :>nat * nat. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end). +Qed. +Print lem1. + +Lemma lem2 : forall k, k=k :> bool. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k => if k as x return x = x then eq_refl else eq_refl). +Qed. +Print lem2. + +Lemma lem3 : forall k, k=k :>nat * nat. +let x := fresh "aa" in +let y := fresh "bb" in +let z := fresh "cc" in +let k := fresh "dd" in +refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl). +Qed. +Print lem3. + +Lemma lem4 x : x+0=0. +match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. +match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. +match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end. +Show. +Abort. + +Lemma lem5 (p:nat) : eq_refl p = eq_refl p. +let y := fresh "n" in (* Checking that y is hidden *) + let z := fresh "e" in (* Checking that z is hidden *) + match goal with + |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let y := fresh "n" in + let z := fresh "e" in + match goal with + |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let y := fresh "n" in + let z := fresh "e" in + match goal with + |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +let p := fresh "p" in + let z := fresh "e" in + match goal with + |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) + end. +Show. +Abort. + +Set Printing Allow Match Default Clause. + +(***************************************************) +(* Testing strategy for factorizing cases branches *) + +(* Factorization + default clause *) +Check fun x => match x with Eq => 1 | _ => 0 end. + +(* No factorization *) +Unset Printing Factorizable Match Patterns. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Factorizable Match Patterns. + +(* Factorization but no default clause *) +Unset Printing Allow Match Default Clause. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Allow Match Default Clause. + +(* No factorization in printing all mode *) +Set Printing All. +Check fun x => match x with Eq => 1 | _ => 0 end. +Unset Printing All. + +(* Several clauses *) +Inductive K := a1|a2|a3|a4|a5|a6. +Check fun x => match x with a3 | a4 => 3 | _ => 2 end. +Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end. + +(* Test redundant clause within a disjunctive pattern *) +Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end. diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out new file mode 100644 index 0000000000..6edc9e09a4 --- /dev/null +++ b/test-suite/output/Coercions.out @@ -0,0 +1,8 @@ +P x + : Prop +R x x + : Prop +fun (x : foo) (n : nat) => x n + : foo -> nat -> nat +"1" 0 + : PAIR diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v new file mode 100644 index 0000000000..6976f35a88 --- /dev/null +++ b/test-suite/output/Coercions.v @@ -0,0 +1,24 @@ +(* Submitted by Randy Pollack *) + +#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. + +Section testSection. +Variables (S : Set) (P : pred S) (R : rel S) (x : S). +Check (P x). +Check (R x x). +End testSection. + +(* Check the removal of coercions with target Funclass *) + +Record foo : Type := {D :> nat -> nat}. +Check (fun (x : foo) (n : nat) => x n). + +(* Check both removal of coercions with target Funclass and mixing + string and numeral scopes *) + +Require Import String. +Open Scope string_scope. +Inductive PAIR := P (s:string) (n:nat). +Coercion P : string >-> Funclass. +Check ("1" 0). diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out new file mode 100644 index 0000000000..9d1d19877e --- /dev/null +++ b/test-suite/output/CompactContexts.out @@ -0,0 +1,7 @@ +1 subgoal + + hP1 : True + a : nat b : list nat h : forall x : nat, {y : nat | y > x} + h2 : True + ============================ + False diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v new file mode 100644 index 0000000000..c409c0ee46 --- /dev/null +++ b/test-suite/output/CompactContexts.v @@ -0,0 +1,5 @@ +Set Printing Compact Contexts. + +Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False. +Show. +Abort. diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out new file mode 100644 index 0000000000..7e290847c1 --- /dev/null +++ b/test-suite/output/Deprecation.out @@ -0,0 +1,3 @@ +File "stdin", line 5, characters 0-3: +Warning: Tactic foo is deprecated since X.Y. Use idtac instead. +[deprecated-tactic,deprecated] diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v new file mode 100644 index 0000000000..04d5eb3d4a --- /dev/null +++ b/test-suite/output/Deprecation.v @@ -0,0 +1,6 @@ +#[deprecated(since = "X.Y", note = "Use idtac instead.")] + Ltac foo := idtac. + +Goal True. +foo. +Abort. diff --git a/test-suite/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out new file mode 100644 index 0000000000..b4aa60a2c8 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures.out @@ -0,0 +1,4 @@ +File "stdin", line 3, characters 0-24: +Error: Could not declare a canonical structure Foo. +Expected an instance of a record or structure. + diff --git a/test-suite/output/ErrorInCanonicalStructures.v b/test-suite/output/ErrorInCanonicalStructures.v new file mode 100644 index 0000000000..49597df6f7 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures.v @@ -0,0 +1,3 @@ +Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }. + +Canonical Structure Foo. diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out new file mode 100644 index 0000000000..ab64e25030 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures2.out @@ -0,0 +1,4 @@ +File "stdin", line 3, characters 0-24: +Error: Could not declare a canonical structure bar. +Expected an instance of a record or structure. + diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v new file mode 100644 index 0000000000..10ee177aaf --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures2.v @@ -0,0 +1,3 @@ +Definition bar := 99. + +Canonical Structure bar. diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out new file mode 100644 index 0000000000..776dfeb550 --- /dev/null +++ b/test-suite/output/ErrorInModule.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v new file mode 100644 index 0000000000..b2e3c3e923 --- /dev/null +++ b/test-suite/output/ErrorInModule.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +Module M. + Definition foo := nonexistent. +End M. diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out new file mode 100644 index 0000000000..776dfeb550 --- /dev/null +++ b/test-suite/output/ErrorInSection.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v new file mode 100644 index 0000000000..505c5ce378 --- /dev/null +++ b/test-suite/output/ErrorInSection.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +Section S. + Definition foo := nonexistent. +End S. diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out new file mode 100644 index 0000000000..cf2d5b2850 --- /dev/null +++ b/test-suite/output/Errors.out @@ -0,0 +1,18 @@ +The command has indeed failed with message: +The field t is missing in Errors.M. +The command has indeed failed with message: +Unable to unify "nat" with "True". +The command has indeed failed with message: +In nested Ltac calls to "f" and "apply x", last call failed. +Unable to unify "nat" with "True". +The command has indeed failed with message: +Ltac call to "instantiate ( (ident) := (lglob) )" failed. +Instance is not well-typed in the environment of ?x. +The command has indeed failed with message: +Cannot infer the domain of the type of f. +The command has indeed failed with message: +Cannot infer the domain of the implicit parameter A of id whose type is +"Type". +The command has indeed failed with message: +Cannot infer the codomain of the type of f in environment: +x : nat diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v new file mode 100644 index 0000000000..edc35f17b4 --- /dev/null +++ b/test-suite/output/Errors.v @@ -0,0 +1,37 @@ +(* coq-prog-args: ("-top" "Errors") *) +(* Test error messages *) + +(* Test non-regression of bug fixed in r13486 (bad printer for module names) *) + +Module Type S. +Parameter t:Type. +End S. +Module M : S. +Fail End M. + +(* A simple check of how Ltac trace are used or not *) +(* Unfortunately, cannot test error location... *) + +Ltac f x := apply x. +Goal True. +Fail simpl; apply 0. +Fail simpl; f 0. +Abort. + +(* Test instantiate error messages *) + +Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1. +intros T1 P1 H1. +eexists ?[x]. +destruct H1 as [x1 H1]. +Fail instantiate (x:=projT1 x1). +Abort. + +(* Test some messages for non solvable evars *) + +Fail Goal forall a f, f a = 0. +Fail Goal forall f x, id f x = 0. +Fail Goal forall f P, P (f 0). + +Definition t := unit. +End M. diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out new file mode 100644 index 0000000000..18f5d89f66 --- /dev/null +++ b/test-suite/output/Existentials.out @@ -0,0 +1,4 @@ +Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 2 = +?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) (shelved) +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Existentials.v b/test-suite/output/Existentials.v new file mode 100644 index 0000000000..924f1f5592 --- /dev/null +++ b/test-suite/output/Existentials.v @@ -0,0 +1,16 @@ +(* Test propagation of clear/clearbody in existential variables *) + +Section Test. + +Variable p:nat. +Let q := S p. + +Goal forall n m:nat, n = m. +intros. +eapply eq_trans. +clearbody q. +clear p. (* Error ... *) + +Show Existentials. +Abort. +End Test. diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out new file mode 100644 index 0000000000..29d50775a9 --- /dev/null +++ b/test-suite/output/Extraction_infix.out @@ -0,0 +1,20 @@ +(** val test : foo **) + +let test = + (fun (b, p) -> bar) (True, False) +(** val test : foo **) + +let test = + True@@?False +(** val test : foo **) + +let test = + True#^^False +(** val test : foo **) + +let test = + True@?:::False +(** val test : foo **) + +let test = + True @?::: False diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v new file mode 100644 index 0000000000..fe5926a36a --- /dev/null +++ b/test-suite/output/Extraction_infix.v @@ -0,0 +1,26 @@ +(* @herbelin's example for issue #6212 *) + +Require Import Extraction. +Inductive I := C : bool -> bool -> I. +Definition test := C true false. + +(* the parentheses around the function wrong signalled an infix operator *) + +Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ]. +Extraction test. + +(* some bonafide infix operators *) + +Extract Inductive I => "foo" [ "(@@?)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(#^^)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(@?:::)" ]. +Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out new file mode 100644 index 0000000000..f738b0d091 --- /dev/null +++ b/test-suite/output/Extraction_matchs_2413.out @@ -0,0 +1,52 @@ +(** val test1 : bool -> bool **) + +let test1 b = + b +(** val test2 : bool -> bool **) + +let test2 _ = + False +(** val wrong_id : 'a1 hole -> 'a2 hole **) + +let wrong_id = function +| Hole -> Hole +| Hole2 -> Hole2 +(** val test3 : 'a1 option -> 'a1 option **) + +let test3 o = + o +(** val test4 : indu -> indu **) + +let test4 = function +| A m -> A (S m) +| x -> x +(** val test5 : indu -> indu **) + +let test5 = function +| A m -> A (S m) +| _ -> B +(** val test6 : indu' -> indu' **) + +let test6 = function +| A' m -> A' (S m) +| E' -> B' +| F' -> B' +| _ -> C' +(** val test7 : indu -> nat option **) + +let test7 = function +| A m -> Some m +| _ -> None +(** val decode_cond_mode : + (word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1 + -> opcode -> 'a2) -> 'a2 decoder_result **) + +let decode_cond_mode condition f w g = + match condition w with + | Some oc -> + (match f w with + | DecUndefined -> DecUndefined + | DecUnpredictable -> DecUnpredictable + | DecInst i -> DecInst (g i oc) + | DecError m -> DecError m) + | None -> DecUndefined diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v new file mode 100644 index 0000000000..f9398fdca9 --- /dev/null +++ b/test-suite/output/Extraction_matchs_2413.v @@ -0,0 +1,130 @@ +(** Extraction : tests of optimizations of pattern matching *) + +Require Coq.extraction.Extraction. + +(** First, a few basic tests *) + +Definition test1 b := + match b with + | true => true + | false => false + end. + +Extraction test1. (** should be seen as the identity *) + +Definition test2 b := + match b with + | true => false + | false => false + end. + +Extraction test2. (** should be seen a the always-false constant function *) + +Inductive hole (A:Set) : Set := Hole | Hole2. + +Definition wrong_id (A B : Set) (x:hole A) : hole B := + match x with + | Hole _ => @Hole _ + | Hole2 _ => @Hole2 _ + end. + +Extraction wrong_id. (** should _not_ be optimized as an identity *) + +Definition test3 (A:Type)(o : option A) := + match o with + | Some x => Some x + | None => None + end. + +Extraction test3. (** Even with type parameters, should be seen as identity *) + +Inductive indu : Type := A : nat -> indu | B | C. + +Definition test4 n := + match n with + | A m => A (S m) + | B => B + | C => C + end. + +Extraction test4. (** should merge branchs B C into a x->x *) + +Definition test5 n := + match n with + | A m => A (S m) + | B => B + | C => B + end. + +Extraction test5. (** should merge branches B C into _->B *) + +Inductive indu' : Type := A' : nat -> indu' | B' | C' | D' | E' | F'. + +Definition test6 n := + match n with + | A' m => A' (S m) + | B' => C' + | C' => C' + | D' => C' + | E' => B' + | F' => B' + end. + +Extraction test6. (** should merge some branches into a _->C' *) + +(** NB : In Coq, "| a => a" corresponds to n, hence some "| _ -> n" are + extracted *) + +Definition test7 n := + match n with + | A m => Some m + | B => None + | C => None + end. + +Extraction test7. (** should merge branches B,C into a _->None *) + +(** Script from bug #2413 *) + +Set Implicit Arguments. + +Section S. + +Definition message := nat. +Definition word := nat. +Definition mode := nat. +Definition opcode := nat. + +Variable condition : word -> option opcode. + +Section decoder_result. + + Variable inst : Type. + + #[universes(template)] Inductive decoder_result : Type := + | DecUndefined : decoder_result + | DecUnpredictable : decoder_result + | DecInst : inst -> decoder_result + | DecError : message -> decoder_result. + +End decoder_result. + +Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode) + (w : word) (inst : Type) (g : mode -> opcode -> inst) : + decoder_result inst := + match condition w with + | Some oc => + match f w with + | DecInst i => DecInst (g i oc) + | DecError _ m => @DecError inst m + | DecUndefined _ => @DecUndefined inst + | DecUnpredictable _ => @DecUnpredictable inst + end + | None => @DecUndefined inst + end. + +End S. + +Extraction decode_cond_mode. +(** inner match should not be factorized with a partial x->x (different type) *) + diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out new file mode 100644 index 0000000000..6879cbc3c2 --- /dev/null +++ b/test-suite/output/Fixpoint.out @@ -0,0 +1,14 @@ +fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : +list B := match l with + | nil => nil + | a :: l0 => f a :: F A B f l0 + end + : forall A B : Set, (A -> B) -> list A -> list B +let fix f (m : nat) : nat := match m with + | 0 => 0 + | S m' => f m' + end in f 0 + : nat +Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1) + = cofix inf : Inf := {| projS := inf |} + : Inf diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v new file mode 100644 index 0000000000..9b25c2dbd3 --- /dev/null +++ b/test-suite/output/Fixpoint.v @@ -0,0 +1,50 @@ +Require Import List. + +Check + (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : + list B := match l with + | nil => nil + | a :: l => f a :: F _ _ f l + end). + +(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf BZ#860) *) +Check + let fix f (m : nat) : nat := + match m with + | O => 0 + | S m' => f m' + end + in f 0. + +Require Import ZArith_base Omega. +Open Scope Z_scope. + +Inductive even: Z -> Prop := +| even_base: even 0 +| even_succ: forall n, odd (n - 1) -> even n +with odd: Z -> Prop := +| odd_succ: forall n, even (n - 1) -> odd n. + +(* Check printing of fix *) +Ltac f id1 id2 := fix id1 2 with (id2 n (H:odd n) {struct H} : n >= 1). +Print Ltac f. + +(* Incidentally check use of fix in proofs *) +Lemma even_pos_odd_pos: forall n, even n -> n >= 0. +Proof. +fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). + intros. + destruct H. + omega. + apply odd_pos_even_pos in H. + omega. + intros. + destruct H. + apply even_pos_odd_pos in H. + omega. +Qed. + +#[universes(template)] CoInductive Inf := S { projS : Inf }. +Definition expand_Inf (x : Inf) := S (projS x). +CoFixpoint inf := S inf. +Eval compute in inf. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out new file mode 100644 index 0000000000..8d2a125c1d --- /dev/null +++ b/test-suite/output/FunExt.out @@ -0,0 +1,19 @@ +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Already an intensional equality. +The command has indeed failed with message: +In nested Ltac calls to "extensionality in (var)" and +"clearbody (ne_var_list)", last call failed. +Hypothesis e depends on the body of H' diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v new file mode 100644 index 0000000000..7658ce718e --- /dev/null +++ b/test-suite/output/FunExt.v @@ -0,0 +1,168 @@ +Require Import FunctionalExtensionality. + +(* Basic example *) +Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z). +intro H. +extensionality in H. +symmetry in H. +assumption. +Qed. + +(* Test rejection of non-equality *) +Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''. +intros H H' H''. +Fail extensionality in H. +clear H'. +Fail extensionality in H. +Fail extensionality in H''. +Abort. + +(* Test success on dependent equality *) +Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1. +intros p H. +extensionality in p. +assumption. +Qed. + +(* Test dependent functional extensionality *) +Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b), + (forall x y, f x y = g x y) -> f = g. +intros * H. +extensionality in H. +assumption. +Qed. + +(* Other tests, courtesy of Jason Gross *) + +Goal forall A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c), (forall a b c, f a b c = g a b c) -> f = g. +Proof. + intros A B C D f g H. + extensionality in H. + match type of H with f = g => idtac end. + exact H. +Qed. + +Section test_section. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = g a b c). + Goal f = g. + Proof. + extensionality in H. + match type of H with f = g => idtac end. + exact H. + Qed. +End test_section. + +Section test2. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + extensionality in H. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H. + Qed. +End test2. + +Section test3. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a c, (fun b => f a b c) = (fun b => g a b c)). + Goal (fun a c b => f a b c) = (fun a c b => g a b c). + Proof. + extensionality in H. + match type of H with (fun a c b => f a b c) = (fun a' c' b' => g a' b' c') => idtac end. + exact H. + Qed. +End test3. + +Section test4. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c -> Type) + (H : forall b, (forall a c d, f a b c d) = (forall a c d, g a b c d)). + Goal (fun b => forall a c d, f a b c d) = (fun b => forall a c d, g a b c d). + Proof. + extensionality in H. + exact H. + Qed. +End test4. + +Section test5. + Goal nat -> True. + Proof. + intro n. + Fail extensionality in n. + constructor. + Qed. +End test5. + +Section test6. + Goal let f := fun A (x : A) => x in let pf := fun A x => @eq_refl _ (f A x) in f = f. + Proof. + intros f pf. + extensionality in pf. + match type of pf with f = f => idtac end. + exact pf. + Qed. +End test6. + +Section test7. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, True -> f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun a b c (_ : True) => f a b c) = (fun a' b' c' (_ : True) => g a' b' c') => idtac end. + constructor. + Qed. +End test7. + +Section test8. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : True -> forall a b c, f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun (_ : True) => f) = (fun (_ : True) => g) => idtac end. + constructor. + Qed. +End test8. + +Section test9. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + pose H as H'. + extensionality in H. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H'. + Qed. +End test9. + +Section test10. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : f = g). + Goal True. + Proof. + Fail extensionality in H. + constructor. + Qed. +End test10. + +Section test11. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = f a b c). + Goal True. + Proof. + pose H as H'. + pose (eq_refl : H = H') as e. + extensionality in H. + Fail extensionality in H'. + clear e. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + lazymatch type of H with f = f => idtac end. + constructor. + Qed. +End test11. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out new file mode 100644 index 0000000000..0b0f501f9a --- /dev/null +++ b/test-suite/output/Implicit.out @@ -0,0 +1,16 @@ +compose (C:=nat) S + : (nat -> nat) -> nat -> nat +ex_intro (P:=fun _ : nat => True) (x:=0) I + : ex (fun _ : nat => True) +d2 = fun x : nat => d1 (y:=x) + : forall x x0 : nat, x0 = x -> x0 = x + +d2 is not universe polymorphic +Arguments x, x0 are implicit +Argument scopes are [nat_scope nat_scope _] +map id (1 :: nil) + : list nat +map id' (1 :: nil) + : list nat +map (id'' (A:=nat)) (1 :: nil) + : list nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v new file mode 100644 index 0000000000..306532c0df --- /dev/null +++ b/test-suite/output/Implicit.v @@ -0,0 +1,53 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +(* Suggested by Pierre Casteran (BZ#169) *) +(* Argument 3 is needed to typecheck and should be printed *) +Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x). +Check (compose (C:=nat) S). + +(* Better to explicitly display the arguments inferable from a + position that could disappear after reduction *) +Inductive ex (A : Set) (P : A -> Prop) : Prop := + ex_intro : forall x : A, P x -> ex P. +Check (ex_intro (P:=fun _ => True) (x:=0) I). + +(* Test for V8 printing of implicit by names *) +Definition d1 y x (h : x = y :>nat) := h. +Definition d2 x := d1 (y:=x). + +Print d2. + +Set Strict Implicit. +Unset Implicit Arguments. + +(* Check maximal insertion of implicit *) + +Require Import List. + +Open Scope list_scope. + +Set Implicit Arguments. +Set Maximal Implicit Insertion. + +Definition id (A:Type) (x:A) := x. + +Check map id (1::nil). + +Definition id' (A:Type) (x:A) := x. + +Arguments id' {A} x. + +Check map id' (1::nil). + +Unset Maximal Implicit Insertion. +Unset Implicit Arguments. + +(* Check explicit insertion of last non-maximal trailing implicit to ensure *) +(* correct arity of partiol applications *) + +Set Implicit Arguments. +Definition id'' (A:Type) (x:A) := x. + +Check map (@id'' nat) (1::nil). + diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out new file mode 100644 index 0000000000..2ba02924c9 --- /dev/null +++ b/test-suite/output/Inductive.out @@ -0,0 +1,7 @@ +The command has indeed failed with message: +Last occurrence of "list'" must have "A" as 1st argument in + "A -> list' A -> list' (A * A)". +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x + +For foo: Argument scopes are [type_scope _] +For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v new file mode 100644 index 0000000000..9eec9a7dad --- /dev/null +++ b/test-suite/output/Inductive.v @@ -0,0 +1,7 @@ +Fail Inductive list' (A:Set) : Set := +| nil' : list' A +| cons' : A -> list' A -> list' (A*A). + +(* Check printing of let-ins *) +#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. +Print foo. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out new file mode 100644 index 0000000000..c17c63e724 --- /dev/null +++ b/test-suite/output/InitSyntax.out @@ -0,0 +1,12 @@ +Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} + +For sig2: Argument A is implicit +For exist2: Argument A is implicit +For sig2: Argument scopes are [type_scope type_scope type_scope] +For exist2: Argument scopes are [type_scope function_scope function_scope _ _ + _] +exists x : nat, x = x + : Prop +fun b : bool => if b then b else b + : bool -> bool diff --git a/test-suite/output/InitSyntax.v b/test-suite/output/InitSyntax.v new file mode 100644 index 0000000000..eb39782ecd --- /dev/null +++ b/test-suite/output/InitSyntax.v @@ -0,0 +1,4 @@ +(* Soumis par Pierre *) +Print sig2. +Check (exists x : nat, x = x). +Check (fun b : bool => if b then b else b). diff --git a/test-suite/output/Int31Syntax.out b/test-suite/output/Int31Syntax.out new file mode 100644 index 0000000000..4e8796c14b --- /dev/null +++ b/test-suite/output/Int31Syntax.out @@ -0,0 +1,14 @@ +I31 + : digits31 int31 +2 + : int31 +660865024 + : int31 +2 + 2 + : int31 +2 + 2 + : int31 + = 4 + : int31 + = 710436486 + : int31 diff --git a/test-suite/output/Int31Syntax.v b/test-suite/output/Int31Syntax.v new file mode 100644 index 0000000000..83be3b976b --- /dev/null +++ b/test-suite/output/Int31Syntax.v @@ -0,0 +1,13 @@ +Require Import Int31 Cyclic31. + +Open Scope int31_scope. +Check I31. (* Would be nice to have I31 : digits->digits->...->int31 + For the moment, I31 : digits31 int31, which is better + than (fix nfun .....) size int31 *) +Check 2. +Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) +Check (add31 2 2). +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Close Scope int31_scope. diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out new file mode 100644 index 0000000000..f2bf25ca65 --- /dev/null +++ b/test-suite/output/Intuition.out @@ -0,0 +1,6 @@ +1 subgoal + + m, n : Z + H : (m >= n)%Z + ============================ + (m >= m)%Z diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v new file mode 100644 index 0000000000..5f1914d21f --- /dev/null +++ b/test-suite/output/Intuition.v @@ -0,0 +1,5 @@ +Require Import ZArith_base. +Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z. +intros; intuition. +Show. +Abort. diff --git a/test-suite/output/InvalidDisjunctiveIntro.out b/test-suite/output/InvalidDisjunctiveIntro.out new file mode 100644 index 0000000000..25a306b458 --- /dev/null +++ b/test-suite/output/InvalidDisjunctiveIntro.out @@ -0,0 +1,16 @@ +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Disjunctive/conjunctive introduction pattern expected. +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Ltac variable H is bound to <tactic closure> which cannot be coerced to +an introduction pattern. +The command has indeed failed with message: +Disjunctive/conjunctive introduction pattern expected. +The command has indeed failed with message: +Ltac variable H' is bound to <tactic closure> which cannot be coerced to +an introduction pattern. diff --git a/test-suite/output/InvalidDisjunctiveIntro.v b/test-suite/output/InvalidDisjunctiveIntro.v new file mode 100644 index 0000000000..4febdf0344 --- /dev/null +++ b/test-suite/output/InvalidDisjunctiveIntro.v @@ -0,0 +1,18 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail intros H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail intro H; destruct H as H. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H := fresh in intro H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail let H := fresh in intros H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail let H := idtac in intros H; destruct H as H. + (* Ltac variable H is bound to <tactic closure> which cannot be +coerced to an introduction pattern. *) + Fail let H := idtac in intros H; destruct H as H'. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H' := idtac in intros H; destruct H as H'. +(* Ltac variable H' is bound to <tactic closure> which cannot +be coerced to an introduction pattern. *) +Abort. diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out new file mode 100644 index 0000000000..ebbd5d422b --- /dev/null +++ b/test-suite/output/Load.out @@ -0,0 +1,10 @@ +f = 2 + : nat + +f is not universe polymorphic +u = I + : True + +u is not universe polymorphic +The command has indeed failed with message: +Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v new file mode 100644 index 0000000000..967507415a --- /dev/null +++ b/test-suite/output/Load.v @@ -0,0 +1,7 @@ +Load "output/load/Load_noproof.v". +Print f. + +Load "output/load/Load_proof.v". +Print u. + +Fail Load "output/load/Load_openproof.v". diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v new file mode 100644 index 0000000000..36992e4dda --- /dev/null +++ b/test-suite/output/MExtraction.v @@ -0,0 +1,12 @@ +Require Import micromega.MExtraction. +Require Import RingMicromega. +Require Import QArith. +Require Import VarMap. +Require Import ZMicromega. +Require Import QMicromega. +Require Import RMicromega. + +Recursive Extraction + List.map simpl_cone (*map_cone indexes*) + denorm Qpower vm_add + normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out new file mode 100644 index 0000000000..c99c8905e0 --- /dev/null +++ b/test-suite/output/Match_subterm.out @@ -0,0 +1,10 @@ +(0 = 1) +(eq 0) +eq +@eq +nat +0 +1 +S +0 +2 diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v new file mode 100644 index 0000000000..bf862c946d --- /dev/null +++ b/test-suite/output/Match_subterm.v @@ -0,0 +1,7 @@ +Goal 0 = 1. +match goal with +| |- context [?v] => + idtac v ; fail +| _ => idtac 2 +end. +Abort. diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out new file mode 100644 index 0000000000..47b19b71b3 --- /dev/null +++ b/test-suite/output/Nametab.out @@ -0,0 +1,39 @@ +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Constant Nametab.Q.N.K.foo +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Module Nametab.Q.N.K + (shorter name to refer to it in current context is Q.N.K) +Module Nametab.Q.N.K + (shorter name to refer to it in current context is Q.N.K) +Module Nametab.Q.N.K +Module Nametab.Q.N.K + (shorter name to refer to it in current context is Q.N.K) +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q.N +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q +Module Nametab.Q (shorter name to refer to it in current context is Q) +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Constant Nametab.Q.N.K.foo +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Constant Nametab.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Module Nametab.Q.N.K +Module Nametab.Q.N.K (shorter name to refer to it in current context is K) +Module Nametab.Q.N.K (shorter name to refer to it in current context is K) +Module Nametab.Q.N.K (shorter name to refer to it in current context is K) +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q.N +Module Nametab.Q.N (shorter name to refer to it in current context is Q.N) +Module Nametab.Q +Module Nametab.Q (shorter name to refer to it in current context is Q) diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v new file mode 100644 index 0000000000..4bbc5ca239 --- /dev/null +++ b/test-suite/output/Nametab.v @@ -0,0 +1,48 @@ +(* coq-prog-args: ("-top" "Nametab") *) +Module Q. + Module N. + Module K. + Definition foo := Set. + End K. + End N. +End Q. + +(* Bad *) Locate foo. +(* Bad *) Locate K.foo. +(* Bad *) Locate N.K.foo. +(* OK *) Locate Q.N.K.foo. +(* OK *) Locate Nametab.Q.N.K.foo. + +(* Bad *) Locate Module K. +(* Bad *) Locate Module N.K. +(* OK *) Locate Module Q.N.K. +(* OK *) Locate Module Nametab.Q.N.K. + +(* Bad *) Locate Module N. +(* OK *) Locate Module Q.N. +(* OK *) Locate Module Nametab.Q.N. + +(* OK *) Locate Module Q. +(* OK *) Locate Module Nametab.Q. + + +Import Q.N. + + +(* Bad *) Locate foo. +(* OK *) Locate K.foo. +(* Bad *) Locate N.K.foo. +(* OK *) Locate Q.N.K.foo. +(* OK *) Locate Nametab.Q.N.K.foo. + +(* OK *) Locate Module K. +(* Bad *) Locate Module N.K. +(* OK *) Locate Module Q.N.K. +(* OK *) Locate Module Nametab.Q.N.K. + +(* Bad *) Locate Module N. +(* OK *) Locate Module Q.N. +(* OK *) Locate Module Nametab.Q.N. + +(* OK *) Locate Module Q. +(* OK *) Locate Module Nametab.Q. diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out new file mode 100644 index 0000000000..c142d28ebe --- /dev/null +++ b/test-suite/output/Naming.out @@ -0,0 +1,63 @@ +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 +1 subgoal + + x3, x, x1, x4, x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 + ============================ + x + x1 = x4 + x0 +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> + x + x1 = x4 + x0 -> foo (S x) +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3, x, x1, x4, x0 : nat + ============================ + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3, x, x1, x4, x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + ============================ + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3, x, x1, x4, x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1) + H0 : x + x1 = x4 + x0 + x5, x6, x7, S : nat + ============================ + x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3, a : nat + H : a = 0 -> forall a : nat, a = 0 + ============================ + a = 0 diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v new file mode 100644 index 0000000000..7f3b332d7d --- /dev/null +++ b/test-suite/output/Naming.v @@ -0,0 +1,92 @@ +(* This file checks the compatibility of naming strategy *) +(* This does not mean that the given naming strategy is good *) + +Parameter x2:nat. +Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y. +Section A. +Variable x3:nat. +Goal forall x x1 x2 x3:nat, + (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3. +Show. +intros. +Show. + +(* Remark: in V8.2, this used to be printed + + x3 : nat + ============================ + forall x x1 x4 x5 : nat, + (forall x0 x6 : nat, x0 + x1 = x4 + x6) -> x + x1 = x4 + x5 + +before intro and + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 + ============================ + x + x1 = x4 + x0 + +after. From V8.3, the quantified hypotheses are printed the sames as +they would be intro. However the hypothesis H remains printed +differently to avoid using the same name in autonomous but nested +subterms *) + +Abort. + +Goal forall x x1 x2 x3:nat, + (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) -> + x+x1 = x2+x3 -> foo (S x). +Show. +unfold foo. +Show. +do 4 intro. (* --> x, x1, x4, x0, ... *) +Show. +do 2 intro. +Show. +do 4 intro. +Show. + +(* Remark: in V8.2, this used to be printed + + x3 : nat + ============================ + forall x x1 x4 x5 : nat, + (forall x0 x6 : nat, + x0 + x1 = x4 + x6 -> + forall x7 x8 x9 S0 : nat, x7 + S0 = x8 + x9 + (S x0 + x1)) -> + x + x1 = x4 + x5 -> forall x0 x6 x7 S0 : nat, x0 + S0 = x6 + x7 + S x + +before the intros and + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + x5 : nat + x6 : nat + x7 : nat + S : nat + ============================ + x5 + S = x6 + x7 + Datatypes.S x + +after (note the x5/x0 and the S0/S) *) + +Abort. + +(* Check naming in hypotheses *) + +Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0. +intros. +Show. +apply H with (a:=a). (* test compliance with printing *) +Abort. + +End A. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out new file mode 100644 index 0000000000..bec4fc1579 --- /dev/null +++ b/test-suite/output/Notations.out @@ -0,0 +1,139 @@ +true ? 0; 1 + : nat +if true as x return (x ? nat; bool) then 0 else true + : nat +fun e : nat * nat => proj1 e + : nat * nat -> nat +decomp (true, true) as t, u in (t, u) + : bool * bool +! (0 = 0) + : Prop +forall n : nat, n = 0 + : Prop +! (0 = 0) + : Prop +forall n : nat, # (n = n) + : Prop +forall n n0 : nat, ## (n = n0) + : Prop +forall n n0 : nat, ### (n = n0) + : Prop +3 + 3 + : Z +3 + 3 + : znat +[1; 2; 4] + : list nat +(1; 2, 4) + : nat * nat * nat +ifzero 3 + : bool +pred 3 + : nat +fun n : nat => pred n + : nat -> nat +fun n : nat => pred n + : nat -> nat +fun x : nat => ifn x is succ n then n else 0 + : nat -> nat +1 - + : bool +-4 + : Z +The command has indeed failed with message: +Cannot find where the recursive pattern starts. +The command has indeed failed with message: +in the right-hand side, y and z should appear in +term position as part of a recursive pattern. +The command has indeed failed with message: +The reference w was not found in the current environment. +The command has indeed failed with message: +in the right-hand side, y and z should appear in +term position as part of a recursive pattern. +The command has indeed failed with message: +z is expected to occur in binding position in the right-hand side. +The command has indeed failed with message: +as y is a non-closed binder, no such "," is allowed to occur. +The command has indeed failed with message: +Cannot find where the recursive pattern starts. +The command has indeed failed with message: +Cannot find where the recursive pattern starts. +The command has indeed failed with message: +Cannot find where the recursive pattern starts. +The command has indeed failed with message: +Cannot find where the recursive pattern starts. +The command has indeed failed with message: +Both ends of the recursive pattern are the same. +SUM (nat * nat) nat + : Set +FST (0; 1) + : Z +Nil + : forall A : Type, list A +NIL : list nat + : list nat +(false && I 3)%bool /\ (I 6)%bool + : Prop +[|1, 2, 3; 4, 5, 6|] + : Z * Z * Z * (Z * Z * Z) +[|0 * (1, 2, 3); (4, 5, 6) * false|] + : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) +fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z + : (Z -> Z -> Z -> Z) -> Z +Init.Nat.add + : nat -> nat -> nat +S + : nat -> nat +Init.Nat.mul + : nat -> nat -> nat +le + : nat -> nat -> Prop +plus + : nat -> nat -> nat +succ + : nat -> nat +Init.Nat.mul + : nat -> nat -> nat +le + : nat -> nat -> Prop +fun x : option Z => match x with + | SOME x0 => x0 + | NONE => 0 + end + : option Z -> Z +fun x : option Z => match x with + | SOME2 x0 => x0 + | NONE2 => 0 + end + : option Z -> Z +fun x : option Z => match x with + | SOME2 x0 => x0 + | NONE2 => 0 + end + : option Z -> Z +fun x : list ?T => match x with + | NIL => NONE2 + | (_ :') t => SOME2 t + end + : list ?T -> option (list ?T) +where +?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1, + x0 cannot be used) +s + : s +10 + : nat +fun _ : nat => 9 + : nat -> nat +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| ONE => ONE +end = p + : forall x : nat, x = x -> Prop +fun (x : nat) (p : x = x) => +match p in (_ = n) return (n = n) with +| 1 => 1 +end = p + : forall x : nat, x = x -> Prop +bar 0 + : nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v new file mode 100644 index 0000000000..2ffc3b14e2 --- /dev/null +++ b/test-suite/output/Notations.v @@ -0,0 +1,302 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + +(**********************************************************************) +(* Notations for if and let (submitted by Roland Zumkeller) *) + +Notation "a ? b ; c" := (if a then b else c) (at level 10). + +Check (true ? 0 ; 1). +Check if true as x return (if x then nat else bool) then 0 else true. + +Notation "'proj1' t" := (let (a,_) := t in a) (at level 1). + +Check (fun e : nat * nat => proj1 e). + +Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1). + +Check (decomp (true,true) as t, u in (t,u)). + +(**********************************************************************) +(* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *) + +Section A. + +Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. + +Check ! (0=0). +Check forall n, n=0. +Check forall n:nat, 0=0. + +End A. + +(**********************************************************************) +(* Behaviour wrt to binding variables (cf bug report #1186) *) + +Section B. + +Notation "# A" := (forall n:nat, n=n->A) (at level 60). +Check forall n:nat, # (n=n). + +Notation "## A" := (forall n n0:nat, n=n0->A) (at level 60). +Check forall n n0:nat, ## (n=n0). + +Notation "### A" := + (forall n n0:nat, match n with O => True | S n => n=n0 end ->A) (at level 60). +Check forall n n0:nat, ### (n=n0). + +End B. + +(**********************************************************************) +(* Conflict between notation and notation below coercions *) + +(* Case of a printer conflict *) + +Require Import BinInt. +Coercion Zpos : positive >-> Z. +Open Scope Z_scope. + + (* Check that (Zpos 3) is better printed by the printer for Z than + by the printer for positive *) + +Check (3 + Zpos 3). + +(* Case of a num printer only below coercion (submitted by Georges Gonthier) *) + +Open Scope nat_scope. + +Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). +Coercion Zpos: nat >-> znat. + +Declare Scope znat_scope. +Delimit Scope znat_scope with znat. +Open Scope znat_scope. + +Parameter addz : znat -> znat -> znat. +Notation "z1 + z2" := (addz z1 z2) : znat_scope. + + (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit, + is printed the same way, and not "S 2 + S 2" as if numeral printing was + only tested with coercion still present *) + +Check (3+3). + +(**********************************************************************) +(* Check recursive notations *) + +Require Import List. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). +Check [1;2;4]. + +Reserved Notation "( x ; y , .. , z )" (at level 0). +Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z). +Check (1;2,4). + +(* Check basic notations involving "match" *) + +Section C. + +Notation "'ifzero' n" := (match n with 0 => true | S _ => false end) + (at level 0, n at level 0). +Check (ifzero 3). + +Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end) + (at level 0, n at level 0). +Check (pred 3). +Check (fun n => match n with 0 => 0 | S n => n end). +Check (fun n => match n with S p as x => p | y => 0 end). + +Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := + (match x with O => u | S n => t end) (at level 0, u at level 0). +Check fun x => ifn x is succ n then n else 0. + +End C. + +(* Check correction of bug #1179 *) + +Notation "1 -" := true (at level 0). +Check 1-. + +(* This is another aspect of bug #1179 (raises anomaly in 8.1) *) + +Require Import ZArith. +Open Scope Z_scope. +Notation "- 4" := (-2 + -2). +Check -4. + +(**********************************************************************) +(* Check ill-formed recursive notations *) + +(* Recursive variables not part of a recursive pattern *) +Fail Notation "( x , y , .. , z )" := (pair x .. (pair y z) ..). + +(* No recursive notation *) +Fail Notation "( x , y , .. , z )" := (pair x (pair y z)). + +(* Left-unbound variable *) +Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..). + +(* Right-unbound variable *) +Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..) (only parsing). + +(* Not the right kind of recursive pattern *) +Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)). +Fail Notation "( x -- y , .. , z )" := (pair y .. (pair z 0) ..) + (y closed binder, z closed binder). + +(* No separator allowed with open binders *) +Fail Notation "( x -- y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)) + (y binder, z binder). + +(* Ends of pattern do not match *) +Fail Notation "( x , y , .. , z )" := (pair y .. (pair (plus z) 0) ..). +Fail Notation "( x , y , .. , z )" := (pair y .. (plus z 0) ..). +Fail Notation "( x1 , x2 , y , .. , z )" := (y y .. (x2 z 0) ..). +Fail Notation "( x1 , x2 , y , .. , z )" := (x1 y .. (x2 z 0) ..). + +(* Ends of pattern are the same *) +Fail Notation "( x , y , .. , z )" := (pair .. (pair (pair y z) x) .. x). + +(**********************************************************************) +(* Check preservation of scopes at printing time *) + +Notation SUM := sum. +Check SUM (nat*nat) nat. + +(**********************************************************************) +(* Check preservation of implicit arguments at printing time *) + +Notation FST := fst. +Check FST (0;1). + +(**********************************************************************) +(* Check notations for references with activated or deactivated *) +(* implicit arguments *) + +Notation Nil := @nil. +Check Nil. + +Notation NIL := nil. +Check NIL : list nat. + + +(**********************************************************************) +(* Test printing of notation with coercions in scope of a coercion *) + +Open Scope nat_scope. + +Coercion is_true := fun b => b=true. +Coercion of_nat n := match n with 0 => true | _ => false end. +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. + +Check (false && I 3)%bool /\ (I 6)%bool. + +(**********************************************************************) +(* Check notations with several recursive patterns *) + +Open Scope Z_scope. + +Notation "[| x , y , .. , z ; a , b , .. , c |]" := + (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)). +Check [|1,2,3;4,5,6|]. + +Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := + (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z)) + (pair .. (pair (pair a u) (pair b u)) .. (pair c u))) + (t at level 39). +Check [|0*(1,2,3);(4,5,6)*false|]. + +(**********************************************************************) +(* Test recursive notations involving applications *) +(* Caveat: does not work for applied constant because constants are *) +(* classified as notations for the particular constant while this *) +(* generic application notation is classified as generic *) + +Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). +Check fun f => {| f; 0; 1; 2 |} : Z. + +(**********************************************************************) +(* Check printing of notations from other modules *) + +(* 1- Non imported case *) + +Require make_notation. + +Check plus. +Check S. +Check mult. +Check le. + +(* 2- Imported case *) + +Import make_notation. + +Check plus. +Check S. +Check mult. +Check le. + +(* Check notations in cases patterns *) + +Notation SOME := Some. +Notation NONE := None. +Check (fun x => match x with SOME x => x | NONE => 0 end). + +Notation NONE2 := (@None _). +Notation SOME2 := (@Some _). +Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). + +Notation NONE3 := @None. +Notation SOME3 := @Some. +Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end). + +Notation "a :'" := (cons a) (at level 12). + +Check (fun x => match x with | nil => NONE | h :' t => SOME3 _ t end). + +(* Check correct matching of "Type" in notations. Of course the + notation denotes a term that will be reinterpreted with a different + universe than the actual one; but it would be the same anyway + without a notation *) + +Notation s := Type. +Check s. + +(* Test bug #2835: notations were not uniformly managed under prod and lambda *) + +Open Scope nat_scope. + +Notation "'foo' n" := (S n) (at level 50): nat_scope. + +Check (foo 9). +Check (fun _ : nat => 9). + +(* Checking parsing and printing of numerical and non-numerical notations for eq_refl *) + +(* This notation was not correctly printed until Pierre B.'s + improvements to the interpretation of patterns *) + +Notation "'ONE'" := eq_refl. +Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. + +(* This one used to failed at parsing until now *) + +Notation "1" := eq_refl. +Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. + +(* Check bug 5693 *) + +Module M. +Definition A := 0. +Definition bar (a b : nat) := plus a b. +Notation "" := A (format "", only printing). +Check (bar A 0). +End M. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out new file mode 100644 index 0000000000..41d1593758 --- /dev/null +++ b/test-suite/output/Notations2.out @@ -0,0 +1,102 @@ +2 3 + : PAIR +2 [+] 3 + : nat +forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x + : Prop +match (0, 0, 0) with +| (x, y, z) => x + y + z +end + : nat +let '(a, _, _) := (2, 3, 4) in a + : nat +exists myx y : bool, myx = y + : Prop +fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y + : (nat -> nat -> Prop) -> nat -> Prop +∃ n p : nat, n + p = 0 + : Prop +let a := 0 in +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d + : Prop +∀ n p : nat, n + p = 0 + : Prop +λ n p : nat, n + p = 0 + : nat -> nat -> Prop +λ (A : Type) (n p : A), n = p + : ∀ A : Type, A -> A -> Prop +λ A : Type, ∃ n p : A, n = p + : Type -> Prop +λ A : Type, ∀ n p : A, n = p + : Type -> Prop +let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 + : bool -> nat +λ (f : nat -> nat) (x : nat), f(x) + S(x) + : (nat -> nat) -> nat -> nat +Notation plus2 n := (S(S(n))) +λ n : list(nat), match n with + | list1 => 0 + | _ => 2 + end + : list(nat) -> nat +λ n : list(nat), +match n with +| list1 => 0 +| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 +end + : list(nat) -> nat +λ n : list(nat), +match n with +| nil => 2 +| 0 :: _ => 2 +| list1 => 0 +| 1 :: _ :: _ => 2 +| plus2 _ :: _ => 2 +end + : list(nat) -> nat +# x : nat => x + : nat -> nat +# _ : nat => 2 + : nat -> nat +# x : nat => # H : x <= 0 => exist (le x) 0 H + : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0} +exist (Q x) y conj + : {x0 : A | Q x x0} +% i + : nat -> nat +% j + : nat -> nat +{1, 2} + : nat -> Prop +a# + : Set +a# + : Set +a≡ + : Set +a≡ + : Set +.≡ + : Set +.≡ + : Set +.a# + : Set +.a# + : Set +.a≡ + : Set +.a≡ + : Set +.α + : Set +.α + : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v new file mode 100644 index 0000000000..923caedace --- /dev/null +++ b/test-suite/output/Notations2.v @@ -0,0 +1,177 @@ +(**********************************************************************) +(* Test call to primitive printers in presence of coercion to *) +(* functions (cf bug #2044) *) + +Inductive PAIR := P (n1:nat) (n2:nat). +Coercion P : nat >-> Funclass. +Check (2 3). + +(* Check that notations with coercions to functions inserted still work *) +(* (were not working from revision 11886 to 12951) *) + +Record Binop := { binop :> nat -> nat -> nat }. +Class Plusop := { plusop : Binop; zero : nat }. +Infix "[+]" := plusop (at level 40). +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; zero := 0 |}. +Check 2[+]3. + +(* Test bug #2091 (variable le was printed using <= !) *) + +Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. + +(* Test recursive notations in cases pattern *) + +Remove Printing Let prod. +Check match (0,0,0) with (x,y,z) => x+y+z end. +Check let '(a,b,c) := ((2,3),4) in a. + +(* Check printing of notations with mixed reserved binders (see bug #2571) *) + +Implicit Type myx : bool. +Check exists myx y, myx = y. + +(* Test notation for anonymous functions up to eta-expansion *) + +Check fun P:nat->nat->Prop => fun x:nat => ex (P x). + +(* Test notations with binders *) + +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity, + format "'[ ' ∃ x .. y ']' , P"). + +Check (∃ n p, n+p=0). + +Check ∃ (a:=0) (x:nat) y (b:=1) (c:=b) (d:=2) z (e:=3) (f:=4), x+y = z+d. + +Notation "∀ x .. y , P":= (forall x, .. (forall y, P) ..) + (x binder, at level 200, right associativity). + +Check (∀ n p, n+p=0). + +Notation "'λ' x .. y , P":= (fun x => .. (fun y => P) ..) + (y binder, at level 200, right associativity). + +Check (λ n p, n+p=0). + +Generalizable Variable A. + +Check `(λ n p : A, n=p). +Check `(∃ n p : A, n=p). +Check `(∀ n p : A, n=p). + +Notation "'let'' f x .. y := t 'in' u":= + (let f := fun x => .. (fun y => t) .. in u) + (f ident, x closed binder, y closed binder, at level 200, + right associativity). + +Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. + +(* In practice, only the printing rule is used here *) +(* Note: does not work for pattern *) +Module A. +Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Open Scope nat_scope. +Check fun f x => f x + S x. + +Open Scope list_scope. +Notation list1 := (1::nil)%list. +Notation plus2 n := (S (S n)). +(* plus2 was not correctly printed in the two following tests in 8.3pl1 *) +Print plus2. +Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Allow Match Default Clause. +Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Factorizable Match Patterns. +Check fun n => match n with list1 => 0 | _ => 2 end. +Set Printing Allow Match Default Clause. +Set Printing Factorizable Match Patterns. + +End A. + +(* This one is not fully satisfactory because binders in the same type + are re-factorized and parentheses are needed even for atomic binder + +Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":= + (let f := fun x => .. (fun y => t) .. in u) + (f ident, x closed binder, y closed binder, at level 200, + right associativity). + +Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. +*) + +(* Check notations for functional terms which do not necessarily + depend on their parameter *) +(* Old request mentioned again on coq-club 20/1/2012 *) + +Notation "# x : T => t" := (fun x : T => t) + (at level 0, t at level 200, x ident). + +Check # x : nat => x. +Check # _ : nat => 2. + +(* Check bug 4677 *) +Check fun x (H:le x 0) => exist (le x) 0 H. + +Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). +Check (exist (Q x) y conj). + +(* Check bug #4854 *) +Notation "% i" := (fun i : nat => i) (at level 0, i ident). +Check %i. +Check %j. + +(* Check bug raised on coq-club on Sep 12, 2016 *) + +Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))). +Check ({1, 2}). + +(**********************************************************************) +(* Check notations of the form ".a", ".a≡", "a≡" *) +(* Only "a#", "a≡" and ".≡" were working properly for parsing. The *) +(* other ones were working only for printing. *) + +Notation "a#" := nat. +Check nat. +Check a#. + +Notation "a≡" := nat. +Check nat. +Check a≡. + +Notation ".≡" := nat. +Check nat. +Check .≡. + +Notation ".a#" := nat. +Check nat. +Check .a#. + +Notation ".a≡" := nat. +Check nat. +Check .a≡. + +Notation ".α" := nat. +Check nat. +Check .α. + +(* A test for #6304 *) + +Module M6304. +Notation "'for' m 'from' 0 'to' N 'updating' ( s1 ) {{ b }} ;; rest" := + (let s1 := + (fix rec(n: nat) := match n with + | 0 => s1 + | S m => let s1 := rec m in b + end) N + in rest) + (at level 20). + +Check fun (a b : nat) => + let res := 0 in + for i from 0 to a updating (res) {{ + for j from 0 to b updating (res) {{ S res }};; + res + }};; res. + +End M6304. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out new file mode 100644 index 0000000000..71d92482d0 --- /dev/null +++ b/test-suite/output/Notations3.out @@ -0,0 +1,271 @@ +{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0} + : Set +[<0, 2 >] + : nat * nat * (nat * nat) +[<0, 2 >] + : nat * nat * (nat * nat) +(0, 2, (2, 2)) + : nat * nat * (nat * nat) +pair (pair O (S (S O))) (pair (S (S O)) O) + : prod (prod nat nat) (prod nat nat) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +<< 0, 2, 4 >> + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (2, (2, 0))) + : nat * nat * nat * (nat * (nat * nat)) +(0, 2, 4, (0, (2, 4))) + : nat * nat * nat * (nat * (nat * nat)) +pair (pair (pair O (S (S O))) (S (S (S (S O))))) + (pair (S (S (S (S O)))) (pair (S (S O)) O)) + : prod (prod (prod nat nat) nat) (prod nat (prod nat nat)) +ETA x y : nat, Nat.add + : nat -> nat -> nat +ETA x y : nat, Nat.add + : nat -> nat -> nat +ETA x y : nat, Nat.add + : nat -> nat -> nat +fun x y : nat => Nat.add x y + : forall (_ : nat) (_ : nat), nat +ETA x y : nat, le_S + : forall x y : nat, x <= y -> x <= S y +fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f + : (forall x : nat * (bool * unit), ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} +where +?T : [x : nat * (bool * unit) |- Type] +fun f : forall x : bool * (nat * unit), ?T => +CURRYINV (x : nat) (y : bool), f + : (forall x : bool * (nat * unit), ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} +where +?T : [x : bool * (nat * unit) |- Type] +fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f + : (forall x : unit * nat * bool, ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} +where +?T : [x : unit * nat * bool |- Type] +fun f : forall x : unit * bool * nat, ?T => +CURRYINVLEFT (x : nat) (y : bool), f + : (forall x : unit * bool * nat, ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} +where +?T : [x : unit * bool * nat |- Type] +forall n : nat, {#n | 1 > n} + : Prop +forall x : nat, {|x | x > 0|} + : Prop +exists2 x : nat, x = 1 & x = 2 + : Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x) + : nat -> Prop +fun n : nat => +foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a) + : nat -> Prop +fun n : nat => +foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0) + : nat -> Prop +fun n : nat => +foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x) + : nat -> Prop +fun n : nat => +foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x) + : nat -> Prop +fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2 + : nat -> Prop +fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2 + : nat -> Prop +fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2 + : nat -> Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x) + : nat -> Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x) + : nat -> Prop +fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3 + : nat -> Prop +fun n : nat => {|n, fun _ : nat => n = 0 |}_3 + : nat -> Prop +fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0)) + : nat -> Prop +fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4 + : nat -> Prop +fun n : nat => {|n, fun _ : nat => n = 0 |}_4 + : nat -> Prop +fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0)) + : nat -> Prop +fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) + : nat -> Prop +tele (t : Type) '(y, z) (x : t0) := tt + : forall t : Type, nat * nat -> t -> fpack +[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2] + : (nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat)))))) +foo5 x nat x + : nat -> nat +fun x : ?A => x === x + : forall x : ?A, x = x +where +?A : [x : ?A |- Type] (x cannot be used) +{{0, 1}} + : nat * nat +{{0, 1, 2}} + : nat * (nat * nat) +{{0, 1, 2, 3}} + : nat * (nat * (nat * nat)) +letpair x [1] = {0}; +return (1, 2, 3, 4) + : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) +((*1).2).3 + : nat +*(1.2) + : nat +! '{{x, y}}, x + y = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + : Prop +exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 + : Prop +exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), +(forall x : A, R x x) + : Prop +exists_true (x : nat) (A : Type) (R : A -> A -> Prop) +(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z + : Prop +{{{{True, nat -> True}}, nat -> True}} + : Prop * Prop * Prop +{{D 1, 2}} + : nat * nat * (nat * nat * (nat * nat)) +! a b : nat # True # + : Prop * (Prop * Prop) +!!!! a b : nat # True # + : Prop * Prop * (Prop * Prop * Prop) +@@ a b : nat # a = b # b = a # + : Prop * Prop +exists_non_null x y z t : nat , x = y /\ z = t + : Prop +forall_non_null x y z t : nat , x = y /\ z = t + : Prop +{{RL 1, 2}} + : nat * (nat * nat) +{{RR 1, 2}} + : nat * nat * nat +@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O) + : prod nat (prod nat nat) +@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O) + : prod (prod nat nat) nat +{{RLRR 1, 2}} + : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * + (nat * nat * nat) +pair + (pair + (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) + (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + : prod + (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) + (prod nat (prod nat nat))) (prod (prod nat nat) nat) +fun x : nat => if x is n .+ 1 then n else 1 + : nat -> nat +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2' {{x, y}}, x = 0 & y = 0 + : Prop +myexists2 x : nat * nat, + let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y + : Prop +fun '({{x, y}} as z) => x + y = 0 /\ z = z + : nat * nat -> Prop +myexists ({{x, y}} as z), x + y = 0 /\ z = z + : Prop +exists '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +∀ '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y + : nat * nat * bool -> nat +myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +fun p : nat => if p is S n then n else 0 + : nat -> nat +fun p : comparison => if p is Lt then 1 else 0 + : comparison -> nat +fun S : nat => [S | S + S] + : nat -> nat * (nat -> nat) +fun N : nat => [N | N + 0] + : nat -> nat * (nat -> nat) +fun S : nat => [[S | S + S]] + : nat -> nat * (nat -> nat) +{I : nat | I = I} + : Set +{'I : True | I = I} + : Prop +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2 '{{y, z}} : nat * nat, y > z & z > y + : Prop +foo = +fun l : list nat => match l with + | _ :: (_ :: _) as l1 => l1 + | _ => l + end + : list nat -> list nat + +foo is not universe polymorphic +Argument scope is [list_scope] +Notation +"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope +(default interpretation) +"'exists' ! x .. y , p" := ex + (unique + (fun x => .. (ex (unique (fun y => p))) ..)) +: type_scope (default interpretation) +Notation +"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope +(default interpretation) +1 subgoal + + ============================ + ##@% + ^^^ +myfoo01 tt + : nat +myfoo01 tt + : nat +myfoo01 tt + : nat +[{0; 0}] + : list (list nat) +[{1; 2; 3}; + {4; 5; 6}; + {7; 8; 9}] + : list (list nat) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) + : unit + +amatch is not universe polymorphic +alist = [0; 1; 2] + : list nat + +alist is not universe polymorphic diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v new file mode 100644 index 0000000000..2caffad1d9 --- /dev/null +++ b/test-suite/output/Notations3.v @@ -0,0 +1,473 @@ +(**********************************************************************) +(* Check precedence, spacing, etc. in printing with curly brackets *) + +Check {x|x=0}+{True/\False}+{forall x, x=0}. + +(**********************************************************************) +(* Check printing of notations with several instances of a recursive pattern *) +(* Was wrong but I could not trigger a problem due to the collision between *) +(* different instances of ".." *) + +Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)). +Check [<0,2>]. +Check ((0,2),(2,0)). +Check ((0,2),(2,2)). +Unset Printing Notations. +Check [<0,2>]. +Set Printing Notations. + +Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)). +Check <<0,2,4>>. +Check (((0,2),4),(4,(2,0))). +Check (((0,2),4),(2,(2,0))). +Check (((0,2),4),(0,(2,4))). +Unset Printing Notations. +Check <<0,2,4>>. +Set Printing Notations. + +(**********************************************************************) +(* Check notations with recursive notations both in binders and terms *) + +Notation "'ETA' x .. y , f" := + (fun x => .. (fun y => (.. (f x) ..) y ) ..) + (at level 200, x binder, y binder). +Check ETA (x:nat) (y:nat), Nat.add. +Check ETA (x y:nat), Nat.add. +Check ETA x y, Nat.add. +Unset Printing Notations. +Check ETA (x:nat) (y:nat), Nat.add. +Set Printing Notations. +Check ETA x y, le_S. + +Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRY (x:nat) (y:bool), f. + +Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYINV (x:nat) (y:bool), f. + +Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYLEFT (x:nat) (y:bool), f. + +Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..) + (at level 200, x binder, y binder). +Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. + +(**********************************************************************) +(* Notations with variables bound both as a term and as a binder *) +(* This is #4592 *) + +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. +Check forall n:nat, {# n | 1 > n}. + +Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. +Notation "{| x | P |}" := (foo x (fun x => P)). +Check forall x:nat, {| x | x > 0 |}. + +Check ex2 (fun x => x=1) (fun x0 => x0=2). + +(* Other tests about alpha-conversions: the following notation + contains all three kinds of bindings: + + - x is bound in the lhs as a term and a binder: its name is forced + by its position as a term; it can bind variables in P + - y is bound in the lhs as a binder only: its name is given by its + name as a binder in the term to display; it can bind variables in P + - z is a binder local to the rhs; it cannot bind a variable in P +*) + +Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop. +Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)). + +(* Not printable: z (resp c, n) occurs in P *) +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x). +Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a). +Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n). +Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x). +Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x). + +(* Printable *) +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x). +Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n). +Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x). + +(* Not printable: renaming x into n would bind the 2nd occurrence of n *) +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x). +Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x). + +(* Other tests *) +Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop. +Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)). + +(* Printable *) +Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z). +Check fun n => foo3 n (fun x y z => (fun _ => z=0) z). + +(* Not printable: renaming z in n would hide the renaming of x into n *) +Check fun n => foo3 n (fun x y z => (fun _ => x=0) z). + +(* Other tests *) +Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop. +Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)). + +(* Printable *) +Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z). +Check fun n => foo4 n (fun x y z => (fun _ => x=0) z). + +(* Not printable: y, z not allowed to occur in P *) +Check fun n => foo4 n (fun x y z => (fun _ => z=0) z). +Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). + +(**********************************************************************) +(* Test printing of #4932 *) + +#[universes(template)] Inductive ftele : Type := +| fb {T:Type} : T -> ftele +| fr {T} : (T -> ftele) -> ftele. + +Fixpoint args ftele : Type := + match ftele with + | fb _ => unit + | fr f => sigT (fun t => args (f t)) + end. + +Definition fpack := sigT args. +Definition pack fp fa : fpack := existT _ fp fa. + +Notation "'tele' x .. z := b" := + (fun x => .. (fun z => + pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) ) + (existT _ x .. (existT _ z tt) .. ) + ) ..) + (at level 85, x binder, z binder). + +Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(* Checking that "fun" in a notation does not mixed up with the + detection of a recursive binder *) + +Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))). +Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ]. + +(* Cyprien's part of bug #4765 *) + +Section Bug4765. + +Notation foo5 x T y := (fun x : T => y). +Check foo5 x nat x. + +End Bug4765. + +(**********************************************************************) +(* Test printing of #5526 *) + +Notation "x === x" := (eq_refl x) (only printing, at level 10). +Check (fun x => eq_refl x). + +(* Test recursive notations with the recursive pattern repeated on the right *) + +Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..). +Check {{0,1}}. +Check {{0,1,2}}. +Check {{0,1,2,3}}. + +(* Test printing of #5608 *) + +Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "'letpair' x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). +Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := + (let x:=a in ( .. (b0,b1) .., b2)). +Check letpair x [1] = {0}; return (1,2,3,4). + +(* Test spacing in #5569 *) + +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. +Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) + (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). +Check 1+1+1. +End S1. + +(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) +Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). +Check !!! (x y:nat), True. + +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Section S2. +Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). +End S2. + +(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) +(* for isolated "forall" (was not working already in 8.6) *) +Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). +Check ! '(x,y), x+y=0. + +(* Check that the terminator of a recursive pattern is interpreted in + the correct environment of bindings *) +Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder). +Check exists_mixed x y '(u,t), x+y=0/\u+t=0. +Check exists_mixed x y '(z,t), x+y=0/\z+t=0. + +(* Check that intermediary let-in are inserted inbetween instances of + the repeated pattern *) +Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). +Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. + +(* Check that generalized binders are correctly interpreted *) + +Module G. +Generalizable Variables A R. +Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. +Check exists_true `{Reflexive A R}, forall x, R x x. +Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +End G. + +(* Allows recursive patterns for binders to be associative on the left *) +Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). +Check !! a b : nat # True #. + +(* Examples where the recursive pattern refer several times to the recursive variable *) + +Notation "{{D x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..). +Check {{D 1, 2 }}. + +Notation "! x .. y # A #" := + ((forall x, x=x), .. ((forall y, y=y), A) ..) + (at level 200, x binder). +Check ! a b : nat # True #. + +Notation "!!!! x .. y # A #" := + (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) + (at level 200, x binder). +Check !!!! a b : nat # True #. + +Notation "@@ x .. y # A # B #" := + ((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..)) + (at level 200, x binder). +Check @@ a b : nat # a=b # b=a #. + +Notation "'exists_non_null' x .. y , P" := + (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) + (at level 200, x binder). +Check exists_non_null x y z t , x=y/\z=t. + +Notation "'forall_non_null' x .. y , P" := + (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..) + (at level 200, x binder). +Check forall_non_null x y z t , x=y/\z=t. + +(* Examples where the recursive pattern is in reverse order *) + +Notation "{{RL c , .. , d }}" := (pair d .. (pair c 0) ..). +Check {{RL 1 , 2}}. + +Notation "{{RR c , .. , d }}" := (pair .. (pair 0 d) .. c). +Check {{RR 1 , 2}}. + +Set Printing All. +Check {{RL 1 , 2}}. +Check {{RR 1 , 2}}. +Unset Printing All. + +Notation "{{RLRR c , .. , d }}" := (pair d .. (pair c 0) .., pair .. (pair 0 d) .. c, pair c .. (pair d 0) .., pair .. (pair 0 c) .. d). +Check {{RLRR 1 , 2}}. +Unset Printing Notations. +Check {{RLRR 1 , 2}}. +Set Printing Notations. + +(* Check insensitivity of "match" clauses to order *) + +Module IfPat. +Notation "'if' t 'is' n .+ 1 'then' p 'else' q" := + (match t with S n => p | 0 => q end) + (at level 200). +Check fun x => if x is n.+1 then n else 1. +End IfPat. + +(* Examples with binding patterns *) + +Check {'(x,y)|x+y=0}. + +Module D. +Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x pattern, p at level 200, right associativity, + format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'") + : type_scope. + +Check exists2' (x,y), x=0 & y=0. +End D. + +(* Ensuring for reparsability that printer of notations does not use a + pattern where only an ident could be reparsed *) + +Module E. +Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := + myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. +Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) + (at level 200, x ident, A at level 200, p at level 200, right associativity, + format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") + : type_scope. +Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). +End E. + +(* A canonical example of a notation with a non-recursive binder *) + +Parameter myex : forall {A}, (A -> Prop) -> Prop. +Notation "'myexists' x , p" := (myex (fun x => p)) + (at level 200, x pattern, p at level 200, right associativity). + +(* A canonical example of a notation with recursive binders *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +(* Check that printing 'pat uses an "as" when the variable bound to + the pattern is dependent. We check it for the three kinds of + notations involving bindings of patterns *) + +Check fun '((x,y) as z) => x+y=0/\z=z. (* Primitive fun/forall *) +Check myexists ((x,y) as z), x+y=0/\z=z. (* Isolated binding pattern *) +Check exists '((x,y) as z), x+y=0/\z=z. (* Applicative recursive binder *) +Check ∀ '((x,y) as z), x+y=0/\z=z. (* Other example of recursive binder, now treated as the exists case *) + +(* Check parsability and printability of irrefutable disjunctive patterns *) + +Check fun '(((x,y),true)|((x,y),false)) => x+y. +Check myexists (((x,y),true)|((x,y),false)), x>y. +Check exists '(((x,y),true)|((x,y),false)), x>y. +Check ∀ '(((x,y),true)|((x,y),false)), x>y. + +(* Check Georges' printability of a "if is then else" notation *) + +Module IfPat2. +Notation "'if' c 'is' p 'then' u 'else' v" := + (match c with p => u | _ => v end) + (at level 200, p pattern at level 100). +Check fun p => if p is S n then n else 0. +Check fun p => if p is Lt then 1 else 0. +End IfPat2. + +(* Check that mixed binders and terms defaults to ident and not pattern *) +Module F. + (* First without an indirection *) +Notation "[ n | t ]" := (n, (fun n : nat => t)). +Check fun S : nat => [ S | S+S ]. +Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *) + (* Then with an indirection *) +Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)). +Notation "[[ n | t ]]" := [[ n | n | t ]]. +Check fun S : nat => [[ S | S+S ]]. +End F. + +(* Check parsability/printability of {x|P} and variants *) + +Check {I:nat|I=I}. +Check {'I:True|I=I}. +Check {'(x,y)|x+y=0}. + +(* Check exists2 with a pattern *) +Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). + +Module Issue7110. +Open Scope list_scope. +Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..) + (at level 0). +Definition foo (l : list nat) := + match l with + | a :: (b :: l) as l1 => l1 + | _ => l +end. +Print foo. +End Issue7110. + +Module LocateNotations. +Locate "exists". +Locate "( _ , _ , .. , _ )". +End LocateNotations. + +Module Issue7731. + +Axiom (P : nat -> Prop). +Parameter (X : nat). +Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'"). +Notation "%" := X. + +Set Printing Width 7. +Goal ## @ % ^^^. +Show. +Abort. + +End Issue7731. + +Module Issue8126. + +Definition myfoo (x : nat) (y : nat) (z : unit) := y. +Notation myfoo0 := (@myfoo 0). +Notation myfoo01 := (@myfoo0 1). +Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) + +End Issue8126. + +(* Test printing of notations guided by scope *) + +Module A. + +Declare Scope line_scope. +Delimit Scope line_scope with line. +Declare Scope matx_scope. +Notation "{ }" := nil (format "{ }") : line_scope. +Notation "{ x }" := (cons x nil) : line_scope. +Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. +Notation "[ ]" := nil (format "[ ]") : matx_scope. +Notation "[ l ]" := (cons l%line nil) : matx_scope. +Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) + (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. + +Open Scope matx_scope. +Check [[0;0]]. +Check [[1;2;3];[4;5;6];[7;8;9]]. + +End A. + +(* Example by Beta Ziliani *) + +Require Import Lists.List. + +Module B. + +Import ListNotations. + +Declare Scope pattern_scope. +Delimit Scope pattern_scope with pattern. + +Declare Scope patterns_scope. +Delimit Scope patterns_scope with patterns. + +Notation "a => b" := (a, b) (at level 201) : pattern_scope. +Notation "'with' p1 | .. | pn 'end'" := + ((cons p1%pattern (.. (cons pn%pattern nil) ..))) + (at level 91, p1 at level 210, pn at level 210) : patterns_scope. + +Definition mymatch (n:nat) (l : list (nat * nat)) := tt. +Arguments mymatch _ _%patterns. +Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). + +Close Scope patterns_scope. +Close Scope pattern_scope. + +Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. +Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) + +Definition alist := [0;1;2]. +Print alist. + +End B. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out new file mode 100644 index 0000000000..94016e170b --- /dev/null +++ b/test-suite/output/Notations4.out @@ -0,0 +1,49 @@ +[< 0 > + < 1 > * < 2 >] + : nat +[< b > + < b > * < 2 >] + : nat +[<< # 0 >>] + : option nat +[1 {f 1}] + : Expr +fun (x : nat) (y z : Expr) => [1 + y z + {f x}] + : nat -> Expr -> Expr -> Expr +fun e : Expr => +match e with +| [x y + z] => [x + y z] +| [1 + 1] => [1] +| _ => [e + e] +end + : Expr -> Expr +[(1 + 1)] + : Expr +Let "x" e1 e2 + : expr +Let "x" e1 e2 + : expr +fun x : nat => (# x)%nat + : nat -> nat +fun x : nat => ## x + : nat -> nat +fun x : nat => # x + : nat -> nat +fun x : nat => ### x + : nat -> nat +fun x : nat => ## x + : nat -> nat +fun x : nat => (x.-1)%pred + : nat -> nat +∀ a : nat, a = 0 + : Prop +((∀ a : nat, a = 0) -> True)%type + : Prop +# + : Prop +# -> True + : Prop +((∀ a : nat, a = 0) -> True)%type + : Prop +## + : Prop +Notation Cn := Foo.FooCn +Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v new file mode 100644 index 0000000000..309115848f --- /dev/null +++ b/test-suite/output/Notations4.v @@ -0,0 +1,183 @@ +(* An example with constr subentries *) + +Module A. + +Declare Custom Entry myconstr. + +Notation "[ x ]" := x (x custom myconstr at level 6). +Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope. +Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope. +Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). +Check [ < 0 > + < 1 > * < 2 >]. + +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + +Declare Custom Entry anotherconstr. + +Notation "[ x ]" := x (x custom myconstr at level 6). +Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr at level 10). +Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). +Check [ << # 0 >> ]. + +End A. + +Module B. + +Inductive Expr := + | Mul : Expr -> Expr -> Expr + | Add : Expr -> Expr -> Expr + | One : Expr. + +Declare Custom Entry expr. +Notation "[ expr ]" := expr (expr custom expr at level 2). +Notation "1" := One (in custom expr at level 0). +Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). +Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). +Notation "( x )" := x (in custom expr at level 0, x at level 2). +Notation "{ x }" := x (in custom expr at level 0, x constr). +Notation "x" := x (in custom expr at level 0, x ident). + +Axiom f : nat -> Expr. +Check [1 {f 1}]. +Check fun x y z => [1 + y z + {f x}]. +Check fun e => match e with +| [x y + z] => [x + y z] +| [1 + 1] => [1] +| y => [y + e] +end. + +End B. + +Module C. + +Inductive Expr := + | Add : Expr -> Expr -> Expr + | One : Expr. + +Declare Custom Entry expr. +Notation "[ expr ]" := expr (expr custom expr at level 1). +Notation "1" := One (in custom expr at level 0). +Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). +Notation "( x )" := x (in custom expr at level 0, x at level 2). + +(* Check the use of a two-steps coercion from constr to expr 1 then + from expr 0 to expr 2 (note that camlp5 parsing is more tolerant + and does not require parentheses to parse from level 2 while at + level 1) *) + +Check [1 + 1]. + +End C. + +(* An example of interaction between coercion and notations from + Robbert Krebbers. *) + +Require Import String. + +Module D. + +Inductive expr := + | Var : string -> expr + | Lam : string -> expr -> expr + | App : expr -> expr -> expr. + +Notation Let x e1 e2 := (App (Lam x e2) e1). + +Parameter e1 e2 : expr. + +Check (Let "x" e1 e2). + +Coercion App : expr >-> Funclass. + +Check (Let "x" e1 e2). + +End D. + +(* Check fix of #8551: a delimiter should be inserted because the + lonely notation hides the scope nat_scope, even though the latter + is open *) + +Module E. + +Notation "# x" := (S x) (at level 20) : nat_scope. +Notation "# x" := (Some x). +Check fun x => (# x)%nat. + +End E. + +(* Other tests of precedence *) + +Module F. + +Notation "# x" := (S x) (at level 20) : nat_scope. +Notation "## x" := (S x) (at level 20). +Check fun x => S x. +Open Scope nat_scope. +Check fun x => S x. +Notation "### x" := (S x) (at level 20) : nat_scope. +Check fun x => S x. +Close Scope nat_scope. +Check fun x => S x. + +End F. + +(* Lower priority of generic application rules *) + +Module G. + +Declare Scope predecessor_scope. +Delimit Scope predecessor_scope with pred. +Declare Scope app_scope. +Delimit Scope app_scope with app. +Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope. +Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope. +Check fun x => pred x. + +End G. + +(* Checking arbitration between in the presence of a notation in type scope *) + +Module H. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. +Check forall a, a = 0. + +Close Scope type_scope. +Check ((forall a, a = 0) -> True)%type. +Open Scope type_scope. + +Notation "#" := (forall a, a = 0). +Check #. +Check # -> True. + +Close Scope type_scope. +Check (# -> True)%type. +Open Scope type_scope. + +Declare Scope my_scope. +Notation "##" := (forall a, a = 0) : my_scope. +Open Scope my_scope. +Check ##. + +End H. + +(* Fixing a bug reported by G. Gonthier in #9207 *) + +Module J. + +Module Import Mfoo. +Module Foo. +Definition FooCn := 2. +Module Bar. +Notation Cn := FooCn. +End Bar. +End Foo. +Export Foo.Bar. +End Mfoo. +About Cn. + +End J. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out new file mode 100644 index 0000000000..bdbc5a5960 --- /dev/null +++ b/test-suite/output/PatternsInBinders.out @@ -0,0 +1,59 @@ +swap = fun '(x, y) => (y, x) + : A * B -> B * A + +swap is not universe polymorphic +fun '(x, y) => (y, x) + : A * B -> B * A +forall '(x, y), swap (x, y) = (y, x) + : Prop +proj_informative = fun '(exist _ x _) => x : A + : {x : A | P x} -> A + +proj_informative is not universe polymorphic +foo = fun '(Bar n b tt p) => if b then n + p else n - p + : Foo -> nat + +foo is not universe polymorphic +baz = +fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 + : Foo -> Foo -> nat + +baz is not universe polymorphic +swap = +fun (A B : Type) '(x, y) => (y, x) + : forall A B : Type, A * B -> B * A + +swap is not universe polymorphic +Arguments A, B are implicit and maximally inserted +Argument scopes are [type_scope type_scope _] +fun (A B : Type) '(x, y) => swap (x, y) = (y, x) + : forall A B : Type, A * B -> Prop +forall (A B : Type) '(x, y), swap (x, y) = (y, x) + : Prop +exists '(x, y), swap (x, y) = (y, x) + : Prop +exists '(x, y) '(z, w), swap (x, y) = (z, w) + : Prop +λ '(x, y), (y, x) + : A * B → B * A +∀ '(x, y), swap (x, y) = (y, x) + : Prop +both_z = +fun pat : nat * nat => +let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) + : forall pat : nat * nat, F pat + +both_z is not universe polymorphic +fun '(x, y) '(z, t) => swap (x, y) = (z, t) + : A * B -> B * A -> Prop +forall '(x, y) '(z, t), swap (x, y) = (z, t) + : Prop +fun (pat : nat) '(x, y) => x + y = pat + : nat -> nat * nat -> Prop +f = fun x : nat => x + x + : nat -> nat + +f is not universe polymorphic +Argument scope is [nat_scope] +fun x : nat => x + x + : nat -> nat diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v new file mode 100644 index 0000000000..0c1b08f5a3 --- /dev/null +++ b/test-suite/output/PatternsInBinders.v @@ -0,0 +1,74 @@ +Require Coq.Unicode.Utf8. + +(** The purpose of this file is to test printing of the destructive + patterns used in binders ([fun] and [forall]). *) + +Parameters (A B : Type) (P:A->Prop). + +Definition swap '((x,y) : A*B) := (y,x). +Print swap. + +Check fun '((x,y) : A*B) => (y,x). + +Check forall '(x,y), swap (x,y) = (y,x). + +Definition proj_informative '(exist _ x _ : { x:A | P x }) : A := x. +Print proj_informative. + +Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo. +Definition foo '(Bar n b tt p) := + if b then n+p else n-p. +Print foo. + +Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1. +Print baz. + +Module WithParameters. + +Definition swap {A B} '((x,y) : A*B) := (y,x). +Print swap. + +Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x). +Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x). + +Check exists '((x,y):A*A), swap (x,y) = (y,x). +Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w). + +End WithParameters. + +(** Some test involving unicode notations. *) +Module WithUnicode. + + Import Coq.Unicode.Utf8. + + Check λ '((x,y) : A*B), (y,x). + Check ∀ '(x,y), swap (x,y) = (y,x). + +End WithUnicode. + +(** * Suboptimal printing *) + +Module Suboptimal. + +(** This test shows an example which exposes the [let] introduced by + the pattern notation in binders. *) + +#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. +Definition F '(n,p) : Type := (Fin n * Fin p)%type. +Definition both_z '(n,p) : F (n,p) := (Z _,Z _). +Print both_z. + +(** Test factorization of binders *) + +Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t). +Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t). + +End Suboptimal. + +(** Test risk of collision for internal name *) +Check fun pat => fun '(x,y) => x+y = pat. + +(** Test name in degenerate case *) +Definition f 'x := x+x. +Print f. +Check fun 'x => x+x. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out new file mode 100644 index 0000000000..3f4d5ef58c --- /dev/null +++ b/test-suite/output/PrintAssumptions.out @@ -0,0 +1,24 @@ +Axioms: +foo : nat +Axioms: +foo : nat +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Axioms: +extensionality : forall (P Q : Type) (f g : P -> Q), + (forall x : P, f x = g x) -> f = g +Closed under the global context +Closed under the global context +Axioms: +M.foo : False +Closed under the global context +Closed under the global context +Closed under the global context +Closed under the global context diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v new file mode 100644 index 0000000000..3d4dfe603d --- /dev/null +++ b/test-suite/output/PrintAssumptions.v @@ -0,0 +1,149 @@ + +(** Print Assumption and opaque modules : + + Print Assumption used to consider as axioms the modular fields + unexported by their signature, cf bug report #2186. This should + now be fixed, let's test this here. *) + +(* First, a minimal test-case *) + +Axiom foo : nat. + +Module Type T. + Parameter bar : nat. +End T. + +Module M : T. + Module Hide. (* An entire sub-module could be hidden *) + Definition x := foo. + End Hide. + Definition bar := Hide.x. +End M. + +Module N (X:T) : T. + Definition y := X.bar. (* A non-exported field *) + Definition bar := y. +End N. + +Module P := N M. + +Print Assumptions M.bar. (* Should answer: foo *) +Print Assumptions P.bar. (* Should answer: foo *) + + +(* The original test-case of the bug-report *) + +Require Import Arith. + +Axiom extensionality : forall P Q (f g:P -> Q), + (forall x, f x = g x) -> f = g. + +Module Type ADD_COMM_EXT. + Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x). +End ADD_COMM_EXT. + +Module AddCommExt_Opaque : ADD_COMM_EXT. + Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x). + Proof. + intro n; apply extensionality; auto with arith. + Qed. +End AddCommExt_Opaque. + +Module AddCommExt_Transparent <: ADD_COMM_EXT. + Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x). + Proof. + intro n; apply extensionality; auto with arith. + Qed. +End AddCommExt_Transparent. + +Print Assumptions AddCommExt_Opaque.add_comm_ext. +(* Should answer: extensionality *) + +Print Assumptions AddCommExt_Transparent.add_comm_ext. +(* Should answer: extensionality *) + +Lemma add1_comm_ext_opaque : + (fun x => x + 1) = (fun x => 1 + x). +Proof (AddCommExt_Opaque.add_comm_ext 1). + +Lemma add1_comm_ext_transparent : + (fun x => x + 1) = (fun x => 1 + x). +Proof (AddCommExt_Transparent.add_comm_ext 1). + +Print Assumptions add1_comm_ext_opaque. +(* Should answer: extensionality *) + +Print Assumptions add1_comm_ext_transparent. +(* Should answer: extensionality *) + +Module Type FALSE_POSITIVE. + Axiom add_comm : forall n x, x + n = n + x. +End FALSE_POSITIVE. + +Module false_positive : FALSE_POSITIVE. + Lemma add_comm : forall n x, x + n = n + x. + Proof. auto with arith. Qed. + + Print Assumptions add_comm. + (* Should answer : Closed under the global context *) +End false_positive. + +Lemma comm_plus5 : forall x, + x + 5 = 5 + x. +Proof (false_positive.add_comm 5). + +Print Assumptions comm_plus5. +(* Should answer : Closed under the global context *) + +(** Print Assumption and Include *) + +Module INCLUDE. + +Module M. +Axiom foo : False. +End M. + +Module N. +Include M. +End N. + +Print Assumptions N.foo. + +End INCLUDE. + +(* Print Assumptions did not enter implementation of submodules (#7192) *) + +Module SUBMODULES. + +Definition a := True. +Module Type B. Axiom f : Prop. End B. +Module Type C. Declare Module D : B. End C. +Module E: C. + Module D <: B. Definition f := a. End D. +End E. +Print Assumptions E.D.f. + +(* Idem in the scope of a functor *) + +Module Type T. End T. +Module F (X : T). + Definition a := True. + Module Type B. Axiom f : Prop. End B. + Module Type C. Declare Module D : B. End C. + Module E: C. + Module D <: B. Definition f := a. End D. + End E. + Print Assumptions E.D.f. +End F. + +End SUBMODULES. + +(* Testing a variant of #7192 across files *) +(* This was missing in the original fix to #7192 *) +Require Import module_bug7192. +Print Assumptions M7192.D.f. + +(* Testing reporting assumptions from modules in files *) +(* A regression introduced in the original fix to #7192 was missing implementations *) +Require Import module_bug8416. +Print Assumptions M8416.f. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out new file mode 100644 index 0000000000..da1fca7134 --- /dev/null +++ b/test-suite/output/PrintInfos.out @@ -0,0 +1,117 @@ +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} + +existT is template universe polymorphic +Argument A is implicit +Argument scopes are [type_scope function_scope _ _] +Expands to: Constructor Coq.Init.Specif.existT +Inductive sigT (A : Type) (P : A -> Type) : Type := + existT : forall x : A, P x -> {x : A & P x} + +For sigT: Argument A is implicit +For existT: Argument A is implicit +For sigT: Argument scopes are [type_scope type_scope] +For existT: Argument scopes are [type_scope function_scope _ _] +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} + +Argument A is implicit +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments A, x are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument A is implicit +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] +eq_refl : forall (A : Type) (x : A), x = x + +eq_refl is not universe polymorphic +When applied to no arguments: + Arguments A, x are implicit and maximally inserted +When applied to 1 argument: + Argument A is implicit +Argument scopes are [type_scope _] +Expands to: Constructor Coq.Init.Logic.eq_refl +eq_refl : forall (A : Type) (x : A), x = x + +When applied to no arguments: + Arguments A, x are implicit and maximally inserted +When applied to 1 argument: + Argument A is implicit +Nat.add = +fix add (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (add p m) + end + : nat -> nat -> nat + +Nat.add is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +Nat.add : nat -> nat -> nat + +Nat.add is not universe polymorphic +Argument scopes are [nat_scope nat_scope] +Nat.add is transparent +Expands to: Constant Coq.Init.Nat.add +Nat.add : nat -> nat -> nat + +plus_n_O : forall n : nat, n = n + 0 + +plus_n_O is not universe polymorphic +Argument scope is [nat_scope] +plus_n_O is opaque +Expands to: Constant Coq.Init.Peano.plus_n_O +Inductive le (n : nat) : nat -> Prop := + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + +For le_S: Argument m is implicit +For le_S: Argument n is implicit and maximally inserted +For le: Argument scopes are [nat_scope nat_scope] +For le_n: Argument scope is [nat_scope] +For le_S: Argument scopes are [nat_scope nat_scope _] +comparison : Set + +comparison is not universe polymorphic +Expands to: Inductive Coq.Init.Datatypes.comparison +Inductive comparison : Set := + Eq : comparison | Lt : comparison | Gt : comparison +bar : foo + +bar is not universe polymorphic +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +Expands to: Constant PrintInfos.bar +*** [ bar : foo ] + +bar is not universe polymorphic +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +Module Coq.Init.Peano +Notation sym_eq := eq_sym +Expands to: Notation Coq.Init.Logic.sym_eq +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments A, x are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument A is implicit and maximally inserted +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] +n:nat + +Hypothesis of the goal context. +h:(n <> newdef n) + +Hypothesis of the goal context. +g:(nat -> nat) + +Constant (let in) of the goal context. +h:(n <> newdef n) + +Hypothesis of the goal context. diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v new file mode 100644 index 0000000000..d7c271c3ec --- /dev/null +++ b/test-suite/output/PrintInfos.v @@ -0,0 +1,48 @@ +(* coq-prog-args: ("-top" "PrintInfos") *) +About existT. +Print existT. +Print Implicit existT. + +Print eq_refl. +About eq_refl. +Print Implicit eq_refl. + +Print Nat.add. +About Nat.add. +Print Implicit Nat.add. + +About plus_n_O. + +Arguments le_S {n} [m] _. +Print le_S. + +About comparison. +Print comparison. + +Definition foo := forall x, x = 0. +Parameter bar : foo. + +Arguments bar [x]. +About bar. +Print bar. + +About Peano. (* Module *) +About sym_eq. (* Notation *) + +Arguments eq_refl {A} {x}, {A} x. +Print eq_refl. + + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. + intros n h h'. + About n. (* search hypothesis *) + About h. (* search hypothesis *) +Abort. + +Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False. + intros n g h h'. + About g. (* search hypothesis *) + About h. (* search hypothesis *) +Abort. diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out new file mode 100644 index 0000000000..1a9bc068c5 --- /dev/null +++ b/test-suite/output/PrintModule.out @@ -0,0 +1,9 @@ +Module N : S with Definition T := nat := M + +Module N : S with Definition T := M + +Module N : S with Module T := K := M + +Module N : S with Module T := M + +Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v new file mode 100644 index 0000000000..54ef305be4 --- /dev/null +++ b/test-suite/output/PrintModule.v @@ -0,0 +1,62 @@ +(* Bug #2169 *) + +Module FOO. + +Module M. + Definition T := nat. +End M. + +Module Type S. + Parameter T : Set. +End S. + +Module N : S with Definition T := nat := M. + +Print Module N. + +Set Short Module Printing. +Print Module N. +Unset Short Module Printing. + +End FOO. + +Module BAR. + +Module K. End K. +Module Type KS. End KS. + +Module M. + Module T := K. +End M. + +Module Type S. + Declare Module T : KS. +End S. + +Module N : S with Module T := K := M. + +Print Module N. + +Set Short Module Printing. +Print Module N. +Unset Short Module Printing. + +End BAR. + +(* Bug #4661 *) + +Module QUX. + +Module Type Test. + Parameter t : Type. +End Test. + +Module Type Func (T:Test). + Parameter x : T.t. +End Func. + +Module Shortest_path (T : Test). +Print Func. +End Shortest_path. + +End QUX. diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out new file mode 100644 index 0000000000..c42e15e4e8 --- /dev/null +++ b/test-suite/output/PrintUnivsSubgraph.out @@ -0,0 +1,5 @@ +Prop < Set +Set < i + < j +i < j + diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v new file mode 100644 index 0000000000..ec9cf44d4f --- /dev/null +++ b/test-suite/output/PrintUnivsSubgraph.v @@ -0,0 +1,9 @@ + +Universes i j k l. + +Definition foo : Type@{j} := Type@{i}. + +Definition baz : Type@{k} := Type@{l}. + +Print Universes Subgraph(i j). +(* should print [i < j], not [l < k] (and not prelude universes) *) diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out new file mode 100644 index 0000000000..e9c28faf1d --- /dev/null +++ b/test-suite/output/Projections.out @@ -0,0 +1,2 @@ +fun S : store => S.(store_funcs) + : store -> host_func diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v new file mode 100644 index 0000000000..2713e6a188 --- /dev/null +++ b/test-suite/output/Projections.v @@ -0,0 +1,11 @@ + +Set Printing Projections. + +Class HostFunction := host_func : Type. + +Section store. + Context `{HostFunction}. + #[universes(template)] Record store := { store_funcs : host_func }. +End store. + +Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out new file mode 100644 index 0000000000..998eb37cc8 --- /dev/null +++ b/test-suite/output/Quote.out @@ -0,0 +1,24 @@ +(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx)) +(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx)))))) +1 subgoal + + H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ + B + ============================ + interp_f + (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) + (f_and (f_atom (Left_idx End_idx)) + (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) + (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx))))) +1 subgoal + + H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ + B + ============================ + interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx))))) diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out new file mode 100644 index 0000000000..e6f7556d96 --- /dev/null +++ b/test-suite/output/RealSyntax.out @@ -0,0 +1,4 @@ +32%R + : R +(-31)%R + : R diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v new file mode 100644 index 0000000000..15ae66010e --- /dev/null +++ b/test-suite/output/RealSyntax.v @@ -0,0 +1,3 @@ +Require Import Reals. +Check 32%R. +Check (-31)%R. diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.out diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v new file mode 100644 index 0000000000..cd667bbd00 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) + +(* Test that mentioning a warning defined in plugins works. The failure +mode here is that these result in a warning about unknown warnings, since the +plugins are not known at command line parsing time. *) diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out new file mode 100644 index 0000000000..d45343fe60 --- /dev/null +++ b/test-suite/output/Record.out @@ -0,0 +1,32 @@ +{| field := 5 |} + : test +{| field := 5 |} + : test +{| field_r := 5 |} + : test_r +build_c 5 + : test_c +build 5 + : test +build 5 + : test +{| field_r := 5 |} + : test_r +build_c 5 + : test_c +fun '(C _ p) => p + : N -> True +fun '{| T := T |} => T + : N -> Type +fun '(C T p) => (T, p) + : N -> Type * True +fun '{| q := p |} => p + : M -> True +fun '{| U := T |} => T + : M -> Type +fun '{| U := T; q := p |} => (T, p) + : M -> Type * True +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v new file mode 100644 index 0000000000..4fe7b051f8 --- /dev/null +++ b/test-suite/output/Record.v @@ -0,0 +1,33 @@ +Record test := build { field : nat }. +Record test_r := build_r { field_r : nat }. +Record test_c := build_c { field_c : nat }. + +Add Printing Constructor test_c. +Add Printing Record test_r. + +Set Printing Records. + +Check build 5. +Check {| field := 5 |}. + +Check build_r 5. +Check build_c 5. + +Unset Printing Records. + +Check build 5. +Check {| field := 5 |}. +Check build_r 5. +Check build_c 5. + +#[universes(template)] Record N := C { T : Type; _ : True }. +Check fun x:N => let 'C _ p := x in p. +Check fun x:N => let 'C T _ := x in T. +Check fun x:N => let 'C T p := x in (T,p). + +#[universes(template)] Record M := D { U : Type; a := 0; q : True }. +Check fun x:M => let 'D T _ p := x in p. +Check fun x:M => let 'D T _ p := x in T. +Check fun x:M => let 'D T p := x in (T,p). +Check fun x:M => let 'D T a p := x in (T,p,a). +Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out new file mode 100644 index 0000000000..5b67f632c9 --- /dev/null +++ b/test-suite/output/RecordFieldErrors.out @@ -0,0 +1,14 @@ +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record contains fields of both t and t'. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record defines several times the field foo. +The command has indeed failed with message: +This record defines several times the field unit. +The command has indeed failed with message: +unit: Not a projection of inductive t. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v new file mode 100644 index 0000000000..27aa07822b --- /dev/null +++ b/test-suite/output/RecordFieldErrors.v @@ -0,0 +1,38 @@ +(** Check that various errors in record fields are reported with the correct +underlying issue. *) + +Record t := + { foo: unit }. + +Record t' := + { bar: unit }. + +Fail Check {| unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| unit := tt; + foo := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + bar := tt |}. +(* This record contains fields of both t and t'. *) + +Fail Check {| unit := tt; + unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + foo := tt |}. +(* This record defines several times the field foo. *) + +Fail Check {| foo := tt; + unit := tt; + unit := tt |}. +(* This is slightly wrong (would prefer "unit: Not a projection."), but it's +acceptable and seems an unlikely mistake. *) +(* This record defines several times the field unit. *) + +Fail Check {| foo := tt; + unit := tt |}. +(* unit: Not a projection of inductive t. *) diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out new file mode 100644 index 0000000000..7c80a6065f --- /dev/null +++ b/test-suite/output/RecordMissingField.out @@ -0,0 +1,4 @@ +File "stdin", line 8, characters 5-22: +Error: Cannot infer field y2p of record point2d in environment: +p : point2d + diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v new file mode 100644 index 0000000000..84f1748fa0 --- /dev/null +++ b/test-suite/output/RecordMissingField.v @@ -0,0 +1,8 @@ +(** Check for error message when missing a record field. Error message +should contain missing field, and the inferred type of the record **) + +Record point2d := mkPoint { x2p: nat; y2p: nat }. + + +Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + 1; |}. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out new file mode 100644 index 0000000000..f4544a0df3 --- /dev/null +++ b/test-suite/output/Search.out @@ -0,0 +1,126 @@ +le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n +le_S: forall n m : nat, n <= m -> n <= S m +le_n_S: forall n m : nat, n <= m -> S n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +le_ind: + forall (n : nat) (P : nat -> Prop), + P n -> + (forall m : nat, n <= m -> P m -> P (S m)) -> + forall n0 : nat, n <= n0 -> P n0 +false: bool +true: bool +is_true: bool -> Prop +negb: bool -> bool +eq_true: bool -> Prop +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +BoolSpec: Prop -> Prop -> bool -> Prop +Nat.eqb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b +eq_true_rec: + forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_rect_r: + forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +Byte.to_bits: + Byte.byte -> + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) +Byte.of_bits: + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> + Byte.byte +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +BoolSpec_ind: + forall (P Q : Prop) (P0 : bool -> Prop), + (P -> P0 true) -> + (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b +Byte.to_bits_of_bits: + forall + b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), + Byte.to_bits (Byte.of_bits b) = b +bool_choice: + forall (S : Set) (R1 R2 : S -> Prop), + (forall x : S, {R1 x} + {R2 x}) -> + {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 +n_Sn: forall n : nat, n <> S n +pred_Sn: forall n : nat, n = Nat.pred (S n) +O_S: forall n : nat, 0 <> S n +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_S: forall x y : nat, x = y -> S x = S y +eq_add_S: forall n m : nat, S n = S m -> n = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y +not_eq_S: forall n m : nat, n <> m -> S n <> S m +mult_n_Sm: forall n m : nat, n * m + n = n * S m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +f_equal2_nat: + forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), + x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +bool_choice: + forall (S : Set) (R1 R2 : S -> Prop), + (forall x : S, {R1 x} + {R2 x}) -> + {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +h: n <> newdef n +h': newdef n <> n +h: n <> newdef n +h': newdef n <> n +h: n <> newdef n +h: n <> newdef n +h: n <> newdef n +h': newdef n <> n +The command has indeed failed with message: +No such goal. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +h: P n +h': ~ P n +h: P n +h': ~ P n +h: P n +h': ~ P n +h: P n +h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v new file mode 100644 index 0000000000..82096f29bf --- /dev/null +++ b/test-suite/output/Search.v @@ -0,0 +1,37 @@ +(* Some tests of the Search command *) + +Search le. (* app nodes *) +Search bool. (* no apps *) +Search (@eq nat). (* complex pattern *) +Search (@eq _ _ true). +Search (@eq _ _ _) true -false. (* andb_prop *) +Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. + cut False. + intros _ n h h'. + Search n. (* search hypothesis *) + Search newdef. (* search hypothesis *) + Search ( _ <> newdef _). (* search hypothesis, pattern *) + Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) + + 1:Search newdef. + 2:Search newdef. + + Fail 3:Search newdef. + Fail 1-2:Search newdef. + Fail all:Search newdef. +Abort. + +Goal forall n (P:nat -> Prop), P n -> ~P n -> False. + intros n P h h'. + Search P. (* search hypothesis also for patterns *) + Search (P _). (* search hypothesis also for patterns *) + Search (P n). (* search hypothesis also for patterns *) + Search (P _) -"h'". (* search hypothesis also for patterns *) + Search (P _) -not. (* search hypothesis also for patterns *) + +Abort. + diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out new file mode 100644 index 0000000000..7038eac22c --- /dev/null +++ b/test-suite/output/SearchHead.out @@ -0,0 +1,39 @@ +le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n +le_S: forall n m : nat, n <= m -> n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_n_S: forall n m : nat, n <= m -> S n <= S m +le_S_n: forall n m : nat, S n <= S m -> n <= m +false: bool +true: bool +negb: bool -> bool +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.eqb: nat -> nat -> bool +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 +pred_Sn: forall n : nat, n = Nat.pred (S n) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_add_S: forall n m : nat, S n = S m -> n = m +eq_S: forall x y : nat, x = y -> S x = S y +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +mult_n_Sm: forall n m : nat, n * m + n = n * S m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +h: newdef n +h: P n diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v new file mode 100644 index 0000000000..2ee8a0d184 --- /dev/null +++ b/test-suite/output/SearchHead.v @@ -0,0 +1,19 @@ +(* Some tests of the Search command *) + +SearchHead le. (* app nodes *) +SearchHead bool. (* no apps *) +SearchHead (@eq nat). (* complex pattern *) + +Definition newdef := fun x:nat => x = x. + +Goal forall n:nat, newdef n -> False. + intros n h. + SearchHead newdef. (* search hypothesis *) +Abort. + + +Goal forall n (P:nat -> Prop), P n -> False. + intros n P h. + SearchHead P. (* search hypothesis also for patterns *) +Abort. + diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out new file mode 100644 index 0000000000..b0ac9ea29f --- /dev/null +++ b/test-suite/output/SearchPattern.out @@ -0,0 +1,90 @@ +false: bool +true: bool +negb: bool -> bool +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.eqb: nat -> nat -> bool +Nat.two: nat +Nat.one: nat +Nat.zero: nat +O: nat +Nat.div2: nat -> nat +Nat.log2: nat -> nat +Nat.succ: nat -> nat +Nat.sqrt: nat -> nat +Nat.pred: nat -> nat +Nat.double: nat -> nat +Nat.square: nat -> nat +S: nat -> nat +Nat.ldiff: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat +Nat.land: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat +Nat.div: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.mul: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.of_uint: Decimal.uint -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat +Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +length: forall A : Type, list A -> nat +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +Nat.div2: nat -> nat +Nat.sqrt: nat -> nat +Nat.log2: nat -> nat +Nat.double: nat -> nat +Nat.pred: nat -> nat +Nat.square: nat -> nat +Nat.succ: nat -> nat +S: nat -> nat +Nat.ldiff: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.land: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.div: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.mul: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.min: nat -> nat -> nat +Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_uint_acc: Decimal.uint -> nat -> nat +Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +mult_n_Sm: forall n m : nat, n * m + n = n * S m +iff_refl: forall A : Prop, A <-> A +le_n: forall n : nat, n <= n +identity_refl: forall (A : Type) (a : A), identity a a +eq_refl: forall (A : Type) (x : A), x = x +Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B +Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +h: n <> newdef n +h: n <> newdef n +h: P n +h': ~ P n +h: P n +h: P n diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v new file mode 100644 index 0000000000..de9f48873a --- /dev/null +++ b/test-suite/output/SearchPattern.v @@ -0,0 +1,36 @@ +(* Some tests of the SearchPattern command *) + +(* Simple, random tests *) +SearchPattern bool. +SearchPattern nat. +SearchPattern le. + +(* With some hypothesis *) +SearchPattern (nat -> nat). +SearchPattern (?n * ?m + ?n = ?n * S ?m). + +(* Non-linearity *) +SearchPattern (_ ?X ?X). + +(* Non-linearity with hypothesis *) +SearchPattern (forall (x:?A) (y:?B), _ ?A ?B). + +(* No delta-reduction *) +SearchPattern (Exc _). + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n <> newdef n -> False. + intros n h. + SearchPattern ( _ <> newdef _). (* search hypothesis *) + SearchPattern ( n <> newdef _). (* search hypothesis *) +Abort. + +Goal forall n (P:nat -> Prop), P n -> ~P n -> False. + intros n P h h'. + SearchPattern (P _). (* search hypothesis also for patterns *) + Search (~P n). (* search hypothesis also for patterns *) + Search (P _) -"h'". (* search hypothesis also for patterns *) + Search (P _) -not. (* search hypothesis also for patterns *) + +Abort. diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out new file mode 100644 index 0000000000..5edea5dff6 --- /dev/null +++ b/test-suite/output/SearchRewrite.out @@ -0,0 +1,5 @@ +plus_n_O: forall n : nat, n = n + 0 +plus_O_n: forall n : nat, 0 + n = n +h: n = newdef n +h: n = newdef n +h: n = newdef n diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v new file mode 100644 index 0000000000..53d043c681 --- /dev/null +++ b/test-suite/output/SearchRewrite.v @@ -0,0 +1,13 @@ +(* Some tests of the SearchRewrite command *) + +SearchRewrite (_+0). (* left *) +SearchRewrite (0+_). (* right *) + +Definition newdef := fun x:nat => x. + +Goal forall n:nat, n = newdef n -> False. + intros n h. + SearchRewrite (newdef _). + SearchRewrite n. (* use hypothesis for patterns *) + SearchRewrite (newdef n). (* use hypothesis for patterns *) +Abort. diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out new file mode 100644 index 0000000000..ca56f032ff --- /dev/null +++ b/test-suite/output/Show.out @@ -0,0 +1,10 @@ +3 subgoals (ID 31) + + H : 0 = 0 + ============================ + 1 = 1 + +subgoal 2 (ID 35) is: + 1 = S (S m') +subgoal 3 (ID 22) is: + S (S n') = S m diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v new file mode 100644 index 0000000000..60faac8dd9 --- /dev/null +++ b/test-suite/output/Show.v @@ -0,0 +1,11 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) + +(* tests of Show output with -emacs flag to coqtop; see bug 5535 *) + +Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). +Proof. + intros. + induction n as [| n']. + induction m as [| m']. + Show. +Admitted. diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out new file mode 100644 index 0000000000..e5520b8dfa --- /dev/null +++ b/test-suite/output/ShowMatch.out @@ -0,0 +1,8 @@ +match # with + | f => + end + +match # with + | A.f => + end + diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v new file mode 100644 index 0000000000..99183f2064 --- /dev/null +++ b/test-suite/output/ShowMatch.v @@ -0,0 +1,14 @@ +(* Bug 5546 complained about unqualified constructors in Show Match output, + when qualification is needed to disambiguate them +*) + +Module A. + #[universes(template)] Inductive foo := f. + Show Match foo. (* no need to disambiguate *) +End A. + +Module B. + #[universes(template)] Inductive foo := f. + (* local foo shadows A.foo, so constructor "f" needs disambiguation *) + Show Match A.foo. +End B. diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out new file mode 100644 index 0000000000..2d4be8bce7 --- /dev/null +++ b/test-suite/output/ShowProof.out @@ -0,0 +1 @@ +(fun x : Type => conj I ?Goal) diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v new file mode 100644 index 0000000000..19822ac50e --- /dev/null +++ b/test-suite/output/ShowProof.v @@ -0,0 +1,7 @@ +(* Was #4524 *) +Definition foo (x : Type) : True /\ True. +Proof. +split. +- exact I. + Show Proof. (* Was not finding an evar name at some time *) +Abort. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out new file mode 100644 index 0000000000..c7e6ef950e --- /dev/null +++ b/test-suite/output/StringSyntax.out @@ -0,0 +1,1089 @@ +byte_rect = +fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") + (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") + (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") + (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") + (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => +match b as b0 return (P b0) with +| "000" => f +| "001" => f0 +| "002" => f1 +| "003" => f2 +| "004" => f3 +| "005" => f4 +| "006" => f5 +| "007" => f6 +| "008" => f7 +| "009" => f8 +| "010" => f9 +| "011" => f10 +| "012" => f11 +| "013" => f12 +| "014" => f13 +| "015" => f14 +| "016" => f15 +| "017" => f16 +| "018" => f17 +| "019" => f18 +| "020" => f19 +| "021" => f20 +| "022" => f21 +| "023" => f22 +| "024" => f23 +| "025" => f24 +| "026" => f25 +| "027" => f26 +| "028" => f27 +| "029" => f28 +| "030" => f29 +| "031" => f30 +| " " => f31 +| "!" => f32 +| """" => f33 +| "#" => f34 +| "$" => f35 +| "%" => f36 +| "&" => f37 +| "'" => f38 +| "(" => f39 +| ")" => f40 +| "*" => f41 +| "+" => f42 +| "," => f43 +| "-" => f44 +| "." => f45 +| "/" => f46 +| "0" => f47 +| "1" => f48 +| "2" => f49 +| "3" => f50 +| "4" => f51 +| "5" => f52 +| "6" => f53 +| "7" => f54 +| "8" => f55 +| "9" => f56 +| ":" => f57 +| ";" => f58 +| "<" => f59 +| "=" => f60 +| ">" => f61 +| "?" => f62 +| "@" => f63 +| "A" => f64 +| "B" => f65 +| "C" => f66 +| "D" => f67 +| "E" => f68 +| "F" => f69 +| "G" => f70 +| "H" => f71 +| "I" => f72 +| "J" => f73 +| "K" => f74 +| "L" => f75 +| "M" => f76 +| "N" => f77 +| "O" => f78 +| "P" => f79 +| "Q" => f80 +| "R" => f81 +| "S" => f82 +| "T" => f83 +| "U" => f84 +| "V" => f85 +| "W" => f86 +| "X" => f87 +| "Y" => f88 +| "Z" => f89 +| "[" => f90 +| "\" => f91 +| "]" => f92 +| "^" => f93 +| "_" => f94 +| "`" => f95 +| "a" => f96 +| "b" => f97 +| "c" => f98 +| "d" => f99 +| "e" => f100 +| "f" => f101 +| "g" => f102 +| "h" => f103 +| "i" => f104 +| "j" => f105 +| "k" => f106 +| "l" => f107 +| "m" => f108 +| "n" => f109 +| "o" => f110 +| "p" => f111 +| "q" => f112 +| "r" => f113 +| "s" => f114 +| "t" => f115 +| "u" => f116 +| "v" => f117 +| "w" => f118 +| "x" => f119 +| "y" => f120 +| "z" => f121 +| "{" => f122 +| "|" => f123 +| "}" => f124 +| "~" => f125 +| "127" => f126 +| "128" => f127 +| "129" => f128 +| "130" => f129 +| "131" => f130 +| "132" => f131 +| "133" => f132 +| "134" => f133 +| "135" => f134 +| "136" => f135 +| "137" => f136 +| "138" => f137 +| "139" => f138 +| "140" => f139 +| "141" => f140 +| "142" => f141 +| "143" => f142 +| "144" => f143 +| "145" => f144 +| "146" => f145 +| "147" => f146 +| "148" => f147 +| "149" => f148 +| "150" => f149 +| "151" => f150 +| "152" => f151 +| "153" => f152 +| "154" => f153 +| "155" => f154 +| "156" => f155 +| "157" => f156 +| "158" => f157 +| "159" => f158 +| "160" => f159 +| "161" => f160 +| "162" => f161 +| "163" => f162 +| "164" => f163 +| "165" => f164 +| "166" => f165 +| "167" => f166 +| "168" => f167 +| "169" => f168 +| "170" => f169 +| "171" => f170 +| "172" => f171 +| "173" => f172 +| "174" => f173 +| "175" => f174 +| "176" => f175 +| "177" => f176 +| "178" => f177 +| "179" => f178 +| "180" => f179 +| "181" => f180 +| "182" => f181 +| "183" => f182 +| "184" => f183 +| "185" => f184 +| "186" => f185 +| "187" => f186 +| "188" => f187 +| "189" => f188 +| "190" => f189 +| "191" => f190 +| "192" => f191 +| "193" => f192 +| "194" => f193 +| "195" => f194 +| "196" => f195 +| "197" => f196 +| "198" => f197 +| "199" => f198 +| "200" => f199 +| "201" => f200 +| "202" => f201 +| "203" => f202 +| "204" => f203 +| "205" => f204 +| "206" => f205 +| "207" => f206 +| "208" => f207 +| "209" => f208 +| "210" => f209 +| "211" => f210 +| "212" => f211 +| "213" => f212 +| "214" => f213 +| "215" => f214 +| "216" => f215 +| "217" => f216 +| "218" => f217 +| "219" => f218 +| "220" => f219 +| "221" => f220 +| "222" => f221 +| "223" => f222 +| "224" => f223 +| "225" => f224 +| "226" => f225 +| "227" => f226 +| "228" => f227 +| "229" => f228 +| "230" => f229 +| "231" => f230 +| "232" => f231 +| "233" => f232 +| "234" => f233 +| "235" => f234 +| "236" => f235 +| "237" => f236 +| "238" => f237 +| "239" => f238 +| "240" => f239 +| "241" => f240 +| "242" => f241 +| "243" => f242 +| "244" => f243 +| "245" => f244 +| "246" => f245 +| "247" => f246 +| "248" => f247 +| "249" => f248 +| "250" => f249 +| "251" => f250 +| "252" => f251 +| "253" => f252 +| "254" => f253 +| "255" => f254 +end + : forall P : byte -> Type, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_rect is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +byte_rec = +fun P : byte -> Set => byte_rect P + : forall P : byte -> Set, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_rec is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +byte_ind = +fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") + (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") + (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") + (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") + (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => +match b as b0 return (P b0) with +| "000" => f +| "001" => f0 +| "002" => f1 +| "003" => f2 +| "004" => f3 +| "005" => f4 +| "006" => f5 +| "007" => f6 +| "008" => f7 +| "009" => f8 +| "010" => f9 +| "011" => f10 +| "012" => f11 +| "013" => f12 +| "014" => f13 +| "015" => f14 +| "016" => f15 +| "017" => f16 +| "018" => f17 +| "019" => f18 +| "020" => f19 +| "021" => f20 +| "022" => f21 +| "023" => f22 +| "024" => f23 +| "025" => f24 +| "026" => f25 +| "027" => f26 +| "028" => f27 +| "029" => f28 +| "030" => f29 +| "031" => f30 +| " " => f31 +| "!" => f32 +| """" => f33 +| "#" => f34 +| "$" => f35 +| "%" => f36 +| "&" => f37 +| "'" => f38 +| "(" => f39 +| ")" => f40 +| "*" => f41 +| "+" => f42 +| "," => f43 +| "-" => f44 +| "." => f45 +| "/" => f46 +| "0" => f47 +| "1" => f48 +| "2" => f49 +| "3" => f50 +| "4" => f51 +| "5" => f52 +| "6" => f53 +| "7" => f54 +| "8" => f55 +| "9" => f56 +| ":" => f57 +| ";" => f58 +| "<" => f59 +| "=" => f60 +| ">" => f61 +| "?" => f62 +| "@" => f63 +| "A" => f64 +| "B" => f65 +| "C" => f66 +| "D" => f67 +| "E" => f68 +| "F" => f69 +| "G" => f70 +| "H" => f71 +| "I" => f72 +| "J" => f73 +| "K" => f74 +| "L" => f75 +| "M" => f76 +| "N" => f77 +| "O" => f78 +| "P" => f79 +| "Q" => f80 +| "R" => f81 +| "S" => f82 +| "T" => f83 +| "U" => f84 +| "V" => f85 +| "W" => f86 +| "X" => f87 +| "Y" => f88 +| "Z" => f89 +| "[" => f90 +| "\" => f91 +| "]" => f92 +| "^" => f93 +| "_" => f94 +| "`" => f95 +| "a" => f96 +| "b" => f97 +| "c" => f98 +| "d" => f99 +| "e" => f100 +| "f" => f101 +| "g" => f102 +| "h" => f103 +| "i" => f104 +| "j" => f105 +| "k" => f106 +| "l" => f107 +| "m" => f108 +| "n" => f109 +| "o" => f110 +| "p" => f111 +| "q" => f112 +| "r" => f113 +| "s" => f114 +| "t" => f115 +| "u" => f116 +| "v" => f117 +| "w" => f118 +| "x" => f119 +| "y" => f120 +| "z" => f121 +| "{" => f122 +| "|" => f123 +| "}" => f124 +| "~" => f125 +| "127" => f126 +| "128" => f127 +| "129" => f128 +| "130" => f129 +| "131" => f130 +| "132" => f131 +| "133" => f132 +| "134" => f133 +| "135" => f134 +| "136" => f135 +| "137" => f136 +| "138" => f137 +| "139" => f138 +| "140" => f139 +| "141" => f140 +| "142" => f141 +| "143" => f142 +| "144" => f143 +| "145" => f144 +| "146" => f145 +| "147" => f146 +| "148" => f147 +| "149" => f148 +| "150" => f149 +| "151" => f150 +| "152" => f151 +| "153" => f152 +| "154" => f153 +| "155" => f154 +| "156" => f155 +| "157" => f156 +| "158" => f157 +| "159" => f158 +| "160" => f159 +| "161" => f160 +| "162" => f161 +| "163" => f162 +| "164" => f163 +| "165" => f164 +| "166" => f165 +| "167" => f166 +| "168" => f167 +| "169" => f168 +| "170" => f169 +| "171" => f170 +| "172" => f171 +| "173" => f172 +| "174" => f173 +| "175" => f174 +| "176" => f175 +| "177" => f176 +| "178" => f177 +| "179" => f178 +| "180" => f179 +| "181" => f180 +| "182" => f181 +| "183" => f182 +| "184" => f183 +| "185" => f184 +| "186" => f185 +| "187" => f186 +| "188" => f187 +| "189" => f188 +| "190" => f189 +| "191" => f190 +| "192" => f191 +| "193" => f192 +| "194" => f193 +| "195" => f194 +| "196" => f195 +| "197" => f196 +| "198" => f197 +| "199" => f198 +| "200" => f199 +| "201" => f200 +| "202" => f201 +| "203" => f202 +| "204" => f203 +| "205" => f204 +| "206" => f205 +| "207" => f206 +| "208" => f207 +| "209" => f208 +| "210" => f209 +| "211" => f210 +| "212" => f211 +| "213" => f212 +| "214" => f213 +| "215" => f214 +| "216" => f215 +| "217" => f216 +| "218" => f217 +| "219" => f218 +| "220" => f219 +| "221" => f220 +| "222" => f221 +| "223" => f222 +| "224" => f223 +| "225" => f224 +| "226" => f225 +| "227" => f226 +| "228" => f227 +| "229" => f228 +| "230" => f229 +| "231" => f230 +| "232" => f231 +| "233" => f232 +| "234" => f233 +| "235" => f234 +| "236" => f235 +| "237" => f236 +| "238" => f237 +| "239" => f238 +| "240" => f239 +| "241" => f240 +| "242" => f241 +| "243" => f242 +| "244" => f243 +| "245" => f244 +| "246" => f245 +| "247" => f246 +| "248" => f247 +| "249" => f248 +| "250" => f249 +| "251" => f250 +| "252" => f251 +| "253" => f252 +| "254" => f253 +| "255" => f254 +end + : forall P : byte -> Prop, + P "000" -> + P "001" -> + P "002" -> + P "003" -> + P "004" -> + P "005" -> + P "006" -> + P "007" -> + P "008" -> + P "009" -> + P "010" -> + P "011" -> + P "012" -> + P "013" -> + P "014" -> + P "015" -> + P "016" -> + P "017" -> + P "018" -> + P "019" -> + P "020" -> + P "021" -> + P "022" -> + P "023" -> + P "024" -> + P "025" -> + P "026" -> + P "027" -> + P "028" -> + P "029" -> + P "030" -> + P "031" -> + P " " -> + P "!" -> + P """" -> + P "#" -> + P "$" -> + P "%" -> + P "&" -> + P "'" -> + P "(" -> + P ")" -> + P "*" -> + P "+" -> + P "," -> + P "-" -> + P "." -> + P "/" -> + P "0" -> + P "1" -> + P "2" -> + P "3" -> + P "4" -> + P "5" -> + P "6" -> + P "7" -> + P "8" -> + P "9" -> + P ":" -> + P ";" -> + P "<" -> + P "=" -> + P ">" -> + P "?" -> + P "@" -> + P "A" -> + P "B" -> + P "C" -> + P "D" -> + P "E" -> + P "F" -> + P "G" -> + P "H" -> + P "I" -> + P "J" -> + P "K" -> + P "L" -> + P "M" -> + P "N" -> + P "O" -> + P "P" -> + P "Q" -> + P "R" -> + P "S" -> + P "T" -> + P "U" -> + P "V" -> + P "W" -> + P "X" -> + P "Y" -> + P "Z" -> + P "[" -> + P "\" -> + P "]" -> + P "^" -> + P "_" -> + P "`" -> + P "a" -> + P "b" -> + P "c" -> + P "d" -> + P "e" -> + P "f" -> + P "g" -> + P "h" -> + P "i" -> + P "j" -> + P "k" -> + P "l" -> + P "m" -> + P "n" -> + P "o" -> + P "p" -> + P "q" -> + P "r" -> + P "s" -> + P "t" -> + P "u" -> + P "v" -> + P "w" -> + P "x" -> + P "y" -> + P "z" -> + P "{" -> + P "|" -> + P "}" -> + P "~" -> + P "127" -> + P "128" -> + P "129" -> + P "130" -> + P "131" -> + P "132" -> + P "133" -> + P "134" -> + P "135" -> + P "136" -> + P "137" -> + P "138" -> + P "139" -> + P "140" -> + P "141" -> + P "142" -> + P "143" -> + P "144" -> + P "145" -> + P "146" -> + P "147" -> + P "148" -> + P "149" -> + P "150" -> + P "151" -> + P "152" -> + P "153" -> + P "154" -> + P "155" -> + P "156" -> + P "157" -> + P "158" -> + P "159" -> + P "160" -> + P "161" -> + P "162" -> + P "163" -> + P "164" -> + P "165" -> + P "166" -> + P "167" -> + P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b + +byte_ind is not universe polymorphic +Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +"000" + : byte +"a" + : byte +"127" + : byte +The command has indeed failed with message: +Expects a single character or a three-digits ascii code. +"000" + : ascii +"a" + : ascii +"127" + : ascii +The command has indeed failed with message: +Expects a single character or a three-digits ascii code. +"000" + : string +"a" + : string +"127" + : string +"€" + : string +"" + : string + = "a"%char + : ascii + = "a"%byte + : byte + = "a"%string + : string + = ["a"%byte] + : list byte + = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167"; + "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"] + : list byte + = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167"; + "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"] + : list ascii diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v new file mode 100644 index 0000000000..aab6e0bb03 --- /dev/null +++ b/test-suite/output/StringSyntax.v @@ -0,0 +1,52 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. +Import ListNotations. + +Set Printing Depth 100000. +Set Printing Width 1000. + +Close Scope char_scope. +Close Scope string_scope. + +Open Scope byte_scope. +Print byte_rect. +Print byte_rec. +Print byte_ind. +Check "000". +Check "a". +Check "127". +Fail Check "€". +Close Scope byte_scope. + +Open Scope char_scope. +Check "000". +Check "a". +Check "127". +Fail Check "€". +Close Scope char_scope. + +Open Scope string_scope. +Check "000". +Check "a". +Check "127". +Check "€". +Check String "001" EmptyString. +Close Scope string_scope. + +Compute ascii_of_byte "a". +Compute byte_of_ascii "a". +Compute string_of_list_byte ("a"::nil)%byte. +Compute list_byte_of_string "a". + +Local Open Scope byte_scope. +Compute List.fold_right + (fun n ls => match Byte.of_nat n with + | Some b => cons b ls + | None => ls + end) + nil + (List.seq 0 256). +Local Close Scope byte_scope. +Local Open Scope char_scope. +Compute List.map Ascii.ascii_of_nat (List.seq 0 256). +Local Close Scope char_scope. diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out new file mode 100644 index 0000000000..8d67a4a4b7 --- /dev/null +++ b/test-suite/output/SuggestProofUsing.out @@ -0,0 +1,7 @@ +The proof of nat should start with one of the following commands: +Proof using . +Proof using Type*. +Proof using Type. +The proof of foo should start with one of the following commands: +Proof using A B. +Proof using All. diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v new file mode 100644 index 0000000000..00b6f8e183 --- /dev/null +++ b/test-suite/output/SuggestProofUsing.v @@ -0,0 +1,31 @@ +Set Suggest Proof Using. + +Section Sec. + Variables A B : Type. + + (* Some normal lemma. *) + Lemma nat : Set. + Proof. + exact nat. + Qed. + + (* Make sure All is suggested even though we add an unused variable + to the context. *) + Let foo : Type. + Proof. + exact (A -> B). + Qed. + + (* Having a [Proof using] disables the suggestion message. *) + Definition bar : Type. + Proof using A. + exact A. + Qed. + + (* Transparent definitions don't get a suggestion message. *) + Definition baz : Type. + Proof. + exact A. + Defined. + +End Sec. diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out new file mode 100644 index 0000000000..bda6a68b01 --- /dev/null +++ b/test-suite/output/Sum.out @@ -0,0 +1,6 @@ +nat + nat + {True} + : Set +{True} + {True} + {True} + : Set +nat + {True} + {True} + : Set diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v new file mode 100644 index 0000000000..f12285a60c --- /dev/null +++ b/test-suite/output/Sum.v @@ -0,0 +1,3 @@ +Check (nat + nat + {True}). +Check ({True} + {True} + {True}). +Check (nat + {True} + {True}). diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out new file mode 100644 index 0000000000..19c9fc4423 --- /dev/null +++ b/test-suite/output/Tactics.out @@ -0,0 +1,8 @@ +Ltac f H := split; [ a H | e H ] +Ltac g := match goal with + | |- context [ if ?X then _ else _ ] => case X + end +The command has indeed failed with message: +H is already used. +The command has indeed failed with message: +H is already used. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v new file mode 100644 index 0000000000..fa12f09a46 --- /dev/null +++ b/test-suite/output/Tactics.v @@ -0,0 +1,24 @@ +(* Test printing of Tactic Notation *) + +Tactic Notation "a" constr(x) := apply x. +Tactic Notation "e" constr(x) := exact x. + +Ltac f H := split; [a H|e H]. +Print Ltac f. + +(* Test printing of match context *) +(* Used to fail after translator removal (see BZ#1070) *) + +Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end. +Print Ltac g. + +(* Test an error message (BZ#5390) *) +Lemma myid (P : Prop) : P <-> P. +Proof. split; auto. Qed. + +Goal True -> (True /\ True) -> True. +Proof. +intros H. +Fail intros [H%myid ?]. +Fail destruct 1 as [H%myid ?]. +Abort. diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out new file mode 100644 index 0000000000..67b65d4b81 --- /dev/null +++ b/test-suite/output/TranspModtype.out @@ -0,0 +1,15 @@ +TrM.A = M.A + : Set + +TrM.A is not universe polymorphic +OpM.A = M.A + : Set + +OpM.A is not universe polymorphic +TrM.B = M.B + : Set + +TrM.B is not universe polymorphic +*** [ OpM.B : Set ] + +OpM.B is not universe polymorphic diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v new file mode 100644 index 0000000000..68eff33a63 --- /dev/null +++ b/test-suite/output/TranspModtype.v @@ -0,0 +1,22 @@ +Module Type SIG. + Axiom A : Set. + Axiom B : Set. +End SIG. + +Module M : SIG. + Definition A := nat. + Definition B := nat. +End M. + +Module N <: SIG := M. + +Module TranspId (X: SIG) <: SIG with Definition A := X.A := X. +Module OpaqueId (X: SIG) : SIG with Definition A := X.A := X. + +Module TrM := TranspId M. +Module OpM := OpaqueId M. + +Print TrM.A. +Print OpM.A. +Print TrM.B. +Print OpM.B. diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out new file mode 100644 index 0000000000..8b38fe0ff4 --- /dev/null +++ b/test-suite/output/TypeclassDebug.out @@ -0,0 +1,18 @@ +Debug: 1: looking for foo without backtracking +Debug: 1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1 : foo +Debug: 1.1-1: looking for foo without backtracking +Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1 : foo +Debug: 1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo +The command has indeed failed with message: +Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. +Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v new file mode 100644 index 0000000000..2e4008ae56 --- /dev/null +++ b/test-suite/output/TypeclassDebug.v @@ -0,0 +1,9 @@ +(* show alternating separators in typeclass debug output; see discussion in PR #868 *) + +Parameter foo : Prop. +Axiom H : foo -> foo. +Hint Resolve H : foo. +Goal foo. +Typeclasses eauto := debug. +Fail typeclasses eauto 5 with foo. +Abort. diff --git a/test-suite/output/UnclosedBlocks.out b/test-suite/output/UnclosedBlocks.out new file mode 100644 index 0000000000..31481e84a5 --- /dev/null +++ b/test-suite/output/UnclosedBlocks.out @@ -0,0 +1,2 @@ +Error: The section Baz, module type Bar and module Foo need to be closed. + diff --git a/test-suite/output/UnclosedBlocks.v b/test-suite/output/UnclosedBlocks.v new file mode 100644 index 0000000000..854bd6a6d5 --- /dev/null +++ b/test-suite/output/UnclosedBlocks.v @@ -0,0 +1,8 @@ +(* -*- mode: coq; coq-prog-args: ("-compile" "UnclosedBlocks.v") *) +Module Foo. + Module Closed. + End Closed. + Module Type Bar. + Section Baz. + (* end-of-compilation error message reports unclosed sections, blocks, and + module types *) diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out new file mode 100644 index 0000000000..a57b3bbad5 --- /dev/null +++ b/test-suite/output/Unicode.out @@ -0,0 +1,41 @@ +1 subgoal + + very_very_long_type_name1 : Type + very_very_long_type_name2 : Type + f : very_very_long_type_name1 → very_very_long_type_name2 → Prop + ============================ + True + → True + → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2), + f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y +1 subgoal + + very_very_long_type_name1 : Type + very_very_long_type_name2 : Type + f : very_very_long_type_name1 → very_very_long_type_name2 → Prop + ============================ + True + → True + → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) + (z : very_very_long_type_name2), f y x ∧ f y z +1 subgoal + + very_very_long_type_name1 : Type + very_very_long_type_name2 : Type + f : very_very_long_type_name1 → very_very_long_type_name2 → Prop + ============================ + True + → True + → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) + (z : very_very_long_type_name2), + f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z +1 subgoal + + very_very_long_type_name1 : Type + very_very_long_type_name2 : Type + f : very_very_long_type_name1 → very_very_long_type_name2 → Prop + ============================ + True + → True + → ∃ (x : very_very_long_type_name1) (y : very_very_long_type_name2), + f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y diff --git a/test-suite/output/Unicode.v b/test-suite/output/Unicode.v new file mode 100644 index 0000000000..42b07e5a08 --- /dev/null +++ b/test-suite/output/Unicode.v @@ -0,0 +1,28 @@ +Require Import Coq.Unicode.Utf8. + +Section test. +Context (very_very_long_type_name1 : Type) (very_very_long_type_name2 : Type). +Context (f : very_very_long_type_name1 -> very_very_long_type_name2 -> Prop). + +Lemma test : True -> True -> + forall (x : very_very_long_type_name1) (y : very_very_long_type_name2), + f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y. +Proof. Show. Abort. + +Lemma test : True -> True -> + forall (x : very_very_long_type_name2) (y : very_very_long_type_name1) + (z : very_very_long_type_name2), + f y x /\ f y z. +Proof. Show. Abort. + +Lemma test : True -> True -> + forall (x : very_very_long_type_name2) (y : very_very_long_type_name1) + (z : very_very_long_type_name2), + f y x /\ f y z /\ f y x /\ f y z /\ f y x /\ f y z. +Proof. Show. Abort. + +Lemma test : True -> True -> + exists (x : very_very_long_type_name1) (y : very_very_long_type_name2), + f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y. +Proof. Show. Abort. +End test. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out new file mode 100644 index 0000000000..0bd6ade690 --- /dev/null +++ b/test-suite/output/UnivBinders.out @@ -0,0 +1,197 @@ +Inductive Empty@{u} : Type@{u} := +Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{u} = +fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p + : forall A : Type@{u}, PWrap@{u} A -> A +(* u |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } + +For RWrap: Argument scope is [type_scope] +For rwrap: Argument scopes are [type_scope _] +runwrap@{u} = +fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap + : forall A : Type@{u}, RWrap@{u} A -> A +(* u |= *) + +runwrap is universe polymorphic +Argument scopes are [type_scope _] +Wrap@{u} = fun A : Type@{u} => A + : Type@{u} -> Type@{u} +(* u |= *) + +Wrap is universe polymorphic +Argument scope is [type_scope] +wrap@{u} = +fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap + : forall A : Type@{u}, Wrap@{u} A -> A +(* u |= *) + +wrap is universe polymorphic +Arguments A, Wrap are implicit and maximally inserted +Argument scopes are [type_scope _] +bar@{u} = nat + : Wrap@{u} Set +(* u |= Set < u *) + +bar is universe polymorphic +foo@{u UnivBinders.17 v} = +Type@{UnivBinders.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.17+1,v+1)} +(* u UnivBinders.17 v |= *) + +foo is universe polymorphic +Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) + = Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) +mono = Type@{mono.u} + : Type@{mono.u+1} +(* {mono.u} |= *) + +mono is not universe polymorphic +mono + : Type@{mono.u+1} +Type@{mono.u} + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +monomono + : Type@{MONOU+1} +mono.monomono + : Type@{mono.MONOU+1} +monomono + : Type@{MONOU+1} +mono + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +bobmorane = +let tt := Type@{UnivBinders.32} in +let ff := Type@{UnivBinders.34} in tt -> ff + : Type@{max(UnivBinders.31,UnivBinders.33)} + +bobmorane is not universe polymorphic +The command has indeed failed with message: +Universe u already bound. +foo@{E M N} = +Type@{M} -> Type@{N} -> Type@{E} + : Type@{max(E+1,M+1,N+1)} +(* E M N |= *) + +foo is universe polymorphic +foo@{u UnivBinders.17 v} = +Type@{UnivBinders.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.17+1,v+1)} +(* u UnivBinders.17 v |= *) + +foo is universe polymorphic +Inductive Empty@{E} : Type@{E} := +Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A +(* K |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +punwrap is transparent +Expands to: Constant UnivBinders.punwrap +The command has indeed failed with message: +Universe instance should have length 3 +The command has indeed failed with message: +Universe instance should have length 0 +The command has indeed failed with message: +This object does not support universe names. +The command has indeed failed with message: +Cannot enforce v < u because u < gU < gV < v +bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) + +bind_univs.mono is not universe polymorphic +bind_univs.poly@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +bind_univs.poly is universe polymorphic +insec@{v} = Type@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* v |= *) + +insec is universe polymorphic +Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} + +For inseccstr: Argument scope is [type_scope] +insec@{u v} = Type@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* u v |= *) + +insec is universe polymorphic +Inductive insecind@{u k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{u k} + +For inseccstr: Argument scope is [type_scope] +insec2@{u} = Prop + : Type@{Set+1} +(* u |= *) + +insec2 is universe polymorphic +inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +inmod is universe polymorphic +SomeMod.inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +SomeMod.inmod is universe polymorphic +inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +inmod is universe polymorphic +Applied.infunct@{u v} = +inmod@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* u v |= *) + +Applied.infunct is universe polymorphic +axfoo@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.56} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) + +axfoo is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant UnivBinders.axfoo +axbar@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) + +axbar is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant UnivBinders.axbar +axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} + +axfoo' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant UnivBinders.axfoo' +axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} + +axbar' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant UnivBinders.axbar' +The command has indeed failed with message: +When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v new file mode 100644 index 0000000000..582a5e969a --- /dev/null +++ b/test-suite/output/UnivBinders.v @@ -0,0 +1,157 @@ +(* -*- coq-prog-args: ("-top" "UnivBinders"); -*- *) + +Set Universe Polymorphism. +Set Printing Universes. +(* Unset Strict Universe Declaration. *) + +(* universe binders on inductive types and record projections *) +Inductive Empty@{u} : Type@{u} := . +Print Empty. + +Set Primitive Projections. +Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }. +Print PWrap. +Print punwrap. + +Unset Primitive Projections. +Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }. +Print RWrap. +Print runwrap. + +(* universe binders also go on the constants for operational typeclasses. *) +Class Wrap@{u} (A:Type@{u}) := wrap : A. +Print Wrap. +Print wrap. + +(* Instance in lemma mode used to ignore the binders. *) +Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. +Print bar. + +Unset Strict Universe Declaration. +(* The universes in the binder come first, then the extra universes in + order of appearance. *) +Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. +Print foo. + +Check Type@{i} -> Type@{j}. + +Eval cbv in Type@{i} -> Type@{j}. + +Set Strict Universe Declaration. + +(* Binders even work with monomorphic definitions! *) +Monomorphic Definition mono@{u} := Type@{u}. +Print mono. +Check mono. +Check Type@{mono.u}. + +Module mono. + Fail Monomorphic Universe u. + Monomorphic Universe MONOU. + + Monomorphic Definition monomono := Type@{MONOU}. + Check monomono. + + Monomorphic Inductive monoind@{i} : Type@{i} := . + Monomorphic Record monorecord@{i} : Type@{i} := mkmonorecord {}. +End mono. +Check mono.monomono. (* qualified MONOU *) +Import mono. +Check monomono. (* unqualified MONOU *) +Check mono. (* still qualified mono.u *) + +Monomorphic Constraint Set < UnivBinders.mono.u. + +Module mono2. + Monomorphic Universe u. +End mono2. + +Fail Monomorphic Definition mono2@{u} := Type@{u}. + +Module SecLet. + Unset Universe Polymorphism. + Section foo. + (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) + Unset Strict Universe Declaration. + Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) + Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) + Definition bobmorane := tt -> ff. + End foo. + Print bobmorane. +End SecLet. + +(* fun x x => foo is nonsense with local binders *) +Fail Definition fo@{u u} := Type@{u}. + +(* Using local binders for printing. *) +Print foo@{E M N}. +(* Underscores discard the name if there's one. *) +Print foo@{_ _ _}. + +(* Also works for inductives and records. *) +Print Empty@{E}. +Print PWrap@{E}. + +(* Also works for About. *) +About punwrap@{K}. + +(* Instance length check. *) +Fail Print foo@{E}. +Fail Print mono@{E}. + +(* Not everything can be printed with custom universe names. *) +Fail Print Coq.Init.Logic@{E}. + +(* Nice error when constraints are impossible. *) +Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. +Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. + +(* Universe binders survive through compilation, sections and modules. *) +Require TestSuite.bind_univs. +Print bind_univs.mono. +Print bind_univs.poly. + +Section SomeSec. + Universe u. + Definition insec@{v} := Type@{u} -> Type@{v}. + Print insec. + + Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. + Print insecind. +End SomeSec. +Print insec. +Print insecind. + +Section SomeSec2. + Universe u. + Definition insec2@{} := Prop. +End SomeSec2. +Print insec2. + +Module SomeMod. + Definition inmod@{u} := Type@{u}. + Print inmod. +End SomeMod. +Print SomeMod.inmod. +Import SomeMod. +Print inmod. + +Module Type SomeTyp. Definition inmod := Type. End SomeTyp. +Module SomeFunct (In : SomeTyp). + Definition infunct@{u v} := In.inmod@{u} -> Type@{v}. +End SomeFunct. +Module Applied := SomeFunct(SomeMod). +Print Applied.infunct. + +(* Multi-axiom declaration + + In polymorphic mode the domain Type gets separate universes for the + different axioms, but all axioms have to declare all universes. In + polymorphic mode they get the same universes, ie the type is only + interpd once. *) +Axiom axfoo@{i+} axbar : Type -> Type@{i}. +Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. + +About axfoo. About axbar. About axfoo'. About axbar'. + +Fail Axiom failfoo failbar@{i} : Type. diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out new file mode 100644 index 0000000000..47409f3ec5 --- /dev/null +++ b/test-suite/output/UsePluginWarning.out @@ -0,0 +1 @@ +type foo = __ diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v new file mode 100644 index 0000000000..c6e0054641 --- /dev/null +++ b/test-suite/output/UsePluginWarning.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) + +Require Extraction. +Axiom foo : Prop. + +Extraction foo. + diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out new file mode 100644 index 0000000000..a70f8ca45a --- /dev/null +++ b/test-suite/output/Warnings.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-22: +Warning: Projection value has no head constant: fun x : B => x in canonical +instance a of b, ignoring it. [projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v new file mode 100644 index 0000000000..0eb5db1733 --- /dev/null +++ b/test-suite/output/Warnings.v @@ -0,0 +1,5 @@ +(* Term in warning was not printed in the right environment at some time *) +#[universes(template)] Record A := { B:Type; b:B->B }. +Definition a B := {| B:=B; b:=fun x => x |}. +Canonical Structure a. + diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out new file mode 100644 index 0000000000..dc41b0aa48 --- /dev/null +++ b/test-suite/output/ZSyntax.out @@ -0,0 +1,26 @@ +32%Z + : Z +fun f : nat -> Z => (f 0%nat + 0)%Z + : (nat -> Z) -> Z +fun x : positive => Z.pos x~0 + : positive -> Z +fun x : positive => (Z.pos x + 1)%Z + : positive -> Z +fun x : positive => Z.pos x + : positive -> Z +fun x : positive => Z.neg x~0 + : positive -> Z +fun x : positive => (Z.pos x~0 + 0)%Z + : positive -> Z +fun x : positive => (- Z.pos x~0)%Z + : positive -> Z +fun x : positive => (- Z.pos x~0 + 0)%Z + : positive -> Z +(Z.of_nat 0 + 1)%Z + : Z +(0 + Z.of_nat (0 + 0))%Z + : Z +Z.of_nat 0 = 0%Z + : Prop +(0 + Z.of_nat 11)%Z + : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v new file mode 100644 index 0000000000..d3640cae44 --- /dev/null +++ b/test-suite/output/ZSyntax.v @@ -0,0 +1,17 @@ +Require Import ZArith. +Check 32%Z. +Check (fun f : nat -> Z => (f 0%nat + 0)%Z). +Check (fun x : positive => Zpos (xO x)). +Check (fun x : positive => (Zpos x + 1)%Z). +Check (fun x : positive => Zpos x). +Check (fun x : positive => Zneg (xO x)). +Check (fun x : positive => (Zpos (xO x) + 0)%Z). +Check (fun x : positive => (- Zpos (xO x))%Z). +Check (fun x : positive => (- Zpos (xO x) + 0)%Z). +Check (Z.of_nat 0 + 1)%Z. +Check (0 + Z.of_nat (0 + 0))%Z. +Check (Z.of_nat 0 = 0%Z). + +(* Submitted by Pierre Casteran *) +Require Import Arith. +Check (0 + Z.of_nat 11)%Z. diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out new file mode 100644 index 0000000000..2761b87b02 --- /dev/null +++ b/test-suite/output/auto.out @@ -0,0 +1,22 @@ +(* info auto: *) +simple apply or_intror (in core). + intro. + assumption. +Debug: (* debug auto: *) +Debug: * assumption. (*fail*) +Debug: * intro. (*fail*) +Debug: * simple apply or_intror (in core). (*success*) +Debug: ** assumption. (*fail*) +Debug: ** intro. (*success*) +Debug: ** assumption. (*success*) +(* info eauto: *) +simple apply or_intror. + intro. + exact H. +Debug: (* debug eauto: *) +Debug: 1 depth=5 +Debug: 1.1 depth=4 simple apply or_intror +Debug: 1.1.1 depth=4 intro +Debug: 1.1.1.1 depth=4 exact H +(* info trivial: *) +exact I (in core). diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v new file mode 100644 index 0000000000..92917cdfc7 --- /dev/null +++ b/test-suite/output/auto.v @@ -0,0 +1,15 @@ +(* testing info/debug auto/eauto *) + +Goal False \/ (True -> True). +info_auto. +Undo. +debug auto. +Undo. +info_eauto. +Undo. +debug eauto. +Qed. + +Goal True. +info_trivial. +Qed. diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out new file mode 100644 index 0000000000..d6056c5098 --- /dev/null +++ b/test-suite/output/bug5778.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs", "abstract b ltac:(())", +"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v new file mode 100644 index 0000000000..0dcd76aeff --- /dev/null +++ b/test-suite/output/bug5778.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out new file mode 100644 index 0000000000..05464755f0 --- /dev/null +++ b/test-suite/output/bug6404.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)", +"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v new file mode 100644 index 0000000000..bbe6b1a00f --- /dev/null +++ b/test-suite/output/bug6404.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := transparent_abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. diff --git a/test-suite/output/bug6821.out b/test-suite/output/bug6821.out new file mode 100644 index 0000000000..7b12b53200 --- /dev/null +++ b/test-suite/output/bug6821.out @@ -0,0 +1,2 @@ +forall f : nat -> Type, f x where x : nat := 1 + : Type diff --git a/test-suite/output/bug6821.v b/test-suite/output/bug6821.v new file mode 100644 index 0000000000..40627e331e --- /dev/null +++ b/test-suite/output/bug6821.v @@ -0,0 +1,8 @@ +(* Was failing at printing time with stack overflow due to an infinite + eta-expansion *) + +Notation "x 'where' y .. z := v " := + ((fun y => .. ((fun z => x) v) ..) v) + (at level 11, v at next level, y binder, z binder). + +Check forall f, f x where x := 1. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out new file mode 100644 index 0000000000..20568f742a --- /dev/null +++ b/test-suite/output/goal_output.out @@ -0,0 +1,12 @@ +Nat.t = nat + : Set + +Nat.t is not universe polymorphic +Nat.t = nat + : Set + +Nat.t is not universe polymorphic +1 subgoal + + ============================ + False diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v new file mode 100644 index 0000000000..327b80b0aa --- /dev/null +++ b/test-suite/output/goal_output.v @@ -0,0 +1,13 @@ +(* From + - https://coq.inria.fr/bugs/show_bug.cgi?id=5529 + - https://coq.inria.fr/bugs/show_bug.cgi?id=5537 + *) + +Print Nat.t. +Timeout 1 Print Nat.t. + +Lemma toto: False. +Set Printing All. +Show. +Abort. + diff --git a/test-suite/output/idtac.out b/test-suite/output/idtac.out new file mode 100644 index 0000000000..3855f88a72 --- /dev/null +++ b/test-suite/output/idtac.out @@ -0,0 +1,11 @@ +"foo" +True +foo +3 +foo +2 +< True False Prop > +< True False Prop > +< > +< > +<< 1 2 3 >> diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v new file mode 100644 index 0000000000..ac60ea9175 --- /dev/null +++ b/test-suite/output/idtac.v @@ -0,0 +1,45 @@ +(* Printing all kinds of Ltac generic arguments *) + +Tactic Notation "myidtac" string(v) := idtac v. +Goal True. +myidtac "foo". +Abort. + +Tactic Notation "myidtac2" ref(c) := idtac c. +Goal True. +myidtac2 True. +Abort. + +Tactic Notation "myidtac3" preident(s) := idtac s. +Goal True. +myidtac3 foo. +Abort. + +Tactic Notation "myidtac4" int_or_var(n) := idtac n. +Goal True. +myidtac4 3. +Abort. + +Tactic Notation "myidtac5" ident(id) := idtac id. +Goal True. +myidtac5 foo. +Abort. + +(* Checking non focussing of idtac for integers *) +Goal True/\True. split. +all:let c:=numgoals in idtac c. +Abort. + +(* Checking printing of lists and its focussing *) +Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">". +Goal True/\True. split. +all:myidtac6 True False Prop. +(* An empty list is focussing because of interp_genarg of a constr *) +(* even if it is not focussing on printing *) +all:myidtac6. +Abort. + +Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>". +Goal True/\True. split. +all:myidtac7 1 2 3. +Abort. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out new file mode 100644 index 0000000000..f545ca679c --- /dev/null +++ b/test-suite/output/inference.out @@ -0,0 +1,18 @@ +P = +fun e : option L => match e with + | Some cl => Some cl + | None => None + end + : option L -> option L + +P is not universe polymorphic +fun n : nat => let y : T n := A n in ?t ?x : T n + : forall n : nat, T n +where +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] +fun n : nat => ?t ?x : T n + : forall n : nat, T n +where +?t : [n : nat |- ?T -> T n] +?x : [n : nat |- ?T] diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v new file mode 100644 index 0000000000..209fedc343 --- /dev/null +++ b/test-suite/output/inference.v @@ -0,0 +1,26 @@ +(* Check that types are not uselessly unfolded *) + +(* Check here that P returns something of type "option L" and not + "option (list nat)" *) + +Definition L := list nat. + +Definition P (e:option L) := + match e with + | None => None + | Some cl => Some cl + end. + +Print P. + +(* Check that the heuristic to solve constraints is not artificially + dependent on the presence of a let-in, and in particular that the + second [_] below is not inferred to be n, as if obtained by + first-order unification with [T n] of the conclusion [T _] of the + type of the first [_]. *) + +(* Note: exact numbers of evars are not important... *) + +#[universes(template)] Inductive T (n:nat) : Type := A : T n. +Check fun n (y:=A n:T n) => _ _ : T n. +Check fun n => _ _ : T n. diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v new file mode 100644 index 0000000000..aaf1ffe26d --- /dev/null +++ b/test-suite/output/load/Load_noproof.v @@ -0,0 +1 @@ +Definition f := 2. diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v new file mode 100644 index 0000000000..204d4ecbfe --- /dev/null +++ b/test-suite/output/load/Load_openproof.v @@ -0,0 +1 @@ +Lemma k : True. diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v new file mode 100644 index 0000000000..e47f66a193 --- /dev/null +++ b/test-suite/output/load/Load_proof.v @@ -0,0 +1,2 @@ +Lemma u : True. +Proof. exact I. Qed. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out new file mode 100644 index 0000000000..efdc94fb1e --- /dev/null +++ b/test-suite/output/ltac.out @@ -0,0 +1,51 @@ +The command has indeed failed with message: +Ltac variable y depends on pattern variable name z which is not bound in current context. +Ltac f x y z := + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize + dependent z +The command has indeed failed with message: +In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call +failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call +failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call +failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "h" and "injection (destruction_arg)", last call +failed. +No primitive equality found. +The command has indeed failed with message: +In nested Ltac calls to "h" and "injection (destruction_arg)", last call +failed. +No primitive equality found. +Hx +nat +nat +0 +0 +Ltac foo := + let x := intros in + let y := intros -> in + let v := constr:(nil) in + let w := () in + let z := 1 in + pose v +2 subgoals + + n : nat + ============================ + (fix a (n0 : nat) : nat := match n0 with + | 0 => 0 + | S n1 => a n1 + end) n = n + +subgoal 2 is: + forall a : nat, a = 0 diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v new file mode 100644 index 0000000000..40e743c3f0 --- /dev/null +++ b/test-suite/output/ltac.v @@ -0,0 +1,83 @@ +(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *) +Goal True. +Fail let T := constr:((fun a b : nat => a+b) 1 1) in + lazymatch T with + | (fun x z => ?y) 1 1 + => pose ((fun x _ => y) 1 1) + end. +Abort. + +(* This should not raise a warning (see #4317) *) +Goal True. +assert (H:= eq_refl ((fun x => x) 1)). +let HT := type of H in +lazymatch goal with +| H1 : HT |- _ => idtac +end. +Abort. + +Ltac f x y z := + symmetry in x, y; + auto with z; + auto; + intros; + clearbody x; + generalize dependent z. + +Print Ltac f. + +(* Error messages *) + +Ltac g1 x := refine x. +Tactic Notation "g2" constr(x) := g1 x. +Tactic Notation "f1" constr(x) := refine x. +Ltac f2 x := f1 x. +Goal False. +Fail g1 I. +Fail f1 I. +Fail g2 I. +Fail f2 I. +Abort. + +Ltac h x := injection x. +Goal True -> False. +Fail h I. +intro H. +Fail h H. +Abort. + +(* Check printing of the "var" argument "Hx" *) +Ltac m H := idtac H; exact H. +Goal True. +let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. +Abort. + +(* Check consistency of interpretation scopes (#4398) *) + +Goal nat*(0*0=0) -> nat*(0*0=0). intro. +match goal with H: ?x*?y |- _ => idtac x end. +match goal with |- ?x*?y => idtac x end. +match goal with H: context [?x*?y] |- _ => idtac x end. +match goal with |- context [?x*?y] => idtac x end. +Abort. + +(* Check printing of let in Ltac and Tactic Notation *) + +Ltac foo := + let x := intros in + let y := intros -> in + let v := constr:(@ nil True) in + let w := () in + let z := 1 in + pose v. +Print Ltac foo. + +(* Ltac renaming was not applied to "fix" and "cofix" *) + +Goal forall a, a = 0. +match goal with +|- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n) +end. +intro. +Show. +Abort. diff --git a/test-suite/output/ltac_extra_args.out b/test-suite/output/ltac_extra_args.out new file mode 100644 index 0000000000..77e799d359 --- /dev/null +++ b/test-suite/output/ltac_extra_args.out @@ -0,0 +1,8 @@ +The command has indeed failed with message: +Illegal tactic application: got 1 extra argument. +The command has indeed failed with message: +Illegal tactic application: got 2 extra arguments. +The command has indeed failed with message: +Illegal tactic application: got 1 extra argument. +The command has indeed failed with message: +Illegal tactic application: got 2 extra arguments. diff --git a/test-suite/output/ltac_extra_args.v b/test-suite/output/ltac_extra_args.v new file mode 100644 index 0000000000..4caf619fee --- /dev/null +++ b/test-suite/output/ltac_extra_args.v @@ -0,0 +1,10 @@ +Ltac foo := idtac. +Ltac bar H := idtac. + +Goal True. +Proof. + Fail foo H. + Fail foo H H'. + Fail bar H H'. + Fail bar H H' H''. +Abort. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out new file mode 100644 index 0000000000..8a00cd3fe5 --- /dev/null +++ b/test-suite/output/ltac_missing_args.out @@ -0,0 +1,40 @@ +The command has indeed failed with message: +The user-defined tactic "foo" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. +The command has indeed failed with message: +The user-defined tactic "bar" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. +The command has indeed failed with message: +The user-defined tactic "bar" was not fully applied: +There are missing arguments for variables y and _, +an argument was provided for variable x. +The command has indeed failed with message: +The user-defined tactic "baz" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. +The command has indeed failed with message: +The user-defined tactic "qux" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. +The command has indeed failed with message: +The user-defined tactic "mydo" was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. +The command has indeed failed with message: +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. +The command has indeed failed with message: +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. +The command has indeed failed with message: +The user-defined tactic "rec" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. +The command has indeed failed with message: +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable x, +an argument was provided for variable tac. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v new file mode 100644 index 0000000000..91331a1de5 --- /dev/null +++ b/test-suite/output/ltac_missing_args.v @@ -0,0 +1,19 @@ +Ltac foo x := idtac x. +Ltac bar x := fun y _ => idtac x y. +Ltac baz := foo. +Ltac qux := bar. +Ltac mydo tac := tac (). +Ltac rec x := rec. + +Goal True. + Fail foo. + Fail bar. + Fail bar True. + Fail baz. + Fail qux. + Fail mydo ltac:(fun _ _ => idtac). + Fail let tac := (fun _ => idtac) in tac. + Fail (fun _ => idtac). + Fail rec True. + Fail let rec tac x := tac in tac True. +Abort. diff --git a/test-suite/output/names.out b/test-suite/output/names.out new file mode 100644 index 0000000000..48be63a46a --- /dev/null +++ b/test-suite/output/names.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +In environment +y : nat +The term "a y" has type "{y0 : nat | y = y0}" +while it is expected to have type "{x : nat | x = y}". +1 focused subgoal +(shelved: 1) + + H : ?n <= 3 -> 3 <= ?n -> ?n = 3 + ============================ + True diff --git a/test-suite/output/names.v b/test-suite/output/names.v new file mode 100644 index 0000000000..e9033bd732 --- /dev/null +++ b/test-suite/output/names.v @@ -0,0 +1,10 @@ +(* Test no clash names occur *) +(* see bug #2723 *) + +Parameter a : forall x, {y:nat|x=y}. +Fail Definition b y : {x:nat|x=y} := a y. + +Goal (forall n m, n <= m -> m <= n -> n = m) -> True. +intro H; epose proof (H _ 3) as H. +Show. +Abort. diff --git a/test-suite/output/onlyprinting.out b/test-suite/output/onlyprinting.out new file mode 100644 index 0000000000..e0a30fcf6b --- /dev/null +++ b/test-suite/output/onlyprinting.out @@ -0,0 +1,2 @@ +0:-) 0 + : nat diff --git a/test-suite/output/onlyprinting.v b/test-suite/output/onlyprinting.v new file mode 100644 index 0000000000..1973385a0a --- /dev/null +++ b/test-suite/output/onlyprinting.v @@ -0,0 +1,5 @@ +Reserved Notation "x :-) y" (at level 50, only printing). + +Notation "x :-) y" := (plus x y). + +Check 0 + 0. diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out new file mode 100644 index 0000000000..94a0b19118 --- /dev/null +++ b/test-suite/output/optimize_heap.out @@ -0,0 +1,8 @@ +1 subgoal + + ============================ + True +1 subgoal + + ============================ + True diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v new file mode 100644 index 0000000000..31b4510397 --- /dev/null +++ b/test-suite/output/optimize_heap.v @@ -0,0 +1,8 @@ +(* optimize_heap should not affect the proof state *) + +Goal True. + idtac. + Show. + optimize_heap. + Show. +Abort. diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out new file mode 100644 index 0000000000..cfa295010f --- /dev/null +++ b/test-suite/output/qualification.out @@ -0,0 +1,5 @@ +File "stdin", line 20, characters 0-7: +Error: Signature components for label test do not match: expected type +"qualification.M2.t = qualification.M2.M.t" but found type +"qualification.M2.t = qualification.M2.t". + diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v new file mode 100644 index 0000000000..877bc84d14 --- /dev/null +++ b/test-suite/output/qualification.v @@ -0,0 +1,20 @@ +(* coq-prog-args: ("-top" "qualification") *) +Module Type T1. + Parameter t : Type. +End T1. + +Module Type T2. + Declare Module M : T1. + Parameter t : Type. + Parameter test : t = M.t. +End T2. + +Module M1 <: T1. + Definition t : Type := bool. +End M1. + +Module M2 <: T2. + Module M := M1. + Definition t : Type := nat. + Lemma test : t = t. Proof. reflexivity. Qed. +End M2. diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out new file mode 100644 index 0000000000..ff327aa5f1 --- /dev/null +++ b/test-suite/output/reduction.out @@ -0,0 +1,4 @@ + = a + : nat + = n + 0 + : nat diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v new file mode 100644 index 0000000000..ab6262823c --- /dev/null +++ b/test-suite/output/reduction.v @@ -0,0 +1,13 @@ +(* Test the behaviour of hnf and simpl introduced in revision *) + +Parameter n:nat. +Definition a:=0. + +Eval simpl in (fix plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (p + m) + end) a a. + +Eval hnf in match (plus (S n) O) with S n => n | _ => O end. + diff --git a/test-suite/output/rewrite_2172.out b/test-suite/output/rewrite_2172.out new file mode 100644 index 0000000000..27b0dc1b7b --- /dev/null +++ b/test-suite/output/rewrite_2172.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +Unable to find an instance for the variable E. diff --git a/test-suite/output/rewrite_2172.v b/test-suite/output/rewrite_2172.v new file mode 100644 index 0000000000..864fc21cdd --- /dev/null +++ b/test-suite/output/rewrite_2172.v @@ -0,0 +1,22 @@ +(* This checks an error message as reported in bug #2172 *) + +Axiom axiom : forall (E F : nat), E = F. +Lemma test : forall (E F : nat), E = F. +Proof. + intros. +(* This used to raise the following non understandable error message: + + Error: Unable to find an instance for the variable x + + The reason this error was that rewrite generated the proof + + "eq_ind ?A ?x ?P ? ?y (axiom ?E ?F)" + + and the equation ?x=?E was solved in the way ?E:=?x leaving ?x + unresolved. A stupid hack for solve this consisted in ordering + meta=meta equations the other way round (with most recent evars + instantiated first - since they are assumed to come first from the + user in rewrite/induction/destruct calls). +*) + Fail rewrite <- axiom. +Abort. diff --git a/test-suite/output/set.out b/test-suite/output/set.out new file mode 100644 index 0000000000..4b72d73eb3 --- /dev/null +++ b/test-suite/output/set.out @@ -0,0 +1,18 @@ +1 subgoal + + y1 := 0 : nat + x := 0 + 0 : nat + ============================ + x = x +1 subgoal + + y1, y2 := 0 : nat + x := y2 + 0 : nat + ============================ + x = x +1 subgoal + + y1, y2, y3 := 0 : nat + x := y2 + y3 : nat + ============================ + x = x diff --git a/test-suite/output/set.v b/test-suite/output/set.v new file mode 100644 index 0000000000..0e745354ab --- /dev/null +++ b/test-suite/output/set.v @@ -0,0 +1,10 @@ +Goal let x:=O+O in x=x. +intro. +set (y1:=O) in (type of x). +Show. +set (y2:=O) in (value of x) at 1. +Show. +set (y3:=O) in (value of x). +Show. +trivial. +Qed. diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out new file mode 100644 index 0000000000..526e468f5b --- /dev/null +++ b/test-suite/output/simpl.out @@ -0,0 +1,15 @@ +1 subgoal + + x : nat + ============================ + x = S x +1 subgoal + + x : nat + ============================ + 0 + x = S x +1 subgoal + + x : nat + ============================ + x = 1 + x diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v new file mode 100644 index 0000000000..5f1926f142 --- /dev/null +++ b/test-suite/output/simpl.v @@ -0,0 +1,13 @@ +(* Simpl with patterns *) + +Goal forall x, 0+x = 1+x. +intro x. +simpl (_ + x). +Show. +Undo. +simpl (_ + x) at 2. +Show. +Undo. +simpl (0 + _). +Show. +Undo. diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out new file mode 100644 index 0000000000..1515954060 --- /dev/null +++ b/test-suite/output/ssr_clear.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Ltac call to "move (ssrmovearg) (ssrclauses)" failed. +No assumption is named NO_SUCH_NAME diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v new file mode 100644 index 0000000000..573ec47e0b --- /dev/null +++ b/test-suite/output/ssr_clear.v @@ -0,0 +1,6 @@ +Require Import ssreflect. + +Example foo : True -> True. +Proof. +Fail move=> {NO_SUCH_NAME}. +Abort. diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out new file mode 100644 index 0000000000..32cfb354bf --- /dev/null +++ b/test-suite/output/ssr_explain_match.out @@ -0,0 +1,55 @@ +File "stdin", line 12, characters 0-61: +Warning: Notation "_ - _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ <= _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ < _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ >= _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ > _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ < _ <= _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ <= _ < _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ < _ < _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ + _" was already used in scope nat_scope. +[notation-overridden,parsing] +File "stdin", line 12, characters 0-61: +Warning: Notation "_ * _" was already used in scope nat_scope. +[notation-overridden,parsing] +BEGIN INSTANCES +instance: (x + y + z) matches: (x + y + z) +instance: (x + y) matches: (x + y) +instance: (x + y) matches: (x + y) +END INSTANCES +BEGIN INSTANCES +instance: (addnC (x + y) z) matches: (x + y + z) +instance: (addnC x y) matches: (x + y) +instance: (addnC x y) matches: (x + y) +END INSTANCES +BEGIN INSTANCES +instance: (addnA x y z) matches: (x + y + z) +END INSTANCES +BEGIN INSTANCES +instance: (addnA x y z) matches: (x + y + z) +instance: (addnC z (x + y)) matches: (x + y + z) +instance: (addnC y x) matches: (x + y) +instance: (addnC y x) matches: (x + y) +END INSTANCES +The command has indeed failed with message: +Ltac call to "ssrinstancesoftpat (cpattern)" failed. +Not supported diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v new file mode 100644 index 0000000000..56ca24b6e2 --- /dev/null +++ b/test-suite/output/ssr_explain_match.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssrmatching. +Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp. + +Definition addnAC := (addnA, addnC). + +Lemma test x y z : x + y + z = x + y. + +ssrinstancesoftpat (_ + _). +ssrinstancesofruleL2R addnC. +ssrinstancesofruleR2L addnA. +ssrinstancesofruleR2L addnAC. +Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *) +Admitted. diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out new file mode 100644 index 0000000000..209b2bc26f --- /dev/null +++ b/test-suite/output/subst.out @@ -0,0 +1,97 @@ +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : 0 = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + HA, HB : True + H4 : 0 = 4 + H3 : 0 = 3 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v new file mode 100644 index 0000000000..e48aa6bb28 --- /dev/null +++ b/test-suite/output/subst.v @@ -0,0 +1,48 @@ +(* Ensure order of hypotheses is respected after "subst" *) + +Set Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *) +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + +Unset Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + + diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out new file mode 100644 index 0000000000..2fadd747b7 --- /dev/null +++ b/test-suite/output/unifconstraints.out @@ -0,0 +1,73 @@ +3 focused subgoals +(shelved: 1) + + ============================ + ?Goal 0 + +subgoal 2 is: + forall n : nat, ?Goal n -> ?Goal (S n) +subgoal 3 is: + nat +unification constraint: + ?Goal ?Goal2 <= + True /\ True /\ True \/ + veeryyyyyyyyyyyyloooooooooooooonggidentifier = + veeryyyyyyyyyyyyloooooooooooooonggidentifier +3 focused subgoals +(shelved: 1) + + n, m : nat + ============================ + ?Goal@{n:=n; m:=m} 0 + +subgoal 2 is: + forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0) +subgoal 3 is: + nat +unification constraint: + ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= + True /\ True /\ True \/ + veeryyyyyyyyyyyyloooooooooooooonggidentifier = + veeryyyyyyyyyyyyloooooooooooooonggidentifier +3 focused subgoals +(shelved: 1) + + m : nat + ============================ + ?Goal1@{m:=m} 0 + +subgoal 2 is: + forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0) +subgoal 3 is: + nat +unification constraint: + + n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= + True /\ True /\ True \/ + veeryyyyyyyyyyyyloooooooooooooonggidentifier = + veeryyyyyyyyyyyyloooooooooooooonggidentifier +3 focused subgoals +(shelved: 1) + + m : nat + ============================ + ?Goal0@{m:=m} 0 + +subgoal 2 is: + forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0) +subgoal 3 is: + nat +unification constraint: + + n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= + True /\ True /\ True \/ + veeryyyyyyyyyyyyloooooooooooooonggidentifier = + veeryyyyyyyyyyyyloooooooooooooonggidentifier +The command has indeed failed with message: +In environment +P : nat -> Type +x : nat +h : P x +Unable to unify "P x" with "?P x" +(unable to find a well-typed instantiation for "?P": cannot ensure that +"nat -> Type" is a subtype of "nat -> Prop"). diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v new file mode 100644 index 0000000000..179dec3fb0 --- /dev/null +++ b/test-suite/output/unifconstraints.v @@ -0,0 +1,28 @@ +(* Set Printing Existential Instances. *) +Unset Solve Unification Constraints. +Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat. +Goal True /\ True /\ True \/ + veeryyyyyyyyyyyyloooooooooooooonggidentifier = + veeryyyyyyyyyyyyloooooooooooooonggidentifier. + refine (nat_rect _ _ _ _). + Show. +Admitted. + +Set Printing Existential Instances. +Goal forall n m : nat, True /\ True /\ True \/ + veeryyyyyyyyyyyyloooooooooooooonggidentifier = + veeryyyyyyyyyyyyloooooooooooooonggidentifier. + intros. + refine (nat_rect _ _ _ _). + Show. + clear n. + Show. + 3:clear m. + Show. +Admitted. +Unset Printing Existential Instances. + +(* Check non regression of error message (the example can eventually + improve though and succeed) *) + +Fail Check fun P (x:nat) (h:P x) => exist _ x (h : P x). |