aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
...
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from ↵Gravatar Guillaume Melquiond2014-04-22
| | | | | | | | Coquelicot. This change removes the need for excluded middle. It also greatly simplifies the proof (no need for geometric series, limits, constructive epsilon, and so on).
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
|
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
|
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
| | | | | | | | Also allow [projT1]/[projT2] to work for [sigT2]s and [proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions. This closes Bug 3044. This closes Pull Request #4.
* Closing bug #3164Gravatar Julien Forest2014-04-04
|
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
|
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
| | | | Helps cbn tactic refolding
* fixup complement FinGravatar Pierre Boutillier2014-02-24
|
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
|
* FinFun.v: results about injective/surjective/bijective fonctions over finite ↵Gravatar Pierre Letouzey2014-02-07
| | | | | | domains + Some extra results about NoDup, Fin.t, ...
* [Coercion]s use [Sortclass], not [Prop] (in docs)Gravatar Jason Gross2014-01-24
| | | | Reported By: J. Ian Johnson
* List: Bug 3039 weaker requirement for fold symmetricGravatar Pierre Boutillier2013-12-20
|
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
| | | | | | | This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies with [fun A (P : A -> Prop) (X : sigT P) => projT1 X]. This closes Bug 3043.
* Generalize eq_proofs_unicityGravatar Jason Gross2013-12-12
| | | | | | | | | | | | | | | The generalizded version is eq_proofs_unicity_one_var. We preserve backwards compatibility, unless someone used nu_left_inv (which was defined as a Remark(!), but whose type depended on a number of Lets.) We could keep going in defining one variable variants, but I was lazy. I'm also not sure if we should be breaking backward compatiblity to generalize these theorems, if we should make separate files for the pointed versions, or if we should just have duplicate theorems in each file. (I'm also not sure if I should call it _one_var or _pointed or something else.) This closes Bug 3019.
* Improved the presentation of the proof of UIP_refl_nat.Gravatar Hugo Herbelin2013-12-04
|
* Add lemma derivable_pt_lim_atan.Gravatar Guillaume Melquiond2013-12-04
| | | | | Note: the choice of the derivative comes from derivable_pt_lim_ps_atan rather than derivable_pt_atan.
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
|
* Remove a useless hypothesis from Rle_Rinv.Gravatar Guillaume Melquiond2013-12-03
|
* Adding Acc_intro_generator in order to help computations of Function in ↵Gravatar forest2013-11-20
| | | | particular
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
| | | | | | When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore Zsqrt compat now that refine works fine with match.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17021 85f007b7-540e-0410-9357-904b9bb8a0f7
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
| | | | | | | | | | | It now uses the same algorithm as pretyping does. This produces pretty weird goal when refining pattern matching terms. Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now. The file Zsqrt_compat.v has two temporary [Admitted] related to this issue. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
| | | | | | | | | new Axiom in Logic.v, proof_admitted : False. admit now simply cases proof_admitted and does not create a new Axiom in the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in definition clos_reflGravatar ppedrot2013-07-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3089. This implied tweaking the definition of the lexicographicGravatar ppedrot2013-07-26
| | | | | | | | product of lists, hence possibly introducing incompatibilities. Parts of the patch by Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a concat function to List theory. Strangely, it was missing.Gravatar ppedrot2013-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16633 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
| | | | | | ... no need to Unset them manually git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 85f007b7-540e-0410-9357-904b9bb8a0f7
* More dynamic argument scopesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
| | | | | | | | | | | | | - hypotheses are introduced in the left-to-right order - intropatterns have to match the number of generated hypotheses, and, if less, new introduction names are automatically generated - clearing the hypothesis on which injection is applied, if any. However, this is a source of incompatibilities (for a variant of injection that is hopefully not used a lot). Compatibility can be restored by "Unset Injection L2R Pattern Order". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving printing of 'rew' notationGravatar herbelin2013-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxing the constraint on eta-expanding on the fly while looking forGravatar herbelin2013-05-05
| | | | | | | | | | | notation to use at printing time. We now allow to print "sigT P" as "{x:_ & P x}", generating a "_" for the missing type, when the notation is defined by 'Notation "{ x : A & P }" := (sigT (fun x:A => P))'. Do better, and change the notation to "(sigT (A:=A) (fun x => P))" so that the type is known even when eta-expansion is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added group properties of eq_refl, eq_sym, eq_transGravatar herbelin2013-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Normalized type for Vector.map2Gravatar pboutill2013-03-25
| | | | | | fix CoRN but there must be an underlying bug ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16355 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16350 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
| | | | | | | | Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
* cbn friendly VectorDefGravatar pboutill2013-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16245 85f007b7-540e-0410-9357-904b9bb8a0f7
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
| | | | | | | | | | The offending functor in NZOrder wasn't actually used, so I've commented it for now. Btw, the Not_found in coqchk is now turned into something slightly more informative git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
| | | | | | | | It is much beter for everything (includind guard condition and simpl refolding) excepts typeclasse inference because unification does not recognize (fun x => f x b) a when it sees f a b ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
| | | | | | | | | | | | | | | | | | | | | | | Inner sub-modules with "Definition t := t" is hard to handle by extraction: "type t = t" is recursive by default in OCaml, and the aliased t cannot easily be fully qualified if it comes from a higher unterminated module. There already exists some workarounds (generating Coq__XXX modules), but this isn't playing nicely with module types, where it's hard to insert code without breaking subtyping. To avoid falling too often in this situation, I've reorganized: - GenericMinMax : we do not try anymore to deduce facts about min by saying "min is a max on the reversed order". This hack was anyway not so nice, some code was duplicated nonetheless (at least statements), and the module structure was complex. - OrdersTac : by splitting the functor argument in two (EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid the need for aliasing the type t, cf NZOrder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16100 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
| | | | | | | hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making subset_eq_compat applying over more general domain "Type" (see #2938).Gravatar herbelin2012-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
| | | | | | | | | | themselves satisfied Uniqueness of Identity Proofs. Otherwise said uniqueness of equality proofs is enough to characterize types whose equality has a degenerated "homotopical" structure (this is a short proof of a result inspired by Voevodsky's proof of inclusion of h-level n into h-level n+1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolating the ingredients of the proof of Prop<>Type (r15973). SeeingGravatar herbelin2012-11-15
| | | | | | | it as a consequence of the derivability of Hurkens' paradox in the presence of a retract from Type to Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some lemmas on property of rewriting. It will probably be worth atGravatar herbelin2012-11-15
| | | | | | | some time to provide a library stating the groupoid structure of equality proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a proof that Prop<>Type, for arbitrary fixed Type.Gravatar herbelin2012-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15973 85f007b7-540e-0410-9357-904b9bb8a0f7
* A decidability property of functional relations over decidable codomains.Gravatar herbelin2012-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15972 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:29:08 +0000