Stream: Coq users

Topic: Axioms Vs Inductive definitions

walker (May 18 2022 at 11:46):

I noted that all the the definitions that are inductively defined can also be defined as sepaarate Axioms and vice versa for instance the axioms of Hoare logic can be inductively defined in Coq, So when would the usage of axioms be different from inductive definition (I am asking from the logic perspective).

Ali Caglayan (May 18 2022 at 11:48):

Axioms don't have the ability to be destructed by a match statement.

Ali Caglayan (May 18 2022 at 11:49):

For instance you can do:

Axiom nat : Type.
Axiom O : nat.
Axiom S : nat -> nat.

But you won't be able to define a function on nat by cases and reduce it.

Ali Caglayan (May 18 2022 at 11:51):

Also, if you care about that sort of thing, inductive types are generally constructable out of sigma types and nat which means they exist in models of type theory, e.g. Set. By assuming axioms you have no guarantee that there is indeed an object that acts this way.

Ali Caglayan (May 18 2022 at 11:52):

Actually more important than functions is the fact that you have no dependent functions i.e. no induction principle. Natural numbers without induction aren't very good at proving much.

walker (May 18 2022 at 11:56):

What about the otherway around something that are axiomatic by nature but then it gets represented by inductive types such as axioms of hoare logic, or separation logic ? I think those do work as axioms on their own yet when developed in coq they are not presented as axioms

Ali Caglayan (May 18 2022 at 11:57):

People define "axioms of logic" all the time using inductive types. However don't conflate the two uses of the word axiom here. One is about the metatheory (Coq) the other has only the meaning you intend to give it. :-)

Ali Caglayan (May 18 2022 at 12:00):

It's the same as usual mathematics: When formalizing Set theory in ZFC you never assume extra axioms on top of ZFC to talk about models of set theory, you simply have a set of sentences which you term "axioms".

Ali Caglayan (May 18 2022 at 12:01):

A simpler example is Peano arithmetic, which is just a list of arithmetic statements you expect should hold and these are termed axioms.

walker (May 18 2022 at 12:01):

because those are provable in ZFC,

walker (May 18 2022 at 12:02):

But axiom of choice is not povable in ZF so they decided to add when when they need it.

walker (May 18 2022 at 12:02):

I assume that hoare logic axioms are not provable in CIC so why was "lets assume CIC + hoare logic axioms" not the way to go ?

walker (May 18 2022 at 12:03):

also I could be wrong, I am just trying to understand why no one did it

Karl Palmskog (May 18 2022 at 12:03):

here is what the ANSSI guide to reviewing Coq code says about axioms:

The introduction of an axiom is delicate, as it may result in making the Coq logic inconsistent. Besides, certain “standard axioms” are known to be inconsistent with Coq logic (e.g., the axiom of description together with the excluded middle). However, the standard library of Coq provides several axioms that can be safely added to Coq, according to the Coq FAQ. That being said, the standard library provides the means to avoid using most of these axioms. For instance, e.g., generalized rewriting can be leveraged in place of relying on the proof irrelevance and functional extensionality axioms.

Ali Caglayan (May 18 2022 at 12:04):

I think you are getting confused here. When you study "hoare logic" in CIC or set theory, you are not "proving its axioms" that doesn't even make sense in most cases because proof systems can have different languages.

Ali Caglayan (May 18 2022 at 12:05):

You can sit down and foramlize the syntax of "hoare logic" in CIC or set theory, and then prove things about it. But the metatheory and theory of hoare logic don't coincide.

Ali Caglayan (May 18 2022 at 12:06):

That's how logic is typically studied in mathematics.

Ali Caglayan (May 18 2022 at 12:06):

Of course there are ways to make the metatheory and theory coincide (somewhat) but this is quite a complicated and delicate topic.

walker (May 18 2022 at 12:07):

Where can I read more about that ?

Ali Caglayan (May 18 2022 at 12:09):

Well there are efforts to formalize the CIC in CIC such as metacoq https://github.com/MetaCoq/metacoq and in mathematical logic you have "formal theories of truth" or "axiomatic theories of truth". I would warn you however, none of this would make much sense without having studied some logic first.

