From 0780de3f579681aa80e5e353d3aaeeaa418f2369 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 1 Dec 2009 12:05:57 +0000 Subject: 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 --- test-suite/output/Naming.out | 96 ++++++++++++++++++++++++++++++++++++++++++++ test-suite/output/Naming.v | 73 +++++++++++++++++++++++++++++++++ 2 files changed, 169 insertions(+) create mode 100644 test-suite/output/Naming.out create mode 100644 test-suite/output/Naming.v (limited to 'test-suite') diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out new file mode 100644 index 0000000000..211a167145 --- /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 0000000000..71587e2eef --- /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) *) -- cgit v1.2.3