Overhauled arithmetic overloading.
Tactic changes:
Improved the unhide tactic.
It is no longer possible to backtrack into the middle of
destructThin or inversion.
Rewriting changes:
Fixed a bug in unrollTypeUniv.
There are more compatibility principles around arithmetic, which allows rewriting through more things.
Better diagnostics.
Library changes:
Added integer division and other material to Integer.
Added Division (natural number division).
Added real numbers (Real, RealExponent, RealSequence, and
RealSupremum) and a proof of Cantor’s theorem (CantorTheorem).
Added Squish (like squash, but with computational content).
Added material to Bool, Decidable, Eventually, Logic,
Nat, and Rational.
Renamed shift lemmas in Integer and Rational:
*_r --> *_rrr
*_l --> *_lll
*_lr --> *_rll
*_rl --> *_lrr
The type of Rational.ltq_from_leqq_neq has changed slightly.
Added material to Quotient. Changed the behavior of destruct
on quotient1. Fixed a bug in destruction of Quotient’s quotients.
Basis changes:
ediv and mod to Int and IntInf.Added Markov’s principle and the Markov library.
Added rules eqEqInv1, eqEqInv2, eqEqInv3, ofFormInv1,
ofFormInv2, ofEqInv1, ofEqInv2, boolIntro1Eq,
boolIntro2Eq, futureArrowIntroOf, futureArrowIntroEq, and
futureArrowIntro.
Added the symmetrical property, and the rule
forallQuotientCommute.
Added the rules quotientStrengthenSequalOf and
quotientStrengthenSequalEq.
Reworked the integer primitives and axioms.
The validation now includes the rules pertaining to native types. All the rules are now validated except those pertaining to definitions.
Istari can be compiled on older versions of SML/NJ.
Library changes:
Partial has new material.Substantial new functionality for dealing with potentially nonterminating computations.
One can now destruct a hidden future hypothesis. The result will be a hypothesis that is both later and hidden.
All rules permit using hidden variables in irrelevant positions.
New tactics:
setFold combines set and fold.
typecheckFixpoint establishes the type of a recursive definition
using fixpoint induction.
fixpointInduction employs fixpoint induction to prove properties
of fixpoints.
termination and seqTermination reason about termination.
totality proves termination for inhabitants of total types.
partiality reasons about membership or equality in partial
types.
Tactic changes:
The behavior of revert on hidden hypotheses has changed; it now
generates an intersect conclusion, rather than a squash under an
arrow. The old behavior can be obtained by using squashHidden
first.
revert now works on later and later-hidden hypotheses.
substitution and subst now support substituting for later
hypotheses.
omega no longer unfolds soft constants in its typing
obligations.
refine has moved from Tactic to RefineTactic.
In RuleTactic, the tactics for several rules that involve
projection now take an additional term argument.
New rewrites:
reduceSeqOutpar is like reduceSeq but it wraps the
substitutend with outpar to preserve typeability.Rewriting changes:
When rewriting, the rewriter invokes type inference on the lemma to fill in its evars if possible. This reduces the number of spurious hits the rewrite finds, and makes it less likely that a rewrite will be rejected due to its target having an evar head.
Fixed a bug in the parsing of ShortTargets, which is used for
the targets for rewrites such as reduce.
In Case, goalHypCaseT and goalHypCaseB now take names. The
old versions that take numbers are renamed to goalHypnCaseT and
goalHypnCaseB.
The typechecker can infer types for paths whose head is partial.
The typechecker now uses the constant Partial.strict for
strictness, instead of the underlying A <: partial A.
Library changes:
Sqstable added.
The Bar library is renamed to Eventually, and many of its
components have been renamed. Notably, bar is now ev.
Additional material has been added.
The order of arguments to Weaksum.unpackt has changed. The
syntactic sugar is unchanged. Weaksum.unpackt_simple has been
renamed to Weaksum.unpackt_simple_param and a simpler lemma has
taken its place.
Logic and Weaksum have additional material.
Partial has new material. Partial.total is defined using
dprod instead of exists. A new Partial.fixpoint_induction
has been added, and the old one is renamed to
Partial.fixpoint_formation.
Rule changes:
Added rules intersectfutIntro, futureLeftHidden,
parametricElim', substitutionLater, substitutionLaterSimple,
partialOfExt, fixpointInductionShift, haltsIntro,
haltsUptype, partialElimHalts, seqHalts, appHalts, pi1Halts,
pi2Halts, and prevHalts, activeIte, activeIteSeq,
iteHalts, iteHaltsInv.
Added rules governing parametricfut.
Added totality, strictness, uptype, and admissibility rules for
forallfut, intersectfut, parametric, and parametricfut.
Added convenience rules for inferring types of paths whose head is partial.
Added rules governing predicate admissibility.
Renamed seqBind to seqBindEq, and added seqBindOf.
Renamed type totality rules: for types t, tTotal becomes
tHalts, and tTotal' becomes tTotal.
The strictness rules use the constant Partial.strict instead of
the underlying A <: partial A.
arrowUptype, arrowAdmiss, and dprodStrict now provide a
hypothesis to their second premise.
Changed the extract of letIntro to use a let term.
Rule premises from which the extract is not used unhide all their hypotheses. (Previously this was not true for some left rules.)
Fixed a sound but incomplete bug in unification in which soft constants were not being unrolled sometimes.
Fixed an unsound bug in the letIntro and forallLeft rules that
allowed hidden variables to appear in extracts.
The typechecker deals better with the future modality, and with type inference for polymorphic, higher-order functions.
Old versions of the typechecker can be loaded from
library/typecheck.
File.import uses the search path to find files that are not in the
current directory.
Proof irrelevance is implemented.
Type parametric added.
Weaksum provides an improved interface for union-like types.
The new reduceParam rewrite is like reduce, but also reduces
parametric application.
The new convertIrr rewrite replaces a constant’s irrelevant
arguments.
The chaining tactics so, apply, exploit, and witness
(often) permit using hidden variables in irrelevant arguments.
The definition of abort has been changed to make it proof
irrelevant.
The forallfut and intersectfut types have been added.
New tactics:
assertLater is like assert, but asserts a “later” fact.
setEq' is like setEq but reverses the direction of the
equality.
Rewriting changes:
eqtp can be rewritten through eq.
eeqtp can be rewritten through bar, eq, eeqtp, option,
letnext, list, and weaksum.
Library changes:
The GirardParadox and SmithParadox libraries are no longer
pre-loaded.
Weaksum, Irrelevant, and Quotient added.
The Union library has been deleted, as Weaksum accomplishes
its purposes better. (Union types still exist.)
In Nat, the boolean tests eqb, leqb, ltb, and neqb now
reduce automatically.
Miscellaneous has been renamed to Misc.
Other minor additions.
Basis changes:
Added Path and FileSystem modules.
Use Unix paths consistently.
Added rules assertLater, assertLater', coguardSubIntro,
eeqEeq, eqEeq, guardSubElim, letnextEeq, and
sequalCompatLam. Also added rules governing parametric functions,
irrelevance, and future functions and intersects, and rules
commuting squash and intensional squash with future.
Bug fixes.
New tactics:
remember' is like remember but reverses the direction of the
equality.Tactic changes:
extensionality on set and iset types now produces a squashed
goal.
intro supports the dprod type.
Better error messages from ambiguous inference.
Library changes:
Kindlike added.
FiniteMap library is reorganized and the finite_map type’s
implementation is changed.
Function has changed extensively.
Kind-like lemmas added to FiniteMap, List, and Option.
New operation Namespace.hide prevents constants from being
exported.
Builds on SML/NJ 110.99.7.1.
Added rules setIntroEqSquash and isetIntroEqSquash.