Re: [Hol-info] Definitions of partial functions (incl. predicates)

My intuition says that working with total functions (and especially predicates) will be easier. Why? I don't know exactly, but here are some possible reasons: you can just use plain rewriting rather than conditional rewriting, and you don't need to state so many assumptions explicitly on your

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Great! sure, I’ll do that! —Chun > Il giorno 05 ott 2017, alle ore 23:16, Ramana Kumar > ha scritto: > > I think it would be good to add this UNIQUE constant to listTheory, if you > have time to make a pull request. > > On 6 October 2017 at 01:49, Chun Tian

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

I think it would be good to add this UNIQUE constant to listTheory, if you have time to make a pull request. On 6 October 2017 at 01:49, Chun Tian (binghe) wrote: > Let me close this question (further comments are welcome, of course). > > I actually got another good

[Hol-info] Definitions of partial functions (incl. predicates)

Hello. What is the preferred way to define functions only for some values? For example, as in arithmetic$DIV in HOL?: ⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n) Here nothing is asserted for the value of DIV for n = 0, thus it is “undefined” in some sense. I know that this can

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Jeremy, >My dominant recollection is the difficulty of getting the system to do the >right type inference, and getting terms to typecheck. I was forever working >out where I needed to put in type annotations. In Coq and Mizar I don't have this experience, in the sense that I hardly ever need

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Let me close this question (further comments are welcome, of course). I actually got another good definition from Robert Beers in a private email: [UNIQUE_DEF] Definition |- ∀x L. UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2 This form is very useful for

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

On 05/10/17 11:53, Jeremy Dawson wrote: > Hi Mario, > > Slightly off-topic, I had experience with the type system of HOL-Omega > (system F, if I recall the terminology right, not dependent types, so my > experience may not be very relevant) > > My dominant recollection is the difficulty of

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Chun Tian, I don't know much about rich(er) type systems, and I'm not well acquainted with Coq, but I'd say that what can be done in Isabelle or HOL should be possible also in richer type systems. Regarding modelling of a proof, the context of what I said is describing, in HOL or

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

On 04/10/17 20:09, Ramana Kumar wrote: > Perhaps it would make more sense to ask people who are using rich type > systems what their motivations are :) > (On this list it's probably mostly people who are satisfied with simple > type theory.) Yes, you are right. I wrote to this list because I am

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Jeremy, I have a relevant question: one time we talked about the differences between Coq and HOL (thread title: "Difficulties when migrating proof scripts from Coq”), and you said: "There's a distinction between an inductively defined set (in Isabelle or HOL) and a datatype, though they can

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Mario, I don't mind the question, but the answer may not be much use because it's a comparison between the 2005 version of Isabelle which I use and HOL4. In terms of the type systems they are identical. Isabelle has schematic variables and type classes, both of which can make proof

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Mario, Slightly off-topic, I had experience with the type system of HOL-Omega (system F, if I recall the terminology right, not dependent types, so my experience may not be very relevant) My dominant recollection is the difficulty of getting the system to do the right type inference, and

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

OK, thanks everyone! So FILTER is what I must use. I think I’m going to use ``(FILTER (\e. e = X) L = [X])`` to assert the unique appearance of X in list L, and after I split the list using MEM_SPLIT, my target props (~MEM X l1) could be re-expressed by EVERY and FILTER, then it may be

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Among others, LENGTH (FILTER (\e. X = e)) = 1 Scott > On 2017/10/05, at 15:55, Chun Tian (binghe) wrote: > > But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just > the appearance of certain element is only one. —Chun > >> Il giorno 05 ott 2017,

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just the appearance of certain element is only one. —Chun > Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind > ha scritto: > > Hi Chun Tian, > > The constant ALL_DISTINCT in listTheory is

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Hi Anthony, Thanks. This definition may work (at least I can see it’s correct), at least that’s what I can start with. But in my proof the next move will be using MEM_SPLIT to divide the list into three pieces: [MEM_SPLIT] Theorem |- ∀x l. MEM x l ⇔ ∃l1 l2. l = l1 ⧺ x::l2 and what I

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Hi Chun Tian, The constant ALL_DISTINCT in listTheory is what you are looking for, I think. Konrad. On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) wrote: > Hi, > > (I'm new to HOL's listTheory). Suppose I have a list L which contains > possibly duplicated

[Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Hi, (I'm new to HOL's listTheory). Suppose I have a list L which contains possibly duplicated elements, and I want to express certain element X is unique (i.e. has only one copy) in that list. How can I do this? It seems "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``. Regards, Chun

[Hol-info] LRTC (Reflexive Transitive Closure with a List)

Hi, In listTheory there's a concept called "LRC": (* -- LRC Where NRC has the number of steps in a transitive path, LRC has a list of the elements in the path (excluding the rightmost)

Re: [Hol-info] Changing thms used by computeLib

Unfortunately I don't know anything better than "run it again". You could also maybe try an older HOL commit (maybe prior to d52c7d66716ddd253b6fd40bd3d38b29a238c392) and see if that's any more reliable. This is all speculation on my part though. The problem could have nothing to do with pointer

Re: [Hol-info] Changing thms used by computeLib

Hello Ramana, yes, the Mk_comb error occurs non-deterministic. Is there a temporary workaround for this, that I could make use of? Cheers, Heiko On 10/05/2017 12:43 PM, Ramana Kumar wrote: Hi Heiko, Does it fail every time when you try to run the proofs non-interactively (with Holmake)?

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hi Ramana, >Perhaps it would make more sense to ask people who are using rich type >systems what their motivations are :) >(On this list it's probably mostly people who are satisfied with simple >type theory.) One can do everything with anything. So dependent tpes certainly are not _needed_ for

[Hol-info] Changing thms used by computeLib

Hello, I have some proofs that I could previously solve by running EVAL_TAC, after modifying computeLib.the_compset with val _ = computeLib.del_funs [sptreeTheory.subspt_def] val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER, sptreeTheory.subspt_eq] As it turns out, the