Add last declarative tactics, modify rewriting tactics

Add types for induction and case analysis to grafiteAst. Add new types
for obtain and conclude

Add pp code for induction, case, obtain, conclude

Add calls in grafiteEngine for induction, case, obtain, conclude

Add parsing rules for induction, case, obtain, conclude

Rename a function for code clarity

Add function to swap two goals on the stack (useful for obtain)

Add a conclude function that checks that the given term is the lhs of
the current goal

Add a obtain function that starts an equality chain beginning with the
given term in a new goal

Modify rewriting step to only handle single equality chains steps

Add implementation for induction and case.

Add signatures for induction, case, conclude, obtain

Add keywords to matita.lang for induction, case, conclude, obtain

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

Many changes

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)

Add drafts for some tactics

Add drafts for assume, suppose, we_need_to_prove.

Add a just type to handle justfications in tactics.

Add drafts for the by_done and by_just_we_proved tactics.

Everything needs testing

Partially restore the suppose tactic

Add a type for the suppose tactic in GrafiteAst

Add pretty printing code for the suppose tactic

Add a parsing rule for the suppose tactic in GrafiteParser

Add a call in to the suppose tactic in GrafiteEngine

Add code for the suppose tactic in Declarative

Add syntax highlight tag for the suppose tactic

Partially restore the assume tactic

Add a type for the assume tactic in GrafiteAst

Add pretty printing code for the assume tactic

Add a parsing rule for the assume tactic in GrafiteParser

Add a call in to the assume tactic in GrafiteEngine

Add a file for the declarative tactics to the ng_tactics module

Add code for the assume tactic in Declarative

Add syntax highlight tag for the assume tactic

Add the exact_tac signature to the interface file of nTactics

supplementary files for web site

+ css file name corrected

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

some supplementary items for web site

one icon and on css file

presentation upload

A newborn in the λδ family: introducing λδ-2B

update in basic_2 and in web site

+ updates on cpce an related concepts
+ "versions" table updated for web site

update in bsasic_2

+ cnv_cpce_trans_lpce started

update in basic_2

+ lpce

update in basic_2, static_2, web site

+ bug fix and first results on cpce
+ crux favicon for web site is now 32x32
+ some auxiliary files for web site committed/rearranged

update in basic_2

+ more properties on types from λδ-1A including:
  type preservation by valid r-equivalence

milestone uupdate in basic_2

extended and restricted type rules justified

update in basic_2

the restricted type rules are justified

auxiliary update in basic_2

- work in progress to justify the type rules for application

update in basic_2

+ nta_drops completed

update in basic_2 and apps_2

+ more results on typing
+ first results on iterated typing
+ minor corrections

update in basic_2 and static_2

+ first results on type assignment
+ more notation for validity
+ eta-conversion defined (for use in linking the notions of validity)

milestone in basic_2, λδ-2A reconstructed

+ confluence of rt-computation (not proved in λδ-2A)
+ preservation of validity for rt-computation

update in ground_2, static_2, basic_2

+ confluence for restricted rt_transition under hyps
+ positive terms wrt the system of reference parked

update in static_2 and basic_2

+ restricted rt-computation;
  more results towards preservation

dependences for ocaml version 4.05.0

update in ground_2, static_2, basic_2

+ minor additioms

update in static_2 and basic_2

+ cnv_cpms_conf_aux proved
  for positive terms wrt the system of reference
+ unused files parked or removed

update in basic_2 and ground_2

+ more results on restricted transition
+ minor additions to the arith library

severe bug found in parallel zeta

+ final commit: component "examples" corrected
+ ex_cpr_omega improved: Ω ➡ Ω in exactly three steps (long awaited property)

severe bug found in parallel zeta

+ partial commit: component "dynamic" corrected
+ some additions towards preservation

severe bug found in parallel zeta

+ partial commit: component "rt_computation" corrected
+ minor additions

severe bug found in parallel zeta

the transition was not parallel, now it is.

+ partial commit: component "rt_transition" corrected and minor bugs ficed
+ some additions in static_2 to support the correction

commit in ground_2, static_2, basic_2, apps_2

+ first steps towards cnv_cpms_conf_aux
+ examples reconstructed
+ additions in the relocation library
+ addition in the arith library

parameter sintax added to axiom statement

the syntax is already present in the other statements

update in ground_2 and basic_2

+ cnv_cpm_conf_lpr_aux (rt-validity implies diamond property)
+ one addition in the arithmetics library

update in ground_2 and basic_2

+ 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

update in basic_2

+ refinement for native validity (lsubv)
  allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity)

update in basic_2 and ground_2