walker (May 18 2022 at 12:10):

I assume boolean logic does not qualify ?

Ali Caglayan (May 18 2022 at 12:10):

If you learn about Godels incompleteness theorem, then you can see these as efforts to thwart it as much as possible.

Ali Caglayan (May 18 2022 at 12:11):

If by boolean logic you mean propositional logic, then probably not since it is too weak to begin talking about its own metatheory.

walker (May 18 2022 at 12:12):

understood, then I got lots of reading to do, sadly..

Karl Palmskog (May 18 2022 at 12:12):

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Ali Caglayan (May 18 2022 at 12:13):

Karl Palmskog said:

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Right, this is what I hinted at when I talked about models earlier up.

Karl Palmskog (May 18 2022 at 12:13):

some systems such as HOL don't even have inductive types built in, instead you have to use "definitional packages" to get something resembling inductive types (but which are just regular stuff, no special status)

Ali Caglayan (May 18 2022 at 12:13):

My advice would be read up on Godel's incompleteness theorems since they will pull in most of the logical theory you need.

walker (May 18 2022 at 12:14):

Ali Caglayan said:

Karl Palmskog said:

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Right, this is what I hinted at when I talked about models earlier up.

My problem is I cannot intuit the reason that gives inductive types this advantage.

walker (May 18 2022 at 12:14):

Ali Caglayan said:

My advice would be read up on Godel's incompleteness theorems since they will pull in most of the logical theory you need.

I will start by reading about that, thanks a lot!

Ali Caglayan (May 18 2022 at 12:15):

walker said:

Ali Caglayan said:

Karl Palmskog said:

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Right, this is what I hinted at when I talked about models earlier up.

My problem is I cannot intuit the reason that gives inductive types this advantage.

If I write down an inductive types there is a "process" that lets me turn it into an equivalent type made out of simpler type formers such as sigma types and the natural numbers. Those are constructable in models of type theory hence it is consistent to assume inductive types exist (they have a possible implementation always).

Ali Caglayan (May 18 2022 at 12:16):

There is no guarantee when I write down an axiom, I am just assuming it.

Ali Caglayan (May 18 2022 at 12:16):

For instance I can write Axiom oops : 0 = 1. and this wouldn't be great for my formalization since I can derive falsehood and prove anything.

Ali Caglayan (May 18 2022 at 12:17):

There are much less obvious axioms which one could assume, that could unintentionally lead to contradictions.

Ali Caglayan (May 18 2022 at 12:17):

Hence what Karl said.

walker (May 18 2022 at 12:18):

understood, I will read about the incompleteness theorem (I vaguely know what is it about but I think I will read the proof now) and move from there.

Paolo Giarrusso (May 18 2022 at 17:50):

I'm not sure I understand why the Gödel theorems are relevant to Hoare logic...

Paolo Giarrusso (May 18 2022 at 17:53):

Ali Caglayan said:

I think you are getting confused here. When you study "hoare logic" in CIC or set theory, you are not "proving its axioms" that doesn't even make sense in most cases because proof systems can have different languages.

To me, of course you want to "prove the axioms of Hoare logic" — by giving a model

Karl Palmskog (May 18 2022 at 17:56):

hmm, I thought one could justify Hoare logic rules by giving a WP calculus and proving relative completeness, etc.

Karl Palmskog (May 18 2022 at 17:58):

the whole "giving a model" stuff sounds separation logic-y

Paolo Giarrusso (May 18 2022 at 18:52):

Separation logic is a kind of Hoare logic, and for this discussion I think they are the same thing.

Paolo Giarrusso (May 18 2022 at 18:56):

Iris treats { P } e { Q } as a notation for P -* WP e { Q }, so I don't know if translating between the two notations is a very interesting proof?

Paolo Giarrusso (May 18 2022 at 18:58):

there might be another cultural divide elsewhere, but a more interesting proof seems the one relating "axiomatic semantics" to e.g. operational semantics.

Paolo Giarrusso (May 18 2022 at 19:01):

