]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 years agoThe precedence of ^-1 has changed.
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:35:24 +0000 (17:35 +0000)]
The precedence of ^-1 has changed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoEquality has one right parameter and thus it's elimination principle has two
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:33:09 +0000 (17:33 +0000)]
Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:27:01 +0000 (17:27 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAxioms were not indexed.
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:35:57 +0000 (14:35 +0000)]
Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAxioms were not indexed.
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:33:55 +0000 (14:33 +0000)]
Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:20:39 +0000 (14:20 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoReal numbers as co-inductive streams of digits (overlapping refining intervals).
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:19:52 +0000 (14:19 +0000)]
Real numbers as co-inductive streams of digits (overlapping refining intervals).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoComputation of the trace.
Andrea Asperti [Wed, 24 Mar 2010 13:04:27 +0000 (13:04 +0000)]
Computation of the trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agotypo in a proof
Matthias Puech [Tue, 23 Mar 2010 18:24:49 +0000 (18:24 +0000)]
typo in a proof

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoOne more case.
Andrea Asperti [Tue, 23 Mar 2010 17:50:12 +0000 (17:50 +0000)]
One more case.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoReadded eqf_2.
Andrea Asperti [Tue, 23 Mar 2010 16:31:55 +0000 (16:31 +0000)]
Readded eqf_2.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosymmetric_eq -> sym_eq
Andrea Asperti [Tue, 23 Mar 2010 15:59:10 +0000 (15:59 +0000)]
symmetric_eq -> sym_eq

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoRe-proved an axiom
Andrea Asperti [Tue, 23 Mar 2010 15:52:29 +0000 (15:52 +0000)]
Re-proved an axiom

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoCommented a few lemmas (copies).
Andrea Asperti [Tue, 23 Mar 2010 15:51:56 +0000 (15:51 +0000)]
Commented a few lemmas (copies).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFixed a few bugs
Andrea Asperti [Tue, 23 Mar 2010 15:48:42 +0000 (15:48 +0000)]
Fixed a few bugs

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago"flat" function (subst unfolding)
Andrea Asperti [Tue, 23 Mar 2010 15:45:06 +0000 (15:45 +0000)]
"flat" function (subst unfolding)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoKeeping only lift_aux e subst_aux (renamed to lift and subst).
Andrea Asperti [Tue, 23 Mar 2010 07:32:33 +0000 (07:32 +0000)]
Keeping only lift_aux e subst_aux (renamed to lift and subst).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMoved compare in a different file.
Andrea Asperti [Tue, 23 Mar 2010 07:31:12 +0000 (07:31 +0000)]
Moved compare in a different file.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoDowngrading level of infix notations involving \sup.
Matthias Puech [Thu, 18 Mar 2010 17:44:52 +0000 (17:44 +0000)]
Downgrading level of infix notations involving \sup.

14 years agoPorting alla nuova def. di negazione
Andrea Asperti [Thu, 18 Mar 2010 11:36:56 +0000 (11:36 +0000)]
Porting alla nuova def. di negazione

14 years agoNuova versione di not.
Andrea Asperti [Thu, 18 Mar 2010 11:35:44 +0000 (11:35 +0000)]
Nuova versione di not.

14 years agoPrintings removed.
Andrea Asperti [Thu, 18 Mar 2010 11:33:10 +0000 (11:33 +0000)]
Printings removed.

14 years agoDebugging disabled.
Andrea Asperti [Thu, 18 Mar 2010 11:28:46 +0000 (11:28 +0000)]
Debugging disabled.

14 years agoDebugging disabled.
Andrea Asperti [Thu, 18 Mar 2010 11:28:22 +0000 (11:28 +0000)]
Debugging disabled.

14 years agoNew demodulation tactics (mostly for debugging purposes).
Andrea Asperti [Thu, 18 Mar 2010 11:23:53 +0000 (11:23 +0000)]
New demodulation tactics (mostly for debugging purposes).
It is called with "nauto demod".

