]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Wed, 2 Apr 2014 12:51:32 +0000 (12:51 +0000)]
commit of the "computation" component with lazy pointwise extensions
one conjecture is still open :(
Ferruccio Guidi [Sun, 30 Mar 2014 19:47:08 +0000 (19:47 +0000)]
update of the partial commit:
we move lleq to the "substitution" component
Ferruccio Guidi [Tue, 25 Mar 2014 19:55:08 +0000 (19:55 +0000)]
- partial commit: just the components below "computation"
the development of lazy pointwise extensions continues ...
- we parked not-lazy pointwise extensions in etc
Ferruccio Guidi [Thu, 20 Mar 2014 11:51:46 +0000 (11:51 +0000)]
continuing on lazy pointwise extensions ...
Ferruccio Guidi [Wed, 19 Mar 2014 14:36:51 +0000 (14:36 +0000)]
we begin to develop lazy pointwisee extensions ...
Ferruccio Guidi [Tue, 11 Mar 2014 18:38:22 +0000 (18:38 +0000)]
update in ground_2 and basic_2 ...
Ferruccio Guidi [Tue, 11 Mar 2014 17:57:05 +0000 (17:57 +0000)]
reaxiomatized lleq fixes a bug in it and allows to park substitution in etc
Ferruccio Guidi [Mon, 10 Mar 2014 19:01:45 +0000 (19:01 +0000)]
some additions ...
Ferruccio Guidi [Sat, 8 Mar 2014 17:32:55 +0000 (17:32 +0000)]
we define the lazy poinwise extension of a relation, that should
allow to derive lleq with corrected lleq_lref, and a new defininition
for lpx (and derivatives), which now contains a bug too :( being not lazy
- we revise the definition of lazy equivakence since lleq_lref contains a bug
Ferruccio Guidi [Sat, 8 Mar 2014 16:57:47 +0000 (16:57 +0000)]
some corrections ...
Claudio Sacerdoti Coen [Fri, 7 Mar 2014 18:05:12 +0000 (18:05 +0000)]
Code changed a bit to make it work as before with OCaml 4.0.
Without this patch, the refresh of the textual widget (e.g. the update
of the locked part) is not immediately done.
This is roughly the visual behaviour the user expects. On the other hand,
we also expect the threads that execute and that responsible for the UI
to work in parallel, which is not the case. The code I just touched stops
the worker thread for, on average, 0.1s per tactic, which is really a lot.
Switching to a multiprocess implementation (in place of a multithread) does
not seem easy. Bad OCaml, bad.
Claudio Sacerdoti Coen [Fri, 7 Mar 2014 15:43:17 +0000 (15:43 +0000)]
Do not assert false for a print not implemented yet.
Claudio Sacerdoti Coen [Fri, 7 Mar 2014 15:16:01 +0000 (15:16 +0000)]
Hocus-pocus code to use the old (and deprecated) implementation of
Hashtbl.hash because the new one changes the behaviour of automation,
breaking the library.
Andrea Asperti [Fri, 7 Mar 2014 13:32:16 +0000 (13:32 +0000)]
Minor changes to make the script more robust to strategy changes.
Ferruccio Guidi [Tue, 4 Mar 2014 21:54:59 +0000 (21:54 +0000)]
some external links updated
Ferruccio Guidi [Tue, 4 Mar 2014 21:52:05 +0000 (21:52 +0000)]
a suggestion was added to avoid 1 pseudo reduction at the cost of 40 proper
reductions :(
Claudio Sacerdoti Coen [Tue, 4 Mar 2014 16:07:36 +0000 (16:07 +0000)]
Inclusions improved to allow compilation from the toplevel.
Claudio Sacerdoti Coen [Tue, 4 Mar 2014 12:24:19 +0000 (12:24 +0000)]
Bug fixed: the tactic to analyze the term and understand whose inductive
type it belongs to did not put the sort in whd before concluding that
it was not a sort.
Claudio Sacerdoti Coen [Tue, 4 Mar 2014 12:07:04 +0000 (12:07 +0000)]
OCaml 4.0 detects a not handled case.
I hope the assertion will never be reached, but I ignore why.
I think this is really a bug and code must be written there.
Claudio Sacerdoti Coen [Tue, 4 Mar 2014 11:56:12 +0000 (11:56 +0000)]
Different behaviour of OCaml 4.0.
Ferruccio Guidi [Mon, 3 Mar 2014 23:00:31 +0000 (23:00 +0000)]
update in basic_2
Ferruccio Guidi [Mon, 3 Mar 2014 22:59:18 +0000 (22:59 +0000)]
some additions for the forthcoming presentation
Ferruccio Guidi [Fri, 28 Feb 2014 14:47:52 +0000 (14:47 +0000)]
update in basic_2
Ferruccio Guidi [Fri, 28 Feb 2014 13:48:27 +0000 (13:48 +0000)]
- some corrections and additions
- lsubr moved from "relocation" to "static"
Claudio Sacerdoti Coen [Thu, 27 Feb 2014 12:40:13 +0000 (12:40 +0000)]
Porting of HOTT from Coq to Matita.
* Overture.ma half completed up to truncations.
* PathGroupoids.ma is next and should depend only on
the part of Overture that has been ported.
Ferruccio Guidi [Tue, 25 Feb 2014 22:00:03 +0000 (22:00 +0000)]
relabelled documantation entries
Ferruccio Guidi [Mon, 24 Feb 2014 19:01:20 +0000 (19:01 +0000)]
update in web site and basic_2
Ferruccio Guidi [Mon, 24 Feb 2014 18:56:46 +0000 (18:56 +0000)]
- we bypassed another false conjecture :) ...
- minor corrections
Ferruccio Guidi [Sat, 22 Feb 2014 11:50:51 +0000 (11:50 +0000)]
addition of unused material :)
Ferruccio Guidi [Sat, 22 Feb 2014 11:36:51 +0000 (11:36 +0000)]
update in ground_2 and basic_2
Ferruccio Guidi [Sat, 22 Feb 2014 11:32:07 +0000 (11:32 +0000)]
a wrong conjecture bypassed!
Ferruccio Guidi [Fri, 21 Feb 2014 16:38:05 +0000 (16:38 +0000)]
update in basic_2 and ground_2
Ferruccio Guidi [Fri, 21 Feb 2014 16:36:20 +0000 (16:36 +0000)]
- main proposition on lsx finally proved!
- long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need)
- unused results on append parked in etc
- some additions to ynat
Ferruccio Guidi [Tue, 18 Feb 2014 17:34:38 +0000 (17:34 +0000)]
- a reinforement in a lemma on ldrop allows to prove a lemma on lsx :)
- some renaming
Ferruccio Guidi [Sun, 16 Feb 2014 18:59:26 +0000 (18:59 +0000)]
- improved definition of lsx allows more invariants
- some additions
- we parked some unnecessary planes (cny, cpye)
Ferruccio Guidi [Tue, 11 Feb 2014 21:12:19 +0000 (21:12 +0000)]
update in basic_2 and ground_2
Ferruccio Guidi [Tue, 11 Feb 2014 21:08:30 +0000 (21:08 +0000)]
some advances on reduction
Ferruccio Guidi [Tue, 4 Feb 2014 20:16:21 +0000 (20:16 +0000)]
evaluation for context-sensitive extended substitution (cpye) completed!
Ferruccio Guidi [Mon, 3 Feb 2014 21:57:36 +0000 (21:57 +0000)]
we start total substitution ...
Ferruccio Guidi [Fri, 31 Jan 2014 15:03:31 +0000 (15:03 +0000)]
some notation renamed and fixed
Ferruccio Guidi [Thu, 30 Jan 2014 22:01:30 +0000 (22:01 +0000)]
normal forms for extended substitution
Ferruccio Guidi [Wed, 29 Jan 2014 18:55:32 +0000 (18:55 +0000)]
bug fix in the notation of normal forms, now we specify that they are
normal forms for reduction. This will allow to enable normal forms for
substitution ...
Andrea Asperti [Tue, 28 Jan 2014 12:34:47 +0000 (12:34 +0000)]
Almost there
Andrea Asperti [Tue, 28 Jan 2014 10:09:51 +0000 (10:09 +0000)]
progress
Ferruccio Guidi [Mon, 27 Jan 2014 22:06:00 +0000 (22:06 +0000)]
some corrections ...
Andrea Asperti [Mon, 27 Jan 2014 07:58:37 +0000 (07:58 +0000)]
working version
Ferruccio Guidi [Sun, 26 Jan 2014 20:12:59 +0000 (20:12 +0000)]
nat: we added a non-indexed theorem
lambda: the corrispondence between terms by level and terms by depth
is proved!
Andrea Asperti [Sun, 26 Jan 2014 16:20:46 +0000 (16:20 +0000)]
more auxiliary machines
Ferruccio Guidi [Sun, 26 Jan 2014 10:08:33 +0000 (10:08 +0000)]
- nat: some additions, plus_minus_commutative renamed plus_minus_associative
- lambda: we study terms in which references are by "level" rather
than by "depth" aiming at establishing a bijection between the two
representations, we start the support for distributed notation as in lambdadelta
Ferruccio Guidi [Mon, 20 Jan 2014 16:00:41 +0000 (16:00 +0000)]
milestone in basic_2
Ferruccio Guidi [Mon, 20 Jan 2014 15:59:12 +0000 (15:59 +0000)]
commit completed: now we support two versions of slicing for local
environments
Ferruccio Guidi [Sat, 18 Jan 2014 22:05:09 +0000 (22:05 +0000)]
- commit of the "reduction" component with two additions ...
- formal bug fix in extended substitution under a binder: now we
follow the paradigm used for reduction under a binder
Ferruccio Guidi [Fri, 17 Jan 2014 19:31:58 +0000 (19:31 +0000)]
commit of the "unfold" component ...
Ferruccio Guidi [Fri, 17 Jan 2014 19:10:33 +0000 (19:10 +0000)]
commit of the "static" component
Ferruccio Guidi [Fri, 17 Jan 2014 17:45:00 +0000 (17:45 +0000)]
- commit of the "substitution" component
- some renaming
- we disabled the old notation for ldrop to capture its instances
syntactically
Ferruccio Guidi [Thu, 16 Jan 2014 21:49:29 +0000 (21:49 +0000)]
commit of the "relocation" component with the new definition of ldrop,
the other components will be committed shortly ...
Ferruccio Guidi [Wed, 15 Jan 2014 16:37:48 +0000 (16:37 +0000)]
we start a criterion on extended computation
Ferruccio Guidi [Mon, 13 Jan 2014 18:13:17 +0000 (18:13 +0000)]
some improvements on the relation lsx ...
Ferruccio Guidi [Fri, 10 Jan 2014 18:06:54 +0000 (18:06 +0000)]
update in ground_2 and basic_2
Ferruccio Guidi [Fri, 10 Jan 2014 18:05:18 +0000 (18:05 +0000)]
new definition of lleq allows to complete the proof of lemma 1000
(lleq_cpx_conf_dx)!
Ferruccio Guidi [Thu, 9 Jan 2014 15:33:21 +0000 (15:33 +0000)]
- ynat: some additions
- lleq: we are ready to remove the old definition :)
Ferruccio Guidi [Mon, 6 Jan 2014 21:32:23 +0000 (21:32 +0000)]
one file was missing :)
Ferruccio Guidi [Mon, 6 Jan 2014 21:17:44 +0000 (21:17 +0000)]
- lleq now uses ynat
- some bugs fixed
Ferruccio Guidi [Sun, 5 Jan 2014 21:13:55 +0000 (21:13 +0000)]
- new definition of lazy equivalence for local environments,
driven by extended multiple substitution for terms
- minor corrections
Ferruccio Guidi [Fri, 3 Jan 2014 17:31:49 +0000 (17:31 +0000)]
- extended multiple substitutions now uses bounds in ynat (ie. they
can be infinite) for use in lleq
- ground_2: additions in ynat
Ferruccio Guidi [Fri, 3 Jan 2014 13:03:26 +0000 (13:03 +0000)]
more arithmetics for natural numbers with infinity ...
Ferruccio Guidi [Sat, 28 Dec 2013 21:11:26 +0000 (21:11 +0000)]
some improvements and new lemmas for
natural numbers with infinity
Ferruccio Guidi [Thu, 26 Dec 2013 14:54:55 +0000 (14:54 +0000)]
the theory of extended multiple substitution for therms is complete
a simpler theory is complete as well but parked in etc for now
Ferruccio Guidi [Fri, 20 Dec 2013 12:50:43 +0000 (12:50 +0000)]
theory of extended iterated substitution begins ...
Ferruccio Guidi [Thu, 19 Dec 2013 15:16:45 +0000 (15:16 +0000)]
theory of cpy is complete!
Ferruccio Guidi [Thu, 19 Dec 2013 14:43:18 +0000 (14:43 +0000)]
the theory of cpy continues ...
Ferruccio Guidi [Tue, 17 Dec 2013 20:10:57 +0000 (20:10 +0000)]
refinement for extended substitution completed
Ferruccio Guidi [Mon, 16 Dec 2013 20:55:49 +0000 (20:55 +0000)]
- lsubr moved down one component
- extended substitution started (for use in lleq)
Ferruccio Guidi [Sun, 15 Dec 2013 15:51:39 +0000 (15:51 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 15 Dec 2013 13:48:17 +0000 (13:48 +0000)]
eliminators of arited terms based on "big tree" proper computation
Ferruccio Guidi [Sat, 14 Dec 2013 22:30:57 +0000 (22:30 +0000)]
update in basic_2 completed
Ferruccio Guidi [Sat, 14 Dec 2013 22:29:06 +0000 (22:29 +0000)]
one file was still missing
Ferruccio Guidi [Sat, 14 Dec 2013 22:22:50 +0000 (22:22 +0000)]
update in basic_2
Ferruccio Guidi [Sat, 14 Dec 2013 22:21:10 +0000 (22:21 +0000)]
commit is now complete :)
Ferruccio Guidi [Sat, 14 Dec 2013 22:18:47 +0000 (22:18 +0000)]
- "big tree" theorem is now proved up to some conjectures involving
just computation
- redefined "big tree" proper computation now replaces its restricted
form and is transitive
- improved definition of "big tree" proper reduction involves lazy
extended computation for local enviroments
Ferruccio Guidi [Mon, 9 Dec 2013 21:53:19 +0000 (21:53 +0000)]
- first results on strongly normalizing local environments
- some updates
Ferruccio Guidi [Fri, 6 Dec 2013 14:41:51 +0000 (14:41 +0000)]
partial commit ...
- fleq removed and replaced by fpns
- improved proper "big tree" reduction
- some missing lemmas
Ferruccio Guidi [Wed, 4 Dec 2013 15:42:45 +0000 (15:42 +0000)]
update in basic_2
Ferruccio Guidi [Wed, 4 Dec 2013 15:39:09 +0000 (15:39 +0000)]
third commutation property on lazy equivalence for
local environments proved, multistep version
Andrea Asperti [Wed, 4 Dec 2013 14:59:15 +0000 (14:59 +0000)]
New approach: we use "iterator" steps in place of pointers.
Ferruccio Guidi [Wed, 4 Dec 2013 14:14:46 +0000 (14:14 +0000)]
update in basic_2
Ferruccio Guidi [Wed, 4 Dec 2013 14:13:30 +0000 (14:13 +0000)]
first and second commutation property on lazy equivalence for
local environments proved (lleq_fqup_trans, lleq_cpxs_trans) multistep
version
Claudio Sacerdoti Coen [Mon, 2 Dec 2013 21:00:51 +0000 (21:00 +0000)]
1. more bugs fixed
2. correctness proof completed
Ferruccio Guidi [Mon, 2 Dec 2013 19:23:46 +0000 (19:23 +0000)]
update in basic_2
Ferruccio Guidi [Mon, 2 Dec 2013 19:19:25 +0000 (19:19 +0000)]
- last patrtial commit of the "reduction" and "computation" components
- we generalized a lemma
Claudio Sacerdoti Coen [Mon, 2 Dec 2013 17:15:14 +0000 (17:15 +0000)]
More progress.
Claudio Sacerdoti Coen [Mon, 2 Dec 2013 16:47:36 +0000 (16:47 +0000)]
Some progress in the correctness proof and a bug fixed.
Ferruccio Guidi [Mon, 2 Dec 2013 15:25:44 +0000 (15:25 +0000)]
initial commit of the "rduction" component
Ferruccio Guidi [Sun, 1 Dec 2013 21:29:08 +0000 (21:29 +0000)]
update in ground_2
Ferruccio Guidi [Sun, 1 Dec 2013 21:24:28 +0000 (21:24 +0000)]
commit of the "substitution" component and of some auxiliary files ...
Ferruccio Guidi [Sun, 1 Dec 2013 20:57:54 +0000 (20:57 +0000)]
- improved arithmetics for natural numbers with infinity
- some properties of equivalence for local environments
- improved lazy equivalence for local environments
- we commit just the "relocation" component
Andrea Asperti [Fri, 29 Nov 2013 17:41:30 +0000 (17:41 +0000)]
A first example that uses a status monad where the status is a tree.
It should be possible to implement it imperatively and efficiently.
Ferruccio Guidi [Fri, 29 Nov 2013 16:33:57 +0000 (16:33 +0000)]
addition for natural numbers with infinity
Ferruccio Guidi [Thu, 28 Nov 2013 16:07:56 +0000 (16:07 +0000)]
update in ground_2, web page for ground_2
Ferruccio Guidi [Thu, 28 Nov 2013 16:02:03 +0000 (16:02 +0000)]
definition of equivalence for local environments,
based on natural numbers with infinity