From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- test-suite/success/apply.v | 193 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 191 insertions(+), 2 deletions(-) (limited to 'test-suite/success/apply.v') diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 4f260696..fcce68b9 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -7,8 +7,197 @@ assumption. Qed. Require Import ZArith. -Open Scope Z_scope. -Goal forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y. +Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z. intros; apply Znot_le_gt, Zgt_lt in H. apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. Qed. + +(* Check if it unfolds when there are not enough premises *) + +Goal forall n, n = S n -> False. +intros. +apply n_Sn in H. +assumption. +Qed. + +(* Check naming in with bindings; printing used to be inconsistent before *) +(* revision 9450 *) + +Notation S':=S (only parsing). +Goal (forall S, S = S' S) -> (forall S, S = S' S). +intros. +apply H with (S0 := S). +Qed. + +(* Check inference of implicit arguments in bindings *) + +Goal exists y : nat -> Type, y 0 = y 0. +exists (fun x => True). +trivial. +Qed. + +(* Check universe handling in typed unificationn *) + +Definition E := Type. +Goal exists y : E, y = y. +exists Prop. +trivial. +Qed. + +Variable Eq : Prop = (Prop -> Prop) :> E. +Goal Prop. +rewrite Eq. +Abort. + +(* Check insertion of coercions in bindings *) + +Coercion eq_true : bool >-> Sortclass. +Goal exists A:Prop, A = A. +exists true. +trivial. +Qed. + +(* Check use of unification of bindings types in specialize *) + +Variable P : nat -> Prop. +Variable L : forall (l : nat), P l -> P l. +Goal P 0 -> True. +intros. +specialize L with (1:=H). +Abort. +Reset P. + +(* Two examples that show that hnf_constr is used when unifying types + of bindings (a simplification of a script from Field_Theory) *) + +Require Import List. +Open Scope list_scope. +Fixpoint P (l : list nat) : Prop := + match l with + | nil => True + | e1 :: nil => e1 = e1 + | e1 :: l1 => e1 = e1 /\ P l1 + end. +Variable L : forall n l, P (n::l) -> P l. + +Goal forall (x:nat) l, P (x::l) -> P l. +intros. +apply L with (1:=H). +Qed. + +Goal forall (x:nat) l, match l with nil => x=x | _::_ => x=x /\ P l end -> P l. +intros. +apply L with (1:=H). +Qed. + +(* The following call to auto fails if the type of the clause + associated to the H is not beta-reduced [but apply H works] + (a simplification of a script from FSetAVL) *) + +Definition apply (f:nat->Prop) := forall x, f x. +Goal apply (fun n => n=0) -> 1=0. +intro H. +auto. +Qed. + +(* The following fails if the coercion Zpos is not introduced around p + before trying a subterm that matches the left-hand-side of the equality + (a simplication of an example taken from Nijmegen/QArith) *) + +Require Import ZArith. +Coercion Zpos : positive >-> Z. +Variable f : Z -> Z -> Z. +Variable g : forall q1 q2 p : Z, f (f q1 p) (f q2 p) = Z0. +Goal forall p q1 q2, f (f q1 (Zpos p)) (f q2 (Zpos p)) = Z0. +intros; rewrite g with (p:=p). +reflexivity. +Qed. + +(* A funny example where the behavior differs depending on which of a + multiple solution to a unification problem is chosen (an instance + of this case can be found in the proof of Buchberger.BuchRed.nf_divp) *) + +Definition succ x := S x. +Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop), + (forall x y, P x -> Q x y) -> + (forall x, P (S x)) -> forall y: I (S 0), Q (succ 0) y. +intros. +apply H with (y:=y). +(* [x] had two possible instances: [S 0], coming from unifying the + type of [y] with [I ?n] and [succ 0] coming from the unification with + the goal; only the first one allows to make the next apply (which + does not work modulo delta) working *) +apply H0. +Qed. + +(* A similar example with a arbitrary long conversion between the two + possible instances *) + +Fixpoint compute_succ x := + match x with O => S 0 | S n => S (compute_succ n) end. + +Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop), + (forall x y, P x -> Q x y) -> + (forall x, P (S x)) -> forall y: I (S 100), Q (compute_succ 100) y. +intros. +apply H with (y:=y). +apply H0. +Qed. + +(* Another example with multiple convertible solutions to the same + metavariable (extracted from Algebra.Hom_module.Hom_module, 10th + subgoal which precisely fails) *) + +Definition ID (A:Type) := A. +Goal forall f:Type -> Type, + forall (P : forall A:Type, A -> Prop), + (forall (B:Type) x, P (f B) x -> P (f B) x) -> + (forall (A:Type) x, P (f (f A)) x) -> + forall (A:Type) (x:f (f A)), P (f (ID (f A))) x. +intros. +apply H. +(* The parameter [B] had two possible instances: [ID (f A)] by direct + unification and [f A] by unification of the type of [x]; only the + first choice makes the next command fail, as it was + (unfortunately?) in Hom_module *) +try apply H. +unfold ID; apply H0. +Qed. + +(* Test coercion below product and on non meta-free terms in with bindings *) +(* Cf wishes #1408 from E. Makarov *) + +Parameter bool_Prop :> bool -> Prop. +Parameter r : bool -> bool -> bool. +Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y. + +Theorem t : r true false. +apply ax with (R := r). +Qed. + +(* Check verification of type at unification (submitted by Stéphane Lengrand): + without verification, the first "apply" works what leads to the incorrect + instantiation of x by Prop *) + +Theorem u : ~(forall x:Prop, ~x). +unfold not. +intro. +eapply H. +apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I). +Defined. + +(* Fine-tuning coercion insertion in presence of unfolding (bug #1883) *) + +Parameter name : Set. +Definition atom := name. + +Inductive exp : Set := + | var : atom -> exp. + +Coercion var : atom >-> exp. + +Axiom silly_axiom : forall v : exp, v = v -> False. + +Lemma silly_lemma : forall x : atom, False. +intros x. +apply silly_axiom with (v := x). (* fails *) -- cgit v1.2.3