1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
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
|
