Zulip Chat Archive

Stream: new members

Topic: Difference between constant and axioms


view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 06:38):

I just noticed that propext is defined as a constant:

constant propext {a b : Prop} : (a  b)  a = b

Is this an alternative to axiom? What would change if I made it an axiom?

view this post on Zulip Kenny Lau (Dec 31 2018 at 06:41):

nothing at all

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 06:45):

Why are there two different commands then? I would think it may make sense to use axiom for things whose type has type Prop and constant for things whose type has some other type (like a function), but the two examples I've seen are exactly the opposite.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 06:47):

I.e. choice defines a function and is an axiom but propext defines a (unproven) proof and is a constant.

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 09:25):

There's no difference between theorem and lemma of course. But for constants and axioms I thought the rule of thumb was that constants were for data and axioms for propositions. As you spotted, this convention does not seem to be being followed here

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 09:37):

The main difference between data and propositions in Lean is that Lean remembers how you constructed data but throws away your proof of a proposition and just remembers that it's proved. But of course here with constants and axioms this information doesn't exist, so they feel a lot more similar to each other than theorems and definitions do. If you're brave enough to look at Lean's source code and know enough C++ to understand it then you could maybe just check to see what the difference is.

view this post on Zulip Gabriel Ebner (Dec 31 2018 at 09:41):

Interestingly enough, propext was an axiom four years ago: https://github.com/leanprover/lean/blob/0da4f191fc2a37e34d53179d5cf924021de4fd15/library/logic/axioms/propext.lean
But yeah, it doesn't matter that much. In the C++ code, you could tell the difference between axiom and constant, but this is not really used and not exposed to lean either. Another difference is that you can do meta constant but not meta axiom.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:22):

By the way, propext and funext together prove that all proofs (of a proposition) are equal, don't they? Since propext shows that f(trivial) = trivial, g(trivial) = trivial for any two functions f : true \to P and g : true \to P. So does that mean type theories in which proofs are distinct lack propext?

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:23):

You don't need any axioms to prove that.

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 10:24):

I think the extra "axiom" is not just that all proofs of P are equal, but that they are definitionally equal.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:24):

look at the theorem proof_irrel.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:25):

Oh. rfl is just anti-climactic.

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 10:26):

:-)

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:26):

But I see actually, even if it wasn't definitional, then propext would imply that anyway.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:27):

Because every true Prop would be equal to true and true has only one proof.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:29):

Proof relevant type theories tend to lack the type Prop altogether I think. Proof irrelevance is the only thing distinguishing Prop and Type so propositions tend to be defined using Type and some of them I think have an is_Prop predicate that says that the type has only one element.

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 10:29):

My recent thoughts about quot, and Mario's comments about them (sparked by Chris' observation that I used quot.sound to prove quot'.sound) made all this a bit clearer to me. There is just a whole bunch of stuff which, if you don't have it, would make maths basically impossible to do, and the CS people have made what appears to a mathematician to be a random small set of this stuff into axioms and then deduced all the rest of it. I'm not sure that the fact that propext is an axiom is remotely important.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:36):

Because every true Prop would be equal to true and true has only one proof.

When I try writing that proof, though, Lean just changes it to eq.refl H1 (when I print it).

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:36):

lemma proof_irrel' {a : Prop} (H1 H2 : a) : H1 = H2 :=
begin
  have ta : a = true,
    apply propext, split, { intro, trivial }, { intro, exact H1 },
  rw ta at H1 H2,
end

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:36):

(deleted)

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:36):

(deleted)

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:36):

Oh wait, I'm using a rewrite so it tries refl.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:38):

Wasn't there a version of rw that didn't try refl?

view this post on Zulip Kenny Lau (Dec 31 2018 at 10:39):

I think you can tweak the settings

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 10:39):

I completely agree that it's a pain to experiment with stuff using rw becasue of this refl thing. I think "dunfold" and "delta" unfold functions without trying refl at the end but I don't know about rw.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:39):

I'm not sure this proof would actually work. Substitutions using equality of types are far more complicated and subtle than they might appear.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:42):

I'm not sure this proof would actually work. Substitutions using equality of types are far more complicated and subtle than they might appear.

? Surely rewrite works on , which is equality of types. E.g.

example (P Q : Prop) (HP : P) (HPQ : P = Q) : sorry := by { rw HPQ at HP, sorry }

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:44):

Actually, it definitely does work.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:45):

This is the easiest way.

lemma proof_irrel' {a : Prop} (H1 H2 : a) : H1 = H2 :=
begin
  have ta : a = true,
    apply propext, split, { intro, trivial }, { intro, exact H1 },
  revert H1 H2,
  rw ta,

end

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:47):

And then use no_confusion? Hm, true doesn't have no_confusion.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:48):

That's because it's unnecessary. But if there was no proof irrelevance there would be.

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:49):

