Stream: Coq users

Topic: Meaning of p: nat ?


view this post on Zulip Anders Larsson (Apr 05 2022 at 19:41):

Quoted here is a typical example from Software Foundations. My novice question is, does the first row here p: nat "mean" anything?

I realize that the example wouldn't work if p had another type, like (p: Type) as the odd and even functions only accept nat. But it's still puzzling that p: nat is (or seem to be?) a hypothesis and not a "just" type declaration.
And so far p : nat and similar is seldom used. (Maybe they participate with the exists tactic sometimes.)

1 subgoal
p : nat
H : forall n : nat, even n = true -> even (S n) = false
H0 : forall n : nat, even n = false -> odd n = true
H1 : even p = true
______________________________________(1/1)
odd (S p) = true

(Maybe everything becomes clear when I come to the "The Curry-Howard Correspondence" chapter. Who knows? :-) )

view this post on Zulip Karl Palmskog (Apr 05 2022 at 19:44):

the general meaning of t : T is that: t is a term that has type T. So, p is here a term that has type nat, and nat is an inductive type defined in the standard library.

view this post on Zulip Karl Palmskog (Apr 05 2022 at 19:45):

there isn't much difference between a term-has-type declaration and a "hypothesis" inside a proof, if that's what you're after, they would both become part of the environment you're working in

view this post on Zulip Karl Palmskog (Apr 05 2022 at 19:52):

but maybe you are after some external mathematical explanation of what a typing judgment is? For example, this recent overview of some of the foundations used by Coq could be helpful.

view this post on Zulip Anders Larsson (Apr 05 2022 at 20:04):

Thanx for the comments and the PDF links. They seem to be somewhat close to what I can digest.

I'm slightly surprised that you call t in t : T a term and not a variable (yes, I'm a programmer. Maybe that shows).
I would have guessed it was a variable containing term of type T.

Coq and this type-centric world is a fascinating place.

view this post on Zulip Gaëtan Gilbert (Apr 05 2022 at 20:07):

yes, I would say that t : T (over the _____ line, or in a binder) is a variable not a term
(: can also be used in terms to force the type, eg (fun x => x) : nat -> nat is a valid term)

view this post on Zulip Gaëtan Gilbert (Apr 05 2022 at 20:09):

(of course a variable x can be used to make a term also written x so it can be a little confusing)

view this post on Zulip Karl Palmskog (Apr 05 2022 at 20:09):

I tend to divide into ground terms like 1, which are definitely not variables, and non-ground terms like x or S x, some of which, e.g., x behave like mathematical variables

view this post on Zulip Karl Palmskog (Apr 05 2022 at 20:10):

not sure this can be refined/justified more theoretically

view this post on Zulip Karl Palmskog (Apr 05 2022 at 20:12):

at least in HOL, which has simpler foundations, the t in t : T is defined as a term in the metalanguage, regardless of whether it's ground or not

view this post on Zulip Paolo Giarrusso (Apr 05 2022 at 22:29):

Even in simple type theory (hence HOL?), there’s a distinction between x : T (a variable) and t : T (a term). It’s not just a distinction for programmers.

view this post on Zulip Karl Palmskog (Apr 06 2022 at 08:26):

from HOL4:

> ``1 : num``;
val it = 1: term
> ``x : num``;
val it = x: term

the x is a (free) variable, sure, which is a form of term in HOL.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 08:29):

Variables are terms in Coq too, but a context is a list of variable : type pairs (with optional terms as definition bodies).

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 08:43):

To recap: all variables are terms; not all terms are variables; your context only can declare variables, not arbitrary terms.

view this post on Zulip Karl Palmskog (Apr 06 2022 at 08:55):

I think you have to qualify "context" to be in some abstract type-theoretic sense or at implementation level then, since users will be faced with stuff like this:

Section sec.
Context (x := 5 + 3).

Lemma x8 : x = 8.
Proof.
(* context shows x := 5 + 3 : nat *)
reflexivity.
Qed.
End sec.

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 09:00):

what qualification is needed?

view this post on Zulip Karl Palmskog (Apr 06 2022 at 09:03):

your context only can declare variables, not arbitrary terms.

Do you think x in my example is a variable? It sure seems declared by the context.

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 09:04):

x is a variable yes

view this post on Zulip Karl Palmskog (Apr 06 2022 at 09:05):

the usual meaning of variable, is that it is given meaning by substitution. But I don't see how I can substitute x for anything (it's already given a definite meaning)

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 09:07):

There is only one part of Coq's logic that is able to distinguish between variable and non-variable: dependent pattern-matching. And according to its rules x := 5 + 3 is not a variable.

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 09:13):

