diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Naming.out | 96 | ||||
| -rw-r--r-- | test-suite/output/Naming.v | 73 |
2 files changed, 169 insertions, 0 deletions
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) *) |