-
Notifications
You must be signed in to change notification settings - Fork 1
/
CHANGES
186 lines (163 loc) · 7.38 KB
/
CHANGES
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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
(* $State: Exp $ $Date: 2005/02/28 14:10:07 $ $Revision: 1.5 $ *)
(**************************************************************)
HISTORY OF THE PROOF SYSTEM PhoX
by
C. Raffalli
Equipe de logique de Paris VII
&
Universite de Savoie
(**************************************************************)
version 0.31b2
- Some convention have been chosen for the library in order to
generate the documentation automatically.
- New commands prop, theo, etc to start a proof.
goal is now obsolete but still available.
- outline-minor-mode in emacs mode (thanks to P. Roziere).
version 0.31b1
- added rename tactic
- fixed a problem with new_elim -i
- fixed a bug in test_seq function
- modified emacs mode with output possible in local buffer
(thanks to P. Roziere).
- menu in emacs mode
version 0.30b9
- added apply tactic
- added absurd tactic
version 0.30b8
- fixed a bug in the bactracking (and undo) mechanism
version 0.30b7 (not public)
- change in the installation procedure:
the preprocessor is only used for main.ml
the config file let you change DELIM and DEFAULT_PATH
- fix in INSTALL and doc/intro.tex (the emacs stuff was not 100% clean)
- af2 now uses the Filename module. Other minor changes to make af2
portable under windows
version 0.30b6
- first public version
version 0.4
- ?
version 0.5
- many bug fixes and minor changes to af2
- work on the documentation and library
- better emacs mode
version 0.6
- change to af2
- polymorphic theorems are now allowed
- only one kind of quantification for all sorts (no more second order
quantfication)
- equality is polymorphic
- possible to add or define new sorts (with the Sort command)
- various bug fixes (three very old bugs now fixed)
- somme tactical added
- change to the emacs-mode
- works better with xemacs
- font-lock cleaned
- sym-lock added to use adobe-symbol font with xemacs
- change to the library
- global: the sort are renamed:
Form -> prop
Term disapear and is replaced by
nat, list[s], ...
- bool.af2: now uses the sort prop instead of term.
all the function on booleans are replaced by the connective.
- prop.af2: new axioms added:
claim equal.proposition /\X,Y (X <-> Y -> X = Y).
claim equal.extensional /\X,Y (/\x (X x = Y x) -> X = Y).
De Morgan law added as equations (no new_rewrite yet)
- change to devtools (developper only)
- check_locked rewritten to be useful
- lock and unlock can work on more than one files
- unrelock added (to propagate to the server and keep the file locked)
version 0.7
- the software if now called PhoX for Proof in Higher Order eXtensible Logic
version 0.8
- too many changes (including better documentation)
version 0.81
- few bug fixes
- rename now works also on hypotheses
version 0.82
- more bug fixes
- tutorial translated in english
version 0.83
- changed associativity of & and or (now right associative)
- changed associativity of + and * (now right associative) and
various changes to be consistant with this choice.
- the intro rule Def.axiom (in prop.phx) is now tried last (option
-o 10.0) to avoid strange behavior in some cases.
- changed the behavior of unification: the order in which term are
unified is more precisely specified (not yet enough).
- a new warning for Prefix and Infix syntax for Prefix and Infix
syntax withless argument than indicated by their type.
- a bug fix in the pretty printer (not enough parenthesis when
using Prefix and Infix syntax with less argument than indicated by
their type).
- a possible infinite loop in unification removed (unification can
still loop: it is higher-order unification !)
- fixed a bug in rewrite: the definition of the head symbol of the
rewriten pattern could be opened and this is not what rewrite should
do.
- added the flag auto_type and changed the meaning of auto_lvl.
- all tactics instanciating unification variables will check if old
goals can be solved when auto_lvl or auto_type are in use (not only
instance).
- new_rewrite renamed in new_equation (and eshow rewrite in eshow
equation) the doc and examples have been updated (the old command
is still accepted. new_equation accepts more that one theorem.
version 0.84
- fixed a bug in unification that provoced useless opening of
definitions (when unifying a term with a constant head and a term
with a define head of generation 0 (a definition using no other
constant of definition such as "in = \x\y (y x)".
- fixed a bug in the intro tactic that could open too much definition.
- fixed a bug: some locally defined symbols could be considered as equal
resulting in the construction of wrong proofs.
- fixed long standing bug in test_clean (cleaning of useless left
rules).
version 0.85
- added support for "proof by contextual menu" with proof-general
- changed the semantics of "flag auto-lvl n". Old goals are also
tested. This means that after an instanciation of a unification
variables, more goals are now automatically resolved.
- in intros and lefts, \/ and & are now grouped (as /\ and -> were
in intros) (this may need an adaptation of proofs)
- fixed a bug in intros that prevented some introduction
- fixed a bug in left(s) that resulted in wrong names choosen for
existential (this may need an adaptation of proofs)
- the semantics of intro and left are now the same (either rule
names of names for new constant). There should be bracket arround
rule names as in apply and left.
- inversed the order in which left generate new goals. This order
was inversed between left and elim (for instance for a disjunction)
and left did present the goals in reverse order compared with the
order of subformulas (this may need an adaptation of proofs).
- you can now add a prefix to proof commands to select goal.
[n] cmd : apply cmd to goal n
[n m ...] : apply cmd to goals n, m ...
[*] (without spaces) : apply cmd to all goals
- relaxed the semantics of "with" in apply and elim:
* "and" is now really commutative.
* the tactics backtracks more to try more combination
* the tactics try to unify the arguments under conjunction,
disjunction and existential. For instance, if the goal is
H := /\x (\/y (A x y & B y) -> C
H0 := A u v
|- C
then elim H with H0 will succeed and ask to prove B v.
* the usage of "then" is now limited to select among many
unification. Giving more argument to "with" may be now a better
way to achieve the same result.
* warning: in theory, the complexity is exponential in the number
of argument to "with", "then" may also be used to decrease the
complexity, although no complexity problem have been observed
yet.
- rewrite -l n is interpreted with n as a limite for the number of
equation while in unfold -l n, n is the number of equation + the
number of definition expansion.
- rename of hypothesis now works properly (there was a bug with undo)
- added by_contradiction command corresponding to
~ A |- False implies |- A
0.89
- compilation with recent OCaml
- new "cd" command
- updated proof general mode to version 4.4 of PG
- compilation with ocamlbuild