Simplify AST types, parsing rules and pp of tactics that had
'that is equivalent to' or 'or equivalently'
Modify grafiteEngine accordingly
Simplify the signature and the code of the implementations of tactics
that had 'that is equivalent to' or 'or equivalently'
A new "volatile_hypo" key is added to the parameter list of the currest
stack level to indicate that the beta rewriting should happen on that
hypothesis, instead of the thesis
Modify beta_rewrite accordingly
Add some "obvious" terms to the given candidates for the automation
(such as refl, sym_eq, trans_eq, etc.)
The weakening of the automation is now only partial: the second flag for
weakening is off. Setting it on makes theorem proving pretty impossible
with the declarative fragment.
Add a BetaRewritingStep tactic, for multiple 'or equivalently'
statements in theorems proofs
Remove old code
Add a key-value list to the tiny-cals stack (parameters list) for
context related infos. Can be used as a general purpose store for
key-value pairs
Adapt code that works on the stack to work with the new parameter list
Add function to add and retrieve key-value pairs to the parameters list
Add the concept of volatile-context: they are contexts that are cleared
after the application of some tactics. E.g., the context for a
beta_rewriting (sequence of 'or equivalently') is a volatile context, as
any tactic breaks the chain
Add a function to clear volatile parameters from the paramters list
Add a case in extract_first_goal_from_status for the case where the
stack is empty
Make the tactics that make use of distribute High tactics
Reimplement the dot tac on top of the stack to handle branching. This
makes use of the second iterator list of the stack
Add a "done_continuation" function that checks whether it needs to dot
or recursively merge branches after a done statement
Add a function to push goals from the focus iterator list of the
previous level on the stack to the second iteretaor list of the current
level
Change conclude and obtain to use a volatile context to obligate the
user to only use = inside it
Change the add_names_to_goals function to use the stack instead of the
metasenv directly
Add a unfocus_branch_tac to unfocus from goals in a stack level (useful
for cases and induction)
Change induction and cases to use a context to obligate the user to use
case only inside it. Furthermore, the new stack based branching for
declarative tactics obligates the user to only switch between cases of
the last level
Change induction and cases to start without focusing on any goal and
without automatically focusing on the next goal after a done. The user
is compelled to use case to switch between each case
Change the case to only change case when the current case has been dealt
with
Add support for proving cases in a different order
Add some debug pretty printing methods and tactics.
Add a tactic to add names to metasenv goals from a given constructor
list
Modify "we_proceed_by_induction_on" to gather info on the inductive type of
the term being eliminated, apply the right constructor to the right
number of Implicit arguments, and name the new open goals
Modify "we_proceed_by_cases_on" in an analogous way to
"we_proceed_by_induction_on"
Add a tactic to focus on a given case, if present, with helper functions
for it
Modify case to search for the given case and focus on it
Modify indtyinfo to memorize also the costructor list of the inductive
type
Remove a useless if-then-else in index_local_equations2
Remove some old code, comments and trailing spaces
Changes to declarative tactics, implementation of equality chain
Fix type for RewritingStep, add a type for Print Stack (a debug tool)
Fix PP for RewritingStep, generalized just_to_tactic_just for the type
[>`Auto of auto_params | `Term of NotationPt.term]
Add parsing rule for print_stack, fix parsing rules for obtain, conclude
e =
Fix indentation for declarative.ml
Change mk_just to return a tactic (instead of a lowtactic)
Modify extract_first_goal_from_status to take the first goal from the
stack, instead of the metasenv
Change assume, suppose, andelim and existselim to use distribute_tac
Add a mustdot function to check whether there's the need to call the
dot_tactic at the end. The dot tactic is used to focus on a single goal
at the time when there are multiple open goals
Change bydone to use the dot tactic to switch between multiple goals
Modify we_need_to_prove to use the dot_tac to focus on a single goal
Add a type_of_tactic_term function to extract the type of a tactic_term
(used in RewritingStep)
Implement rewritingstep, which covers conclude and =; obtain is in the
works
Implement print_stack, for debug purposes (prints the stack to stderr)
Modify declarative's signature to add the new functions
Add firs_tac to nTactic's signature
Change auto_lowtac's signature to return a tactic
Correct natural_deduction.ma for the new version. Had to change some
\forall with \Pi
Change auto_params in grafiteAst.ml from being abstract on the 'term list
to being concretized to nterm list. Modify type just accordingly. Modify ntactic
types accordingly.
Add ExistsElim, AndElim, RewritingStep, Thesisbecomes types to ntactic.
Add pretty printing for ExistsElim, AndElim, RewritingStep, Thesisbecomes.
Add calls in grafite engine for the implementation of ExistsElim, AndElim, Thesisbecomes.
Add parsing rule for the "let x := t" tactic. It uses the NLetIn
ntactic.
Add parsing rules for Thesisbecomes and Rewritingstep (conclude, obtain
and =).
Modify mk_just to use the new auto_lowtac entry point for automation for
LCF-like tactics.
Remove same_type function in declarative.ml.
Add are_convertible function in declarative that uses beta-conversion.
Add a lambda_abstract tactic that abstracts the common parts of suppose
and assume. Add 3 Exception types for this tactic to handle error
situations. Modify assume and suppose accordingly
Add assert_tac that verifies that a given term is the same as the
conclusion and that two given types are beta-convertible, if a second
type is given. If all checks pass a continuation is exec'd, otherwise an
exception is raised.
Modify we_need_to_prove, by_just_we_proved to use assert_tac.
Add implementation of thesisbecomes.
Add implementation of existselim and andelim.
Modify declarative signature to add the new tactics.
Add a flag to index_local_equations and index_local_equations2 to
inhibit the use of global candidates. Modify all the functions that call
these two functions and the calls to those functions accordingly
(auto_main, do_something, top_cache, intros, auto_clusters)
Add a flag to auto_tac' to specify whether to use local candidates or
not. Modify the part where the local cands are calculated to check the
flag before proceeding.
Add auto_params to nnAuto.
Modify auto_tac to auto_tac' which takes the candidates to use
explicitly as a parameter and two flags that indicate whether to use
local candidates and whether to use only the given candidates.
Add a candidates_from_ctx function to calculate the candidates in a
given context.
Add a auto_lowtac entry point for LCF-like tactics.
Modify nnAuto signature to use auto_params instead of its explicit
version (nterm list * (string * string) list).
Add new "keywords" to matita.lang.
Add debug prints for a bug where the program would freeze. (They can
probably be removed)
+ modification in cnv allows to improve cnv_cpm_trans_lpr_aux
+ modification in lsubv allows to prove its transitivity
+ one lemma added to the arithmetic library
+ advances on the support for models
+ tentative definition of shift (incomplete because unary binders are missing in terms)
+ minor updates and corrections
notations of existentials must differ according to arity of the involved predicates
+ porting to the updated version of xoa
+ one addition in predefined virtuals
Ferruccio Guidi [Thu, 29 Mar 2018 22:28:23 +0000 (00:28 +0200)]
decentralizing core notation
centralized core notation (one single file) has two disadvantages:
- when some core notation is added the whole "world" must be recompiled
- unused core notation loaded in the parser gets in the way when defining contrib-specific notation
by defining core notation on a "one notation per file" basis:
+ every contrib file can load just the needed notation
+ sharing is possible as before in that two contrib files can load the same notation file
decentralalization will occur is stages:
this is the first stage meant to solve some issues in
+ lambdadelta (! blocked by fact)
+ certifiedRev (o{} blocked by compose, comprehension, singl, subset)
projects / helm.git / log