This file was contributed by Carl R. Witty
This file documents the tactics, tacticals, conversions,
conversionals, etc. that are available at the MetaPRL command line
(basically everything that is declared with "topval" in a .mli file).
Notes and caveats: This has undergone only minimal editing. There are
definite style problems. I probably didn't use the correct MetaPRL
terminology. The tactics are documented somewhat unevenly; for some,
I specify exactly what the subgoals are. For others, I just give a
brief description of the effect. I wrote this by reading the source,
with basically no experimentation; it's possible that some of what I
wrote is wrong because I didn't understand what the source was doing.
Parts of this document read like new-user documentation, but I doubt
that the document as a whole would be useful to users who didn't have
experience with tactic-based theorem provers. The document won't help
much if you don't already understand the ITT logic. I should probably
describe the type inference process (and its extensions) in the same
way I discuss other resources.
However, I did set goals for myself that I believe I have met.
1) Every "topval" in Itt_theory is at least mentioned.
2) Every extension to dT, autoT, eqcdT, subtype, and reduceC is
at least mentioned.
3) Everywhere that withT, withTermsT, atT, altT, selT, thinningT, or
withTypeT makes a difference is documented.
----------------------------------------
tacticals:
Tactics apply to the current goal and return a (possibly empty) list
of subgoals. If the subgoal list is empty, the goal has been proved.
Each goal has a goal sequent and a (possibly empty) list of assumption
sequents; the assumptions do not change throughout a proof. The goal
sequent is composed of a conclusion and a list of hypotheses; the
conclusion and the hypotheses are collectively called the clauses of
the goal. Each hypothesis declares a variable.
The goal has a label (a string); this has no semantic meaning, but it
lets tactics communicate with each other about where the goal came
from (which can affect the kind of strategy you would want to use to
prove it).
A goal/subgoal is called "main" if its label is main, upcase,
downcase, basecase, truecase, falsecase, or subterm; "non-main" otherwise.
* refine : tactic -> unit
refine takes a tactic and applies it to the current goal. (Note that
refine is actually a parser keyword; it does not use the normal
function-call syntax.
refine rwh foo 0;;
means
refine (rwh foo 0);;
and not
((refine rwh) foo) 0;;
)
* idT : tactic
The identity tactic; has one subgoal which is the same as the goal.
* cutT : term -> tactic
(cutT t) creates two subgoals. In one, t is the new goal; in the
other, t is an assumption. (So in a sequent-based theory like ITT, t
should be an entire sequent.)
* failT : tactic
A tactic that always fails.
* failWithT : string -> tactic
A tactic that always fails with the given string as its error message.
* nthAssumT : int -> tactic
A tactic that succeeds if the goal sequent matches the given
hypothesis sequent.
* timingT : tactic -> tactic
refine timingT (...)
prints out the time taken for the given tactic application. (timingT
should always be the top-level tactical, as shown above; something
like
refine timingT (...) thenT (...)
will probably not do what you expect.)
* completeT : tactic -> tactic
Runs the argument tactic. If the argument tactic succeeds and
produces subgoals, then completeT fails.
* progressT : tactic -> tactic
Runs the argument tactic. If the argument tactic succeeds and
produces a single subgoal which is the same as the original goal, then
progressT fails.
* whileProgressT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals while there is a progress.
* untilFailT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals until it fails.
* repeatT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals until it fails or no more
progress is made.
* repeatForT : int -> tactic -> tactic
Repeatedly execute the given tactic on all subgoals until the given
maximum depth is reached.
* seqOnSameConclT : tactic list -> tactic
Apply the tactics in the input list in turn on all subgoals until the
conclusion changes.
* orelseT (infix) : tactic -> tactic -> tactic
Apply the first tactic. If it fails, apply the second instead.
* andalsoT, thenT (infix) : tactic -> tactic -> tactic
Apply the first tactic and then the second.
* orthenT (infix) : tactic -> tactic -> tactic
Apply the first tactic and then the second. If one of the tactics
fails, it is ignored; if both fail, the composite tactic fails.
* firstT : tactic list -> tactic
Apply the first non-failing tactic in the list. If they all fail,
fail.
* tryT : tactic -> tactic
Apply the tactic. If it fails, succeed and do nothing.
* thenLT (infix) : tactic -> tactic list -> tactic
Applies the first tactic, which must succeed with a list of subgoals
equal in length to the second argument. It then applies each of the
second argument tactics to the subgoals in turn.
* then_OnFirstT (infix) : tactic -> tactic -> tactic
Apply the first tactic, then apply the second tactic to its first subgoal.
* then_OnLastT (infix) : tactic -> tactic -> tactic
Apply the first tactic, then apply the second tactic on its last subgoal.
* then_OnSameConclT (infix) : tactic -> tactic -> tactic
Apply the first tactic, then apply the second tactic on any subgoals
with the same conclusion.
* addHiddenLabelT : string -> tactic
Create a single subgoal, which is the same as the current goal except
that its label is set to the given string.
* removeHiddenLabelT : string -> tactic
= addHiddenLabelT "main"
* keepingLabelT : tactic -> tactic
Apply the tactic, then set the label of any subgoals to be the same as
the label of the original goal.
* ifLabT : string -> tactic -> tactic -> tactic
If the current goal has the given string as its label, then apply the
first argument tactic; otherwise apply the second argument tactic.
* thenMT (infix) : tactic -> tactic -> tactic
Applies the first tactic, then applies the second tactic to any "main"
subgoals.
* thenMLT (infix) : tactic -> tactic list -> tactic
Applies the first tactic, then pairs up the members of the tactic list
with the "main" subgoals (it is an error if the number of "main"
subgoals is not the same as the length of the tactic list).
* thenAT (infix) : tactic -> tactic -> tactic
Applies the first tactic, then applies the second tactic to non-main
subgoals.
* thenALT (infix) : tactic -> tactic list -> tactic
Applies the first tactic, then pairs up the members of the tactic list
with the "non-main" subgoals (it is an error if the number of "non-main"
subgoals is not the same as the length of the tactic list).
* thenWT (infix) : tactic -> tactic -> tactic
Applies the first tactic, then applies the second tactic to any
subgoals labeled "wf".
* thenET (infix) : tactic -> tactic -> tactic
Applies the first tactic, then applies the second tactic to any
subgoals labeled "equality".
* thenPT (infix) : tactic -> tactic -> tactic
Applies the first tactic, then applies the second tactic to any
subgoals labeled "set predicate", "rewrite subgoal", "assertion", or
"antecedent".
* repeatMT : tactic -> tactic
* whileProgressMT : tactic -> tactic
* untilFailMT : tactic -> tactic
Work the same as repeatT, whileProgressT, untilFailT, repeatForT, but apply the
tactic only to "main" subgoals.
* repeatMForT : int -> tactic -> tactic
Apply the tactic, then apply it recursively to "main" subgoals, to the
given depth.
* seqOnMT : tactic list -> tactic
Apply the first listed tactic, then apply the rest of the tactics in
sequence to "main" subgoals.
* seqT : tactic list -> tactic
Apply the tactics listed in sequence.
* completeMT : tactic -> tactic
Apply the tactic, then fail if any "main" subgoals remain.
* labProgressT : tactic -> tactic
Apply the tactic, then fail if it produces a single subgoal which is
the same as the current goal (and the label is the same).
* onClauseT : int -> (int -> tactic) -> tactic
onClause i tac p = tac i p
* onHypT : int -> (int -> tactic) -> tactic
onHypT = onClauseT
* onConclT : (int -> tactic) -> tactic
onConclT tac = tac 0
* onClausesT : int list -> (int -> tactic) -> tactic
onClausesT lst tac = seqT (List.map tac lst)
* onHypsT = onClausesT
* onMClausesT : int list -> (int -> tactic) -> tactic
as onClausesT, except seqOnMT instead of seqT
* onMHypsT = onMClausesT
* onAllHypsT : (int -> tactic) -> tactic
onAllHypsT = onHypsT [1..n]
where n is the number of hypotheses in the initial goal
* onAllClausesT : (int -> tactic) -> tactic
= onAllHypsT tac thenT onConclT tac
* onAllAssumT : (int -> tactic) -> tactic
= onHypsT [1..n]
where n is the number of assumptions in the initial goal
* tryOnAllHypsT : (int -> tactic) -> tactic
= onAllHypsT (function i -> tryT (tac i))
* tryOnAllClausesT : (int -> tactic) -> tactic
= onAllClausesT (function i -> tryT (tac i))
* onAllMHypsT, onAllMClausesT, onAllMAssumT, tryOnAllMHypsT, tryOnAllMClausesT:
as the above five functions, but using onMHypsT
* onSomeAssumT : (int -> tactic) -> tactic
Tries to apply the argument to [1..n] (where n is the number of
assumptions), taking the first success.
* onSomeHypT : (int -> tactic) -> tactic
Tries to apply the argument to [n..1] (where n is the number of
hypotheses), taking the first success.
* withTermT : string -> term -> tactic -> tactic
* withTypeT : string -> term -> tactic -> tactic
* withBoolT : string -> bool -> tactic -> tactic
* withIntT : string -> int -> tactic -> tactic
Some tactics take optional arguments. Optional arguments are annoying
to express in ML; these functions are one way of doing so. Optional
arguments are passed to a tactic in environments mapping strings to
the argument type. There are separate environments for terms, lists
of terms, types (which are also terms), ints, bools, and strings
(plus some that are internal implementation details). Each of the
above functions adds to the appropriate environment.
* withTermsT : term list -> tactic -> tactic
= withTermsListT "with"
(Note that withTermsListT is not exported to the standard toploop; it
acts the same as the functions described in the above paragraph.)
* withT : term -> tactic -> tactic
withT t = withTermsT [t]
* atT : term -> tactic -> tactic
= withTypeT "univ"
* selT : int -> tactic -> tactic
= withIntT "sel"
* altT : tactic -> tactic
= withBoolT "alt" true
* thinningT : bool -> tactic -> tactic
= withBoolT "thin"
* doNotThinT : tactic -> tactic
= thinningT false
* nameHypT : int -> string -> tactic
Renames bound variable for a hypothesis
* nameHypsT : (int list) -> (string list) -> tactic
Renames bound variables for hypotheses
----------------------------------------
conversionals:
A conversion is applied at some particular address within a sequent.
It tries to rewrite the term at that point.
* rw : conv -> int -> tactic
Applies the given conversion to the sequent clause named by the int
argument.
* rwc : conv -> int -> int -> tactic
(rwc conv assump clause) applies the conversion to the given clause of
the given assumption.
* rwAll : conv -> tactic
Applies the conversion to all clauses of the goal sequent.
* rwcAll : conv -> int -> tactic
Applies the conversion to all clauses of the givem assumptiom.
* rwAllAll : conv -> tactic
Applies the conversion to all clauses of all assumption and to the goal
sequent.
* rwh, rwch, rwhAll, rwchAll, rwhAllAll are the same as
rw, rwc, rwAll, rwcAll, rwAllAll, but use (higherC conv).
* rwa, rwca, rwaAll, rwcaAll, rwaAllAll are the same as
rw, rwc, rwAll, rwcAll, rwAllAll, but have (conv list) as an argument
and use (applyAllC convs) instead of conv.
* thenC (infix) : conv -> conv -> conv
Apply the first conversion and then the second.
* orelseC (infix) : conv -> conv -> conv
Apply the first conversion. If it fails, apply the second instead.
* addrC : int list -> conv -> conv
Apply the conversion at the specified address. An address is a list
of ints; the address [0; 1; 2] refers to the third subterm of the
second subterm of the first subterm of the current term.
* clauseC : int -> conv -> conv
(clauseC clause conv) takes the given conversion and applies it to the
given clause. You probably only want to use this with rw;
(rwh (clauseC 1 conv) 0) would do something like apply conv at each
position in the first hypothesis which exists in the conclusion.
* idC : conv
Does nothing.
* foldC : term -> conv -> conv
foldC t c replaces the current subterm by t, if c can convert t to the
current subterm. Otherwise, it fails.
* makeFoldC : term -> conv -> conv
As foldC, but doesn't work on all conversions. However, when it
does work, it's more efficient than foldC.
* cutC : term -> conv
Replaces the current subterm with the argument term. Creates a
"rewrite" subgoal.
* rewriteC : term
rewriteC <<'a ~ 'b>> substitutes 'a for 'b and produces the additional subgoal: a~b.
* failC : string -> conv
Fails with the given string as an error message.
* tryC : conv -> conv
Tries to apply the given conversion. If it fails, succeed and do
nothing.
* progressC : conv -> conv
Runs the argument conv. Fails if it does not make any progress.
* someSubC : conv -> conv
Applies the conversion to the first subterm of the current term on
which it succeeds. Fails if the conversion fails on all subterms.
(Here I mean "exact subterm" rather than "recursive subterm".)
* allSubC : conv -> conv
Applies the conversion to every subterm of the current term; fails if
any of them fail. (Again, this is "exact subterm".)
* allSubThenC : conv -> conv -> conv
(allSubThenC c1 c2) tries to apply c1 to every exact subterm. If it succeed in
at least one case then applies c2.
* higherC : conv -> conv
Apply the conversion to outermost terms.
* lowerC : conv -> conv
Apply the conversion to the leftmost, innermost term to which it
applies. If the conversion applies nowhere, fail.
* sweepUpC : conv -> conv
Apply the conversion to all terms possible from innermost to
outermost.
* sweepDnC : conv -> conv
Apply the conversion to all terms possible from outermost to
innermost.
* firstC : conv list -> conv
Apply the first conversion from the list that succeeds.
* applyAllC : conv list -> conv
= sweepUpC (firstC convs)
Apply all conversions to all terms possible from outermost to
innermost (it does not apply conversions recursively).
* untilFailC : conv -> conv
Apply the conversion repeatedly until it fails.
* whileProgressC : conv -> conv
Apply the conversion repeatedly until it makes no change
(returns a term alpha-equivalent to the term it was applied to).
Will fail if conv fails on one of the iterations.
* repeatC : conv -> conv
Apply the conversion until it either fails or makes no change.
* repeatForC : int -> conv -> conv
repeatForC n c applies c n times.
* ifEqualC : term -> conv -> conv -> conv
Apply the first conversion if the term its applied to is alpha equal to term and
the other conversion otherwise.
* replaceUsingC : term -> conv -> conv
replaceUsingC t c = ifEqualC t c failC -- replace a term t using conv c.
* reduceTopC : conv
Tries to "reduce" the current term. This is a resource-based
conversion. It looks up the current term to determine the correct
conversion to apply.
* reduceC : conv
= repeatC (higherC reduceTopC)
* reduceT : tactic
= rwAll reduceC - reduces the goal sequent
----------------------------------------
dtactic:
* dT : int -> tactic
Tries to "destruct" the given sequent clause. This is a
resource-based tactic. It looks at the form of the clause to
determine the correct tactic to apply.
(dT 0) is part of the autoT tactic.
(dT n) will sometimes delete the n'th hypothesis after it has applied
the rule. If this is the case, the description of the effect will end
with "and thins"; you can avoid this deletion with
(thinningT false (dT n)).
* dForT : int -> tactic
Applies (dT 0) the given number of times on "main" subgoals.
----------------------------------------
auto_tactic:
* nthHypT : int -> tactic
This is a simple resource-driven tactic that is supposed to finish the proof
when the conclusion is "similar enough" to the given hypothesis. For example,
in type theory if i'th hypothesis is << x: 'A >>, and the conclusion is << 'A >>,
<< 'x in 'A >> or << 'A Type >>, then (nthHypT i) succeeds with no subgoals.
Auto family of tactics perform resource-based automated reasoning.
They apply all the all the available tactics in turn, until none of
them succeed:
* trivialT : tactic
Applies AutoTrivial tactics. Normally AutoTrivial tactics (and
consequentally the trivialT itself) do not produce suggoals when
successfull. "onSomeHypT nthHypT" is one of the AutoTrivial tactics.
* weakAutoT : tactic (not exported, use autoT instead)
Applies AutoTrivial and AutoNormal tactics
* strongAutoT : tactic
Applies AutoTrivial, AutoNormal and AutoComplete tactics
* tcaT : tactic
Equivalent to "tryT (completeT strongAutoT)"
* autoT : tactic
Equivalent to "weakAutoT thenT tcaT". In other words, it first applies
AutoTrivial and AutoNormal and then it starts applying all awailable
tactics (includeing AutoComplete ones), but falls back it this fails
to completely prove the subgoal.
* tryAutoT : tactic -> tactic
tryAutoT tac is equivalent to tac thenT tcaT. Note that one can use a
macro "tac ttca" instead of "tryAutoT tac".
* byDefT : conv -> tactic
Applies conv everywhere, then runs autoT.
* repeatWithRwsT : conv list -> tactic -> tactic
Tries to apply some conversional from the @i{convs} list to the goal
and in case of a progress applies the tactic @i{tac},
then repeats it as far as possible.
----------------------------------------
base_rewrite:
* d_rewrite_axiomT : int -> tactic
If the argument is 0, this solves a goal with a conclusion of the form
<< "rewrite"{'x; 'x} >>. It is part of the trivialT tactic.
* rewriteT : term -> tactic
(rewriteT << "rewrite"{'a; 'b} >>) changes occurrences of << 'a >> in
the conclusion to << 'b >>. If you want to substitute for some but
not all occurrences of << 'a >>, you can wrap the tactic in
(withT << bind{x. 'C['x]} >> ...), where the conclusion must be
<< 'C['a] >>.
----------------------------------------
itt_equal:
new terms:
"type"{'a}
univ[i:l]
equal{'T; 'a; 'b}
"true"
"false"
cumulativity[i:l, j:l]
Input shortcuts:
('x = 'y in 'T) = equal{'T; 'x; 'y}
('x IN 'T) = equal{'T; 'x; 'x}
Notice that "in" has to be lowercase in the first case and uppercase in the
second one.
* reduce_cumulativity: conv
Rewrites a term of the form << cumulativity[i:l, j:l] >> to "true" (if
i>. This is a resource-based tactic. It looks at
the form of 'a to determine the correct tactic to apply.
In its initial state, it can handle
<< univ[j:l] = univ[j:l] in univ[i:l] >> and
<< it = it in ('a = 'b in 'T) >>.
* typeAssertT : tactic
Deduces << "type"{'T} >> from << 'T >>.
* equalAssumT : int -> tactic
(equalAssumT i) deduces << 'x = 'x in 'T >> if << 'x: 'T >> is the i'th
hypothesis.
* equalRefT : term -> tactic
(equalRefT t) changes the goal from << 'x = 'x in 'T >> to
<< 'x = t in 'T >>.
* equalSymT : tactic
equalSymT changes the goal from << 'x = 'y in 'T >> to
<< 'y = 'x in 'T >>.
* equalTransT : term -> tactic
(equalTransT t) splits a goal << 'x = 'y in 'T >> into two subgoals,
<< 'x = t in 'T >> and << t = 'y in 'T >>.
* equalTypeT : term -> term -> tactic
(equalTypeT a b) changes the goal from << "type"{'T} >> to
<< 'a = 'b in 'T >>.
* univTypeT : term -> tactic
(univTypeT t) changes the goal from << "type"{'x} >> to
<< 'x = 'x in t >> (t must be of the form << univ[i:l] >>).
* univAssumT : int -> tactic
(univAssumT i) deduces << "type"{'x} >> if the i'th hypothesis is
<< x: univ[i:l] >>.
* cumulativityT : term -> tactic
(cumulativityT << univ[j:l] >>) changes the goal from
<< 'x = 'y in univ[i:l] >> to << 'x = 'y in univ[j:l] >>, if the
universe level j is less than the universe level i.
This file adds to the dT tactic:
If the conclusion is of the form << "true" >>,
(dT 0) solves it with no subgoals. (This is not the same << "true" >>
defined in Itt_logic.)
If the conclusion is of the form
<< ('a1 = 'b1 in 'T1) = ('a2 = 'b2 in 'T2) in univ[i:l] >>,
(dT 0) creates 3 equality subgoals.
If the conclusion is of the form << "type"{. 'a = 'b in 'T } >>,
(dT 0) creates 2 membership subgoals.
If the conclusion is of the form << "type"{. 'a IN 'T } >>,
(dT 0) creates one membership subgoal.
(note: until the precedences in term tables are implemented correctly,
the previous dT addition may take precedence over this one)
If the conclusion is of the form << it IN ('a = 'b in 'T) >>,
(dT 0) creates one equality subgoal.
If the n'th hypothesis is of the form << x: 'a = 'b in 'T >>,
(dT n) replaces << x >> with << it >> in the rest of the sequent.
If the conclusion is of the form << univ[i:l] IN univ[j:l] >>,
(dT 0) reduces it to a cumulativity subgoal and tries to prove this
subgoal.
If the conclusion is of the form << "type"{univ[l:l]} >>,
(dT 0) solves it with no subgoals.
This file adds to the trivalT tactic:
trivialT can solve goals with a conclusion of the form
<< 'x IN 'T >> if there is a hypothesis << x: 'T >>,
or goals with a conclusion of the form << "type"{'x} >>
if there is a hypothesis << x: univ[i:l] >>.
trivialT can use equalRefT and equalSymT to match an
equality conclusion against an equality hypothesis.
----------------------------------------
itt_struct:
new terms:
bind{x. 'T['x]} (Note that this is only used for syntactic purposes;
it has no semantic meaning.)
* thinT : int -> tactic
If the i'th hypothesis is << x: 'A >>, and x does not appear free in
the rest of the sequent, then (thinT i) deletes the hypothesis.
* thinAllT : int -> int -> tactic
(thinAllT i j) deletes the hypotheses numbered i through j
(inclusive).
* nthAssumT : int -> tactic
Matches the current goal against an assumption, doing thinning and
squashing/unsquashing if necessary.
* assertT : term -> tactic
(assertT t) creates two subgoals; one where << t >> is the conclusion,
and one which adds << x: t >> as a new hypothesis (at the end of the
hypothesis list).
* assertAtT : int -> term -> tactic
As assertT, but lets you specify where the new hypothesis is to be
added.
* moveHypT : int -> int -> tactic
Moves i'th hypothesis to j'th place in a sequent.
* copyHypT : int -> int -> tactic
Copies i'th hypothesis to j'th place in a sequent.
* splitHypT : int -> int -> tactic
Works as copyHypT, but conclusion and hypotheses after j will depend
on a new copy of the hypothesis (useful for elimination
rules where we want to keep the original hypothesis intact).
* tryAssertT : term -> tactic -> tactic -> tactic
Runs assertT, then runs the two tactics on the two subgoals
correspondingly. Hoewever, if the goal already has the right
conslusion, it will only run the first tactic.
* dupT : tactic
Creates two subgoals, both the same as the current goal. (This might
be useful for performance testing or debugging; it is useless in a
normal proof.)
* useWitnessT : term -> tactic
(useWitnessT t) changes a conclusion << 'T >> into
<< t = t in 'T >>.
* substT : term -> int -> tactic
(substT << 'a = 'b in 'T >> n) substitutes << 'b >> for << 'a >> in
the n'th clause of the sequent, creating several subgoals. If you
want to substitute for some but not all occurrences of a, you can wrap
the tactic in (withT << bind{x. 'B['x]} >> ...), where the n'th clause
must be << 'B['a] >>.
* hypSubstT : int -> int -> tactic
(hypSubsT j n) is like (substT ... n) where the equality comes from
the j'th hypothesis (so you don't need to prove the equality as one of
the subgoals). (You can still use withT to specify which occurrences
to substitute.)
* revHypSubstT : int -> int -> tactic
Like hypSubstT, but substitutes in the other direction.
* replaceHypT : term -> int -> tactic
(atT << univ[i:l] >> (replaceHypT t i)) changes the i'th hypothesis
from << x: 'A >> to << x: t >>, and adds an extra subgoal
<< 'A = t in univ[i:l] >>.
* equalTypeT : term -> term -> tactic
Replaces a goal << "type"{'T} >> with << 'a = 'b in 'T >>
* memberTypeT : term -> tactic
Replaces a goal << "type"{'T} >> with << 'a IN 'T>> then tries to
prove it using tcaT
This file adds to the trivialT tactic.
- trivialT can solve goals with a hypothesis << x: 'A >> and a goal
<< 'A >>.
- trivialT will use the improved nthAssumT to match the goal against an
assumption.
- trivialT will prove goals of the form << "type"{'A} >> from an assumption
<< 't1 = 't2 in 'A >> provided in can thin things to get the exact match
between the hypotheses of the goal and the hypotheses of the assumption.
----------------------------------------
itt_struct2:
* combineT m n
Combines m hypothesis starting from the n-th one into a product of them.
For example when apply combineT 3 2 to sequent << ; x:A; y:B; z:C; >- T >> we get
<< ; p: A*B*C; >- T >> and some well-formedness subgoals.
* separateT m n
Is opposite to the combineT tactic.
* varElimT n
Eliminates a variable x using the equality in the n$th$ hypothesis x=t in A or
t=x in A, if A is a sqsimple type.
This tactic is opposite to the letT tactic.
* allVarElimT
Eliminates all possible variables.
----------------------------------------
itt_squash:
new term:
squash{'A}
Based on a squash resource:
* squashT : tactic
Squashes the conclusion terms
* unsquashT : int -> tactic
Unsquashes the hypothesys
* unsquashAllT : tactic
Tries unsquashing all the hypotheses.
* sqsquashT : tactic
Squashed the sequent argument
* unsqsquashT : term -> tactic
If the current goal sequent is squashed, replaces the sequent argument
with the given term.
This theory adds to dT tactic:
If the conclusion is of the form <>,
(dT 0) reduces it to << 'A1 = 'A2 in univ[i:l] >>
If the conclusion is of the form << "type"{.squash{'A}} >>,
(dT 0) reduces it to << "type"{'A} >>
If the conclusion is of the form << squash{'A} >>,
(dT 0) will replace if with just <<'A>> (this rule is only added to
strongAuto).
If the conclusion is of the form << it IN squash{'A} >>,
(dT 0) will replace it with << squash{'A} >>
If the hypothesis i is of the form << squash{'A} >>,
(dT i) is equivalent to (unsquashT i)
This theory adds to autoT:
autoT will attempt to run unsquashAllT and sqsquashT thus unsquashing
all the hypothesis and squashing the goal sequent whenever possible.
----------------------------------------
itt_subtype:
new terms:
subtype{'A; 'B}
* subtypeT : term -> tactic
subtypeT <> replaces a conclusion of the form <> with
<> and conclusion of any other form <**> with just
<****> and generates an "aux" subgoal of the form <>.
* type_subtype_leftT: term -> tactic
* type_subtype_rightT : term -> tactic
type_subtype_leftT t will replace a conclusion of the form
<< "type"{'B} >> with the conclusion << subtype{t, 'B} >>.
Similarly, type_subtype_rightT t replaces << "type"{'A} >>
with << subtype{'A; t} >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< subtype{'A1; 'B1} = subtype{'A2; 'B2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{subtype{'A; 'B}} >>,
(dT 0) creates two subgoals, with conclusions << "type"{'A} >>
and << "type"{'B} >>.
If the conclusion is of the form << subtype{'A; 'B} >>,
(dT 0) tries to prove it using the sub_resource (note: as of
2001.07.22 sub_resource is never really used). If that fails,
it creates two subgoals. One (marked "wf") has a conclusion of
<< "type"{'A} >>; the other (marked "main") is of the form
<< x: 'A >- 'x IN 'B >>.
If the n'th hypothesis is of the form << x: subtype{'A; 'B} >>,
(dT n) replaces << 'x >> with << it >> in the rest of the sequent.
(withT t (dT n)) creates two subgoals.
The first has a conclusion of << t IN 'A >>. The
second has an extra hypothesis, << y: t IN 'B >>.
* bySubtypeT : int -> tactic
proves that x:A .. >- x in B form A subtype B
----------------------------------------
itt_void:
new terms:
void
* squash_voidT : tactic
Changes the goal to be a "squash" sequent if the conclusion is of the
form << void >>. This is part of the squashT tactic.
This file adds to the dT tactic:
If the conclusion is of the form << void IN univ[i:l] >>,
(dT 0) succeeds with no subgoals.
If the conclusion is of the form << "type"{void} >>, then
(dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << x: void >>, then
(dT n) succeeds with no subgoals.
This file adds to the subtypeT tactic.
subtypeT proves << void >> is a subtype of every type directly.
----------------------------------------
itt_rfun:
new terms:
"fun"{'A; x. 'B['x]}
rfun{'A; f, x. 'B['f; 'x]}
lambda{x. 'b['x]}
apply{'f; 'a}
well_founded{'A; x, y. 'R['x; 'y]}
well_founded_assum{'A; a1, a2. 'R['a1; 'a2]; 'P}
well_founded_prop{'A}
well_founded_apply{'P; 'a}
fix{f. 'b['f]}
Here, << well_founded{'A; x, y. 'R['x; 'y]} >> has the standard
meaning: over a type << 'A >>, the relation << 'R['x; 'y] >> is
well-founded (has no infinite descending chains). You can think of
<< well_founded_prop{'A} >> as being like the power set of << 'A >>;
any member of << well_founded_prop{'A} >> acts like a subset of
<< 'A >>. (There is a standard notion which is similar to this, where
<< 'A -> univ[i:l] >> acts like the power set of << 'A >>. That's not
suitable for use in the well-foundedness definition, because it forces
you to pick a universe level.) If << 'P >> is a member of
<< well_founded_prop{'A} >>, you can test whether a member << 'a >> of
<< 'A >> is in << 'P >> with << well_founded_apply{'P; 'a} >>.
Finally, << well_founded_assum{'A; x, y. 'R['x; 'y]; 'P} >> holds if
whenever all the << 'R >>-predecessors of an element are in << 'P >>,
that element is in << 'P >>. A partial order << 'R >> is well-founded
over a type << 'A >> iff
<< well_founded_assum{'A; x, y. 'R['x; 'y]; 'P} >> implies that every
member of << 'A >> is in << 'P >>.
* reduce_beta : conv
Rewrites << lambda{v. 'b['v]} 'a >> to << 'b['a] >>.
* reduce_fix : conv
Rewrites << fix{f. 'b['f]} >> to << 'b[fix{f. 'b['f]}] >>.
* rfunction_extensionalityT : term -> term -> tactic
(rfunction_extensionalityT t1 t2) applies to a goal of the form
<< 'f1 = 'f2 in { g | x:'A -> 'B['g; 'x] } >>. It takes two terms
giving types of the form << { g1 | x1:'A1 -> 'B1['g1; 'x1] } >>
for << 'f1 >> and << 'f2 >> respectively. It creates subgoals
to verify that << 'f1 >> and << 'f2 >> really are of the respective
types, that the type << { g | x:'A -> 'B['g; 'x] } >> is well-formed,
and that << 'f1 >> and << 'f2 >> are extensionally equal.
This file adds to the dT tactic.
If the n'th hypothesis is of the form
<< p: well_founded_assum{'A; a1, a2. 'R['a1; 'a2]; 'P} >>,
(withT a (dT n)) creates 3 subgoals and thins. Two of the subgoals
say that a is a member of << 'A >> and that every << 'R >>-predecessor
of a is in << 'P >>. The third subgoal has an extra hypothesis which
says that a is in << 'P >>.
If the conclusion is of the form << well_founded{'A; a, b. 'R['a; 'b]} >>,
(dT 0) creates 2 well-formedness subgoals and 4 main subgoals. Three
of the main subgoals say that << 'R >> is irreflexive, antisymmetric
(is that the right term?), and transitive. The fourth says that if
you know << well_founded_assum{'A; a2, a3. 'R['a2; 'a3]; 'P} >> then
every member of << 'A >> is in << 'P >>.
If the conclusion is of the form
<< well_founded_apply{'P; 'a} IN univ[i:l] >>,
(withT t (dT 0)) creates 3 membership subgoals. Here t must be the
type of << 'a >>.
If the conclusion is of the form
<< { f1 | a1:'A1 -> 'B1['f1; 'a1] }
= { f2 | a2:'A2 -> 'B2['f2; 'a2] }
in univ[i:l] >>,
<< "type"{. { f | a:'A -> 'B['f; 'a] } } >>, or
<< { f | x:'A -> 'B['f; 'x] } >>,
(withT r (dT 0)) creates 3 subgoals. (The argument r, which gives the
well-founded relation validating the rfun types, must be of the
form << lambda{a. lambda{b. 'R['a; 'b]}} >>.)
If the conclusion is of the form
<< lambda{x1. 'b1['x1]}
= lambda{x2. 'b2['x2]}
in { f | x: 'A -> 'B['f; 'x] } >>,
(dT 0) creates 2 subgoals.
If the n'th hypothesis is of the form
<< f: { g | x:'A -> 'B['g; 'x] } >>,
(withT a (dT n)) adds hypotheses giving the type of << 'f a >> (and
another goal with conclusion << a IN 'A >>).
If the conclusion is of the form
<< subtype{.{ f1 | x1: 'A1 -> 'B1['f1; 'x1] };
.{ f2 | x2: 'A2 -> 'B2['f2; 'x2] } } >>,
(withT r (dT 0)) creates 5 subgoals. (The argument r, which gives the
well-founded relation validating the rfun types, must be of the
form << lambda{a. lambda{b. 'R['a; 'b]}} >>.)
This file adds to the eqcdT tactic.
eqcdT can handle conclusions of the form
<< rfun{'A; f, x. 'B['f; 'x]} = rfun{'A2; f2, x2. 'B2['f2; 'x2]} in univ[i:l] >>
(although it must be wrapped in a withT giving a well-order relation
of the form << lambda{a. lambda{b. 'R['a; 'b]}} >>).
eqcdT can also handle conclusions of the form
<< lambda{x1. 'b1['x1]} = lambda{x2. 'b2['x2]} in { f | x: 'A -> 'B['f; 'x] } >>.
eqcdT can also handle conclusions of the form
<< 'f1 'a1 = 'f2 'a2 in 'B['f1; 'a1] >> (although it must be wrapped
in a withT giving the type of << 'f1 >> in the form
<< ({ f | x:'A -> 'B['f; 'x] }) >>).
This file adds to the reduceTopC conversion.
It adds the reduce_beta and reduce_fix conversions.
----------------------------------------
itt_dfun:
* reduceEta : term -> conv
Rewrites << lambda{x. 'f 'x} >> to << 'f >>, under the condition
<< 'f = 'f in (x: 'A -> 'B['x]) >>. Takes << x: 'A -> 'B['x] >> as an
argument.
* unfold_dfun : conv
Rewrites << (x: 'A -> 'B['x]) >> to << ({ f | x: 'A -> 'B['x] }) >>.
* dfun_extensionalityT : term -> term -> tactic
(dfun_extensionalityT t1 t2) applies to a goal of the form
<< 'f = 'g in x:'A -> 'B['x] >>. It takes two terms giving types of
the form << y:'C -> 'D['y] >> for << 'f >> and << 'g >> respectively.
It creates subgoals to verify that << 'f >> and << 'g >> really are of
the respective types, that the type << x:'A -> 'B['x] >> is
well-formed, and that << 'f >> and << 'g >> are extensionally equal.
This file adds to the dT tactic.
If the conclusion is of the form << well_founded{'A; a1, a2. void} >>,
(dT 0) reduces it to << "type"{'A} >>.
If the conclusion is of the form
<< (a1:'A1 -> 'B1['a1]) = (a2:'A2 -> 'B2['a2]) in univ[i:l] >>,
(dT 0) reduces it to 2 equality subgoals.
If the conclusion is of the form
<< "type"{. a1:'A1 -> 'B1['a1] } >>,
(dT 0) reduces it to 2 typehood subgoals.
If the conclusion is of the form << a:'A -> 'B['a] >>,
(dT 0) reduces it to << z: 'A >- 'B['z] >> (and an extra
well-formedness subgoal).
If the conclusion is of the form
<< lambda{a1. 'b1['a1]} = lambda{a2. 'b2['a2]} in a:'A -> 'B['a] >>,
(dT 0) reduces it to << x: 'A >- 'b1['x] = 'b2['x] in 'B['x] >>
(and an extra well-formedness subgoal).
If the n'th hypothesis is of the form << f: x:'A -> 'B['x] >>,
(withT a (dT n)) adds new hypotheses indicating the type of
<< 'f a >>, and creates a new subgoal << 'a IN 'A >>.
If the conclusion is of the form
<< subtype{ (a1:'A1 -> 'B1['a1]); (a2:'A2 -> 'B2['a2]) } >>,
(dT 0) creates 2 subtype subgoals, with contravariant argument
and covariant return types.
This file adds to the eqcdT tactic.
eqcdT can handle conclusions of the form
<< (x1:'A1 -> 'B1['x1]) = (x2:'A2 -> 'B2['x2]) in univ[i:l] >>.
This file adds to the subtypeT tactic.
subtypeT proves that << a1:'A1 -> 'B1['a1] >> is a subtype of
<< a2:'A2 -> 'B2['a2] >> by proving << 'B1['a] >> is a subtype of
<< 'B2['a] >> and << 'A2 >> is a subtype of << 'A1 >>.
----------------------------------------
itt_fun:
* reduceIndependentEta : term -> conv
Rewrites << lambda{x. 'f 'x} >> to << 'f >>, under the condition
<< 'f = 'f in ('A -> 'B) >>. Takes << 'A -> 'B >> as an argument.
* unfold_fun : conv
Rewrites << 'A -> 'B >> to << x: 'A -> 'B >>.
* fnExtensionalityT : term -> term -> tactic
Reduces a goal of the form << 'f = 'g in fun >> (where fun is either
a function type, or a dependent funtion type, or a very dependent
fuction type), to proving that 'f and 'g return equal results for
equal arguments. The term arguments for fnExtensionalityT should
be the types of 'f and 'g respectively. The term arguments should be
function types of the same ``dependency level'' as << fun >>
* fnExtenT : term -> tactic
fnExtenT t = fnExtensionalityT t t. Calling fnExtenT << fun >> is useful
when proving goals of the form << 'f in fun' >> in case it is easier to
show that << 'f >> is in << fun >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< ('A1 -> 'B1) = ('A2 -> 'B2) in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{. 'A1 -> 'B1 } >>,
(dT 0) changes it to << x: 'A1 >- "type"{'B1} >> (and adds an extra
well-formedness subgoal).
If the conclusion is of the form << 'A -> 'B >>,
(dT 0) changes it to << z: 'A >- 'B >> (and adds an extra
well-formedness subgoal).
If the conclusion is of the form
<< lambda{a1. 'b1['a1]} = lambda{a2. 'b2['a2]} in 'A -> 'B >>,
(dT 0) changes it to << x: 'A >- 'b1['x] = 'b2['x] in 'B >> (and adds
an extra well-formedness subgoal).
If the conclusion is of the form << 'f1 'a1 = 'f2 'a2 in 'T >>,
(withT t (dT 0)) converts it to 2 equality subgoals, checking that
<< 'f1 >> equals << 'f2 >> and << 'a1 >> equals << 'a2 >>. The
argument t must be the type of << 'f1 >> and << 'f2 >>, and it must be
of one of the forms << { f | x:'A -> 'B['f; 'x] } >>,
<< x:'A -> 'B['x] >>, or << 'A -> 'B >>. Without the withT wrapper,
(dT 0) tries to infer the type of << 'f1 >>.
XXX
If the conclusion is of the form << "type"{('f 'a)} >>,
(withT t (dT 0)) first checks that t is of the form << 'A -> univ[i:l] >>
or << x: 'A -> univ[i:l] >>. It then changes the conclusion to
<< ('f 'a) IN univ[i:l] >> and applies (withT t eqcdT) (which
fails miserably). If t is not given, it attempts to infer the type of
<< 'f >>.
If the n'th hypothesis is of the form << f: ('A -> 'B) >>,
(withT a (dT n)) adds hypotheses giving the type of << 'f a >>, and
adds a new subgoal << a IN 'A >>. (dT n) (without being wrapped
by withT) adds a new hypothesis of type << 'B >> and adds a new
subgoal << 'A >>.
This file adds to the eqcdT tactic.
eqcdT can handle conclusions of the form
<< ('A1 -> 'B1) = ('A2 -> 'B2) in univ[i:l] >>.
eqcdT can also handle conclusions of the form
<< lambda{x1. 'b1['x1]} = lambda{x2. 'b2['x2]} in ('A -> 'B) >>.
This file adds to the subtypeT tactic.
subtypeT proves that << 'A1 -> 'B1 >> is a subtype of
<< 'A2 -> 'B2 >> by proving << 'B1 >> is a subtype of << 'B2 >>
and << 'A2 >> is a subtype of << 'A1 >>.
----------------------------------------
itt_dprod:
new terms:
prod{'A; x. 'B['x]}
pair{'a; 'b}
spread{'e; u, v. 'b['u; 'v]}
fst{'e}
snd{'e}
* reduceSpread : conv
Rewrites << spread{'u, 'v; a, b. 'c['a; 'b]} >> to << 'c['u; 'v] >>.
* unfoldFst : conv
Rewrites << fst{'e} >> to << spread{'e; u, v. 'u} >>.
* unfoldSnd : conv
Rewrites << snd{'e} >> to << spread{'e; u, v. 'v} >>.
* reduceFst : conv
Rewrites << fst{pair{'a; 'b}} >> to << 'a >>.
* reduceSnd : conv
Rewrites << snd{pair{'a; 'b}} >> to << 'b >>.
This file adds to the reduceTopC conversion.
It adds the reduceSpread, reduceFst, and reduceSnd conversions.
This file adds to the dT tactic.
If the conclusion is of the form
<< x1:'A1 * 'B1['x1] = x2:'A2 * 'B2['x2] in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form
<< "type"{.y:'A1 * 'A2['y]} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << x:'A * 'B['x] >>,
(withT a (dT 0)) creates subgoals << a IN 'A >> and << 'B[a] >>
(and an extra well-formedness subgoal).
If the conclusion is of the form
<< ('a1, 'b1) = ('a2, 'b2) in x:'A * 'B['x] >>,
(dT 0) creates 2 equality subgoals and one well-formedness subgoal.
If the n'th hypothesis is of the form << z: x:'A * 'B['x] >>,
(dT n) creates one subgoal with extra hypotheses
<< u: 'A; v: 'B['u] >>, changes << 'z >> to << 'u, 'v >> in the rest
of the sequent, and thins.
If the conclusion is of the form
<< spread{'e1; u1, v1. 'b1['u1; 'v1]} =
spread{'e2; u2, v2. 'b2['u2; 'v2]} in 'T >>
(withT t (dT 0)) creates 2 equality subgoals. Here, t must be
the type of << 'e1 >> and << 'e2 >>, and it must be of the form
<< w:'A * 'B['w] >>. Without the withT wrapper, (dT 0) will try
to infer the type of << 'e1 >>. You can also use
(withTermsT [<< bind{x. 'B['x]} >>; t] (dT 0)). In this case, t
is as above, and it must be the case that << 'T >> is << 'B['e1] >>.
If the conclusion is of the form
<< subtype{ (a1:'A1 * 'B1['a1]); (a2:'A2 * 'B2['a2]) } >>,
(dT 0) creates 2 subtype goals.
XXX
This file adds to the subtypeT tactic.
subtypeT would prove (except for a copy-and-paste bug) that
<< x1:'A1 * 'B1['x1] >> is a subtype of << x2:'A2 * 'B2['x2] >>
by proving << 'A1 >> is a subtype of << 'A2 >> and << 'B1['x] >> is a
subtype of << 'B2['x] >>.
----------------------------------------
itt_prod:
* unfoldProd : conv
Rewrites << ('A * 'B) >> to << (x:'A * 'B) >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< 'A1 * 'B1 = 'A2 * 'B2 in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{.'A1 * 'A2} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << 'A * 'B >>,
(dT 0) creates subgoals << 'A >> and << 'B >>.
If the n'th hypothesis is of the form << z: 'A * 'B >>,
(dT n) adds extra hypotheses << u: 'A; v: 'B >>, changes << 'z >> to
<< 'u, 'v >> in the rest of the sequent, and thins.
If the conclusion is of the form
<< ('a1, 'b1) = ('a2, 'b2) in 'A * 'B >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form
<< subtype{ ('A1 * 'B1); ('A2 * 'B2) } >>,
(dT 0) creates 2 subtype goals.
This file adds to the eqcdT tactic.
eqcdT can handle conclusions of the forms
<< ('A1 * 'B1) = ('A2 * 'B2) in univ[i:l] >> and
<< ('a1, 'b1) = ('a2, 'b2) in ('A * 'B) >>.
This file adds to the subtypeT tactic.
subtypeT proves that << 'A1 * 'B1 >> is a subtype of << 'A2 * 'B2 >>
by proving << 'A1 >> is a subtype of << 'A2 >> and << 'B1 >> is a
subtype of << 'B2 >>.
----------------------------------------
itt_union:
new terms:
union{'A; 'B}
inl{'x}
inr{'x}
decide{'x; y. 'a['y]; z. 'b['z]}
* reduceDecideInl : conv
Rewrites << decide{inl{'x}; u. 'l['u]; v. 'r['v]} >> to << 'l['x] >>.
* reduceDecideInr : conv
Rewrites << decide{inr{'x}; u. 'l['u]; v. 'r['v]} >> to << 'r['x] >>.
This file adds to the reduceTopC conversion.
It adds the reduceDecideInl and reduceDecideInr conversions.
This file adds to the dT tactic.
If the conclusion is of the form << 'A1 + 'B1 = 'A2 + 'B2 in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << 'A + 'B >>,
(selT 1 (dT 0)) creates subgoals << 'A >> and << "type"{'B} >>.
(selT 2 (dT 0)) creates subgoals << 'B >> and << "type"{'A} >>.
If the conclusion is of the form << inl{'a1} = inl{'a2} in 'A + 'B >>,
(dT 0) creates subgoals << 'a1 = 'a2 in 'A >> and << "type"{'B} >>.
If the conclusion is of the form << inr{'b1} = inr{'b2} in 'A + 'B >>,
(dT 0) creates subgoals << 'b1 = 'b2 in 'B >> and << "type"{'A} >>.
If the n'th hypothesis is of the form << x: 'A + 'B >>,
(dT n) creates 2 subgoals and thins. One has an extra hypothesis
<< u: 'A >>, and replaces << 'x >> by << inl{'u} >> in the rest of the
sequent. The other has an extra hypothesis << v: 'B >>, and replaces
<< 'x >> by << inr{'v} >> in the rest of the sequent.
If the conclusion is of the form
<< decide{'e1; u1. 'l1['u1]; v1. 'r1['v1]} =
decide{'e2; u2. 'l2['u2]; v2. 'r2['v2]} in 'T >>,
(withTermsT [<< bind{z. 'B['z]} >>; << 'A + 'B >>] (dT 0)) creates 3
subgoals. Here << 'B['e1] >> must be the same as << 'T >>, and
<< 'A + 'B >> must be the type of << 'e1 >> and << 'e2 >>.
XXX decideMember is broken (has equality conclusion)
If the conclusion is of the form
<< subtype{ ('A1 + 'B1); ('A2 + 'B2) } >>,
(dT 0) creates 2 subtype subgoals.
If the n'th hypothesis is of the form << x: inl{'y} = inr{'z} in 'T >>
or << x: inr{'y} = inl{'z} in 'T >>,
(dT n) succeeds with no subgoals.
This file adds to the subtypeT tactic.
subtypeT proves that << 'A1 + 'B1 >> is a subtype of << 'A2 + 'B2 >>
by proving << 'A1 >> is a subtype of << 'A2 >> and << 'B1 >> is a
subtype of << 'B2 >>.
----------------------------------------
itt_unit:
new terms:
unit
This file adds to the dT tactic.
If the conclusion is of the form << unit IN univ[i:l] >>,
<< "type"{unit} >>, << unit >>, << it IN unit >>,
(dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << x: unit >>,
(dT n) replaces << 'x >> with << it >> in the rest of the sequent.
If the conclusion is of the form << "rewrite"{'e1; it} >>,
(dT 0) creates a subgoal << 'e1 = it in unit >>.
This file adds to the squashT tactic.
squashT succeeds if the conclusion is of the form << unit >>.
----------------------------------------
itt_logic:
new terms, conversions:
unfold_prop: "prop"[i:l] --> "univ"[i:l]
unfold_true: "true" --> unit
unfold_false: "false" --> void
unfold_not: "not"{'a} --> 'a -> void
unfold_and: "and"{'a; 'b} --> 'a * 'b
unfold_or: "or"{'a; 'b} --> 'a + 'b
unfold_implies: "implies"{'a; 'b} --> 'a -> 'b
unfold_iff: "iff"{'a; 'b} --> (('a -> 'b) & ('b -> 'a))
unfold_cand: "cand"{'a; 'b} --> "and"{'a; 'b}
unfold_cor: "cor"{'a; 'b} --> "or"{'a; ("cand"{("not"{'a}); 'b})}
unfold_all: "all"{'A; x. 'B['x]} --> x: 'A -> 'B['x]
unfold_exists: "exists"{'A; x. 'B['x]} --> x: 'A * 'B['x]
* fold_true, fold_false, fold_not, fold_implies, fold_iff, fold_and,
fold_or, fold_cand, fold_cor, fold_all, fold_exists : conv
These are the inverses of the above conversions.
* univCDT : tactic
Applies (dT 0) if the conclusion is a "all", "dfun", "implies", or
"fun" term; then recurse (on "main" subgoals).
* genUnivCDT : tactic
As univCDT, but also applies on "and", "prod", and "iff" conclusions.
* instHypT : term list -> int -> tactic
(instHypT tl i) instantiates the i'th hypothesis (which must be a
"all", "dfun", or "implies" term) with the terms in the term list.
* backThruHypT : int -> tactic
(backThruHypT i) works if the i'th hypothesis is a universally
quantified formula, with a body that matches the sequent conclusion.
It unifies the conclusion against the formula body to discover
variable instantiations; it then instantiates the formula.
* assumT : int -> tactic
(assumT i) turns the i'th assumption sequent into a universally
quantified formula and adds it as a new hypothesis to the current
sequent.
* backThruAssumT : int -> tactic
(backTrhuAssumT i) uses (assumT i) to pull in the i'th assumption
sequent, and then backchains through it (using backThruHypT).
* moveToConclVarsT : string list -> tactic
Takes all the hypotheses which either declare a variable in the list
or in which a variable in the list occurs free, and
moves them into the conclusion (as implications or as universal
quantification, depending on whether that hypothesis's variable occurs
free in the conclusion).
* moveToConclT : int -> tactic
(moveToConclT i) calls moveToConclVarsT with the single variable
declared by the i'th hypothesis.
* squash_falseT : tactic
Changes the goal to be a "squash" sequent if the conclusion is
<< false >>.
* genAssumT : int list -> tactic
There are several plausible ways to write a sequent that you intend to
prove. For instance, if you want to prove that plus is commutative,
you could write:
sequent ['ext] { 'H >- all a: int. all b: int. 'a +@ 'b = 'b +@ 'a in int }
or
sequent ['ext] { 'H; a: int; b: int >- 'a +@ 'b = 'b +@ 'a in int }
or
sequent ['ext] { 'H >- 'a IN int } -->
sequent ['ext] { 'H >- 'b IN int } -->
sequent ['ext] { 'H >- 'a +@ 'b = 'b +@ 'a in int }
In MetaPRL, it is easier to apply rules of the third form, so that's
what you would typically write. However, it is more straightforward
to prove rules given in the first or second forms. This tactic
converts from the third form to the mix of the first and second form.
Assumptions which have membership conclusions where the member is not
a single variable also work. The first membership assumption would be
converted to a hypothesis binding, and the rest - to universal quantifiers.
Assumptions which do not have membership conclusions are converted
into non-binding hypothesis up until the first time the universal quantifier
is used and the rest are converted into implications.
Here is a larger
(meaningless) example. (genAssumT [3; 1; 2]) would convert
sequent ['ext] { 'H >- 'b +@ 'c IN int } -->
sequent ['ext] { 'H >- interesting{'a; 'b; 'b +@ 'c} } -->
sequent ['ext] { 'H >- 'a IN int } -->
sequent ['ext] { 'H >- happy{'b +@ 'c; 'c; 'a} }
to
sequent ['ext] { 'H; a: int >-
all v: int.
interesting{'a; 'b; 'v} -> happy{'v; 'c; 'a} }
The tactic is not always able to prove that this transformation is
valid (indeed, sometimes the transformation is not valid). In that
case, there will be some extra subgoals for you to prove.
This file adds to the dT tactic.
If the conclusion is of the form << "true" IN univ[i:l] >>,
<< "type"{."true"} >>, << "true" >>, << "false" IN univ[i:l] >>,
<< "type"{."false"} >>, (dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << x: "false" >>,
(dT n) succeeds with no subgoals (and thins?!?).
If the conclusion is of the form
<< "not"{'t1} = "not"{'t2} in univ[i:l] >>,
(dT 0) reduces it to << 't1 = 't2 in univ[i:l] >>.
If the conclusion is of the form << "type"{."not"{'t}} >>,
(dT 0) reduces it to << "type"{'t} >>.
If the conclusion is of the form << "not"{'t} >>,
(dT 0) reduces it to << "type"{'t} >> and << x: 't >- "false" >>.
If the n'th hypothesis is of the form << x: "not"{'t} >>,
(dT n) changes the conclusion to << 't >>.
If the conclusion is of the form
<< "and"{'a1; 'a2} = "and"{'b1; 'b2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form
<< "type"{."and"{'a1; 'a2}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "and"{'a1; 'a2} >>,
(dT 0) creates subgoals << 'a1 >> and << 'a2 >>.
If the n'th hypothesis is of the form << x: "and"{'a1; 'a2} >>,
(dT n) removes that hypothesis, adds hypotheses << y: 'a1; z: 'a2 >>,
and replaces << 'x >> by << 'y, 'z >> in the rest of the sequent.
If the conclusion is of the form
<< "or"{'a1; 'a2} = "or"{'b1; 'b2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."or"{'a1; 'a2}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "or"{'a1; 'a2} >>,
(selT 1 (dT 0)) creates subgoals << 'a1 >> and << "type"{'a2} >>.
(selT 2 (dT 0)) creates subgoals << 'a2 >> and << "type"{'a1} >>.
If the n'th hypothesis is of the form << x: "or"{'a1; 'a2} >>,
(dT n) creates 2 subgoals. In one, the hypothesis is replaced by
<< y: 'a1 >>, and << 'x >> is replaced by << inl{'y} >> in the rest of
the sequent. In the other, the hypothesis is replaced by
<< y: 'a2 >>, and << 'x >> is replaced by << inr{'y} >> in the rest of
the sequent.
If the conclusion is of the form
<< "implies"{'a1; 'a2} = "implies"{'b1; 'b2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."implies"{'a1; 'a2}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "implies"{'a1; 'a2} >>,
(dT 0) creates subgoals << "type"{'a1} >> and << x: 'a1 >- 'a2 >>.
If the n'th hypothesis is of the form << x: "implies"{'a1; 'a2} >>,
(dT n) creates 2 subgoals and thins. One has conclusion << 'a1 >>,
and the other has a new hypothesis << y: 'a2 >>.
If the conclusion is of the form
<< "iff"{'a1; 'a2} = "iff"{'b1; 'b2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."iff"{'a1; 'a2}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "iff"{'a1; 'a2} >>,
(dT 0) creates subgoals << 'a1 => 'a2 >> and << 'a2 => 'a1 >>.
If the n'th hypothesis is of the form << x: "iff"{'a1; 'a2} >>,
(dT n) replaces this hypothesis with the hypotheses
<< y: "implies"{'a1; 'a2}; z: "implies"{'a2; 'a1} >> and replaces
<< 'x >> with << 'y, 'z >> in the rest of the sequent.
If the conclusion is of the form
<< "cand"{'a1; 'a2} = "cand"{'b1; 'b2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."cand"{'a1; 'a2}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "cand"{'a1; 'a2} >>,
(dT 0) creates subgoals << 'a1 >> and << x: 'a1 >- 'a2 >>.
If the n'th hypothesis is of the form << x: "cand"{'a1; 'a2} >>,
(dT n) replaces this hypothesis with the hypotheses
<< y: 'a1; z: 'a2 >>, and replaces << 'x >> with << 'y, 'z >> in the
rest of the sequent.
If the conclusion is of the form
<< "cor"{'a1; 'a2} = "cor"{'b1; 'b2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."cor"{'a1; 'a2}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "cor"{'a1; 'a2} >>,
(selT 1 (dT 0)) creates 2 subgoals << x: "not"{'a1} >- "type"{.'a2} >>
and << 'a1 >>. (selT 2 (dT 0)) creates 3 subgoals,
<< "type"{.'a1} >>, << "not"{'a1} >>, and << x: "not"{'a1} >- 'a2 >>.
If the n'th hypothesis is of the form << x: "cor"{'a1; 'a2} >>,
(dT n) creates 2 subgoals. In the first, the hypothesis is replaced
by the hypothesis << u: 'a1 >>, and << 'x >> is replaced by
<< inl{'u} >> in the rest of the sequent. In the second, the
hypothesis is replaced by the hypotheses << u: "not"{'a1}; v: 'a2 >>,
and << 'x >> is replaced by << inr{'u, 'v} >> in the rest of the
sequent.
If the conclusion is of the form
<< "all"{'t1; x1. 'b1['x1]} = "all"{'t2; x2. 'b2['x2]} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."all"{'t; v. 'b['v]}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "all"{'t; v. 'b['v]} >>,
(dT 0) creates subgoals << "type"{'t} >> and << x: 't >- 'b['x] >>.
If the n'th hypothesis is of the form << x: all a: 'A. 'B['a] >>,
(withT a (dT n)) creates subgoals << a IN 'A >> and
<< w: 'B[a] >- 'C['x] >> and thins.
If the conclusion is of the form
<< "exists"{'t1; x1. 'b1['x1]} = "exists"{'t2; x2. 'b2['x2]} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form
<< "type"{."exists"{'t; v. 'b['v]}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << "exists"{'t; v. 'b['v]} >>,
(withT a (dT 0)) creates subgoals << a IN 't >>,
<< 'b[a] >>, and << x: 't >- "type"{'b['x]} >>.
If the n'th hypothesis is of the form << x: exst v: 'a. 'b['v] >>,
(dT n) replaces it with hypotheses << y: 'a; z: 'b['y] >>,
and replaces << 'x >> with << 'y, 'z >> in the rest of the sequent.
This file adds to the trivialT tactic.
If any of the hypotheses are of the form << x: "false" >> or
<< x: void >>, then trivialT will succeed with no subgoals.
This file adds to the autoT tactic.
If any of the hypotheses are "and", "prod", "dprod", or "exists"
terms, autoT will decompose them (with dT).
autoT will attempt backThruHypT on all hypotheses.
autoT will attempt backThruAssumT on all assumptions whose goal
matches the current sequent's goal.
----------------------------------------
itt_bool:
new terms:
"bool"
"btrue"
"bfalse"
bor{'a; 'b}
band{'a; 'b}
bimplies{'a; 'b}
bnot{'a}
"assert"{'t}
ifthenelse{'e1; 'e2; 'e3}
* unfold_bool : conv
Rewrites << bool >> to << unit + unit >>.
* unfold_btrue : conv
Rewrites << btrue >> to << inl{it} >>.
* unfold_bfalse : conv
Rewrites << bfalse >> to << inr{it} >>.
* reduce_ifthenelse_true : conv
Rewrites << ifthenelse{btrue; 'x; 'y} >> to << 'x >>.
* reduce_ifthenelse_false : conv
Rewrites << ifthenelse{bfalse; 'x; 'y} >> to << 'y >>.
* unfold_bor : conv
Rewrites << bor{'a; 'b} >> to << ifthenelse{'a; btrue; 'b} >>.
* unfold_band : conv
Rewrites << band{'a; 'b} >> to << ifthenelse{'a; 'b; bfalse} >>.
* unfold_bimplies : conv
Rewrites << bimplies{'a; 'b} >> to << ifthenelse{'a; 'b; btrue} >>.
* unfold_bnot : conv
Rewrites << bnot{'a} >> to << ifthenelse{'a; bfalse; btrue} >>.
* unfold_assert : conv
Rewrites << "assert"{'a} >> to << 'a = btrue in bool >>.
* fold_bool, fold_btrue, fold_bfalse, fold_bor, fold_band,
fold_bimplies, fold_bnot, fold_assert : conv
These are the inverses of the above conversions.
* extBoolT : tactic
Destructs conclusions of the form << 'x = 'y in bool >>.
* magicT : tactic
Lets you prove conclusions of the form << "assert"{'t} >> by
contradiction.
* splitBoolT : term -> int -> tactic
(splitBoolT t i) lets you do case analysis on a term << t >> of type
<< "bool" >> in the i'th clause. If you want to affect some but not
all instances of the term in the clause, you can wrap the call in
(withT << bind{x. 'B['x]} >> ...) in the standard way (where the
i'th clause must be << 'B[t] >>).
* splitITE : int -> tactic
Split the first free ifthenelse in the i'th clause. You can specify a
particular ifthenelse to split by wrapping the call in
(withT << t >> ...), where << t >> is the test of the ifthenelse you
want to split (every ifthenelse with this test will be split).
* squash_assertT : tactic
Changes the goal to be a "squash" sequent if the conclusion is of the
form << "assert"{'t} >>. This is part of the autoT tactic.
This file adds to the reduceTopC conversion.
It adds the reduce_ifthenelse_true and reduce_ifthenelse_false
conversions; in addition, the following terms:
<< bnot{btrue} >>,
<< bnot{bfalse} >>,
<< bor{btrue; 'x} >>,
<< bor{bfalse; 'x} >>,
<< band{btrue; 'x} >>,
<< band{bfalse; 'x} >>,
<< bimplies{btrue; 'x} >>,
<< bimplies{bfalse; 'x} >>
are reduced in the obvious way.
This file adds to the dT tactic.
If the conclusion is of the form << "bool" IN univ[i:l] >>,
<< "type"{bool} >>, << btrue IN "bool" >>, << bfalse IN "bool" >>,
(dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << x: "bool" >> or
<< x: hide{"bool"} >>,
(dT n) creates 2 subgoals. In the first, the hypothesis is removed
and << 'x >> is replaced by << btrue >>; in the second, the hypothesis
is removed and << 'x >> is replaced by << bfalse >>.
If the conclusion is of the form << "type"{ifthenelse{'e; 'A; 'B}} >>,
(dT 0) creates 2 typehood subgoals and the subgoal
<< 'e IN bool >>.
If the n'th hypothesis is of the form << x: btrue = bfalse in bool >>
or << x: bfalse = btrue in bool >>,
(dT n) succeeds with no subgoals.
If the conclusion is of the form
<< ifthenelse{'e1; 'x1; 'y1} = ifthenelse{'e2; 'x2; 'y2} in 'T >>,
(dT 0) creates 3 equality subgoals.
If the conclusion is of one of the forms
<< bor{'t1; 't2} IN bool >>, << band{'t1; 't2} IN bool >>,
or << bimplies{'t1; 't2} IN bool >>,
(dT 0) creates 2 membership subgoals.
If the conclusion is of the form << bnot{'a} IN bool >>,
(dT 0) creates 1 membership subgoal.
If the conclusion is of the form << "type"{."assert"{'t}} >>,
(dT 0) creates subgoal << 't IN bool >>.
If the conclusion is of the form << "assert"{btrue} >>,
(dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << x: "assert"{bfalse} >>,
(dT n) succeeds with no subgoals.
If the conclusion is of the form << "assert"{bnot{'t1}} >>,
(dT 0) creates subgoal << x: "assert"{'t1} >- "false" >> (and an extra
well-formedness subgoal).
If the n'th hypothesis is of the form << x: "assert"{bnot{'t}} >>,
(dT n) removes the hypothesis, replaces << 'x >> with << it >> in the
rest of the hypotheses, and changes the conclusion to
<< "assert"{'t} >>.
If the n'th hypothesis is of the form << x: "assert"{bor{'t1; 't2}} >>,
(dT n) creates 3 subgoals. In one, the hypothesis is changed to
<< x: "assert"{'t1} >>, and << 'x >> is changed to << it >> in the
rest of the sequent. In the second, the hypothesis is changed to
<< x: "assert"{'t2} >>, and << 'x >> is changed to << it >> in the
rest of the sequent. The third is a well-formedness subgoal.
If the n'th hypothesis is of the form << x: "assert"{band{'t1; 't2}} >>,
(dT n) replaces the hypothesis with the hypotheses
<< y: "assert"{'t1}; z: "assert"{'t2} >> and changes << 'x >> to
<< it >> in the rest of the sequent. It also creates a
well-formedness subgoal.
If the n'th hypothesis is of the form
<< x: "assert"{bimplies{'t1; 't2}} >>,
(dT n) creates 2 subgoals. The first removes the hypothesis, changes
<< 'x >> to << it >>, and has conclusion << "assert"{'t1} >>.
The second removes the hypothesis, changes << 'x >> to << it >>,
and adds a new hypothesis << y: "assert"{'t2} >>.
If the conclusion is of the form << "assert"{bor{'t1; 't2}} >>,
(selT 1 (dT 0)) creates subgoals << 't2 IN bool >> and
<< "assert"{'t1} >>. (selT 2 (dT 0)) creates subgoals
<< 't1 IN bool >> and << "assert"{'t2} >>.
If the conclusion is of the form << "assert"{band{'t1; 't2}} >>,
(dT 0) creates subgoals << "assert"{'t1} >> and << "assert"{'t2} >>.
If the conclusion is of the form << "assert"{bimplies{'t1; 't2}} >>,
(dT 0) creates a subgoal << x: "assert"{'t1} >- "assert"{'t2} >> (and
a well-formedness subgoal).
If the conclusion is of one of the forms << "rewrite"{'x; btrue} >>,
<< "rewrite"{'x; bfalse} >>, << "rewrite"{btrue, 'x} >>, or
<< "rewrite"{bfalse; 'x} >>, (dT 0) changes it to a << bool >>
equality.
This file adds to the eqcdT tactic.
eqcdT can handle conclusions of the forms
<< bool = bool in univ[i:l] >>,
<< btrue = btrue in bool >>,
<< bfalse = bfalse in bool >>,
<< ifthenelse{'x1; 'y1; 'z1} = ifthenelse{'x2; 'y2; 'z2} in 'T >>,
This file adds to the autoT tactic.
The autoT tactic will call squash_assertT.
----------------------------------------
itt_atom:
new terms:
atom
token[t:t]
* atomSqequalT : tactic
This tactic changes conclusions of the form << "rewrite"{'x; 'y} >>
to << 'x = 'y in atom >>.
This file adds to the dT tactic.
If the conclusion is of the form << atom = atom in univ[i:l] >>,
<< "type"{atom} >>, or << token[t:t] = token[t:t] in atom >>,
(dT 0) succeeds with no subgoals.
If the conclusion is of the form << atom >>,
(dT 0) succeeds with no subgoals (with an extract term of
<< token["token":t] >>).
----------------------------------------
itt_atom_bool:
new terms:
eq_atom{'x; 'y}
* reduce_eq_atom : conv
Reduces a term of the form << eq_atom{token[x:t]; token[y:t]} >>
to << btrue >> or << bfalse >>.
This file adds to the dT tactic.
If the conclusion is of the form << eq_atom{'x; 'y} IN bool >>,
(dT 0) creates subgoals << 'x IN atom >> and << 'y IN atom >>.
If the conclusion is of the form << "assert"{eq_atom{'x; 'y}} >>,
(dT 0) changes it to << 'x = 'y in atom >>.
If the n'th hypothesis is of the form << z: "assert"{eq_atom{'x; 'y}} >>,
(dT n) changes it to << z: 'x = 'y in atom >>, and replaces << 'z >>
with << it >> in the rest of the sequent.
----------------------------------------
itt_int:
new terms:
int
number[n:n]
ind{'i; m, z. 'down['m; 'z]; 'base; m, z. 'up['m; 'z]}
"add"{'a; 'b}
"sub"{'a; 'b}
"mul"{'a; 'b}
"div"{'a; 'b}
"rem"{'a; 'b}
"lt"{'a; 'b}
"le"{'a; 'b}
"ge"{'a; 'b}
"gt"{'a; 'b}
* unfold_le : conv
Rewrites << le{'a; 'b} >> to << ('a < 'b or 'a = 'b in int) >>.
* unfold_gt : conv
Rewrites << gt{'a; 'b} >> to << ('b < 'a) >>.
* unfold_ge : conv
Rewrites << ge{'a; 'b} >> to << ('b < 'a or 'a = 'b in int) >>.
* reduce_add, reduce_sub, reduce_mul, reduce_div, reduce_rem,
reduce_lt, reduce_eq : conv
These are probably not useful to the average user.
* reduce_ind_down : conv
Reduces ind terms under the condition that the argument is less than
0.
* reduce_ind_up : conv
Reduces ind terms under the condition that the argument is greater
than 0.
* reduce_ind_base : conv
Reduces ind terms under the condition that the argument is equal to 0.
* reduce_ind : conv
Reduces ind terms where the argument is a number literal.
* intSqequalT : tactic
This tactic changes conclusions of the form << "rewrite"{'x; 'y} >>
to << 'x = 'y in int >>.
* decideT : term -> tactic
If the argument term is of the form << 'i < 'j >> or
<< 'i = 'j in int >>, this tactic does a case split on the term (and
adds 2 well-formedness subgoals).
This file adds to the reduceTopC conversion.
It adds the reduce_ind conversion. Also, "add", "sub", "mul", "div",
and "rem" applied to number literals are reduced.
This file adds to the dT tactic.
If the conclusion is of the form << "type"{int} >>,
<< int IN univ[i:l] >>, << number[n:n] IN int >>, or
(dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << n: int >>,
(dT n) performs induction and thins.
If the conclusion is of the form
<< ind{'x1; i1, j1. 'down1['i1; 'j1]; 'base1; k1, l1. 'up1['k1; 'l1]}
= ind{'x2; i2, j2. 'down2['i2; 'j2]; 'base2; k2, l2. 'up2['k2; 'l2]}
in 'T >>,
(withT << lambda{z. 'B['z]} >> (dT 0)) creates 4 equality subgoals
(where << 'B['x1] >> must be the same as << 'T >>).
If the conclusion is of the form
<< 'i1 < 'j1 = 'i2 < 'j2 in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << it = it in ('a < 'b) >>,
(dT 0) changes it to << 'a < 'b >>.
XXX
If the n'th hypothesis is of the form << x: 'a < 'b >>,
(dT n) would change << 'x >> to << it >> in the rest of the sequent
EXCEPT THAT it is overridden by another elimination tactic, below.
If the conclusion is of the form << add{'i; 'j} IN int >>,
<< sub{'i; 'j} IN int >>, << mul{'i; 'j} IN int >>, << "div"{'i; 'j} IN int >>,
<< "rem"{'i; 'j} IN int >>, << "type"{lt{'i; 'j}} >>, << "type"{gt{'i; 'j}} >>,
<< "type"{le{'i; 'j}} >>, << "type"{ge{'i; 'j}} >>,
<< lt{'i; 'j} IN univ [i:l] >>, << gt{'i; 'j} IN univ [i:l] >>,
<< le{'i; 'j} IN univ [i:l] >>, or
<< ge{'i; 'j} IN univ [i:l] >>,
(dT n) creates subgoals << 'i IN int >> and << 'j IN int >>.
If the n'th hypothesis is of the form << x: ('i < 'j) >>,
(dT n) adds a new hypothesis << y: "not"{.'j < 'i} >>.
If the conclusion is of the form << ('i +@ 'k) < ('j +@ 'k) >>
or << ('i -@ 'k) < ('j -@ 'k) >>,
(dT n) changes it to << 'i < 'j >>.
----------------------------------------
itt_int_bool:
new terms:
eq_int{'i; 'j}
lt_int{'i; 'j}
le_int{'i; 'j}
gt_int{'i; 'j}
ge_int{'i; 'j}
* reduce_eq_int, reduce_lt_int, reduce_gt_int : conv
These conversions reduce comparisons of numeric literals to << btrue >>
or << bfalse >>.
* reduce_le_int : conv
Rewrites << le_int{'i; 'j} >> to << bor{eq_int{'i; 'j}; lt_int{'i; 'j}} >>.
* reduce_ge_int : conv
Rewrites << ge_int{'i; 'j} >> to << bor{eq_int{'i; 'j}; gt_int{'i; 'j}} >>.
This file adds to the reduceTopC conversion.
It adds the above conversions.
This file adds to the dT tactic.
If the conclusion is of the form << eq_int{'i; 'j} IN bool >>,
(dT 0) creates subgoals with conclusions << 'i IN int >>
and << 'j IN int >>.
If the conclusion is of the form << "assert"{eq_int{'i; 'j}} >>,
(dT 0) changes it to << 'i = 'j in int >>.
If the n'th hypothesis is of the form << z: "assert"{eq_int{'i; 'j}} >>,
(dT n) changes it to << z: ('i = 'j in int) >>, and replaces << 'z >>
with << it >> in the rest of the sequent.
----------------------------------------
itt_arith:
This file is not finished; it doesn't do anything that affects the
prover.
----------------------------------------
itt_set:
new terms:
set{'A; x. 'B['x]}
hide{'A}
* squashT : tactic
This is a slight variant on the squashT tactic in itt_squash; this
version does nothing if the goal is already a squash sequent.
This file adds to the dT tactic.
If the conclusion is of the form
<< { a1:'A1 | 'B1['a1] } = { a2:'A2 | 'B2['a2] } in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{.{ a1:'A1 | 'B1['a1] }} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << { x:'A | 'B['x] } >>,
(withT a (dT 0)) creates subgoals << a = a in 'A >> and << 'B[a] >>
(and a well-formedness subgoal).
If the conclusion is of the form << 'a1 = 'a2 in { a:'A | 'B['a] } >>,
(dT 0) creates subgoals << 'a1 = 'a2 in 'A >> and << 'B['a1] >> (and a
well-formedness subgoal).
If the n'th hypothesis is of the form << u: { x:'A | 'B['x] } >>,
(dT n) replaces it with the hypotheses << u: 'A; v: hide{'B['u]} >>.
If the conclusion is of the form << subtype{ { a: 'A | 'B['a] }; 'A } >>,
(dT 0) replaces it with a well-formedness subgoal.
This file adds to the subtypeT tactic.
subtypeT proves that << 'A >> is a subtype of << { x: 'A | 'B['x] } >>
directly.
----------------------------------------
itt_isect:
new terms:
"isect"{'A; x. 'B['x]}
top
* unfold_top : conv
Rewrites << top >> to << "isect"{void; x. void} >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< isect x1: 'A1. 'B1['x1] = isect x2: 'A2. 'B2['x2] in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{."isect"{'A; x. 'B['x]}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << top IN univ[i:l] >> or
<< "type"{top} >>,
(dT 0) succeeds with no subgoals.
If the conclusion is of the form << isect x: 'A. 'B['x] >>,
(dT 0) creates 2 subgoals.
If the conclusion is of the form << 'b1 = 'b2 in isect x: 'A. 'B['x] >>,
(dT 0) creates an equality subgoal and a well-formedness subgoal.
If the conclusion is of the form << 'b1 = 'b2 in top >>,
(dT 0) succeeds with no subgoals.
If the n'th hypothesis is of the form << x: isect y: 'A. 'B['y] >>,
(withT a (dT n)) creates 2 subgoals. One has conclusion
<< a = a in 'A >>; the other has extra hypotheses
<< z: 'B['a]; v: 'z = 'x in 'B['a] >>.
If the conclusion is of the form
<< subtype{ (isect a1:'A1. 'B1['a1]); (isect a2:'A2. 'B2['a2]) } >>,
(dT 0) creates 2 subtype subgoals.
If the conclusion is of the form << subtype{'T; top} >>,
(dT 0) changes the conclusion to << "type"{'T} >>.
This file adds to the subtypeT tactic.
subtypeT proves that << isect a1:'A1. 'B1['a1] >> is a subtype of
<< isect a2:'A2. 'B2['a2] >> by proving << 'A2 >> is a subtype of << 'A1 >>
and << 'B1['x] >> is a subtype of << 'B2['x] >>.
----------------------------------------
itt_tunion:
new terms:
tunion{'A; x. 'B['x]}
This file adds to the dT tactic.
If the conclusion is of the form
<< tunion{'A1; x1. 'B1['x1]} = tunion{'A2; x2. 'B2['x2] } in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{tunion{'A; x. 'B['x]}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << 'x1 = 'x2 in tunion{'A; x. 'B['x]} >>,
(withT a (dT 0)) creates subgoals << a = a in 'A >> and
<< 'x1 = 'x2 in 'B['a] >> (and a well-formedness subgoal).
If the conclusion is of the form << tunion{'A; x. 'B['x]} >>,
(withT a (dT 0)) creates subgoals << a = a in 'A >> and << 'B[a] >>
(and a well-formedness subgoal).
If the n'th hypothesis is of the form << x: tunion{'A; y. 'B['y]} >>,
(dT n) adds new hypotheses
<< w: hide{'A}; z: 'B['w]; w2: 'z = 'x in tunion{'A; y. 'B['y]} >>.
----------------------------------------
itt_bisect:
new terms:
bisect{'A; 'B}
* unfold_bisect : conv
Rewrites << bisect{'A; 'B} >> to
<< "isect"{bool; x. ifthenelse{'x; 'A; 'B}} >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< bisect{'A1; 'B1} = bisect{'A2; 'B2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{bisect{'A; 'B}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << 'x = 'y in bisect{'A; 'B} >>,
(dT 0) creates subgoals << 'x = 'y in 'A >> and << 'x = 'y in 'B >>.
If the n'th hypothesis is of the form << x: bisect{'A; 'B} >>,
(selT 1 (dT n)) adds new hypotheses << y: 'A; z: 'y = 'x in 'A >>.
(selT 2 (dT n)) adds new hypotheses << y: 'B; z: 'y = 'x in 'B >>.
If the conclusion is of the form << subtype{bisect{'A; 'B}; 'C} >>,
(selT 1 (dT 0)) creates subgoals << "type"{'B} >> and
<< subtype{'A; 'C} >>. (selT 2 (dT 0)) creates subgoals
<< "type"{'A} >> and << subtype{'B; 'C} >>.
If the conclusion is of the form << subtype{'C; bisect{'A; 'B}} >>,
(dT 0) creates subgoals << subtype{'C; 'A} >> and << subtype{'C; 'B} >>.
----------------------------------------
itt_bunion:
new terms:
bunion{'A; 'B}
* unfold_bunion : conv
Rewrites << bunion{'A; 'B} >> to
<< tunion{bool; x. ifthenelse{'x; 'A; 'B}} >>.
* fold_bunion : conv
This is the inverse of the above conversion.
This file adds to the dT tactic.
If the conclusion is of the form
<< bunion{'A1; 'B1} = bunion{'A2; 'B2} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{bunion{'A; 'B}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << 'x = 'y in bunion{'A; 'B} >>,
(selT 1 (dT 0)) creates subgoals << 'x = 'y in 'A >> and
<< "type"{'B} >>. (selT 2 (dT 0)) creates subgoals
<< 'x = 'y in 'B >> and << "type"{'A} >>.
If the n'th hypothesis is of the form << x: bunion{'A; 'B} >>,
(dT n) creates 2 subgoals and thins. One subgoal has new hypotheses
<< y: 'A; z: 'y = 'x in bunion{'A; 'B} >>; the other has new
hypotheses << y: 'B; z: 'y = 'x in bunion{'A; 'B} >>.
----------------------------------------
itt_w:
new terms:
w{'A; x. 'B['x]}
tree{'a; 'f}
tree_ind{'z; a, f, g. 'body['a; 'f; 'g]}
* reduce_tree_ind : conv
Reduces terms of the form
<< tree_ind{tree{'a1; 'f1}; a2, f2, g2. 'body['a2; 'f2; 'g2]} >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< w{'A1; x1. 'B1['x1]} = w{'A2; x2. 'B2['x2]} in univ[i:l] >>,
(dT 0) creates 2 equality subgoals.
If the conclusion is of the form << "type"{.w{'A1; y.'A2['y]}} >>,
(dT 0) creates 2 typehood subgoals.
If the conclusion is of the form << w{'A; x. 'B['x]} >>,
(withT a (dT 0)) creates subgoals << a = a in 'A >> and
<< 'B['a] -> w{'A; x. 'B['x]} >> (and a well-formedness subgoal).
If the conclusion is of the form
<< tree{'a1; 'b1} = tree{'a2; 'b2} in w{'A; x. 'B['x]} >>,
(dT 0) creates 2 equality subgoals and a well-formedness subgoal.
If the n'th hypothesis is of the form << z: w{'A; x. 'B['x]} >>,
(dT n) performs induction on << 'z >> and thins.
If the conclusion is of the form
<< tree_ind{'z1; a1, f1, g1. 'body1['a1; 'f1; 'g1]}
= tree_ind{'z2; a2, f2, g2. 'body2['a2; 'f2; 'g2]}
in 'T >>,
(withT t (dT 0)) creates 2 equality subgoals. Here << t >> is the
type of << 'z1 >> and << 'z2 >>; it must be of the form
<< w{'A; x. 'B['x]} >>.
----------------------------------------
itt_prec:
new terms:
"prec"{T, x. 'B['T; 'x]; 'a}
precind{'a; p, h. 'g['p; 'h]}
* reducePrecInd : conv
Rewrites << precind{'a; p, h. 'g['p; 'h]} >> to
<< 'g[lambda{a. precind{'a; p, h. 'g['p; 'h]}}; 'a] >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< "prec"{A1, x1. 'B1['A1; 'x1]; 'a1}
= "prec"{A2, x2. 'B2['A2; 'x2]; 'a2}
in univ[i:l] >>,
(withT A (dT 0)) creates 3 equality subgoals. Here A must be the type
of << 'a1 >> and << 'a2 >>.
If the conclusion is of the form << "prec"{T, x. 'B['T; 'x]; 'a} >>,
(dT 0) creates 2 subgoals.
If the conclusion is of the form
<< 'a1 = 'a2 in "prec"{T, x. 'B['T; 'x]; 'a} >>,
(dT 0) creates an equality subgoal and a typehood subgoal.
If the n'th hypothesis is of the form
<< r: "prec"{T, x. 'B['T; 'x]; 'a} >>,
(withTermsT [<< lambda{z. 'G['z]} >>; a; A; << univ[i:l] >>] (dT n))
creates 2 subgoals and thins. Here the conclusion must be
<< 'G[a] >>; a must be << 'a >>; A must be the type of << 'a >>; and
<< univ[i:l] >> also plays some role I don't understand. (I'm not
sure whether you actually have to pass a.) (XXX This rule might be
inaccessible due to being overridden by the following rule.)
If the n'th hypothesis is of the form
<< r: "prec"{T, x. 'B['T; 'x]; 'a} >>,
(dT 0) adds new hypotheses and thins.
If the conclusion is of the form
<< precind{'r1; h1, z1. 't1['h1; 'z1]}
= precind{'r2; h2, z2. 't2['h2; 'z2]}
in 'S >>,
(withTermsT [<< lambda{x. 'B['x]} >>;
<< (a:'A * "prec"{T, y. 'B['T; 'y]; 'a}) >>;
<< univ[i:l] >>] (dT 0))
creates 2 equality subgoals and thins. Here << 'S >> must be << 'B['r1] >>,
the second argument must be the type of << 'r1 >> and << 'r2 >>, and
<< univ[i:l] >> plays some role I don't understand.
----------------------------------------
itt_srec:
new terms:
srec{T. 'B['T]}
srecind{'a; p, h. 'g['p; 'h]}
* unfold_srecind : conv
Rewrites << srecind{'a; p, h. 'g['p; 'h]} >> to
<< 'g[lambda{a. srecind{'a; p, h. 'g['p; 'h]}}; 'a] >>.
This file adds to the dT tactic.
If the conclusion is of the form
<< srec{T1. 'B1['T1]} = srec{T2. 'B2['T2]} in univ[i:l] >>,
(dT 0) creates an equality subgoal and a subtype subgoal.
If the conclusion is of the form << "type"{srec{T. 'B['T]}} >>,
(withT << univ[i:l] >> (dT 0)) creates a subtype subgoal.
If the conclusion is of the form << srec{T. 'B['T]} >>,
(dT 0) creates a subgoal << 'B[srec{T. 'B['T]}] >> (and a
well-formedness subgoal).
If the conclusion is of the form << 'x1 = 'x2 in srec{T. 'B['T]} >>,
(dT 0) creates an equality subgoal (and a well-formedness subgoal).
If the n'th hypothesis is of the form << x: srec{T. 'B['T]} >>,
(withTermsT [<< srec{T. 'B['T]} >>; << univ[i:l] >>] (dT n))
performs induction on << 'x >> and thins. The first argument is
another copy of the type of << 'x >> (I don't know if this is really
required); the second argument plays a role I haven't figured out yet.
(XXX This is probably overridden by the below rule.)
If the n'th hypothesis is of the form << x: srec{T. 'B['T]} >>,
(dT n) adds new hypotheses and thins.
XXX
If the conclusion is of the form
<< srecind{'r1; h1, z1. 't1['h1; 'z1]}
= srecind{'r2; h2, z2. 't2['h2; 'z2]}
in 'S >>,
(withTermsT [<< lambda{x. 'S1['x]} >>;
<< srec{T. 'B['T]} >>;
u;
<< univ[i:l] >>] (dT 0))
creates 2 equality subgoals. Here << 'S >> must be << 'S1['r1] >>,
<< srec{T. 'B['T]} >> must be the type of << 'r1 >> and << 'r2 >>,
and << univ[i:l] >> plays some role I haven't figured out yet. The
third argument is just silly; I don't know if it's actually required.
----------------------------------------
itt_quotient:
new terms:
"quot"{'A; x, y. 'E['x; 'y]}
This file adds to the dT tactic.
If the conclusion is of the form
<< quot x1, y1: 'A1 // 'E1['x1; 'y1]
= quot x2, y2: 'A2 // 'E2['x2; 'y2]
in univ[i:l] >>,
(dT 0) creates 2 equality subgoals and 3 subgoals verifying that
<< 'E1['x; 'y] >> is an equivalence relation.
If the conclusion is of the form
<< quot x1, y1: 'A1 // 'E1['x1; 'y1]
= quot x2, y2: 'A2 // 'E2['x2; 'y2]
in univ[i:l] >>,
(selT 1 (dT 0)) creates 2 reflexive equality subgoals, one non-reflexive
equality subgoal, and 2 subgoals verifying that << 'E1['x; 'y] >> is
equivalent to << 'E2['x; 'y] >>. Note that you don't have to prove
that the relations are equivalence relations; the reflexive equality
subgoals take care of that. This alternate form is more powerful than
the above rule; it proves quotient types equal if the predicates are
equivalent (in the sense of iff), whereas the original requires that
the predicates be equal.
If the conclusion is of the form
<< "type"{.quot x, y: 'A // 'E['x; 'y]} >>,
(dT 0) creates 2 typehood subgoals and 3 subgoals verifying that
<< 'E['x; 'y] >> is an equivalence relation.
If the conclusion is of the form << quot x, y: 'A // 'E['x; 'y] >>,
(dT 0) creates a subgoal << 'A >> (and a well-formedness subgoal).
If the conclusion is of the form
<< 'a1 = 'a2 in quot x, y: 'A // 'E['x; 'y] >>,
(dT 0) creates a subgoal << 'a1 = 'a2 in 'A >> (and a well-formedness
subgoal). (XXX This rule is inaccessible due to being overridden by
the following rule.)
If the conclusion is of the form
<< 'a1 = 'a2 in quot x, y: 'A // 'E['x; 'y] >>,
(dT 0) creates the subgoal << 'E['a1; 'a2] >> and 3 well-formedness
subgoals.
If the conclusion is of the form
<< 'l IN (quot x, y: 'A // 'E['x; 'y]) >>,
(dT 0) creates a membership subgoal and a well-formedness subgoal.
If the n'th hypothesis is of the form
<< a: quot x, y: 'A // 'E['x; 'y] >>, and the conclusion is an
equality,
(dT n) creates an equality subgoal and a well-formedness subgoal, and
thins. XXX There are two versions of this rule (varying in the
location of some added hypotheses); I believe that one variant is
inaccessible because of the other, and that both are inaccessible due
to the following rule.
If the n'th hypothesis is of the form
<< x: 'a1 = 'a2 in quot x, y: 'A // 'E['x; 'y] >>,
(dT n) adds a new hypothesis << v: hide('E['a1; 'a2]) >> and thins.
This file adds to the subtypeT tactic.
subtypeT proves that << quot x1, y1: 'A1 // 'E1['x1; 'y1] >> is a
subtype of << quot x2, y2: 'A2 // 'E2['x2; 'y2] >> by proving << 'A1 >>
is a subtype of << 'A2 >>.
----------------------------------------
itt_list:
new terms:
nil
cons{'a; 'b}
list{'a}
list_ind{'e; 'base; h, t, f. 'step['h; 't; 'f]}
* reduce_listindNil : conv
Rewrites << list_ind{nil; 'base; h, t, f. 'step['h; 't; 'f]} >> to
<< 'base >>.
* reduce_listindCons : conv
Rewrites << list_ind{('u :: 'v); 'base; h, t, f. 'step['h; 't; 'f]} >>
to << 'step['u; 'v; list_ind{'v; 'base; h, t, f. 'step['h; 't; 'f]}] >>.
This file adds to the reduceTopC conversion.
It adds the reduce_listindNil and reduce_listindCons conversions.
This file adds to the dT tactic.
If the conclusion is of the form << "type"{list{'A}} >>,
(dT 0) creates a typehood subgoal.
If the conclusion is of the form << list{'A} = list{'B} in univ[i:l] >>,
(dT 0) creates an equality subgoal.
If the conclusion is of the form << list{'A} >>,
(dT 0) creates a subgoal << "type"{'A} >> (with extract term << nil >>).
If the conclusion is of the form << nil IN list{'A} >> or
(dT 0) creates a subgoal << "type"{'A} >>.
If the conclusion is of the form
<< cons{'u1; 'v1} = cons{'u2; 'v2} in list{'A} >>,
(dT 0) creates 2 equality subgoals.
If the n'th hypothesis is of the form << l: list{'A} >>,
and the conclusion is of the form << 'C['l] >>,
(dT 0) creates two subgoals. The first has conclusion << 'C[nil] >>;
the second has extra arguments << u: 'A; v: list{'A}; w: 'C['v] >> and
conclusion << 'C['u::'v] >>.
If the conclusion is of the form
<< list_ind{'e1; 'base1; u1, v1, z1. 'step1['u1; 'v1; 'z1]}
= list_ind{'e2; 'base2; u2, v2, z2. 'step2['u2; 'v2; 'z2]}
in 'T >>,
(withTermsT [<< lambda{l. 'B['l]} >>; << list{'A} >>] (dT 0)) creates
3 equality subgoals. Here << 'B['e1] >> must be << 'T >> and
<< list{'A} >> must be the common type of << 'e1 >> and << 'e2 >>.
If the n'th hypothesis is of the form
<< x: nil = cons{'h; 't} in list{'T} >> or
<< x: cons{'h; 't} = nil in list{'T} >>,
(dT n) succeeds with no subgoals.
This file adds to the subtypeT tactic.
subtypeT proves that << list{'A} >> is a subtype of << list{'B} >> by
proving that << 'A >> is a subtype of << 'B >>.
----------------------------------------
itt_list2:
new terms:
is_nil{'l}
append{'l1; 'l2}
ball2{'l1; 'l2; x, y. 'b['x; 'y]}
assoc{'eq; 'x; 'l; 'y. 'b['y]; 'z}
rev_assoc{'eq; 'x; 'l; y. 'b['y]; 'z}
map{'f; 'l}
fold_left{'f; 'v; 'l}
length{'l}
nth{'l; 'i}
replace_nth{'l; 'i; 'v}
* unfold_is_nil : conv
Rewrites << is_nil{'l} >> to << list_ind{'l; btrue; h, t, g. bfalse} >>.
* unfold_append : conv
Rewrites << append{'l1; 'l2} >> to << list_ind{'l1; 'l2; h, t, g. 'h :: 'g} >>.
* unfold_ball2 : conv
Rewrites << ball2{'l1; 'l2; x, y. 'b['x; 'y]} >> to
<< (list_ind{'l1; lambda{z. list_ind{'z; btrue; h, t, g. bfalse}};
h1, t1, g1. lambda{z. list_ind{'z; bfalse;
h2, t2, g2. band{'b['h1; 'h2]; .'g1 't2}}}} 'l2) >>.
* unfold_assoc : conv
Rewrites << assoc{'eq; 'x; 'l; y. 'b['y]; 'z} >> to
<< list_ind{'l; 'z; h, t, g.
spread{'h; u, v.
ifthenelse{.'eq 'u 'x; 'b['v]; 'g}}} >>.
* unfold_rev_assoc : conv
Rewrites << rev_assoc{'eq; 'x; 'l; y. 'b['y]; 'z} >> to
<< list_ind{'l; 'z; h, t, g.
spread{'h; u, v.
ifthenelse{.'eq 'v 'x; 'b['u]; 'g}}} >>.
* unfold_map : conv
Rewrites << map{'f; 'l} >> to
<< list_ind{'l; nil; h, t, g. cons{.'f 'h; 'g}} >>.
* unfold_fold_left : conv
Rewrites << fold_left{'f; 'v; 'l} >> to
<< list_ind{'l; lambda{v. 'v}; h, t, g. lambda{v. 'g ('f 'h 'v)}} 'v >>.
* unfold_nth : conv
Rewrites << nth{'l; 'i} >> to
<< (list_ind{'l;
it;
u, v, g. lambda{j. ifthenelse{eq_int{'j; 0};
'u;
.'g ('j -@ 1)}}} 'i) >>.
* unfold_replace_nth : conv
Rewrites << replace_nth{'l; 'i; 't} >> to
<< (list_ind{'l;
nil;
u, v, g. lambda{j. ifthenelse{eq_int{'j; 0};
cons{'t; 'v};
cons{'u; .'g ('j -@ 1)}}}} 'i) >>
* unfold_length : conv
Rewrites << length{'l} >> to
<< list_ind{'l; 0; u, v, g. 'g +@ 1} >>.
* fold_is_nil, fold_append, fold_ball2, fold_assoc, fold_rev_assoc,
fold_map, fold_fold_left, fold_nth, fold_replace_nth, fold_length : conv
The opposites of the above conversions.
This file adds to the reduceTopC conversion.
It reduces terms of the following forms in the obvious way:
<< is_nil{nil} >>,
<< is_nil{cons{'h; 't}} >>,
<< append{cons{'h; 't}; 'l} >>,
<< append{nil; 'l} >>,
<< ball2{nil; nil; x, y. 'b['x; 'y]} >>,
<< ball2{nil; cons{'h; 't}; x, y. 'b['x; 'y]} >>,
<< ball2{cons{'h; 't}; nil; x, y. 'b['x; 'y]} >>,
<< ball2{cons{'h1; 't1}; cons{'h2; 't2}; x, y. 'b['x; 'y]} >>,
<< assoc{'eq; 'x; nil; v. 'b['v]; 'z} >>,
<< assoc{'eq; 'x; cons{pair{'u; 'v}; 'l}; y. 'b['y]; 'z} >>,
<< rev_assoc{'eq; 'x; nil; v. 'b['v]; 'z} >>,
<< rev_assoc{'eq; 'x; cons{pair{'u; 'v}; 'l}; y. 'b['y]; 'z} >>,
<< map{'f; nil} >>,
<< map{'f; cons{'h; 't}} >>,
<< fold_left{'f; 'v; nil} >>,
<< fold_left{'f; 'v; cons{'h; 't}} >>,
<< length{nil} >>,
<< length{cons{'u; 'v}} >>,
<< nth{cons{'u; 'v}; 'i} >>, and
<< replace_nth{cons{'u; 'v}; 'i; 't} >>.
This file adds to the dT tactic.
If the conclusion is of the form << is_nil{'l} IN bool >>,
(withT t (dT 0)) changes it to << 'l IN list{t} >>.
If the conclusion is of the form << append{'l1; 'l2} IN list{'T} >>,
(dT 0) creates 2 membership subgoals.
If the conclusion is of the form
<< ball2{'l1; 'l2; x, y. 'b['x; 'y]} IN bool >>,
(withTermsT [t1; t2] (dT 0)) creates subgoals
<< 'l1 IN list{t1} >> and << 'l2 IN list{t2} >> (and 3
well-formedness subgoals).
If the conclusion is of the form
<< assoc{'eq; 'x; 'l; v. 'b['v]; 'z} IN 'T >>
(withTermsT [t1; t2] (dT 0)) creates membership subgoals for
<< 'eq >>, << 'x >>, << 'l >>, << 'b['a] >>, and << 'z >>, and a
typehood subgoal for t2. Here << 'l >> must have type
<< list{(t1 * t2)} >>.
If the conclusion is of the form
<< rev_assoc{'eq; 'x; 'l; v. 'b['v]; 'z} IN 'T >>,
(withTermsT [t1; t2] (dT 0)) creates membership subgoals for
<< 'eq >>, << 'x >>, << 'l >>, << 'b['a] >>, and << 'z >>, and a
typehood subgoal for t1. Here << 'l >> must have type
<< list{(t1 * t2)} >>.
If the conclusion is of the form
<< map{'f; 'l} IN list{'T2} >>,
(withT t (dT 0)) creates 2 membership subgoals and 2 typehood
subgoals. Here << 'l >> must have type << list{t} >>.
XXX
If the conclusion is of the form
<< fold_left{'f; 'v; 'l} IN 'T2 >>,
(withTermsT [t1; t2] (dT 0)) creates 3 membership subgoals and 2
typehood subgoals. Here << 'l >> must have type << list{t1} >>, and
the second argument is silly.
If the conclusion is of the form << length{'l} IN int >>,
(withT t (dT 0)) creates a subgoal << 'l IN list{t} >> (and a
well-formedness subgoal).
If the conclusion is of the form << nth{'l; 'i} IN 'T >>,
(dT 0) creates subgoals stating that << 'T >> is a type, << 'l >> is
of type << list{'T} >>, and that << 'i >> is in range.
If the conclusion is of the form
<< replace_nth{'l; 'i; 't} IN list{'T} >>,
(dT 0) creates subgoals stating that << 'T >> is a type, << 'l >> is
of type << list{'T} >>, << 'i >> is in range, and << 't >> is of type
<< 'T >>.
# The following "commented-out" paragraphs are no longer correct;
# I'm leaving them in in hopes that the descriptions of the type
# inference which used to be done and is not done any more will
# inspire somebody to add the type inference back in.
#
#If the conclusion is of the form << is_nil{'l} IN bool >>,
#(atT t (dT 0)) changes it to << 'l IN t >> (t must be of the
#form << list{'T} >>). (If you don't specify a type with atT, dT will
#try to infer the type of << 'l >>.)
#
#If the conclusion is of the form << append{'l1; 'l2} IN list{'T} >>,
#(dT 0) creates subgoals << 'l1 IN list{'T} >> and
#<< 'l2 IN list{'T} >>.
#
#If the conclusion is of the form
#<< ball2{'l1; 'l2; x, y. 'b['x; 'y]} IN bool >>,
#(dT 0) will try to infer the types of the members of << 'l1 >> and
#<< 'l2 >>, coming up with << T1 >> and << T2 >>. (If it can infer
#types for only one of << 'l1 >> and << 'l2 >>, it will assume that
#they both have the same type.) It will then create subgoals (one with
#extra hypotheses) << "type"{T1} >>, << "type"{T2} >>,
#<< 'l1 IN list{T1} >>, << 'l2 IN list{T2} >>, and
#<< u: T1; v: T2 >- 'b['u; 'v] IN bool >>. You can use
#(atT t (dT 0)) to use << t >> as the type for both << T1 >> and
#<< T2 >> (but there's no way to specify two different types).
#
#If the conclusion is of the form
#<< assoc{'eq; 'x; 'l; v. 'b['v]; 'z} IN 'T >>,
#(dT 0) will try to infer the type of 'l (which must be of the form
#<< T1 * T2 >>). It will then create subgoals (one with an extra
#hypothesis) << "type"{T2} >>, << 'eq IN (T1 -> T1 -> bool)} >>,
#<< 'x IN T1 >>, << 'l IN list{(T1 * T2) >>,
#<< 'z IN 'T >>, and << z: T2 >- 'b['z] IN 'T >>. You can
#specify the type of << 'l >> with atT. Conclusions of the form
#<< rev_assoc{'eq; 'x; 'l; v. 'b['v]; 'z} IN 'T >> are handled
#similarly.
----------------------------------------
itt_derive:
* applyT : term -> int -> tactic
(applyT << f a >> 0) tries to infer the type of << f >> to get << T >>,
which must be a "dfun", "fun", "all", or "implies" term; say
<< x: A -> B['x] >>. The conclusion is of the form << 'C[f a] >>.
The tactic adds a hypothesis and changes the conclusion to get
<< y: 'B[a] >- 'C['y] >> (and adds several other subgoals).
* anyApplyT : term list -> int -> tactic
(anyApplyT tl 0) applies (applyT t 0) on the first member << t >> of
tl for which it succeeds.
* autoApplyT : int -> tactic
(autoApplyT 0) finds every application in the conclusion for which the
function is a declared variable of a hypothesis (except that it does
not descend into the types of equality terms). It then calls
anyApplyT with this list.
----------------------------------------
itt_prop_decide:
* propDecideT : tactic
This is a decision procedure for propositional logic.
----------------------------------------
itt_record_renaming
new terms:
rename[a:t, b:t]{'r}
rename_add_mul{'add}
rename_mul_add{'mul}
as_additive{'r}
Added to reduceC:
rename[a:t, b:t]{rcrd[a:t]{'x;'r}} <--> rcrd[b:t]{'x;rename[a:t, b:t]{'r}}
rename[a:t, b:t]{rcrd[b:t]{'x;'r}} <--> rcrd[a:t]{'x;rename[a:t, b:t]{'r}}
rename[a:t, b:t]{rcrd[c:t]{'x;'r}} <--> rcrd[c:t]{'x;rename[a:t, b:t]{'r}} if c<>a,b
rename[a:t, b:t]{ rcrd } <--> rcrd
field[a:t]{rename[a:t, b:t]{'r}} <--> field[b:t]{'r}
field[b:t]{rename[a:t, b:t]{'r}} <--> field[a:t]{'r}
field[c:t]{rename[a:t, b:t]{'r}} <--> field[c:t]{'r} if c<>a,b
rename[a:t, a:t]{'r} <--> 'r
rename[a:t, b:t]{rename[b:t, a:t]{'r}} <--> 'r
field[c:t]{rename_mul_add{'r}} <--> ...
field[c:t]{rename_add_MIL{'r}} <--> ...
rename_mul_add{ rename_add_mul{'add} } <--> 'add
rename_add_mul{ rename_mul_add{ 'mul }} <--> 'mul
* renameFieldC <>
replaces r by <> in the immediate subterms of the term and then do @em{exactly one} reduction on the term.
(It fails if it can not do the reduction).
For example:
<> --> <>
<> --> <>
<> --> <> if c<> a,b
* renameFieldT term = rwhAll (renameFieldC term)
* foldAdditiveC term = allSubThenC (use_as_additive term) (reduceTopC)
replaces $r$ by rename_mul_add{ as_additive{'r} } in the immediate subterms
and then do @em{exactly one} reduction.
For example foldAdditiveC <<'r>> replaces <<'r^"+">> by <> and <<'r^car>> by <>
* unfoldAdditiveC term =allSubThenC unfold_as_additive (reduceTopC)
oposite to foldAdditiveC
* foldAdditiveT term = rwhAll (foldAdditiveC term)
* unfoldAdditiveT term = rwhAll (unfoldAdditiveC term)
* useAdditiveWithT term tac = foldAdditiveT term thenT tac thenT unfoldAdditiveT term
* useAdditiveWithAutoT term = useAdditiveWithT term autoT thenT autoT
----------------------------------------
itt_fset:
new terms:
fset{'eq; 'T}
feset{'eq; 'T}
fempty
fsingleton{'x}
funion{'eq; 't1; 't2}
fisect{'eq; 't1; 't2}
fsub{'eq; 't1; 't2}
fisempty{'t1}
fmember{'eq; 'x; 't1}
fsubseteq{'eq; 's1; 's2}
fequal{'eq; 't1; 't2}
fequalp{'eq; 'T}
fsquash{'eq; 's}
fball{'s; x. 'b['x]}
fbexists{'s; x. 'b['x]}
fall{'eq; 'T; 's; x. 'b['x]}
fexists{'eq; 'T; 's; x. 'b['x]}
foflist{'l}
* unfold_fcompare : conv
Rewrites << fcompare{'eq; 'x; 'y} >> to << ('eq 'x 'y) >>.
* unfold_fequalp : conv
Rewrites << fequalp{'eq; 'T} >> to
<< ('eq IN ('T -> 'T -> bool))
& (all x: 'T. "assert"{.fcompare{'eq; 'x; 'x}})
& (all x: 'T. all y: 'T.
("assert"{fcompare{'eq; 'x; 'y}} => "assert"{fcompare{'eq; 'y; 'x}}))
& (all x: 'T. all y: 'T. all z: 'T.
("assert"{fcompare{'eq; 'x; 'y}} =>
"assert"{fcompare{'eq; 'y; 'z}} =>
"assert"{fcompare{'eq; 'x; 'z}}))) >>.
* unfold_fset : conv
Rewrites << fset{'eq; 'T} >> to
<< (quot x, y : list{'T} // "assert"{fequal{'eq; 'x; 'y}}) >>.
* unfold_fempty : conv
Rewrites << fempty >> to << nil >>.
* unfold_fsingleton : conv
Rewrites << fsingleton{'x} >> to << cons{'x; nil} >>.
* unfold_funion : conv
Rewrites << funion{'eq; 's1; 's2} >> to << append{'s1; 's2} >>.
* unfold_fisect : conv
Rewrites << fisect{'eq; 's1; 's2} >> to
<< list_ind{'s1; nil; h, t, g. ifthenelse{fmember{'eq; 'h; 's2};
cons{'h; 'g};
'g}} >>.
* unfold_fsub : conv
Rewrites << fsub{'eq; 's1; 's2} >> to
<< list_ind{'s1; nil; h, t, g. ifthenelse{fmember{'eq; 'h; 's2};
'g;
cons{'h; 'g}}} >>.
* unfold_fmember : conv
Rewrites << fmember{'eq; 'x; 's1} >> to
<< list_ind{'s1; bfalse; h, t, g. bor{.fcompare{'eq; 'x; 'h}; 'g}} >>.
* unfold_fisempty : conv
Rewrites << fisempty{'s1} >> to
<< list_ind{'s1; btrue; h, t, g. bfalse} >>.
* unfold_fsubseteq : conv
Rewrites << fsubseteq{'eq; 's1; 's2} >> to
<< list_ind{'s1; btrue; h, t, g. band{fmember{'eq; 'h; 's2}; 'g}} >>.
* unfold_fequal : conv
Rewrites << fequal{'eq; 's1; 's2} >> to
<< band{fsubseteq{'eq; 's1; 's2}; fsubseteq{'eq; 's2; 's1}} >>.
* unfold_fsquash : conv
Rewrites << fsquash{'eq; 's1} >> to
<< list_ind{'s1; nil; h, t, g. ifthenelse{fmember{'eq; 'h; 't};
'g;
cons{it; 'g}}} >>.
* unfold_fball : conv
Rewrites << fball{'s; x. 'b['x]} >> to
<< list_ind{'s; btrue; x, t, g. band{'b['x]; 'g}} >>.
* unfold_fbexists : conv
Rewrites << fbexists{'s; x. 'b['x]} >> to
<< list_ind{'s; bfalse; x, t, g. bor{'b['x]; 'g}} >>.
* unfold_fall : conv
Rewrites << fall{'eq; 'T; 's; x. 'b['x]} >> to
<< all x: { y: 'T | "assert"{fmember{'eq; 'y; 's}} }. 'b['x] >>.
* unfold_fexists : conv
Rewrites << fexists{'eq; 'T; 's; x. 'b['x]} >> to
<< exst x: { y: 'T | "assert"{fmember{'eq; 'y; 's}} }. 'b['x] >>.
* unfold_feset : conv
Rewrites << feset{'eq; 'T} >> to
<< (quot x, y: 'T // "assert"{fcompare{'eq; 'x; 'y}}) >>.
* unfold_foflist : conv
Rewrites << foflist{'l} >> to << 'l >>.
* fold_fequalp, fold_fset, fold_fempty, fold_fsingleton, fold_fisect,
fold_fsub, fold_fmember, fold_fisempty, fold_fsubseteq, fold_fequal,
fold_fsquash, fold_fball, fold_fbexists, fold_feset, fold_fall,
fold_fexists, fold_foflist : conv
The opposites of the above conversions.
# The following topvals are no longer available. I'm leaving
# the descriptions here because the source code is still in
# itt_fset.ml .
#
#* d_fsubseteq_consT : tactic
#(withT t (d_fsubseteq_consT)) reduces a conclusion of the form
#<< "assert"{fsubseteq{'eq; 'l1; cons{'u; 'l2}}} >> to
#<< "assert"{fsubseteq{'eq; 'l1; 'l2}} >> (plus some other subgoals).
#Here t must be the type of elements of << 'l1 >> and << 'l2 >>, and
#the type of << 'u >>.
#
#* fmember_subst_elementT : term -> tactic
#(fmember_subst_elementT y) reduces a conclusion of the form
#<< "assert"{fmember{'eq; 'x; 'l}} >> to subgoals
#<< "assert"{fmember{'eq; y; 'l}} >> and
#<< "assert"{fcompare{'eq; 'x; y}} >> (and some other subgoals). The
#tactic tries to infer the list element type by inferring the type of
#<< 'x >>; you can specify the type explicitly with atT.
#
#* fsub_nonmemberT : tactic
#fsub_nonmemberT reduces a conclusion of the form
#<< 's = fsub{'eq; 's; fsingleton{'u}} in list{'T} >> to
#<< "assert"{bnot{fmember{'eq; 'u; 's}}} >> (and some other subgoals).
#The tactic tries to infer the list element type by inferring the type
#of << 's >>; you can specify the type explicitly with atT.
#
#* fsquash_memberT : tactic
#fsquash_memberT reduces a conclusion of the form
#<< fsquash{'eq; 's} =
# cons{it; fsquash{'eq; fsub{'eq; 's; fsingleton{'u}}}}
# in list{unit} >> to
#<< "assert"{fmember{'eq; 'u; 's}} >> (and some other subgoals).
#The tactic tries to infer the list element type by inferring the type
#of << 's >>; you can specify the type explicitly with atT.
#
#* fcompareRefT : tactic
#fcompareRefT breaks down a conclusion of the form
#<< "assert"{fcompare{'eq; 'x; 'x}} >>. The tactic tries to infer the
#type of << 'x >>; you can specify the type explicitly with atT.
#
#* fcompareSymT : tactic
#fcompareSymT reduces a conclusion of the form
#<< "assert"{fcompare{'eq; 'x; 'y}} >> to
#<< "assert"{fcompare{'eq; 'y; 'x}} >> (and some other subgoals). The
#tactic tries to infer the type of << 'x >> and << 'y >>; you can
#specify the type explicitly with atT.
#
#* fcompareTransT : term -> tactic
#(fcompareTransT t) reduces a conclusion of the form
#<< "assert"{fcompare{'eq; 'x; 'y}} >> to
#<< "assert"{fcompare{'eq; 'x; t}} >> and
#<< "assert"{fcompare{'eq; t; 'y}} >> (and some other subgoals). The
#tactic tries to infer the type of << 'x >> and << 'y >>; you can
#specify the type explicitly with atT.
#
#* testT : tactic
#Internal testing only.
#
#* dupRT : tactic -> int -> tactic
#(dupRT tac i) creates i+1 copies of the current goal, then applies tac
#to each.
This file adds to the reduceTopC conversion.
It reduces terms of the following forms in the obvious way:
<< fmember{'eq; 'x; nil} >>,
<< fmember{'eq; 'x; cons{'h; 't}} >>,
<< fmember{'eq; 'x; fsingleton{'y}} >>,
<< fsubseteq{'eq; nil; 'l} >>,
<< fsubseteq{'eq; cons{'h; 't}; 'l} >>,
<< funion{'eq; nil; 's} >>,
<< funion{'eq; cons{'h; 't}; 's} >>,
<< fisect{'eq; nil; 's} >>,
<< fisect{'eq; cons{'h; 't}; 's} >>,
<< fsub{'eq; nil; 's} >>,
<< fsub{'eq; cons{'h; 't}; 's} >>,
<< fsquash{'eq; nil} >>,
<< fsquash{'eq; cons{'h; 't}} >>,
<< fball{nil; x. 'b['x]} >>,
<< fball{cons{'h; 't}; x. 'b['x]} >>,
<< fbexists{nil; x. 'b['x]} >>, and
<< fbexists{cons{'h; 't}; x. 'b['x]} >>.
# This file does not add to the dT tactic. I have left the following
# partial description of what this file used to do to the dT tactic,
# because the code is still in itt_fset.ml .
#
#If the conclusion is of the form << fcompare{'eq; 'x; 'y} IN bool >>,
#(dT 0) breaks it down into subgoals. It tries to infer the type of
#<< 'y >> and << 'x >>, but you can specify the type explicitly with atT.
#
#If the conclusion is of the form
#<< fmember{'eq; 's1; 's2} IN bool >>, << fsubseteq{'eq; 's1; 's2} IN bool >>, or
#<< fequal{'eq; 's1; 's2} IN bool >>,
#(dT 0) breaks it down into subgoals. It tries to infer the type of
#<< 's2 >> and << 's1 >>, but you can specify the type explicitly with
#atT. You can specify either a "fset" or a "list" type.
#
#If the conclusion is of the form
#<< fball{'s; x.'b['x]} IN bool >> or
#<< fbexists{'s; x.'b['x]} IN bool >>,
#(dT 0) breaks it down into subgoals. It tries to infer the type of
#<< 'b['x] >>, but you can specify the type explicitly with
#atT. You can specify either a "fset" or a "list" type.
#
#If the conclusion is of the form
#<< fsquash{'eq; 's} IN list{unit} >>,
#(dT 0) breaks it down into subgoals. It tries to infer the type of
#<< 's >>, but you can specify the type explicitly with
#atT. You can specify either a "fset" or a "list" type.
#
#If the conclusion is of one of the forms
#<< funion{'eq; 's1; 's2} IN list {'T} >>,
#<< fisect{'eq; 's1; 's2}} IN list {'T} >>,
#<< fsub{'eq; 's1; 's2} IN list {'T} >>, << fsingleton{'x}} IN list {'T} >>,
#<< fempty IN list {'T} >>, << funion{'eq; 's1; 's2}} IN fset{'eq; 'T} >>,
#<< fisect{'eq; 's1; 's2} IN fset{'eq; 'T} >>,
#<< fsub{'eq; 's1; 's2} IN fset{'eq; 'T} >>,
#<< fsingleton{'x} IN fset{'eq; 'T} >>, << fempty IN fset{'eq; 'T} >>, or
#<< foflist{'l} IN fset{'eq; 'T} >>,
#(dT 0) breaks it down into subgoals.
#
#I left off documenting at the definition of d_fsubseteq_assertT...
----------------------------------------
itt_int_base
Introduces additive ordered integers with induction:
int - type of integers
+@,-@(sub), minus - addition, subtraction and unary minus
ind - recursion over integers
beq_int - boolean equality over integers
lt_bool - boolean less-relation
< - propositional less-relation, defined as assert(lt_bool)
Integers are defined to be canonical, i.e. equality is computational
meaning that any integer may be replaced with equal in any context.
That's why we use rewrites for most of axioms.
In this module we define group properties of addition;
irreflexivity, transitivity, descreteness of <-rel., etc.
No high-level tactics defiend here, see itt_int_arith for them.
----------------------------------------
itt_int_ext
Continues definition of integers by multiplicative properties and
other common order relations:
*@ - multiplication
/@ - division, defined recursively
%@ - remainder, defined recursively
<=, >=, >, <> - boolean and propositional versions of remaining order relations
No high-level tactics defiend here, see itt_int_arith for them.
----------------------------------------
itt_int_arith
normalizeC - converts any polynomial (it may actually contain any functional
symbols, they will be treated as variables) to its canonical form
arithT - proves simple systems of inequalities (linear fragment without
monotonicity, i.e. does not use a**** a+c**