There is only one part of Coq's logic that is able to distinguish between variable and non-variable: dependent pattern-matching.

how so?

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 09:28):

The abstraction that is performed upon the branches of a match is forced to discard any definition and to keep only declarations. (Perhaps it is possible to create a kernel term with branches of the form let x := 5 + 3 in ... instead of fun x => ..., but this is certainly not available from the surface language.)

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 09:33):

can you give an example because I don't get it

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 09:41):

In a match construct, the return clause as well as the branches are all represented by abstractions. It is impossible to put a let-in construct in there. (At least not in the source language. I remember that, in the early days, SSReflect was wrecking havoc in the kernel by creating branches that were not abstractions.)

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 10:10):

that's not the case anymore since 8.14

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 10:11):

match branches (and return clause) have exactly the same shape as the context of the corresponding inductive (including let-ins)

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 10:11):

except that they don't store any data, just the names (no types, and no body for the let)

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 11:41):

Just by curiosity, does that mean that it would now be possible to lighten the requirement of the return clause being well-typed? (That is something we were discussing with Christine Paulin recently. This would give UIP in the general case, and hopefully without introducing any inconsistency, but who knows.)

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:51):

what does that mean?

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:51):

you need the type of the return clause to type check the match

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:52):

if it's not well-typed...

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:52):

(also, we already have UIP through SProp if you set the right flag)

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 11:53):

you could say that the return clause needs to be well-typed after substituting for each branch and for the return type, but not in its abstracted form

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:53):

how do you guarantee it's still well-typed as a type applied to variables?

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 11:55):

so you get

Definition K {A x} (e : x = x :> A) : e = eq_refl
  := match e as e in _ = y return e = eq_refl with eq_refl => eq_refl end.
(* inside branch: eq_refl = eq_refl
   return type: e = eq_refl with e : x = x *)

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 11:56):

Pierre-Marie Pédrot said:

how do you guarantee it's still well-typed as a type applied to variables?

not sure I understand the question but I guess you don't

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:57):

give me the typing rule of a match

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:57):

in your example if e : x = y it doesn't type check

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 11:59):

(I know that historically in the old CIC versions, pattern-matching was enforcing UIP, but I never quite understood the rule)

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 12:03):

something like

Γ  e : Ind params indices
Γ  rt[varis:=indices, vare:=e] : Type
Γ, patvars  branch : rt[varis:=indices of (c params patvars), vare:=(c params patvars)]
  (implies Γ, patvars  rt[...c params patvars...] : Type)
————————————————————————————————————————————————————————————————————————————
Γ  match e in Ind _ varis as vare return rt with c _ patvars => branch end : rt[varis:=indices, vare:=e]

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:04):

you forgot the type of the whole expression...

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 12:04):

lol

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:06):

how do you know that the substitution for the type of branches is valid?

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 12:06):

??

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:07):

I mean, you check it already when you say 'implies ...'

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 12:07):

the usual Γ ⊢ e : t ==> Γ ⊢ t : Type theorem

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:07):

I see

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 12:09):

the inference algorithm probably checks it semi-redundantly since it has to convert with whatever gets inferred for the branch

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 12:11):

As Gaetan said, what I meant is that the n+1 instances of the return clause are well-typed (with n the number of constructors), but the return clause itself does not need to be well-typed in isolation.

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 12:13):

Christine's claim is that this is strictly equivalent to UIP. (But I have yet to double check.)

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:13):

a least propositional UIP

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 12:14):

Yes.

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:15):

Isn't this what agda people call the difference between pattern matching and pattern matching without K? https://agda.readthedocs.io/en/v2.6.1/language/without-k.html

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:15):

not sure how you define being equivalent, because you'll probably get more reduction rules in one case still ?

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:16):

@Ali Caglayan at least that was the way 30 years ago people were calling these different things

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:16):

claims that "pattern-matching" (i.e. with K) was more expressive that MLTT recursors

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 12:17):

The reduction rules do not depend on the types, so I do not see how it would change anything in that regard.

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:18):

wdym? You can phrase UIP as "there exists an axiom uip : forall A (x : a) (e : x = x), e = refl"

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:18):

but this breaks canonicity immediately

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:18):

with the generalized pattern-matching you don't lose canonicity a priori

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:19):

(you might lose SN, in which case you lose canonicity strictly speaking but you still have progress)

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:19):

I guess you want uip to literally be refl, but that doesn't quite typecheck right?

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 12:20):

Yes, sorry, I thought you meant the reduction rules of the match construct. Indeed, you need a dedicated rule for UIP itself.

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:20):

this is definitional uip

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:20):

