aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2008-03-05Backtrack sur la révision #10401 : suppression de le_minus de la base de ↵notin
hints arith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10621 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04still one more substituion s/Set/Type/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10618 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04one more substitution s/Set/Type/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-02A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)letouzey
... but still no idea why it was working fine on some machines even without this patch... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10614 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-01Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_Oherbelin
(rapport de bug 1807). Cf explication dans le fichier et/ou dans le bug-tracker. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10613 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-29Argumentation plus poussée de pourquoi on retire la condition x>0 dansherbelin
Rpower_O alors qu'on la garde pour les autres propriétés de la puissance. (résultat d'une discussion avec Assia et Jean-Marc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10609 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Some suggestions about FMap by P. Casteran: letouzey
- clarifications about Equality on maps Caveat: name change, what used to be Equal is now Equivb - the prefered equality predicate (the new Equal) is declared a setoid equality, along with several morphisms - beginning of a filter/for_all/exists_/partition section in FMapFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28cardinal is promoted to the rank of primitive member of the FMap interfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Do not open type_scope in SetoidClass.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10603 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Fix compilation problem (hopefully).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10602 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Nicer third spec of choose. letouzey
The old version is now a properties in FSetProperties.OrdProperties git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27For more uniformity, use implicits in FSetAVLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10600 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Application patch #1807 sur hypothèse inutile de Rpower_Oherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10599 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
(Axiom/Variable...). New tactic clapply to apply unapplied class methods in tactic mode, simple solution to the fact that apply does not work up-to classes yet. Add Functions.v for class definitions related to functional morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Backtrack changes on eauto, move specialized version of eauto inmsozeau
class_tactics for further customizations. Add Equivalence.v for typeclass definitions on equivalences and clrewrite.v test-suite for clrewrite. Debugging the tactic I found missing morphisms that are now in Morphisms.v and removed some that made proof search fail or take too long, not sure it's complete however. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10565 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
class_setoid to class_tactics... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place d'une option "modulo_conv" pour contrôler l'usage de cette delta. - Pour éviter que rewrite ne réussise trop souvent, la delta est désactivée pour les tactiques d'élimination (une étude fine reste à faire). - On n'utilise aussi delta que sur les sous-termes du problème d'unification initial. C'est une heuristique qui est intuitive mais qui reste à être évaluée. - Au bilan, le surcoût en temps de compilation des theories est d'un peu moins d'1%. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Backport Program Instance into Instance. Proper early error message ifmsozeau
trying to declare an instance with an already existing name. Add possibility of not giving all the fields in Instance declarations, using Refine.refine to generate the subgoals. No control over opacity in this case though... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Proposal of a nice notation for constructors xI and xO of type positiveletouzey
More details in the header of BinPos.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10547 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Major revision: use of Function, including some non-structural onesletouzey
Sequel of commit 10545 on FSetAVL. This time, no compile-time penality since there are fewer non-structural functions in FMapAVL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10546 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Major revision of FSetAVL: more Function, including some non-structural onesletouzey
NB: this change adds about 10s of compile-time to a file that is already taking about 30s on my machine. If somebody strongly objects to this, contact me. I really think that the gain in uniformity, clarity, and computability (in Coq) worth the extra compile-time: no more function-by-tactic, everything (vm_)computes, and quite efficiently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10545 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08misc improvementsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10539 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08better comments in FMapInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10536 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08better comments in FSetInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10535 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
eauto instead of an arbitrary tactic. Export more from eauto to allow easier debugging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08more complete FSets.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10528 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08one forgotten compatibility lemmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10526 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06Fix obligations not being discharged due to new definition of complement.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10516 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05kill some useless module aliases E:=X (for better name printing, see Elie's ↵letouzey
14097) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Add Morphisms for Qceiling and Qfloorroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10508 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
Thanks to Elie's work and especially "Include Type ...", full sets can be simply expressed as extensions of weak sets. Moreover, Facts and Properties functors can be factorized almost completely. As a result, things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB, Same with maps / weak maps ... No backward compatibility intended for weak sets / maps, but porting scripts should mostly amounts to name changes (see above). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
for basic functional programming and relation definitions respectively. Classes.Relations also includes the definition of Morphism and instances for the standard morphisms and relations (eq, iff, impl, inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic has been reimplemented on top of these definitions, hence it doesn't require a setoid implementation anymore. It also generates obligations for missing reflexivity proofs, like the current setoid_rewrite. It has not been tested on large examples but it should handle directions and occurences. Works with in if no obligations are generated at this time. What's missing is being able to rewrite by a lemma instead of a simple hypothesis with no premises. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide ↵letouzey
(from A. Bohannon) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10500 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Thanks to Elie, we can share duplicated stuff in FSets: for a start, ↵letouzey
FSetWeakFacts and FSetFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10498 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Debug implementation of dependent induction/dependent destruction and ↵msozeau
document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Support for occurences and 'in' in class_setoid, work on corresponding ↵msozeau
tactics in SetoidClass git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10486 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Nicer proofs.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10476 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24remove Fourier Failure warnings.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10474 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Prove the decidability of arithmetical statements using the real numbers.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10473 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Keep the Z_scope local to this file.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10471 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-23Changing R to a local definition so that it isn't exported.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10470 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-23Typonotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10464 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-22Adding Zdiv_le_compat_lthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10461 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ↵msozeau
wrapper around Ltac program_simpl ::= . !!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ↵msozeau
Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-17Fix Makefile bug, using .v instead of .vo and document SetoidDec.vmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10447 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:26:15 +0000