+ auxiliary lemmas for preservation begin
+ one addition in the arith library
+ some typos in names fixed

update in apps_2

+ the model is now aware of polarized abbreviation
+ the term model is on its way

update in functional

+ support for multiple filling

update in ground_2

+ basic relocation swap
+ one name fixed
+ bugs emerging in cpr fixed

updated xoa and predefined virtuals

+ xoa: existing decentralized files are not overwritten by default
+ predefined virtuals: an addition for use in λδ

update in static_2 and app_2

+ term model started
+ functional relocation reactivated
+ some renaming

update in static_2 and app_2

+ advances on the support for models
+ tentative definition of shift (incomplete because unary binders are missing in terms)
+ minor updates and corrections

syntactic components detached from basic_2 become static_2

+ web site updated accordingly

renaming in basic_2

+ a notation problem solved

renaming

+ the predicate in elimination principles in now Q uniformly

renaming in basic_2

nv is now cnv

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

# Conflicts:
# matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl

bug fix in basic_2

+ cpcs_aaa_mono marked as lemma 1500
+ fix in basic_2 web page

bug fix in basic_2

+ cpcs_aaa_mono marked as lemma 1500
+ fix in basic_2 web page

update in basic_2

+ advances on nv ...

update in basic_2

+ component rt_equivalence completed!

milestone update in basic_2

componemt rt_computation cpmpleted!

update in basic_2

+ cprs completed

update in ground_2 and basic_2

+ advances on cpms, cprs, lprs
+ support for decentralized xoa

update in ground_2 and basic_2

+ more results on cpm, and cpms

update in basic_2

+ lprs started ...

commit completed in basic_2

+ fpbs, fpbg, fsb reconstructed

partial commit in basic_2

+ rdsx (was lsx) reconstructed: replaces lfsx

partial update update in basic_2

+ lpxs reconstructed

update in ground_2 and basic_2 (partial commit)

+ preferring lpx and lpr over lfpx and lfpr since lpx seems unavoidable
+ rt_computation will be updated by the next commit

update in basic_2

+ advances on native validity

update in ground_2 and basic_2

+ more results on cpms

update in basic_2

+ moreresults on cpms and cprs

update in basic_2

+ first file on r-equivalence
+ renaming

update in basic_2

definition of native validity

update in basic_2

+ cprs.ma completely ported

update in basic_2

+ first results on cpms and cprs

update in ground_2

set up for equality insertion lemmas

update in basic_2

+ weight of a global environment
+ renaming

update in groud_2 and models

+ denotation is preserved by r-transition
+ minor additions

update in grond_2 and models

+ denotation is preserved by lifts in extensional models

update in apps_2

+ update to web site

update in basic_2

+ list length is now in a separate file

update in ground_2 and basic_2

+ updated notation for lists
+ updated structure for global environments

update in ground_2 and models

+ bug fixed in local environment interpretation
  extensional equality of evaluations allows to prove a lemma

notational update in lambdadelta completed

+ minor improvements

partial notational update in ground_2 and basic_2 ....

+ the notation for lists and streams contains a bug

update in models and ground_2

+ model declaration completed
+ compatibility with veq, first results
+ some old files moved in etc for now

initial definition of λδ model

+ intensional and extensional variant
+ denotational equivalence

this is previously uncommitted matter ported to current version of λδ

update in basic_2

+ first results on cpms
+ minor improvements

update in ground_2 and basic_2

+ old and unused definition llstar replaced with new definition ltc to appear in cpms

notational update in ground_2 and basic_2

+ one addition in predefined_virtuals
+ works citing \lambda\delta updated on web site

decentralizing core notation continues ...

+ uparrows and downarrows clash with \lambda\delta
+ improved list of failing files

update in basic_2 and ground_2

+ some notational changes
+ some renaming
+ some dependences updated

anniversary push

+ one more work citing\lambda\delta
+ more predefined virtuals

bug fixed in xoa generator

notations of existentials must differ according to arity of the involved predicates
+ porting to the updated version of xoa
+ one addition in predefined virtuals

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)

milestone update in basic_2

+ big tree theorem proved!

update in basic_2

+ lemma csx_fsb proved

update in basic_2

+ last property of fpbs proved

update in basic_2

+ first results on fsb

update in basic_2

+ fpbg completed

update in basic_2

+ advances on fpbg
+ Makefile update

update in basic_2

+ fpbs completed (some lemmas parked)

update in basic_2

+ first results on fpbs
+ minor fixes

update in basic_2

+ advances on fpbq
+ minor updates

update in basic_2

+ advances on fpb completed

update in basic_2

advances on fpb to be continued ...