or to the "canonical" semantics for your programming language (the one that's the official "language definition"), whatever that is.

Karl Palmskog (May 18 2022 at 19:05):

but if you define P e Q using a WP calculus, then your Hoare "rules" are not axioms anyway. To me, it's fine to make the WP calculus definition the canonical semantics. But sure, it's a form of validating/justifying one form of semantics if you relate it to another form

Karl Palmskog (May 18 2022 at 19:08):

but a WP calculus is a form of characterization of the state you get after running a program. It's an unambiguous description that could be used by a compiler implementer. Where does the model stuff come in? Is it really needed?

Paolo Giarrusso (May 18 2022 at 19:09):

because of that notational, I'm not sure what's the difference between Hoare logic and WP semantics. Are you saying that people would choose different axioms in the two?

Paolo Giarrusso (May 18 2022 at 19:09):

(I'd say the standard Hoare rules for loops seem something I'd want to prove and not a primitive)

Karl Palmskog (May 18 2022 at 19:11):

in my reading of the classic presentation, the Hoare logic rules are taken as given "from nothing". You could/should declare them axiomatically as a bunch of logical implications.

Paolo Giarrusso (May 18 2022 at 19:12):

sure, that seems mostly a stylistic choice. You can take those as primitive or prove them sound relative to an operational semantics.

Karl Palmskog (May 18 2022 at 19:12):

then people figure out that this WP stuff, with an actual predicate transformer function, is actually a better way to do it, both in implementation and in formalization

Paolo Giarrusso (May 18 2022 at 19:13):

one Hoare-separation difference is that it's probably more reasonable to take a Hoare logic than a modern separation logic as primitive — with some emphasis on "modern"

Paolo Giarrusso (May 18 2022 at 19:14):

but a WP calculus is a form of characterization of the state you get after running a program.

I don't think that's of the WP rules in Iris, but that might be on the "modern separation logic" part in Iris

Paolo Giarrusso (May 18 2022 at 19:16):

I just checked software foundations, and they indeed use a shallow embedding of Hoare logic using operational semantics: https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html#hoare_triple

Karl Palmskog (May 18 2022 at 19:18):

yeah, I guess you can do that, but that's not how it's done classically I believe? the most convincing formalizations separate each semantic approach and have standalone theorems connecting them

Paolo Giarrusso (May 18 2022 at 19:19):

I'm not pushing strongly for shallow embeddings, just saying "here's a common textbook which gives a model for Hoare logic"

Karl Palmskog (May 18 2022 at 19:20):

ah OK, so that's what you mean by give a model in this context

Paolo Giarrusso (May 18 2022 at 19:21):

yep, that's what we do in separation logics as well

Paolo Giarrusso (May 18 2022 at 19:21):

I wasn't hinting at domain-theoretic denotational semantics or anything like that :sweat_smile:

Karl Palmskog (May 18 2022 at 19:22):

but we agree that one could just as well take the Hoare-sep-log as primitive, and prove the opsem "correct" by giving it a "Hoare model"? Or one might say: interpreting the opsem in terms of Hoare-sep-log

Paolo Giarrusso (May 18 2022 at 19:24):

yes, tho I confess I wouldn't know how to set that up — but I recall Mitchell's Foundations of Programming Languages shows both directions?

Paolo Giarrusso (May 18 2022 at 19:25):

in practice, if you used Iris, then Iris experts might object strongly but for other reasons (and I suspect the same could be true in other such logics)

Karl Palmskog (May 18 2022 at 19:26):

hmm, but couldn't I write my WP calculus / predicate transformer separately from Iris?

Karl Palmskog (May 18 2022 at 19:26):

and then just plug it in and get proof mode stuff?

Paolo Giarrusso (May 18 2022 at 19:27):

re proofmode: yes but let's set that aside

Paolo Giarrusso (May 18 2022 at 19:30):

re "separate WP calculus", wikipedia's example has an imperative language without aliasing, which simplifies questions a bit too much

Karl Palmskog (May 18 2022 at 19:31):

my naive understanding has been that if I bring with me some PL semantics in some reasonable form, I can get something close to "my own VST" from Iris, i.e., a Hoare interface of sorts to prove my before-after specs for stateful programs

Paolo Giarrusso (May 18 2022 at 19:32):

Iris is a flexible framework, but the Iris program logics proper demands specifically an operational semantics

Karl Palmskog (May 18 2022 at 19:33):

ah, so the Iris WP calc is "fixed" and based on the operational semantics parameter?

Karl Palmskog (May 18 2022 at 19:33):

that's a bit less flexible than I expected

Paolo Giarrusso (May 18 2022 at 19:34):

the definition of WP by the core program logic is fixed and based on operational semantics; the "actual WP calculus" is something that you derive on top...

Paolo Giarrusso (May 18 2022 at 19:34):

but also

Paolo Giarrusso (May 18 2022 at 19:34):

you _can_ swap out the program logics with something else.

Paolo Giarrusso (May 18 2022 at 19:35):

you can just reuse the proofmode (as you said), or you can also reuse the Iris base logic (which gives you step-indexing, higher-order ghost state, etc.)

Paolo Giarrusso (May 18 2022 at 19:36):

I think the main rub is that nobody knows how to make sense of _step-indexing_ without steps

Paolo Giarrusso (May 18 2022 at 19:37):

and that there are too many ways to write fancy theorems which amount to True or False -> ...

Paolo Giarrusso (May 18 2022 at 19:38):

(a funny way to write True is ∃ i, \later^i False)

Paolo Giarrusso (May 18 2022 at 19:39):

just for reference, the abstract https://drops.dagstuhl.de/opus/volltexte/2017/7275/ also mentions that Iris relies on some operational semantics:

Iris only applies to languages with an operational interleaving semantic

Karl Palmskog (May 18 2022 at 19:39):

hmm, I think this is the problem with these separation logic specs, there are so many fancy built-in predicates it's really hard to follow what's going on

Paolo Giarrusso (May 18 2022 at 19:39):

yeah that's basically it

Karl Palmskog (May 18 2022 at 19:40):

ah, interesting, then also the Nuprl style "logic of events" is ruled out (based on happens-before relation rather than interleaving)

Paolo Giarrusso (May 18 2022 at 19:41):

and there are tons of "obviously true" rules which are unsound — if you store propositions P in ghost state, for instance, you can't read them precisely

Paolo Giarrusso (May 18 2022 at 19:42):

more accurately: if you store step-indexed predicates in ghost state :wink:

Paolo Giarrusso (May 18 2022 at 19:42):

I don't know that logic of events but I've seen happens-before for concurrency, and that paper transforms indeed such an axiomatic semantics (for C/C++/...) into an operational one to apply Iris on top.

Paolo Giarrusso (May 18 2022 at 19:45):

anyway, you shouldn't worry about those fancy predicates for Iris works: they apply Iris adequacy to end up with Iris-free top-level theorems about operational semantic traces

Karl Palmskog (May 18 2022 at 19:47):

I think I would be happy with trace properties as a final deliverable regardless of whether they came out of an operational semantics or not. Nakata and Uustalu even did a Hoare logic over traces, so it should be doable in Iris?

walker (May 18 2022 at 19:49):

/me trying to follow the dicussion, the problem is there are things I don't know and I don't even know what they are.

Karl Palmskog (May 18 2022 at 19:51):

the recent discussion has been about programming language theory, in particular programming language semantics. I think it's a bit unfortunate that Hoare conflated his particular PL semantics style with "logic" and "axioms"

Karl Palmskog (May 18 2022 at 19:52):

I think there are other semantics styles that could just as well be said to be about logic, such as denotational

Paolo Giarrusso (May 18 2022 at 19:53):

@walker sorry for hijacking the discussion, this discussion is probably not the most accessible

Paolo Giarrusso (May 18 2022 at 19:54):

but back to your questions, it's not impossible that Gödel's theorems are relevant, I just guess they're unlikely to be especially relevant depending on what you want to do

Paolo Giarrusso (May 18 2022 at 19:55):

maybe if you say a bit more we can be more helpful

walker (May 18 2022 at 19:59):

So let me see, I was watching prof Dreyer talking once about Iris and saying that the problem with previous separation logic is that have complex axioms, but then When I read an iris journal paper for iris 3, The axioms (I am not even sure if that is the right name) are really really complex. So I thought that perhaps a better approach would be to extend CIC to reason about pointer accesses given that CIC is powerful, this might be similar to the way typed lambda calculus was extended with inductive constructions to form CIC. But given my theoretical knowledge is really shallow, I wanted to know why didn't anyone do that before.

Paolo Giarrusso (May 18 2022 at 20:00):

walker said:

I assume that hoare logic axioms are not provable in CIC so why was "lets assume CIC + hoare logic axioms" not the way to go ?

https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html "proves the axioms" of Hoare logic

walker (May 18 2022 at 20:01):

it feels to me that they didn't prove it, they modeled it ?

walker (May 18 2022 at 20:02):

isn't it possible to also model unsound logic rules the same way ?

Paolo Giarrusso (May 18 2022 at 20:02):

no you can't model unsound logics

Paolo Giarrusso (May 18 2022 at 20:03):

or rather: the point of a modeling logic A (hoare logic) in logic B (Coq) is to prove relative soundness: if A is unsound, then B is unsound as well!

Paolo Giarrusso (May 18 2022 at 20:04):

From another POV:

So I thought that perhaps a better approach would be to extend CIC to reason about pointer accesses given that CIC is powerful, this might be similar to the way typed lambda calculus was extended with inductive constructions to form CIC.

When people add rules to CIC, they also write complex proofs to make sure those rules are sound.

Paolo Giarrusso (May 18 2022 at 20:05):

Finally, people _have_ built tools that take complex separation logics as primitive rules. The only question is whether those axioms are true.

walker (May 18 2022 at 20:06):

Paolo Giarrusso said:

When people add rules to CIC, they also write complex proofs to make sure those rules are sound.

Are these proofs something different from the local soundness and local completeness proofs (eliminating introductions and going the other way round)?

Paolo Giarrusso (May 18 2022 at 20:07):

it sounds like you're referring to Pfenning's concepts? Those are different indeed.

Paolo Giarrusso (May 18 2022 at 20:07):

(deleted)

Paolo Giarrusso (May 18 2022 at 20:07):

sorry

walker (May 18 2022 at 20:07):

Paolo Giarrusso said:

it sounds like you're referring to Pfenning's concepts? Those are different indeed.

Yes I learned it from one of his lectures.

Paolo Giarrusso (May 18 2022 at 20:08):

Reposting:

Finally, people _have_ built tools that take complex separation logics as primitive rules. The only question is whether those axioms are true.

... It's a bit as if somebody wrote rules as complex as those of Iris, said "these rules are obviously sound", and skipped writing a proof.

walker (May 18 2022 at 20:08):

Paolo Giarrusso said:

Reposting:

Finally, people _have_ built tools that take complex separation logics as primitive rules. The only question is whether those axioms are true.

... It's a bit as if somebody wrote rules as complex as those of Iris, said "these rules are obviously sound", and skipped writing a proof.

yes I understand.

walker (May 18 2022 at 20:09):

one last question, so what is the problem with Pfenning's concepts approach to soundness and completeness proofs?

Paolo Giarrusso (May 18 2022 at 20:10):

there's no problem, but the soundness in "local soundness" is just a different thing.

Paolo Giarrusso (May 18 2022 at 20:10):

(I'm not even entirely sure why it has that name...)

walker (May 18 2022 at 20:11):

I understand ... thanks for the discussion I will do a bit more research/ learning.

Paolo Giarrusso (May 18 2022 at 20:11):

I should take back the last answer; I'm not entirely sure

walker (May 18 2022 at 20:12):

If I recall correctly he always talked about local soundeness vs global soundness but never mentioned what that global soundness is.

Paolo Giarrusso (May 18 2022 at 20:12):

but "soundness" in general means "you can't prove False", and for a logic as complex as Coq you can't just prove local soundness

Paolo Giarrusso (May 18 2022 at 20:14):

for instance, Coq's soundness is proven by showing that there's all proofs can be normalized, and that there's no proof of False in normal form

Paolo Giarrusso (May 18 2022 at 20:14):

(oversimplifying quite a bit!)

Paolo Giarrusso (May 18 2022 at 20:14):

"no proof of False in normal form" is typically easy

Paolo Giarrusso (May 18 2022 at 20:15):

"all proofs can be normalized" is very hard

walker (May 18 2022 at 20:15):

Paolo Giarrusso said:

but "soundness" in general means "you can't prove False", and for a logic as complex as Coq you can't just prove local soundness

It is funny because Coq's logic looks deceivingly simple and very very small so I would never think of it as complex until I hear from people or go read papers about metacoq.

Gaëtan Gilbert (May 18 2022 at 20:17):

https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions is not that simple or small

Gaëtan Gilbert (May 18 2022 at 20:17):

imo

walker (May 18 2022 at 20:19):

the notion looks complex, but I assumed they are the ones here https://hal.inria.fr/hal-01094195/document

Karl Palmskog (May 18 2022 at 20:22):

nearly all of us want inductive types to get our work done. So we can either choose to build inductive types from inside the logic (lots of encoding work), or the designers of the logic can make inductive types primitive. If we do the latter, the designers and implementers of the logic have a lot of work to prove soundness. With a logic without inductive types, we have to do work over and over to get inductive types, but we know we are sound without extra work.

Ali Caglayan (May 18 2022 at 20:25):

Paolo Giarrusso said:

I'm not sure I understand why the Gödel theorems are relevant to Hoare logic...

I mentioned Godel not because I know anything about Hoare, but because it highlights the difficulties in formalizing logic in logic. The question from before was roughly "where can I learn about logics who are their own meta theory" and I replied with some pointers but that in order to appreciate them, studying Godel is a good first step.

Paolo Giarrusso (May 18 2022 at 20:27):

@Karl Palmskog we know they’re sound, but I’ve seen people point out that “do they have the right meaning?” can be tricky (e.g. Enrico I think brought that up?)

Karl Palmskog (May 18 2022 at 20:29):

I agree, if you make inductive types primitive, there are many ways that can be sound but useless/strange

Paolo Giarrusso (May 18 2022 at 20:29):

Enrico’s point was about the encodings

Karl Palmskog (May 18 2022 at 20:30):

OK, a logic like HOL is to me a very "extensional" logic - one shouldn't really look inside, just take stuff at face value.

Karl Palmskog (May 18 2022 at 20:31):

so most of the time, you don't really care that these encodings of inductive types are super convoluted, because the system shields you from the horrible details

Paolo Giarrusso (May 18 2022 at 20:31):

But what happens if the elaboration in HOL is buggy?

Karl Palmskog (May 18 2022 at 20:31):

I can definitely see that in a "non-extensional" theory like Coq's, bad encodings can make the whole thing crumble

Karl Palmskog (May 18 2022 at 20:32):

I mean, someone can correct me here, but HOL really doesn't do much elaboration, at least it's very modest [compared to Coq]

Paolo Giarrusso (May 18 2022 at 20:32):

You know HOL better than me, but in principle a buggy encoding could let you prove 0 = 1, right?

Karl Palmskog (May 18 2022 at 20:33):

every definition has to go through the core operations

Paolo Giarrusso (May 18 2022 at 20:33):

Of course, but that doesn’t prevent Pollack inconsistency

Karl Palmskog (May 18 2022 at 20:33):

OK, sure, yes, HOL doesn't protect from that

Paolo Giarrusso (May 18 2022 at 20:34):

And maybe 0 = 1 holds because the code that encodes inductive types has a Pollack-inconsistency bug,

Karl Palmskog (May 18 2022 at 20:34):

hmm, not immediately obvious, but, maybe?

Karl Palmskog (May 18 2022 at 20:35):

I have a colleague who works on soundness of Isabelle/HOL kernel, can ask him at some point

Paolo Giarrusso (May 18 2022 at 20:36):

IIUC, this isn't about the "kernel"

Karl Palmskog (May 18 2022 at 20:36):

the definitional mechanism interacts directly with the kernel

Paolo Giarrusso (May 18 2022 at 20:37):

but IIUC somebody (@Enrico Tassi ?) was pointing out that HOL does not let you prove 0 = 1, only "crazy encoding of 0 = crazy encoding of 1", so if the crazy encoding is subtly wrong it could produce equivalent results for 0 and 1

Paolo Giarrusso (May 18 2022 at 20:38):

hence (he said) if you don't check that the crazy encoding did the right thing, you need to treat it as part of your TCB. Which seems pretty much tautological.

Karl Palmskog (May 18 2022 at 20:38):

not sure how that would work, but I can't say it's impossible

Paolo Giarrusso (May 18 2022 at 20:38):

Coq elaboration has the same problem in principle, but people here suggest you should look at the elaboration result for the top-level theorems

Paolo Giarrusso (May 18 2022 at 20:39):

(anyway, sorry @walker we digressed again in your thread)

walker (May 18 2022 at 21:20):

don't be sorry, I am really enjoying reading stuff.

Enrico Tassi (May 19 2022 at 05:32):

I confirm I consider the non trivial encoding of datatypes in HOL part of TCB, exactly as the positivity checker or the termination checker are part of the Coq one. But some Isabelle core devs had different ipinions IIRC last time a loophole was found in their datatype definitiona mechanism (which let you prove false in HOL but not in Pure).

The elboration of Coq can be left out since its output is not totally different than the input, still you can have Pollack's inconsistencies due to notations and stuff like that... but well, that is a matter of UI to me: it is like if vscode would stop colorimg errors in red, not food for logicians :-)

Guillaume Melquiond (May 19 2022 at 06:31):

I think Coq's users are a bit too eager to forget that there is a ton of encoding in Coq too. Equality, existential, disjunction, even implication, are all encoded. And there is not even a consensus about this encoding. We had to modify the public API of Coq to please the many users that redefine equality with their own version.

Pierre-Marie Pédrot (May 19 2022 at 06:35):

Where do you put the limit between an encoding and a definition then?

Guillaume Melquiond (May 19 2022 at 06:38):

There is no limit. There is a continuum. My point was more than, if you actually compare the encoding of 0 = 1 in HOL and Coq, the one in HOL does not look so crazy anymore.

Guillaume Melquiond (May 19 2022 at 06:47):

For example, if you take a bunch of students with only basic knowledge of first-order logic, set theory, Peano's arithmetic, etc, I would not be surprised if you can convince them faster that the HOL's encoding of 0 = 1 makes sense.

walker (May 19 2022 at 10:32):

quick question, is coq not a HOL ? @Guillaume Melquiond you are putting distinction between both of them ?

Enrico Tassi (May 19 2022 at 10:39):

I'm a bit lost, how can you see peano numbers in Coq as encoded? They are literally how you find them on paper.

Karl Palmskog (May 19 2022 at 12:04):

"HOL" is usually used to mean a specific higher order logic variant: https://plato.stanford.edu/entries/type-theory-church/

This does not rule out that there are other higher order logics

Guillaume Melquiond (May 19 2022 at 12:12):

Enrico Tassi said:

I'm a bit lost, how can you see peano numbers in Coq as encoded? They are literally how you find them on paper.

No, Peano never talked about inductive types. And the equality he used was the primitive one from the logic, not a really strange thing with hard to explain eliminators.

Guillaume Melquiond (May 19 2022 at 12:15):

walker said:

quick question, is coq not a HOL ?

And to extend on Karl's answer, what people tend to call HOL (written as such) is the logic used in the HOL family of proof systems: Isabelle/HOL, HOL4, HOL Light, and so on. Coq is completely unrelated to it and follows different paradigms.

Enrico Tassi (May 19 2022 at 13:31):

Hum, it did no call it as such because the concept was not there... But the fact that naturals are made of a base symbol and another one meaning the successor is, afaict, very close to what the inductive nat says in Coq. If you start to define plus as a type theoretic function with computational rules the you start to diverge, but you don't need that to write 0=1. And the equal of Coq is the equality of the logic. The inductive incarnates the introduction and elimination of that concept, which is hardcoded (unlike say, setoids). That is technical to explain, sure.

Karl Palmskog (May 19 2022 at 15:48):

maybe relevant here, the paper on the verified subset of HOL Light incl user interaction came out: https://cakeml.org/itp22-candle.pdf

It outlines what is typically assumed in a proof assistant implementation (background ZF(C) set theory)

Last updated: Sep 30 2023 at 05:01 UTC