From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- plugins/extraction/ExtrOcamlNatInt.v | 14 ++-- plugins/extraction/ExtrOcamlZInt.v | 32 ++++----- plugins/extraction/extraction.ml | 36 +++++++--- plugins/extraction/modutil.ml | 60 ++++++++-------- plugins/funind/glob_term_to_relation.ml | 17 ++--- plugins/romega/ReflOmegaCore.v | 117 ++++++++++++-------------------- plugins/subtac/subtac_obligations.ml | 1 + 7 files changed, 138 insertions(+), 139 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index fd134899..956ece79 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -14,6 +14,10 @@ Require Import ExtrOcamlBasic. (** Disclaimer: trying to obtain efficient certified programs by extracting [nat] into [int] is definitively *not* a good idea: + - This is just a syntactic adaptation, many things can go wrong, + such as name captures (e.g. if you have a constant named "int" + in your development, or a module named "Pervasives"). See bug #2878. + - Since [int] is bounded while [nat] is (theoretically) infinite, you have to make sure by yourself that your program will not manipulate numbers greater than [max_int]. Otherwise you should @@ -34,17 +38,17 @@ Require Import ExtrOcamlBasic. (** Mapping of [nat] into [int]. The last string corresponds to a [nat_case], see documentation of [Extract Inductive]. *) -Extract Inductive nat => int [ "0" "succ" ] +Extract Inductive nat => int [ "0" "Pervasives.succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". (** Efficient (but uncertified) versions for usual [nat] functions *) Extract Constant plus => "(+)". -Extract Constant pred => "fun n -> max 0 (n-1)". -Extract Constant minus => "fun n m -> max 0 (n-m)". +Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)". +Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)". Extract Constant mult => "( * )". -Extract Inlined Constant max => max. -Extract Inlined Constant min => min. +Extract Inlined Constant max => "Pervasives.max". +Extract Inlined Constant min => "Pervasives.min". (*Extract Inlined Constant nat_beq => "(=)".*) Extract Inlined Constant EqNat.beq_nat => "(=)". Extract Inlined Constant EqNat.eq_nat_decide => "(=)". diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index c8c40e73..ab634329 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -34,12 +34,12 @@ Extract Inductive N => int [ "0" "" ] (** Efficient (but uncertified) versions for usual functions *) Extract Constant Pos.add => "(+)". -Extract Constant Pos.succ => "succ". -Extract Constant Pos.pred => "fun n -> max 1 (n-1)". -Extract Constant Pos.sub => "fun n m -> max 1 (n-m)". +Extract Constant Pos.succ => "Pervasives.succ". +Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)". +Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)". Extract Constant Pos.mul => "( * )". -Extract Constant Pos.min => "min". -Extract Constant Pos.max => "max". +Extract Constant Pos.min => "Pervasives.min". +Extract Constant Pos.max => "Pervasives.max". Extract Constant Pos.compare => "fun x y -> if x=y then Eq else if x @@ -47,12 +47,12 @@ Extract Constant Pos.compare_cont => Extract Constant N.add => "(+)". -Extract Constant N.succ => "succ". -Extract Constant N.pred => "fun n -> max 0 (n-1)". -Extract Constant N.sub => "fun n m -> max 0 (n-m)". +Extract Constant N.succ => "Pervasives.succ". +Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)". +Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)". Extract Constant N.mul => "( * )". -Extract Constant N.min => "min". -Extract Constant N.max => "max". +Extract Constant N.min => "Pervasives.min". +Extract Constant N.max => "Pervasives.max". Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b". Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b". Extract Constant N.compare => @@ -60,19 +60,19 @@ Extract Constant N.compare => Extract Constant Z.add => "(+)". -Extract Constant Z.succ => "succ". -Extract Constant Z.pred => "pred". +Extract Constant Z.succ => "Pervasives.succ". +Extract Constant Z.pred => "Pervasives.pred". Extract Constant Z.sub => "(-)". Extract Constant Z.mul => "( * )". Extract Constant Z.opp => "(~-)". -Extract Constant Z.abs => "abs". -Extract Constant Z.min => "min". -Extract Constant Z.max => "max". +Extract Constant Z.abs => "Pervasives.abs". +Extract Constant Z.min => "Pervasives.min". +Extract Constant Z.max => "Pervasives.max". Extract Constant Z.compare => "fun x y -> if x=y then Eq else if x "fun p -> p". -Extract Constant Z.abs_N => "abs". +Extract Constant Z.abs_N => "Pervasives.abs". (** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e76c6919..0a17453c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -130,7 +130,7 @@ let rec nb_default_params env c = (* Enriching a signature with implicit information *) -let sign_with_implicits r s = +let sign_with_implicits r s nb_params = let implicits = implicits_of_global r in let rec add_impl i = function | [] -> [] @@ -139,7 +139,7 @@ let sign_with_implicits r s = if sign = Keep && List.mem i implicits then Kill Kother else sign in sign' :: add_impl (succ i) s in - add_impl 1 s + add_impl (1+nb_params) s (* Enriching a exception message *) @@ -667,20 +667,23 @@ and extract_cst_app env mle mlt kn args = let head = put_magic_if magic1 (MLglob (ConstRef kn)) in (* Now, the extraction of the arguments. *) let s_full = type2signature env (snd schema) in - let s_full = sign_with_implicits (ConstRef kn) s_full in + let s_full = sign_with_implicits (ConstRef kn) s_full 0 in let s = sign_no_final_keeps s_full in let ls = List.length s in let la = List.length args in (* The ml arguments, already expunged from known logical ones *) let mla = make_mlargs env mle s args metas in let mla = - if not magic1 then + if magic1 || lang () <> Ocaml then mla + else try + (* for better optimisations later, we discard dependent args + of projections and replace them by fake args that will be + removed during final pretty-print. *) let l,l' = list_chop (projection_arity (ConstRef kn)) mla in if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla with _ -> mla - else mla in (* For strict languages, purely logical signatures with at least one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left @@ -726,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let type_cons = instantiation (nb_tvars, type_cons) in (* Then, the usual variables [s], [ls], [la], ... *) let s = List.map (type2sign env) types in - let s = sign_with_implicits (ConstructRef cp) s in + let s = sign_with_implicits (ConstructRef cp) s params_nb in let ls = List.length s in let la = List.length args in assert (la <= ls + params_nb); @@ -805,7 +808,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let l = List.map f oi.ip_types.(i) in (* the corresponding signature *) let s = List.map (type2sign env) oi.ip_types.(i) in - let s = sign_with_implicits r s in + let s = sign_with_implicits r s mi.ind_nparams in (* Extraction of the branch (in functional form). *) let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) @@ -876,7 +879,7 @@ let extract_std_constant env kn body typ = let l,t' = type_decomp (expand env (var2var' t)) in let s = List.map (type2sign env) l in (* Check for user-declared implicit information *) - let s = sign_with_implicits (ConstRef kn) s in + let s = sign_with_implicits (ConstRef kn) s 0 in (* Decomposing the top level lambdas of [body]. If there isn't enough, it's ok, as long as remaining args aren't to be pruned (and initial lambdas aren't to be all @@ -923,6 +926,19 @@ let extract_std_constant env kn body typ = in trm, type_expunge_from_sign env s t +(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) +let extract_axiom env kn typ = + reset_meta_count (); + (* The short type [t] (i.e. possibly with abbreviations). *) + let t = snd (record_constant_type env kn (Some typ)) in + (* The real type [t']: without head products, expanded, *) + (* and with [Tvar] translated to [Tvar'] (not instantiable). *) + let l,_ = type_decomp (expand env (var2var' t)) in + let s = List.map (type2sign env) l in + (* Check for user-declared implicit information *) + let s = sign_with_implicits (ConstRef kn) s 0 in + type_expunge_from_sign env s t + let extract_fixpoint env vkn (fi,ti,ci) = let n = Array.length vkn in let types = Array.make n (Tdummy Kother) @@ -959,8 +975,8 @@ let extract_constant env kn cb = in Dtype (r, vl, t) in let mk_ax () = - let t = snd (record_constant_type env kn (Some typ)) in - Dterm (r, MLaxiom, type_expunge env t) + let t = extract_axiom env kn typ in + Dterm (r, MLaxiom, t) in let mk_def c = let e,t = extract_std_constant env kn c typ in diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 257e1c1c..bd997d2d 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -26,9 +26,9 @@ let rec msid_of_mt = function (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) -let se_iter do_decl do_spec = +let se_iter do_decl do_spec do_mp = let rec mt_iter = function - | MTident _ -> () + | MTident mp -> do_mp mp | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' | MTwith (mt,ML_With_type(idl,l,t))-> let mp_mt = msid_of_mt mt in @@ -38,7 +38,12 @@ let se_iter do_decl do_spec = in let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) - | MTwith (mt,_)->mt_iter mt + | MTwith (mt,ML_With_module(idl,mp))-> + let mp_mt = msid_of_mt mt in + let mp_w = + List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl + in + mt_iter mt; do_mp mp_w; do_mp mp | MTsig (_, sign) -> List.iter spec_iter sign and spec_iter = function | (_,Spec s) -> do_spec s @@ -51,15 +56,16 @@ let se_iter do_decl do_spec = me_iter m.ml_mod_expr; mt_iter m.ml_mod_type | (_,SEmodtype m) -> mt_iter m and me_iter = function - | MEident _ -> () + | MEident mp -> do_mp mp | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt | MEapply (me,me') -> me_iter me; me_iter me' | MEstruct (msid, sel) -> List.iter se_iter sel in se_iter -let struct_iter do_decl do_spec s = - List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s +let struct_iter do_decl do_spec do_mp s = + List.iter + (function (_,sel) -> List.iter (se_iter do_decl do_spec do_mp) sel) s (*s Apply some fonctions upon all references in [ml_type], [ml_ast], [ml_decl], [ml_spec] and [ml_structure]. *) @@ -141,7 +147,7 @@ let decl_ast_search f = function | _ -> () let struct_ast_search f s = - try struct_iter (decl_ast_search f) (fun _ -> ()) s; false + try struct_iter (decl_ast_search f) (fun _ -> ()) (fun _ -> ()) s; false with Found -> true let rec type_search f = function @@ -165,7 +171,9 @@ let spec_type_search f = function | Sval (_,u) -> type_search f u let struct_type_search f s = - try struct_iter (decl_type_search f) (spec_type_search f) s; false + try + struct_iter (decl_type_search f) (spec_type_search f) (fun _ -> ()) s; + false with Found -> true @@ -247,34 +255,32 @@ let dfix_to_mlfix rv av i = let c = Array.map (subst 0) av in MLfix(i, ids, c) +(* [optim_se] applies the [normalize] function everywhere and does the + inlining of code. The inlined functions are kept for the moment in + order to preserve the global interface, later [depcheck_se] will get + rid of them if possible *) + let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - if top && i && not (library ()) && not (List.mem r to_appear) - then optim_se top to_appear s lse - else - let d = match optimize_fix a with - | MLfix (0, _, [|c|]) -> - Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) - | a -> Dterm (r, a, t) - in (l,SEdecl d) :: (optim_se top to_appear s lse) + let d = match optimize_fix a with + | MLfix (0, _, [|c|]) -> + Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) + | a -> Dterm (r, a, t) + in + (l,SEdecl d) :: (optim_se top to_appear s lse) | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in - let all = ref true in (* This fake body ensures that no fixpoint will be auto-inlined. *) let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s - else all := false done; - if !all && top && not (library ()) - && (array_for_all (fun r -> not (List.mem r to_appear)) rv) - then optim_se top to_appear s lse - else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) + (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} in (l,SEmodule m) :: (optim_se top to_appear s lse) @@ -289,7 +295,7 @@ and optim_me to_appear s = function (* After these optimisations, some dependencies may not be needed anymore. For non-library extraction, we recompute a minimal set of dependencies - for first-level objects *) + for first-level definitions (no module pruning yet). *) exception NoDepCheck @@ -362,7 +368,7 @@ let rec depcheck_se = function end | t :: se -> let se' = depcheck_se se in - se_iter compute_deps_decl compute_deps_spec t; + se_iter compute_deps_decl compute_deps_spec add_needed_mp t; t :: se' let rec depcheck_struct = function @@ -370,7 +376,7 @@ let rec depcheck_struct = function | (mp,lse)::struc -> let struc' = depcheck_struct struc in let lse' = depcheck_se lse in - (mp,lse')::struc' + if lse' = [] then struc' else (mp,lse')::struc' let check_implicits = function | MLexn s -> @@ -389,9 +395,9 @@ let optimize_struct to_appear struc = List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) struc in - let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in ignore (struct_ast_search check_implicits opt_struc); - if library () then opt_struc + if library () then + List.filter (fun (_,lse) -> lse<>[]) opt_struc else begin reset_needed (); List.iter add_needed (fst to_appear); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c88c6669..43b08840 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -308,13 +308,14 @@ let build_constructors_of_type ind' argl = (Global.env ()) construct in - let argl = - if argl = [] - then + let argl = match argl with + | None -> Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) + (Array.init cst_narg (fun _ -> mkGHole ()) ) - else argl + | Some l -> + Array.to_list + (Array.init npar (fun _ -> mkGHole ()))@l in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) @@ -653,7 +654,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind [] in + let case_pats = build_constructors_of_type ind None in assert (Array.length case_pats = 2); let brl = list_map_i @@ -669,12 +670,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GLetTuple(_,nal,_,b,e) -> begin let nal_as_glob_constr = - List.map + Some (List.map (function Name id -> mkGVar id | Anonymous -> mkGHole () ) - nal + nal) in let b_as_constr = Pretyping.Default.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 11d9a071..ab424c22 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -14,14 +14,14 @@ Delimit Scope Int_scope with I. Module Type Int. - Parameter int : Set. + Parameter t : Set. - Parameter zero : int. - Parameter one : int. - Parameter plus : int -> int -> int. - Parameter opp : int -> int. - Parameter minus : int -> int -> int. - Parameter mult : int -> int -> int. + Parameter zero : t. + Parameter one : t. + Parameter plus : t -> t -> t. + Parameter opp : t -> t. + Parameter minus : t -> t -> t. + Parameter mult : t -> t -> t. Notation "0" := zero : Int_scope. Notation "1" := one : Int_scope. @@ -33,14 +33,14 @@ Module Type Int. Open Scope Int_scope. (* First, int is a ring: *) - Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int). + Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t). (* int should also be ordered: *) - Parameter le : int -> int -> Prop. - Parameter lt : int -> int -> Prop. - Parameter ge : int -> int -> Prop. - Parameter gt : int -> int -> Prop. + Parameter le : t -> t -> Prop. + Parameter lt : t -> t -> Prop. + Parameter ge : t -> t -> Prop. + Parameter gt : t -> t -> Prop. Notation "x <= y" := (le x y): Int_scope. Notation "x < y" := (lt x y) : Int_scope. Notation "x >= y" := (ge x y) : Int_scope. @@ -61,7 +61,7 @@ Module Type Int. forall i j k, 0 < k -> i < j -> k*i int -> comparison. + Parameter compare : t -> t -> comparison. Infix "?=" := compare (at level 70, no associativity) : Int_scope. Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j. Axiom compare_Lt : forall i j, compare i j = Lt <-> i t1 = t2. Proof. - simple induction t1; intros until t2; case t2; simpl in *; - try (intros; discriminate; fail); - [ intros; elim beq_true with (1 := H); trivial - | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; - elim H with (1 := H4); elim H0 with (1 := H5); - trivial - | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; - elim H with (1 := H4); elim H0 with (1 := H5); - trivial - | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5; - elim H with (1 := H4); elim H0 with (1 := H5); - trivial - | intros t21 H3; elim H with (1 := H3); trivial - | intros; elim beq_nat_true with (1 := H); trivial ]. + induction t1; destruct t2; simpl in *; try discriminate; + (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal; + auto using beq_true, beq_nat_true. +Qed. + +Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true. +Proof. + induction t0; simpl in *; try (apply andb_true_iff; split); trivial. + - now apply beq_iff. + - now apply beq_nat_true_iff. Qed. Ltac trivial_case := unfold not; intros; discriminate. @@ -1058,31 +1056,7 @@ Ltac trivial_case := unfold not; intros; discriminate. Theorem eq_term_false : forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2. Proof. - simple induction t1; - [ intros z t2; case t2; try trivial_case; simpl; unfold not; - intros; elim beq_false with (1 := H); simplify_eq H0; - auto - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; - intros t21 t22 H3; unfold not; intro H4; - elim andb_false_elim with (1 := H3); intros H5; - [ elim H1 with (1 := H5); simplify_eq H4; auto - | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; - intros t21 t22 H3; unfold not; intro H4; - elim andb_false_elim with (1 := H3); intros H5; - [ elim H1 with (1 := H5); simplify_eq H4; auto - | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; - intros t21 t22 H3; unfold not; intro H4; - elim andb_false_elim with (1 := H3); intros H5; - [ elim H1 with (1 := H5); simplify_eq H4; auto - | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3; - unfold not; intro H4; elim H1 with (1 := H3); - simplify_eq H4; auto - | intros n t2; case t2; try trivial_case; simpl; unfold not; - intros; elim beq_nat_false with (1 := H); simplify_eq H0; - auto ]. + intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H. Qed. (* \subsubsection{Tactiques pour éliminer ces tests} @@ -1919,9 +1893,9 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := end end. -Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t). +Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace). Proof. - simple induction t; simpl; + simple induction trace; simpl; [ exact reduce_stable | intros stp l H; case stp; [ apply compose_term_stable; @@ -2093,11 +2067,8 @@ Definition constant_not_nul (i : nat) (h : hyps) := Theorem constant_not_nul_valid : forall i : nat, valid_hyps (constant_not_nul i). Proof. - unfold valid_hyps, constant_not_nul; intros; - generalize (nth_valid ep e i lp); Simplify; simpl. - - elim_beq i1 i0; auto; simpl; intros H1 H2; - elim H1; symmetry ; auto. + unfold valid_hyps, constant_not_nul; intros i ep e lp H. + generalize (nth_valid ep e i lp H); Simplify. Qed. (* \paragraph{[O_CONSTANT_NEG]} *) @@ -2131,12 +2102,12 @@ Definition not_exact_divide (k1 k2 : int) (body : term) end. Theorem not_exact_divide_valid : - forall (k1 k2 : int) (body : term) (t i : nat), - valid_hyps (not_exact_divide k1 k2 body t i). + forall (k1 k2 : int) (body : term) (t0 i : nat), + valid_hyps (not_exact_divide k1 k2 body t0 i). Proof. unfold valid_hyps, not_exact_divide; intros; generalize (nth_valid ep e i lp); Simplify. - rewrite (scalar_norm_add_stable t e), <-H1. + rewrite (scalar_norm_add_stable t0 e), <-H1. do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros. absurd (interp_term e body * k1 + k2 = 0); [ now apply OMEGA4 | symmetry; auto ]. @@ -2509,9 +2480,9 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := execute_omega cont (apply_oper_2 i1 i2 (state m s) l) end. -Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t). +Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr). Proof. - simple induction t; simpl; + simple induction tr; simpl; [ unfold valid_list_hyps; simpl; intros; left; apply (constant_not_nul_valid n ep e lp H) | unfold valid_list_hyps; simpl; intros; left; @@ -2522,7 +2493,7 @@ Proof. (apply_oper_1_valid m (divide_and_approx k1 k2 body n) (divide_and_approx_valid k1 k2 body n) ep e lp H) | unfold valid_list_hyps; simpl; intros; left; - apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H) + apply (not_exact_divide_valid _ _ _ _ _ ep e lp H) | unfold valid_list_hyps, valid_hyps; intros k body n t' Ht' m ep e lp H; apply Ht'; apply @@ -2618,10 +2589,10 @@ Qed. (* \subsubsection{Exécution de la trace} *) Theorem execute_goal : - forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps), - interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l. + forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps), + interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l. Proof. - intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H). + intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H). Qed. @@ -2936,13 +2907,13 @@ Proof. | intro; apply ne_left_2; assumption ] | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s); simpl; intro H1; - [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1; + [ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1; rewrite plus_permute; rewrite plus_opp_r; rewrite plus_0_r; trivial - | apply (fun a b => plus_le_reg_r a b (- interp_term e t)); + | apply (fun a b => plus_le_reg_r a b (- interp_term e t0)); rewrite plus_opp_r; assumption | rewrite ge_le_iff; - apply (fun a b => plus_le_reg_r a b (- interp_term e t0)); + apply (fun a b => plus_le_reg_r a b (- interp_term e t1)); rewrite plus_opp_r; assumption | rewrite gt_lt_iff; apply lt_left_inv; assumption | apply lt_left_inv; assumption diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 6a5878b3..dfcc8526 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -663,6 +663,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) let admit_obligations n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in + let obls = Array.copy obls in Array.iteri (fun i x -> match x.obl_body with -- cgit v1.2.3