Actually, this is what you should do.

lemma proof_irrel' {a : Prop} (H1 H2 : a) : H1 = H2 :=
begin
  have ta : a = true,
    apply propext, split, { intro, trivial }, { intro, exact H1 },
  revert H1 H2,
  rw ta,
  assume H1 H2,
  cases H1, cases H2,
  refl

end

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:49):

no_confusion is usually good for proving things are not equal.

view this post on Zulip Abhimanyu Pallavi Sudhir (Dec 31 2018 at 10:51):

Yeah, I got confused (between the uniqueness of the constructors and their exhaustiveness)

view this post on Zulip Chris Hughes (Dec 31 2018 at 10:51):

To illustrate how complicated proof relevant equality can be, try proving this example without using eq anywhere in the proof. (Hint: it's impossible)

inductive eq2 {α : Type*} (a : α) : α  Type
| refl : eq2 a

example {α : Type*} (a b : α) (h₁ h₂ : eq2 a b) : eq2 h₁ h₂ := sorry

view this post on Zulip Kenny Lau (Dec 31 2018 at 11:05):

prelude

universe u

notation `Prop` := Sort 0

structure iff (a b : Prop) : Prop :=
(mp : a  b) (mpr : b  a)

inductive eq {α : Sort u} (a : α) : α  Prop
| refl : eq a

infix `  `:20 := iff
infix ` = `:50 := eq

@[elab_as_eliminator, subst]
lemma eq.subst {α : Sort u} {P : α  Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
eq.rec h₂ h₁

infixr `  `:75 := eq.subst

constant propext {a b : Prop} : (a  b)  (a = b)

inductive true : Prop
| intro : true

lemma proof_irrel {a : Prop} (H1 H2 : a) : H1 = H2 :=
have true = a, from propext ⟨λ _, H1, λ _, true.intro,
(this  (λ H1 H2, true.drec_on H1 (true.drec_on H2 (eq.refl true.intro))) :  H1 H2 : a, H1 = H2) H1 H2

view this post on Zulip Chris Hughes (Dec 31 2018 at 12:43):

What does the subst attribute do?

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 14:04):

Where is a complete list of all attributes and their explanations? Oh -- is [subst] it only used in core? Are users not supposed to use it?

view this post on Zulip Kenny Lau (Dec 31 2018 at 14:06):

I have no idea, I just copied the code out of the core library

view this post on Zulip Patrick Massot (Dec 31 2018 at 14:32):

Proof relevant type theories tend to lack the type Prop altogether I think. Proof irrelevance is the only thing distinguishing Prop and Type so propositions tend to be defined using Type and some of them I think have an is_Prop predicate that says that the type has only one element.

This is not true. Impredicativity is also an important difference. I think Coq has Prop for this reason, and no definitional proof irrelevance

view this post on Zulip Chris Hughes (Dec 31 2018 at 15:09):

What do you mean precisely by impredicativity?

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 15:12):

Coq has no definitional proof irrelevance? But does it have proof irrelevance?

view this post on Zulip Chris Hughes (Dec 31 2018 at 15:17):

I heard once it was an optional extra like propext. Though I guess that means Prop would still be special in the sense that any two proofs are not provably unequal.

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:26):

right, you have to have this property if impredicativity is to be consistent

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:27):

because if a type has two elements, then you can build a cantor's paradox sort of thing using impredicativity

view this post on Zulip Chris Hughes (Dec 31 2018 at 18:28):

What does impredicativity mean precisely?

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:35):

forall x : A, P : Prop if P : Prop

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:35):

even if A : Type

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:36):

this means that propositions can quantify over themselves

view this post on Zulip Kevin Buzzard (Dec 31 2018 at 18:38):

(forall x : A, P) : Prop is what we're talking about here, presumably. The universe isn't the max, it's the imax.

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:39):

in a predicative universe, the pi type has level max of the universe levels of the parts

view this post on Zulip Mario Carneiro (Dec 31 2018 at 18:39):

but we have this funny imax thing for level 0

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 01 2019 at 04:12):

this means that propositions can quantify over themselves

Isn't that just P → P?

view this post on Zulip Abhimanyu Pallavi Sudhir (Jan 01 2019 at 04:13):

Even with functions between types, the type of P → Q is the types of P and Q, so I don't understand why this makes Prop special.

view this post on Zulip Mario Carneiro (Jan 01 2019 at 04:25):

I mean a function whose domain of quantification includes itself

view this post on Zulip Mario Carneiro (Jan 01 2019 at 04:30):

which permits self application

def p :  p : Prop⦄, p  p = p := λ x _, rfl
def X := p p

view this post on Zulip Mario Carneiro (Jan 01 2019 at 04:30):

you can use this to do a variety of diagonalization type arguments

