diff options
Diffstat (limited to 'test-suite/success/apply.v')
-rw-r--r-- | test-suite/success/apply.v | 120 |
1 files changed, 113 insertions, 7 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 0d8bf556..21b829aa 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -164,8 +164,8 @@ intros. apply H with (y:=y). (* [x] had two possible instances: [S 0], coming from unifying the type of [y] with [I ?n] and [succ 0] coming from the unification with - the goal; only the first one allows to make the next apply (which - does not work modulo delta) working *) + the goal; only the first one allows the next apply (which + does not work modulo delta) work *) apply H0. Qed. @@ -336,25 +336,43 @@ Qed. (* From 12612, descent in conjunctions is more powerful *) (* The following, which was failing badly in bug 1980, is now properly rejected, as descend in conjunctions builds an - ill-formed elimination from Prop to Type. *) + ill-formed elimination from Prop to Type. + + Added Aug 2014: why it fails is now that trivial unification ?x = goal is + rejected by the descent in conjunctions to avoid surprising results. *) Goal True. Fail eapply ex_intro. exact I. Qed. -(* The following, which were not accepted, are now accepted as - expected by descent in conjunctions *) +Goal True. +Fail eapply (ex_intro _). +exact I. +Qed. + +(* Note: the following succeed directly (i.e. w/o "exact I") since + Aug 2014 since the descent in conjunction does not use a "cut" + anymore: the iota-redex is contracted and we get rid of the + uninstantiated evars + + Is it good or not? Maybe it does not matter so much. Goal True. eapply (ex_intro (fun _ => True) I). -exact I. +exact I. (* Not needed since Aug 2014 *) +Qed. + +Goal True. +eapply (ex_intro (fun _ => True) I _). +exact I. (* Not needed since Aug 2014 *) Qed. Goal True. eapply (fun (A:Prop) (x:A) => conj I x). -exact I. +exact I. (* Not needed since Aug 2014 *) Qed. +*) (* The following was not accepted from r12612 to r12657 *) @@ -430,3 +448,91 @@ Undo. (* H' is displayed as (forall n0, n=n0) *) apply H' with (n0:=0). Qed. + +(* Check that evars originally present in goal do not prevent apply in to work*) + +Goal (forall x, x <= 0 -> x = 0) -> exists x, x <= 0 -> 0 = 0. +intros. +eexists. +intros. +apply H in H0. +Abort. + +(* Check correct failure of apply in when hypothesis is dependent *) + +Goal forall H:0=0, H = H. +intros. +Fail apply eq_sym in H. + +(* Check that unresolved evars not originally present in goal prevent + apply in to work*) + +Goal (forall x y, x <= 0 -> x + y = 0) -> exists x, x <= 0 -> 0 = 0. +intros. +eexists. +intros. +Fail apply H in H0. +Abort. + +(* Check naming pattern in apply in *) + +Goal ((False /\ (True -> True))) -> True -> True. +intros F H. +apply F in H as H0. (* Check that H0 is not used internally *) +exact H0. +Qed. + +Goal ((False /\ (True -> True/\True))) -> True -> True/\True. +intros F H. +apply F in H as (?,?). +split. +exact H. (* Check that generated names are H and H0 *) +exact H0. +Qed. + +(* This failed at some time in between 18 August 2014 and 2 September 2014 *) + +Goal forall A B C: Prop, (True -> A -> B /\ C) -> A -> B. +intros * H. +apply H. +Abort. + +(* This failed between 2 and 3 September 2014 *) + +Goal forall A B C D:Prop, (A<->B)/\(C<->D) -> A -> B. +intros. +apply H in H0. +pose proof I as H1. (* Test that H1 does not exist *) +Abort. + +Goal forall A B C D:Prop, (A<->B)/\(C<->D) -> A. +intros. +apply H. +pose proof I as H0. (* Test that H0 does not exist *) +Abort. + +(* The first example below failed at some time in between 18 August + 2014 and 2 September 2014 *) + +Goal forall x, 2=0 -> x+1=2 -> (forall x, S x = 0) -> True. +intros x H H0 H1. +eapply eq_trans in H. 2:apply H0. +rewrite H1 in H. +change (x+0=0) in H. (* Check the result in H1 *) +Abort. + +Goal forall x, 2=x+1 -> (forall x, S x = 0) -> 2 = 0. +intros x H H0. +eapply eq_trans. apply H. +rewrite H0. +change (x+0=0). +Abort. + +(* 2nd order apply used to have delta on local definitions even though + it does not have delta on global definitions; keep it by + compatibility while finding a more uniform way to proceed. *) + +Goal forall f:nat->nat, (forall P x, P (f x)) -> let x:=f 0 in x = 0. +intros f H x. +apply H. +Qed. |