14 years agoExporting the demodulation function.
Andrea Asperti [Thu, 18 Mar 2010 11:22:11 +0000 (11:22 +0000)]
Exporting the demodulation function.

14 years agoNew option "demod" for auto.
Andrea Asperti [Thu, 18 Mar 2010 11:19:53 +0000 (11:19 +0000)]
New option "demod" for auto.

14 years agoPorting the new definition of equality.
Andrea Asperti [Thu, 18 Mar 2010 11:06:34 +0000 (11:06 +0000)]
Porting the new definition of equality.

14 years agoDo not index examples (concrete syntax: nremark).
Claudio Sacerdoti Coen [Thu, 18 Mar 2010 10:21:46 +0000 (10:21 +0000)]
Do not index examples (concrete syntax: nremark).

14 years agonremark => `Example (not to be indexed)
Claudio Sacerdoti Coen [Thu, 18 Mar 2010 10:21:14 +0000 (10:21 +0000)]
nremark => `Example (not to be indexed)

14 years agoapp of app inside smart application.
Andrea Asperti [Thu, 18 Mar 2010 07:18:36 +0000 (07:18 +0000)]
app of app inside smart application.

14 years agodr
Ferruccio Guidi [Wed, 17 Mar 2010 15:10:12 +0000 (15:10 +0000)]
dr
brs line, and those below, will be ignored--

M    ng_tactics/.depend.opt

14 years agoqualche caso del lemma 5.2.11
Andrea Asperti [Wed, 17 Mar 2010 14:58:51 +0000 (14:58 +0000)]
qualche caso del lemma 5.2.11

14 years agoOCaml's inferred type simplified.
Claudio Sacerdoti Coen [Wed, 17 Mar 2010 14:56:31 +0000 (14:56 +0000)]
OCaml's inferred type simplified.

14 years ago...
Claudio Sacerdoti Coen [Wed, 17 Mar 2010 14:29:27 +0000 (14:29 +0000)]
...

14 years agoSplitted gpts in two files.
Andrea Asperti [Wed, 17 Mar 2010 11:51:01 +0000 (11:51 +0000)]
Splitted gpts in two files.

14 years agoAggiornamento alla negazione.
Andrea Asperti [Wed, 17 Mar 2010 11:48:50 +0000 (11:48 +0000)]
Aggiornamento alla negazione.

14 years agoNuova definizione della negazione.
Andrea Asperti [Wed, 17 Mar 2010 11:47:03 +0000 (11:47 +0000)]
Nuova definizione della negazione.

14 years agoComparison of two applications with a different number of arguments not
Claudio Sacerdoti Coen [Tue, 16 Mar 2010 17:57:49 +0000 (17:57 +0000)]
Comparison of two applications with a different number of arguments not
implemented yet.

14 years ago1) intros cleans up the cache (because the context changes) and this means
Claudio Sacerdoti Coen [Tue, 16 Mar 2010 16:41:40 +0000 (16:41 +0000)]
1) intros cleans up the cache (because the context changes) and this means
   that the case of an empty list of under_inspection is possible
2) every time we merge goals we need to remove the currently under inspection
   goal from the list

14 years agorefreshing of inferred type was missing
Claudio Sacerdoti Coen [Tue, 16 Mar 2010 15:34:34 +0000 (15:34 +0000)]
refreshing of inferred type was missing

14 years ago...
Claudio Sacerdoti Coen [Tue, 16 Mar 2010 14:17:51 +0000 (14:17 +0000)]
...

14 years agoFirst version of PTS
Andrea Asperti [Fri, 12 Mar 2010 12:25:43 +0000 (12:25 +0000)]
First version of PTS

14 years agoNew definition of negation
Andrea Asperti [Fri, 12 Mar 2010 12:23:31 +0000 (12:23 +0000)]
New definition of negation