(I was answering to @Ali Caglayan )

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:22):

Since you can prove that uip = refl, definitional uip is the only way to have uip and canonicity right?

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:23):

looks like a legit argument but I am somewhat still unconvinced

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:25):

is the fact that CIC + pattern-matching with K not canonical a known thing?

view this post on Zulip Gaëtan Gilbert (Apr 06 2022 at 12:26):

uip=refl is not well typed

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:26):

If you match end points then it is true no?

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:26):

hmm, you can prove forall (e : x = x), e = refl for sure

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:27):

but by canonicity there is only one such closed e

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:27):

and that's refl, so your pattern-matching reduces

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:27):

this should still be canonical

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:28):

I believe I heard that lean3 does this now

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:28):

the Lean3 story is a totally different one

view this post on Zulip Pierre-Marie Pédrot (Apr 06 2022 at 12:28):

they have definitional UIP

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:28):

Ok I won't open that box here :)

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:30):

Going back to Guillaume's question, which J rule is the match supposed to be?

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:30):

The usual one or Christine's one?

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:31):

i.e. is the first end point of = an index or a parameter?

view this post on Zulip Ali Caglayan (Apr 06 2022 at 12:32):

Having an untyped return clause is like not typing J right?

view this post on Zulip Guillaume Melquiond (Apr 06 2022 at 12:33):

It is like not typing the argument P of J. J itself is still typed.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 13:47):

Karl Palmskog said:

the usual meaning of variable, is that it is given meaning by substitution. But I don't see how I can substitute x for anything (it's already given a definite meaning)

Yes, the context just instructs which substitution to use. "Variable" isn't a semantic or philosophical concept here...
Formally, we let x range over a countable set of variables, and define t ::= x | t t | lambda x. t | let x := t in t | ... — no difference here. The only funky thing is that Coq contexts are given Gamma ::= <empty> | Gamma, x : t | Gamma, x : t := t.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 13:51):

And indeed, the elaborated term x = 8 (or rather, @eq nat x 8) is the same no matter what x is bound to — depending on Gamma, it might be well-typed or not.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 13:53):

To be precise, I'm talking of the raw term/Curry term/preterm here — some formalisms combine the term and the typing derivation, while I'm talking of the term separate from the typing derivations.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 13:55):

since the term is the same, we can also substitute x by 7 or any other term — even if the result might not be well-typed.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 13:55):

And of course, if a term is typed assuming x := 8, substituting x by 7 won't preserve well-typing.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 14:03):

Having said all that, https://coq.inria.fr/refman/language/cic.html#id6 seems to claim that top-level definitions are constants. But that's a bit funny: the module system lets you instantiate Parameter by Definition but "not via constants" such as inductive types and their constructors...

Quotes:

Local context. A local context is an ordered list of declarations of variables. The declaration of a variable 𝑥 is either an assumption, written 𝑥:𝑇 (where 𝑇 is a type) or a definition, written 𝑥:=𝑡:𝑇.

Definitions are written as 𝑐:=𝑡:𝑇, indicating that 𝑐 has the value 𝑡 and type 𝑇. We shall call such names constants.

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 14:15):

To be clear: while all this is a matter of definitions, there are pretty standard ways to set things up in core calculi; but since calculi leave out top-level definitions, matters there are less standard :-)

view this post on Zulip Paolo Giarrusso (Apr 06 2022 at 14:18):

more precisely, standard in the type system community (and probably also in type theory?); I'm not speaking for interactive theorem proving/formal methods/... etc, because as usual they seem like separate communities.

view this post on Zulip Meven Lennon-Bertrand (Apr 07 2022 at 12:04):

Gaëtan Gilbert said:

the usual Γ ⊢ e : t ==> Γ ⊢ t : Type theorem

Validity is not a thing when you do bidirectional typing. Or rather, not for checking: if you call it (which is what you do with branches, at least in the current situation), then you must ensure that the type you give is well formed. Here it is not… So if you want to do that you’d have to at least separately check that the type you give for each branch is sensible.

view this post on Zulip James Wood (Apr 20 2022 at 09:00):

Ali Caglayan said:

Since you can prove that uip = refl, definitional uip is the only way to have uip and canonicity right?

Sorry for the late reply, but it looks like this wasn't cleared up. As I understand it, the claim was that ⊢ uip A x e : e = refl, so we should have uip A x e ↝ refl. But I think with a pattern-matching definition of uip, we already have this. Proof sketch: by canonicity (inductively), e must be refl. But in that case, we hit a pattern for uip, and indeed uip A x refl ↝ refl.


Last updated: Feb 06 2023 at 12:04 UTC