From 3478ffda0a0a83951db341eb68fc6b71877c1392 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 28 Apr 2008 09:27:17 +0000 Subject: Backtrack on using metas eagerly in auto, only done in "new auto" for now. Fix proof scripts that failed correspondingly. Should make many contribs compile again... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/blast.ml | 15 ++++++++++----- pretyping/unification.ml | 3 ++- tactics/auto.ml | 18 +++++++++++++----- tactics/auto.mli | 4 +++- tactics/eauto.ml4 | 17 +++++++++++------ test-suite/bugs/closed/shouldsucceed/1784.v | 2 +- theories/Ints/num/NMake.v | 6 ++++++ theories/Lists/List.v | 2 ++ theories/ZArith/Zpow_facts.v | 1 + 9 files changed, 49 insertions(+), 19 deletions(-) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 4df6108b6..10fafaefc 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -168,11 +168,14 @@ let rec e_trivial_fail_db db_list local_db goal = and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in + let flags = Auto.auto_unif_flags in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) + (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) + (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = fun (st, ({pri=b; pat = p; code=t} as _patac)) -> @@ -380,12 +383,14 @@ let rec trivial_fail_db db_list local_db gl = (trivial_resolve db_list local_db (pf_concl gl)))) gl and my_find_search db_list local_db hdc concl = + let flags = Auto.auto_unif_flags in let tacl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) + (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_auto (hdc,concl) db)) - (local_db::db_list) + list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) + (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in List.map (fun (st, {pri=b; pat=p; code=t} as _patac) -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 578afdb75..1063342e5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -145,7 +145,8 @@ let expand_constant env flags c = let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = let nb = nb_rel env in let trivial_unify pb (metasubst,_) m n = - match subst_defined_metas metasubst m with + let subst = if flags.use_metas_eagerly then metasubst else fst subst in + match subst_defined_metas subst m with | Some m -> (match flags.modulo_conv_on_closed_terms with Some flags -> diff --git a/tactics/auto.ml b/tactics/auto.ml index 0b1f29dc3..816bd61ca 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -591,9 +591,9 @@ let auto_unif_flags = { (* Try unification with the precompiled clause, then use registered Apply *) -let unify_resolve st (c,clenv) gls = +let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver false ~flags:{auto_unif_flags with modulo_delta = st} clenv' gls in + let _ = clenv_unique_resolver false ~flags clenv' gls in h_apply true false (c,NoBindings) gls (* builds a hint database from a constr signature *) @@ -649,24 +649,32 @@ let rec trivial_fail_db mod_delta db_list local_db gl = (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl and my_find_search mod_delta db_list local_db hdc concl = + let flags = + if mod_delta then {auto_unif_flags with use_metas_eagerly = true} + else auto_unif_flags + in let tacl = if occur_existential concl then list_map_append (fun (st, db) -> - let st = if mod_delta then st else empty_transparent_state in + let st = + if mod_delta then + {flags with modulo_delta = st} + else flags + in List.map (fun x -> (st,x)) (Hint_db.map_all hdc db)) (local_db::db_list) else list_map_append (fun ((ids, csts as st), db) -> let st, l = if not mod_delta then - empty_transparent_state, Hint_db.map_auto (hdc,concl) db + flags, Hint_db.map_auto (hdc,concl) db else let l = if (Idpred.is_empty ids && Cpred.is_empty csts) then Hint_db.map_auto (hdc,concl) db else Hint_db.map_all hdc db - in st, l + in {flags with modulo_delta = st}, l in List.map (fun x -> (st,x)) l) (local_db::db_list) in diff --git a/tactics/auto.mli b/tactics/auto.mli index 91f4182fa..7853235be 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -138,8 +138,10 @@ val priority : (int * 'a) list -> 'a list val default_search_depth : int ref +val auto_unif_flags : Unification.unify_flags + (* Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve : transparent_state -> (constr * clausenv) -> tactic +val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic (* [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 62d137b7a..3894dfd1f 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -85,14 +85,15 @@ TACTIC EXTEND prolog END open Auto +open Unification (***************************************************************************) (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) (***************************************************************************) -let unify_e_resolve (c,clenv) gls = +let unify_e_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver false clenv' gls in + let _ = clenv_unique_resolver false ~flags clenv' gls in h_simplest_eapply c gls let rec e_trivial_fail_db db_list local_db goal = @@ -112,9 +113,13 @@ and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun (st, db) -> + let flags = {auto_unif_flags with modulo_delta = st} in + List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> st, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun (st, db) -> + let flags = {auto_unif_flags with modulo_delta = st} in + List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = fun (st, {pri=b; pat = p; code=t}) -> @@ -122,10 +127,10 @@ and e_my_find_search db_list local_db hdc concl = let tac = match t with | Res_pf (term,cl) -> unify_resolve st (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve st (term,cl) | Give_exact (c) -> e_give_exact_constr c | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve (term,cl)) + tclTHEN (unify_e_resolve st (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index d6b7660b2..616dd26f5 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -85,7 +85,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := end end. -Next Obligation. apply H; inversion H0; subst; trivial. reflexivity. Defined. +Next Obligation. apply H; inversion H0; subst; trivial. Defined. Next Obligation. inversion H. Defined. Next Obligation. inversion H. Defined. Next Obligation. inversion H; subst. Defined. diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index c857da385..8cb779350 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -5182,6 +5182,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^1) with (2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_2; unfold to_Z. apply (znz_of_pos_correct w2_spec). @@ -5189,6 +5190,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^2) with (2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_3; unfold to_Z. apply (znz_of_pos_correct w3_spec). @@ -5196,6 +5198,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^3) with (2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_4; unfold to_Z. apply (znz_of_pos_correct w4_spec). @@ -5203,6 +5206,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^4) with (2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_5; unfold to_Z. apply (znz_of_pos_correct w5_spec). @@ -5210,6 +5214,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^5) with (2 * 2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_6; unfold to_Z. apply (znz_of_pos_correct w6_spec). @@ -5217,6 +5222,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^6) with (2 * 2 * 2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n. intros H1; rewrite spec_reduce_n; unfold to_Z. simpl minus; rewrite <- minus_n_O. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 78a2db534..51d3f192d 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -687,6 +687,7 @@ Section ListOps. rewrite (minus_plus_simpl_l_reverse (length l) n 1). replace (1 + length l) with (S (length l)); auto with arith. rewrite <- minus_Sn_m; auto with arith. + apply IHl ; auto with arith. rewrite rev_length; auto. Qed. @@ -1362,6 +1363,7 @@ End Fold_Right_Recursor. destruct n; destruct d; simpl; auto. destruct a; destruct (split l); simpl; auto. destruct a; destruct (split l); simpl in *; auto. + apply IHl. Qed. Lemma split_length_l : forall (l:list (A*B)), diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 9524bd44f..8f86fdf79 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -171,6 +171,7 @@ Qed. Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. Proof. intros x y; case y; auto with zarith. + simpl ; auto with zarith. intros p H1; assert (H: 0 <= Zpos p); auto with zarith. generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith. intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. -- cgit v1.2.3