14 years agoSubst was missing in perforate small (apparently, gty is not
Andrea Asperti [Fri, 12 Mar 2010 07:40:38 +0000 (07:40 +0000)]
Subst was missing in perforate small (apparently, gty is not
meta-closed).

14 years agoremoved debug from the inteface
Andrea Asperti [Fri, 12 Mar 2010 07:39:13 +0000 (07:39 +0000)]
removed debug from the inteface

14 years agoIn line with the ml.
Andrea Asperti [Thu, 4 Mar 2010 08:27:05 +0000 (08:27 +0000)]
In line with the ml.

14 years ago1. For smart application, we only perforate small terms (terms with sort
Andrea Asperti [Thu, 4 Mar 2010 08:06:43 +0000 (08:06 +0000)]
1. For smart application, we only perforate small terms (terms with sort
Type0). E.g. Not(P(a)) is perforated to Not(P(?)) and not to Not(?) as
before.
2. At maxdepth, we restrict the analysis to facts only in case the goal
is not reducible to a Pi. Example: if Not A = A -> False, Not A is not a
fact, and the previous politics would prune its application.

14 years agoSmall changes for debugging
Andrea Asperti [Thu, 4 Mar 2010 07:55:14 +0000 (07:55 +0000)]
Small changes for debugging

14 years agoFixed a bug in deep_eq: we generated new clauses but neglected the
Andrea Asperti [Thu, 4 Mar 2010 07:54:40 +0000 (07:54 +0000)]
Fixed a bug in deep_eq: we generated new clauses but neglected the
relocating subst. Caused problems in proof reconstruction.

14 years agoCorrected a bug relative to the application of substs in the "on goal"
Andrea Asperti [Thu, 4 Mar 2010 07:52:45 +0000 (07:52 +0000)]
Corrected a bug relative to the application of substs in the "on goal"
case.

14 years agoAdded reverse rewriting principle in Type[0].
Wilmer Ricciotti [Tue, 2 Mar 2010 16:39:15 +0000 (16:39 +0000)]
Added reverse rewriting principle in Type[0].

14 years agoSome integrations to the ng library.
Wilmer Ricciotti [Tue, 2 Mar 2010 16:19:18 +0000 (16:19 +0000)]
Some integrations to the ng library.

14 years agoAdded syntax for ninversion tactic (still experimental).
Wilmer Ricciotti [Tue, 2 Mar 2010 14:06:40 +0000 (14:06 +0000)]
Added syntax for ninversion tactic (still experimental).

14 years agoConstants are indexed using the Reference, not the Uri, so that constructors
Enrico Tassi [Tue, 2 Mar 2010 11:53:57 +0000 (11:53 +0000)]
Constants are indexed using the Reference, not the Uri, so that constructors
are different!

14 years agoFixed a bug in the unification, which prevented some reduction steps from being
Wilmer Ricciotti [Mon, 1 Mar 2010 18:07:54 +0000 (18:07 +0000)]
Fixed a bug in the unification, which prevented some reduction steps from being
performed in the case "match vs. match", when the types of the matching term
were not the same. The procedure used to always raise an Uncertain exception,
while in many cases the good choice would be to raise KeepReducing. This caused
the nnormalize tactic to fail with an error in some cases.

14 years ago-bugfix in the "profile" entry
Ferruccio Guidi [Thu, 25 Feb 2010 21:19:29 +0000 (21:19 +0000)]
-bugfix in the "profile" entry

14 years ago- pipeline support for generated entities in text mode completed
Ferruccio Guidi [Thu, 25 Feb 2010 19:42:00 +0000 (19:42 +0000)]
- pipeline support for generated entities in text mode completed

14 years agoMinimal example in Z showing a problem in the nnormalize tactic.
Wilmer Ricciotti [Thu, 25 Feb 2010 12:42:56 +0000 (12:42 +0000)]
Minimal example in Z showing a problem in the nnormalize tactic.

14 years ago- a couple of new entities
Ferruccio Guidi [Wed, 24 Feb 2010 20:04:39 +0000 (20:04 +0000)]
- a couple of new entities

14 years ago- the text model now supports invocations of the entity generator (to
Ferruccio Guidi [Tue, 23 Feb 2010 12:00:26 +0000 (12:00 +0000)]
- the text model now supports invocations of the entity generator (to
be implemented)
- the XML objects can be exported to a specified directory (via the -x
command line option)

14 years ago- we completed the text parser fixing the syntactic shortcuts
Ferruccio Guidi [Mon, 22 Feb 2010 18:53:10 +0000 (18:53 +0000)]
- we completed the text parser fixing the syntactic shortcuts
- we can now parse several files without loosing the status
- some imperative variables refactored

14 years ago- we added some syntactic sugar in the text parser
Ferruccio Guidi [Sun, 21 Feb 2010 19:09:07 +0000 (19:09 +0000)]
- we added some syntactic sugar in the text parser

14 years ago- we implemented the hierarchy and sort names declaration in text parser
Ferruccio Guidi [Sat, 20 Feb 2010 22:18:47 +0000 (22:18 +0000)]
- we implemented the hierarchy and sort names declaration in text parser
- we implemented a basic taxonomy for the entities in the text parser
- we fixed the visibility rules in the text-to-crg transformation
- we corrected a bug in the text-to-crg transformation (a continuation was not called)
- we removed the hierarchy parameter from the type checker status
- we created an directory with the examples we can typecheck
- we changed the semantics of the -r command-line option

14 years agoOpen goals fixed (it also returned closed goals).
Andrea Asperti [Fri, 19 Feb 2010 17:15:41 +0000 (17:15 +0000)]
Open goals fixed (it also returned closed goals).

14 years ago- we added a parser for lambda-delta textual syntax (file extension .hln)
Ferruccio Guidi [Fri, 19 Feb 2010 16:27:17 +0000 (16:27 +0000)]
- we added a parser for lambda-delta textual syntax (file extension .hln)
- we now parse the input files with a straming policy
- we added a Meta attribute for explanatory metalinguistic comments
- brg: missing type casts were not inserted (fixed)

14 years agoRemoved debug printings.
Andrea Asperti [Fri, 19 Feb 2010 07:45:40 +0000 (07:45 +0000)]
Removed debug printings.

14 years agoadded lazy
Andrea Asperti [Fri, 19 Feb 2010 07:38:54 +0000 (07:38 +0000)]
added lazy

14 years agoNuova versione di auto.
Andrea Asperti [Fri, 19 Feb 2010 07:36:11 +0000 (07:36 +0000)]
Nuova versione di auto.

14 years agoNew proofs.
Andrea Asperti [Fri, 19 Feb 2010 07:30:16 +0000 (07:30 +0000)]
New proofs.

14 years agoWilmer's stuff for destruct.
Andrea Asperti [Fri, 19 Feb 2010 07:27:31 +0000 (07:27 +0000)]
Wilmer's stuff for destruct.

14 years ago(no commit message)
Andrea Asperti [Fri, 19 Feb 2010 07:25:04 +0000 (07:25 +0000)]

14 years agoAdded an implicit parameter to branch_tac to allow branching on a
Andrea Asperti [Fri, 19 Feb 2010 07:19:01 +0000 (07:19 +0000)]
Added an implicit parameter to branch_tac to allow branching on a
single goal.

14 years agoMore theorems
Andrea Asperti [Tue, 16 Feb 2010 09:21:04 +0000 (09:21 +0000)]
More theorems

14 years agoMinor fixings.
Andrea Asperti [Tue, 16 Feb 2010 07:34:33 +0000 (07:34 +0000)]
Minor fixings.

14 years agoThe height of fixpoint applications was not computed correctly.
Claudio Sacerdoti Coen [Mon, 15 Feb 2010 12:41:44 +0000 (12:41 +0000)]
The height of fixpoint applications was not computed correctly.

14 years ago cerco documentation
Cosimo Oliboni [Fri, 12 Feb 2010 21:06:50 +0000 (21:06 +0000)]
 cerco documentation

14 years agominimal sequent height set to 1
Enrico Tassi [Thu, 11 Feb 2010 10:34:32 +0000 (10:34 +0000)]
minimal sequent height set to 1

14 years agosome experiment filtering with height
Enrico Tassi [Thu, 11 Feb 2010 09:49:47 +0000 (09:49 +0000)]
some experiment filtering with height

14 years agoaddenda
Andrea Asperti [Wed, 10 Feb 2010 09:23:29 +0000 (09:23 +0000)]
addenda

14 years agoAdded a count_occurrences function.
Andrea Asperti [Tue, 9 Feb 2010 07:20:55 +0000 (07:20 +0000)]
Added a count_occurrences function.

14 years agoBug fixing.
Andrea Asperti [Mon, 8 Feb 2010 07:26:18 +0000 (07:26 +0000)]
Bug fixing.

14 years agoRemoved debug printings.
Andrea Asperti [Mon, 8 Feb 2010 07:25:32 +0000 (07:25 +0000)]
Removed debug printings.

14 years agoSome changes towards integration of setoid-rewriting.
Andrea Asperti [Mon, 8 Feb 2010 07:24:34 +0000 (07:24 +0000)]
Some changes towards integration of setoid-rewriting.

14 years ago freescale porting
Cosimo Oliboni [Sat, 6 Feb 2010 13:13:17 +0000 (13:13 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sat, 6 Feb 2010 10:30:51 +0000 (10:30 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Fri, 5 Feb 2010 07:43:09 +0000 (07:43 +0000)]
 freescale porting

14 years ago...
Claudio Sacerdoti Coen [Thu, 4 Feb 2010 13:31:41 +0000 (13:31 +0000)]
...

14 years agoAdded count_occurrences.
Andrea Asperti [Thu, 4 Feb 2010 11:23:52 +0000 (11:23 +0000)]
Added count_occurrences.
Type of does_not_occur corrected.

14 years agoBug fixed: goto_top used to reset the status to the first one and then
Andrea Asperti [Thu, 4 Feb 2010 10:32:30 +0000 (10:32 +0000)]
Bug fixed: goto_top used to reset the status to the first one and then
reset_buffer (re-implemented yesterday) used to do the time travel
again. Fixed by getting rid of goto_top.

Note: the old implementation was slightly more efficient since the
initial notation of Matita was not re-loaded every time you go back to
top. In practice, this does not seem to matter.

14 years ago freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 07:54:26 +0000 (07:54 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 03:42:47 +0000 (03:42 +0000)]
 freescale porting

14 years ago...
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:14:47 +0000 (23:14 +0000)]
...

14 years agoEnd of curryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:10:57 +0000 (23:10 +0000)]
End of curryfication of binary_morphisms.

14 years agoCurryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:58:49 +0000 (22:58 +0000)]
Curryfication of binary_morphisms.

14 years agoCurryfication of binary setoids.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:46:21 +0000 (22:46 +0000)]
Curryfication of binary setoids.

14 years agoCurryfication of binary morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:03:37 +0000 (22:03 +0000)]
Curryfication of binary morphisms.

14 years agoWork in Progress: Who needs binary_morphisms? Curryfication is your friend.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 20:03:57 +0000 (20:03 +0000)]
Work in Progress: Who needs binary_morphisms? Curryfication is your friend.

But...

 1) the hints are uglier
 2) you really need to apply mk_binary_morphism to prove a curryfied binary
    morphism if you want to remain sane...

Note: with non uniform coercions everywhere we should be able to finally get
a beautiful script. Yet to be done.

14 years agoDisabled debug prints in ndestruct tactic.
Wilmer Ricciotti [Wed, 3 Feb 2010 17:00:36 +0000 (17:00 +0000)]
Disabled debug prints in ndestruct tactic.

14 years agoDebug code commented out.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 17:00:11 +0000 (17:00 +0000)]
Debug code commented out.