view this post on Zulip Kenny Lau (Jan 01 2019 at 05:03):

@Abhimanyu Pallavi Sudhir if you quantify over all Type, you get Type 1

view this post on Zulip Reid Barton (Jan 01 2019 at 13:36):

A classic example of an impredicative definition of a Prop is defining the subgroup generated by a subset S of a group G to be the intersection of all the subgroups of G which contain S

view this post on Zulip Reid Barton (Jan 01 2019 at 13:39):

which is to say def belongs_to_subgroup_generated_by (S : set G) (x : G) : Prop := \forall (P : G \to Prop), is_subgroup P \and (\forall y, S y \to P y) \to P x

view this post on Zulip Reid Barton (Jan 01 2019 at 13:40):

If Prop had a universe hierarchy like Type, you wouldn't be allowed to use the same Prop on both sides of that equation

view this post on Zulip Chris Hughes (Jan 01 2019 at 13:41):

It hadn't occurred to me how important this was.

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:47):

of course it hadn't, you guys don't even care about foundations / of course it hadn't, this is hard core logic stuff

view this post on Zulip Reid Barton (Jan 01 2019 at 13:48):

It's really hard to imagine from a classical perspective how anyone could object to the construction "take all the subsets of G, keep the ones which are subgroups containing S, and form their intersection".

view this post on Zulip Reid Barton (Jan 01 2019 at 13:48):

Before using Lean, I was not convinced that "impredicative" meant anything at all.

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:49):

From a "classical perspective", you run into issues like Δ0-predicates are absolute

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:50):

that somehow P(ω) (i.e. powerset of ω) is not absolute

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:50):

because taking powerset is not a predicative thing to do

view this post on Zulip Reid Barton (Jan 01 2019 at 13:52):

Right, well, so the conclusion is that caring about predicativity is not a math thing to do.

view this post on Zulip Reid Barton (Jan 01 2019 at 13:53):

Especially since this example of an impredicative definition is something that one will encounter in a first course on algebra, it's not some scary thing involving universes or whatever.

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:53):

mathematicians have gone too far, doing impredicative stuff like that

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:54):

how are they going to compute their examples if their definitions are impredicative

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:54):

who cares about examples? We want theorems!

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:55):

what do you want theorems for?

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:55):

fun

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:55):

and promotion

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:55):

wasn't number theory created to solve diophantine equations

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:55):

yes but now its job is to create theorems explaining what the structure of the solutions is

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:56):

because solving them all turned out to be too hard

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:56):

but now your impredicative definitions are not helping us to solve the equations, because they are incomputable

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:57):

yes but we don't care about solving them because that's too hard. We now care about whether the solutions lie on some union of simple subvarieties or something. Nobody will get promoted for solving a Diophantine equation.

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:58):

Can you compute the integers of Q[X]/(X^3-3X+1)?

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:59):

sure, I read an algorithm to do that once

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:59):

that doesn't mean you can compute it

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:59):

it's in Cohen's book on computational number theory

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:59):

sure it means I can compute it

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:59):

I just ask a PhD student to compute it for me

view this post on Zulip Kenny Lau (Jan 01 2019 at 13:59):

that isn't you computing it

view this post on Zulip Kevin Buzzard (Jan 01 2019 at 13:59):

I think you have a lot to learn about the real world

view this post on Zulip Chris Hughes (Jan 01 2019 at 14:18):

Lean is designed for computer science, so impredicative definitions can't be that useless from a computational perspective. You can't compute with them, but you can still use them to help prove your program does what it's supposed to.

view this post on Zulip Mario Carneiro (Jan 01 2019 at 15:20):

By the way, HoTT uses predicative universes only (in the usual setup), so if you thought it would be a great thing that solves all your problems then this is one place where it isn't all sunshine and roses

view this post on Zulip Mario Carneiro (Jan 01 2019 at 15:21):

Also Agda makes a big deal about being 100% predicative

view this post on Zulip Mario Carneiro (Jan 01 2019 at 15:24):

It's true that in regular math predicativity doesn't really come up, but it shows up in non-absoluteness like Kenny says, or in model theory where adding more ordinals causes new subsets of nat to appear... you have this weird situation where you've built the set but not the elements, and that's where things like Cohen reals come from

view this post on Zulip Mario Carneiro (Jan 01 2019 at 15:27):

Also, we've discussed impredicative encodings of inductive types before, like xnat : Type := \all X : Type, X -> (X -> X) -> X, which doesn't typecheck in lean because Type is predicative

view this post on Zulip Mario Carneiro (Jan 01 2019 at 15:29):

Or when we have an object that is "defined by a universal property" and we want to just write that property but it doesn't work because the universe quantifier isn't large enough, so instead we re-express it by some kind of construction "from below"... that's predicativity


Last updated: May 11 2021 at 13:22 UTC