diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-01 12:05:57 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-01 12:05:57 +0000 |
commit | 0780de3f579681aa80e5e353d3aaeeaa418f2369 (patch) | |
tree | 6b7972209d1f181bf2182f6c8228f96ea2910824 | |
parent | 986dc499c5ff0bfda89537ee1be7b6c512c2846d (diff) |
Continuing r12485-12486 (cleaning around name generation)
- backtrack on incompatibility introduced in intro while trying to
simplify the condition about when to restart the subscript of a name
(the legacy says: find a new name from x0 if the name xN exists in
the context but find a new name from xN+1 if the name xN does not
exists in the context but is a global to avoid).
- made the names chosen by "intro" compliant with the ones printed in
the goal and used for "intros until" (possible source of rare
incompatibilities) [replaced the use of visibly_occur_id for
printing the goal into a call to next_name_away_in_goal]
- also made the names internal to T in "T -> U" printed the same in
the goal as they are while printing T after it is introducted in the
hypotheses [non contravariant propagation of boolean isgoal in
detype_binder]
- simplified a bit visibly_occur_id (the Rel and Var cases were useless as
soon as the avoid list contained the current env); still this function is
costly with polynomial time in the depth of binders
- see file output/Naming.v for examples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/environ.mli | 5 | ||||
-rw-r--r-- | library/impargs.ml | 11 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 3 | ||||
-rw-r--r-- | pretyping/clenv.ml | 4 | ||||
-rw-r--r-- | pretyping/detyping.ml | 48 | ||||
-rw-r--r-- | pretyping/namegen.ml | 186 | ||||
-rw-r--r-- | pretyping/namegen.mli | 19 | ||||
-rw-r--r-- | pretyping/termops.ml | 11 | ||||
-rw-r--r-- | pretyping/termops.mli | 1 | ||||
-rw-r--r-- | test-suite/output/Naming.out | 96 | ||||
-rw-r--r-- | test-suite/output/Naming.v | 73 |
11 files changed, 334 insertions, 123 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 315bddd1f..667a0ed43 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -161,8 +161,9 @@ val set_engagement : engagement -> env -> env (************************************************************************) (* Sets of referred section variables *) -(* [global_vars_set env c] returns the list of [id]'s occurring as - [VAR id] in [c] *) +(* [global_vars_set env c] returns the list of [id]'s occurring either + directly as [Var id] in [c] or indirectly as a section variable + dependent in a global reference occurring in [c] *) val global_vars_set : env -> constr -> Idset.t (* the constr must be a global reference *) val vars_of_global : env -> constr -> identifier list diff --git a/library/impargs.ml b/library/impargs.ml index f82ef03e9..fead921a5 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -200,15 +200,18 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc = (* calcule la liste des arguments implicites *) -let find_displayed_name_in all = - if all then compute_and_force_displayed_name_in else compute_displayed_name_in +let find_displayed_name_in all avoid na b = + if all then + compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b + else + compute_displayed_name_in (RenamingElsewhereFor b) avoid na b let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in all None avoid names na b in + let na',avoid' = find_displayed_name_in all avoid na b in add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) | _ -> @@ -220,7 +223,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = in match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all None [] [] na b in + let na',avoid = find_displayed_name_in all [] na b in let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in Array.to_list v | _ -> [] diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 469f87f15..5c910c424 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,7 +51,8 @@ open Genarg let compute_renamed_type gls c = - rename_bound_vars_as_displayed (pf_env gls) [] (pf_type_of gls c) + let ids = collect_visible_vars c in + rename_bound_vars_as_displayed ids (pf_type_of gls c) let qed () = Lemmas.save_named true let defined () = Lemmas.save_named false diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index fe84141ee..aa58a0808 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -32,6 +32,7 @@ open Coercion.Default (* Abbreviations *) let pf_env gls = Global.env_of_context gls.it.evar_hyps +let pf_hyps gls = named_context_of_val gls.it.evar_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c let pf_concl gl = gl.it.evar_concl @@ -146,7 +147,8 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None let mk_clenv_rename_from_n gls n (c,t) = - mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed (pf_env gls) [] t) + let ids = collect_visible_vars t in + mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed ids t) let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c152f3ca8..f1da217a6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -171,27 +171,23 @@ let computable p k = let avoid_flag isgoal = if isgoal then Some true else None let lookup_name_as_displayed env t s = - let rec lookup avoid env_names n c = match kind_of_term c with + let rec lookup avoid n c = match kind_of_term c with | Prod (name,_,c') -> - (match compute_displayed_name_in (Some true) avoid env_names name c' with - | (Name id,avoid') -> - if id=s then (Some n) - else lookup avoid' (add_name (Name id) env_names) (n+1) c' - | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c')) + (match compute_displayed_name_in RenamingForGoal avoid name c' with + | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c' + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> - (match compute_displayed_name_in (Some true) avoid env_names name c' with - | (Name id,avoid') -> - if id=s then (Some n) - else lookup avoid' (add_name (Name id) env_names) (n+1) c' - | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c')) - | Cast (c,_,_) -> lookup avoid env_names n c + (match compute_displayed_name_in RenamingForGoal avoid name c' with + | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c' + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) + | Cast (c,_,_) -> lookup avoid n c | _ -> None - in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t + in lookup (ids_of_named_context (named_context env)) 1 t let lookup_index_as_renamed env t n = let rec lookup n d c = match kind_of_term c with | Prod (name,_,c') -> - (match compute_displayed_name_in (Some true) [] empty_names_context name c' with + (match compute_displayed_name_in RenamingForGoal [] name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if n=0 then @@ -201,7 +197,7 @@ let lookup_index_as_renamed env t n = else lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> - (match compute_displayed_name_in (Some true) [] empty_names_context name c' with + (match compute_displayed_name_in RenamingForGoal [] name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if n=0 then @@ -226,6 +222,7 @@ let update_name na ((_,e),c) = na let rec decomp_branch n nal b (avoid,env as e) c = + let flag = if b then RenamingForGoal else RenamingForCasesPattern in if n=0 then (List.rev nal,(e,c)) else let na,c,f = @@ -235,7 +232,7 @@ let rec decomp_branch n nal b (avoid,env as e) c = | _ -> Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])), compute_displayed_name_in in - let na',avoid' = f (Some b) avoid env na c in + let na',avoid' = f flag avoid na c in decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c let rec build_tree na isgoal e ci cl = @@ -533,16 +530,15 @@ and detype_eqn isgoal avoid env constr construct_nargs branch = buildrec [] [] avoid env construct_nargs branch and detype_binder isgoal bk avoid env na ty c = + let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in let na',avoid' = - if bk = BLetIn then - compute_displayed_let_name_in (avoid_flag isgoal) avoid env na c - else - compute_displayed_name_in (avoid_flag isgoal) avoid env na c in + if bk = BLetIn then compute_displayed_let_name_in flag avoid na c + else compute_displayed_name_in flag avoid na c in let r = detype isgoal avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r) - | BLambda -> RLambda (dl, na',Explicit,detype isgoal avoid env ty, r) - | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r) + | BProd -> RProd (dl, na',Explicit,detype false avoid env ty, r) + | BLambda -> RLambda (dl, na',Explicit,detype false avoid env ty, r) + | BLetIn -> RLetIn (dl, na',detype false avoid env ty, r) let rec detype_rel_context where avoid env sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in @@ -553,8 +549,10 @@ let rec detype_rel_context where avoid env sign = match where with | None -> na,avoid | Some c -> - if b<>None then compute_displayed_let_name_in None avoid env na c - else compute_displayed_name_in None avoid env na c in + if b<>None then + compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c + else + compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in let b = Option.map (detype false avoid env) b in let t = detype false avoid env t in (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 027dbb3ff..c4349624f 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -140,40 +140,75 @@ let it_mkLambda_or_LetIn_name env b hyps = (**********************************************************************) (* Fresh names *) +let default_x = id_of_string "x" + +(* Looks for next "good" name by lifting subscript *) + let next_ident_away_from id bad = let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in - if bad id then - let id0 = if not (has_subscript id) then id else - (* Ce serait sans doute mieux avec quelque chose inspiré de - *** make_ident id (Some 0) *** mais ça brise la compatibilité... *) - forget_subscript id in - name_rec id0 - else id + name_rec id -let next_ident_away id avoid = - next_ident_away_from id (fun id -> List.mem id avoid) +(* Restart subscript from x0 if name starts with xN, or x00 if name + starts with x0N, etc *) -let next_name_away_with_default default name avoid = - let id = match name with Name id -> id | Anonymous -> id_of_string default in - next_ident_away id avoid +let restart_subscript id = + if not (has_subscript id) then id else + (* Ce serait sans doute mieux avec quelque chose inspiré de + *** make_ident id (Some 0) *** mais ça brise la compatibilité... *) + forget_subscript id -let next_name_away = next_name_away_with_default "H" +(* Now, there are different renaming strategies... *) -let default_x = id_of_string "x" +(* 1- Looks for a fresh name for printing in cases pattern *) let next_name_away_in_cases_pattern na avoid = let id = match na with Name id -> id | Anonymous -> default_x in next_ident_away_from id (fun id -> List.mem id avoid or is_constructor id) +(* 2- Looks for a fresh name for introduction in goal *) + +(* The legacy strategy for renaming introduction variables is not very uniform: + - if the name to use is fresh in the context but used as a global + name, then a fresh name is taken by finding a free subscript + starting from the current subscript; + - but if the name to use is not fresh in the current context, the fresh + name is taken by finding a free subscript starting from 0 *) + let next_ident_away_in_goal id avoid = - let bad id = - List.mem id avoid || (is_global id & not (is_section_variable id)) in + let id = if List.mem id avoid then restart_subscript id else id in + let bad id = List.mem id avoid || (is_global id & not (is_section_variable id)) in next_ident_away_from id bad +let next_name_away_in_goal na avoid = + let id = match na with Name id -> id | Anonymous -> id_of_string "H" in + next_ident_away_in_goal id avoid + +(* 3- Looks for next fresh name outside a list that is moreover valid + as a global identifier; the legacy algorithm is that if the name is + already used in the list, one looks for a name of same base with + lower available subscript; if the name is not in the list but is + used globally, one looks for a name of same base with lower subscript + beyond the current subscript *) + let next_global_ident_away id avoid = + let id = if List.mem id avoid then restart_subscript id else id in let bad id = List.mem id avoid || is_global id in next_ident_away_from id bad +(* 4- Looks for next fresh name outside a list; if name already used, + looks for same name with lower available subscript *) + +let next_ident_away id avoid = + if List.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> List.mem id avoid) + else id + +let next_name_away_with_default default na avoid = + let id = match na with Name id -> id | Anonymous -> id_of_string default in + next_ident_away id avoid + +let next_name_away = next_name_away_with_default "H" + let make_all_name_different env = let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context @@ -183,8 +218,38 @@ let make_all_name_different env = push_rel (Name id,c,t) newenv) env +(* 5- Looks for next fresh name outside a list; avoids also to use names that + would clash with short name of global references; if name is already used, + looks for name of same base with lower available subscript beyond current + subscript *) + +let visibly_occur_id id c = + let rec occur c = match kind_of_term c with + | Const _ | Ind _ | Construct _ + when shortest_qualid_of_global Idset.empty (global_of_constr c) + = qualid_of_ident id -> raise Occur + | _ -> iter_constr occur c + in + try occur c; false + with Occur -> true + | Not_found -> false (* Happens when a global is not in the env *) + +let next_ident_away_for_default_printing t id avoid = + let bad id = List.mem id avoid or visibly_occur_id id t in + next_ident_away_from id bad + +let next_name_away_for_default_printing t na avoid = + let id = match na with + | Name id -> id + | Anonymous -> + (* In principle, an anonymous name is not dependent and will not be *) + (* taken into account by the function compute_displayed_name_in; *) + (* just in case, invent a valid name *) + id_of_string "H" in + next_ident_away_for_default_printing t id avoid + (**********************************************************************) -(* The algorithm to display distinct bound variables *) +(* Displaying terms avoiding bound variables clashes *) (* Renaming strategy introduced in December 1998: @@ -199,84 +264,47 @@ let make_all_name_different env = but f and f0 contribute to the list of variables to avoid (knowing that f and f0 are how the f's would be named if introduced, assuming no other f and f0 are already used). - - The objective was to have the same names in goals before and after intros. *) -type avoid_flags = bool option - -let is_rel_id_in_env p env id = - try lookup_name_of_rel p env = Name id - with Not_found -> false (* Unbound indice : may happen in debug *) - -let visibly_occur_id nenv id0 c = - let rec occur n c = match kind_of_term c with - | Var id when id=id0 -> raise Occur - | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur - | Ind ind_sp - when basename_of_global (IndRef ind_sp) = id0 -> - raise Occur - | Construct cstr_sp - when basename_of_global (ConstructRef cstr_sp) = id0 -> - raise Occur - | Rel p when p>n & is_rel_id_in_env (p-n) nenv id0 -> raise Occur - | _ -> iter_constr_with_binders succ occur n c - in - try occur 1 c; false - with Occur -> true - | Not_found -> false (* Happens when a global is not in the env *) +type renaming_flags = + | RenamingForCasesPattern + | RenamingForGoal + | RenamingElsewhereFor of constr -let next_name_not_occurring avoid_flags name l env_names t = - let rec next id = - if List.mem id l or visibly_occur_id env_names id t or - (* Further restrictions ? *) - match avoid_flags with None -> false | Some not_only_cstr -> - (if not_only_cstr then - (* To be consistent with the intro mechanism *) - is_global id & not (is_section_variable id) - else - (* To avoid constructors in pattern-matchings *) - is_constructor id) - then next (lift_subscript id) - else id - in - match name with - | Name id -> next id - | Anonymous -> - (* In principle, an anonymous name is not dependent and will not be *) - (* taken into account by the function compute_displayed_name_in; *) - (* just in case, invent a valid name *) - next (id_of_string "H") +let next_name_for_display flags = + match flags with + | RenamingForCasesPattern -> next_name_away_in_cases_pattern + | RenamingForGoal -> next_name_away_in_goal + | RenamingElsewhereFor t -> next_name_away_for_default_printing t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in avoid_flags l env_names n c = - if n = Anonymous & noccurn 1 c then - (Anonymous,l) +let compute_displayed_name_in flags avoid na c = + if na = Anonymous & noccurn 1 c then + (Anonymous,avoid) else - let fresh_id = next_name_not_occurring avoid_flags n l env_names c in + let fresh_id = next_name_for_display flags na avoid in let idopt = if noccurn 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::l) + (idopt, fresh_id::avoid) -let compute_and_force_displayed_name_in avoid_flags l env_names n c = - if n = Anonymous & noccurn 1 c then - (Anonymous,l) +let compute_and_force_displayed_name_in flags avoid na c = + if na = Anonymous & noccurn 1 c then + (Anonymous,avoid) else - let fresh_id = next_name_not_occurring avoid_flags n l env_names c in - (Name fresh_id, fresh_id::l) + let fresh_id = next_name_for_display flags na avoid in + (Name fresh_id, fresh_id::avoid) -let compute_displayed_let_name_in avoid_flags l env_names n c = - let fresh_id = next_name_not_occurring avoid_flags n l env_names c in - (Name fresh_id, fresh_id::l) +let compute_displayed_let_name_in flags avoid na c = + let fresh_id = next_name_for_display flags na avoid in + (Name fresh_id, fresh_id::avoid) -let rec rename_bound_vars_as_displayed env avoid c = - let env_names = names_of_rel_context env in +let rec rename_bound_vars_as_displayed avoid c = let rec rename avoid c = match kind_of_term c with | Prod (na,c1,c2) -> - let na',avoid' = compute_displayed_name_in None avoid env_names na c2 in + let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in mkProd (na', c1, rename avoid' c2) | LetIn (na,c1,t,c2) -> - let na',avoid' = compute_displayed_let_name_in None avoid env_names na c2 in + let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in mkLetIn (na',c1,t, rename avoid' c2) | Cast (c,k,t) -> mkCast (rename avoid c, k,t) | _ -> c diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 0587b886b..096c09b51 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -61,20 +61,17 @@ val next_name_away_with_default : string -> name -> identifier list -> (**********************************************************************) (* Making name distinct for displaying *) -type avoid_flags = bool option - (* Some true = avoid all globals (as in intro); - Some false = avoid only global constructors; - None = don't avoid globals *) +type renaming_flags = + | RenamingForCasesPattern (* avoid only global constructors *) + | RenamingForGoal (* avoid all globals (as in intro) *) + | RenamingElsewhereFor of constr val make_all_name_different : env -> env val compute_displayed_name_in : - avoid_flags -> identifier list -> name list -> name -> constr -> - name * identifier list + renaming_flags -> identifier list -> name -> constr -> name * identifier list val compute_and_force_displayed_name_in : - avoid_flags -> identifier list -> name list -> name -> constr -> - name * identifier list + renaming_flags -> identifier list -> name -> constr -> name * identifier list val compute_displayed_let_name_in : - avoid_flags -> identifier list -> name list -> name -> constr -> - name * identifier list -val rename_bound_vars_as_displayed : env -> identifier list -> types -> types + renaming_flags -> identifier list -> name -> constr -> name * identifier list +val rename_bound_vars_as_displayed : identifier list -> types -> types diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 4de4bde2c..07ac5df21 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -523,6 +523,17 @@ let collect_metas c = in List.rev (collrec [] c) +(* collects all visible var occurences (does not include indirect + dependencies of section variables via global references) *) + +let collect_visible_vars c = + let rec collrec acc c = + match kind_of_term c with + | Var id -> list_add_set id acc + | _ -> fold_constr collrec acc c + in + List.rev (collrec [] c) + (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 59f7750d3..44a96b613 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -109,6 +109,7 @@ val free_rels : constr -> Intset.t val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val collect_metas : constr -> int list +val collect_visible_vars : constr -> identifier list val occur_term : constr -> constr -> bool (* Synonymous of dependent *) (* Substitution of metavariables *) diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out new file mode 100644 index 000000000..211a16714 --- /dev/null +++ b/test-suite/output/Naming.out @@ -0,0 +1,96 @@ +Welcome to Coq localhost:/home/herbelin/coq/git,namegen (cd25d05cf1d1aa17f9c4f90d999559c2e7570b56) +Parameter x2:nat. +x2 is assumed +Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y. +foo is defined +Section A. +Variable x3:nat. +x3 is assumed +Goal forall x x1 x2 x3:nat, + (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3. +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x5 x6 : nat, x5 + x1 = x4 + x6) -> x + x1 = x4 + x0 +intros. +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 + ============================ + x + x1 = x4 + x0 +Abort. +Current goal aborted +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). +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x5 x6 : nat, x5 + x1 = x4 + x6 -> foo (S x5 + x1)) -> + x + x1 = x4 + x0 -> foo (S x) +unfold foo. +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x5 x6 : nat, + x5 + x1 = x4 + x6 -> + forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +do 4 intro. +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + ============================ + (forall x5 x6 : nat, + x5 + x1 = x4 + x6 -> + forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +do 2 intro. +1 subgoal + + 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 + ============================ + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +do 4 intro. +1 subgoal + + 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 diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v new file mode 100644 index 000000000..71587e2ee --- /dev/null +++ b/test-suite/output/Naming.v @@ -0,0 +1,73 @@ +(* 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. +intros. + +(* 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). +unfold foo. +do 4 intro. (* --> x, x1, x4, x0, ... *) +do 2 intro. +do 4 intro. + +(* 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) *) |