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