Zulip Chat Archive

Stream: general

Topic: Axioms vs Inductive Types

Daniel Geisz (Sep 01 2021 at 21:06):

I'm fairly new to lean, and I wanted to get something straightened out related to inductive types. In "Theorem Proving in Lean," the prod operator is introduced as follows:

inductive prod (α : Type u) (β : Type v)
| mk : α  β  prod

def fst {α : Type u} {β : Type v} (p : α × β) : α :=
prod.rec_on p (λ a b, a)

def snd {α : Type u} {β : Type v} (p : α × β) : β :=
prod.rec_on p (λ a b, b)

However, it seems to me you could introduce the same construction using axiom. For example:

axiom prod : (Type u)  (Type v)  Type (max u v)
axiom mk : Π {α : Type u} {β : Type v} (a : α) (b : β), prod α β
axiom fst : Π {α : Type u} {β : Type v}, prod α β  α
axiom snd : Π {α : Type u} {β : Type v}, prod α β  β

What is the primary reason why you should favor the first method of defining prod over the second? I understand that inductive types lend themselves nicely to recursion/induction, but it feels as though recursive and inductive behaviors could also be defined in terms of axioms. Perhaps it has something to do with how lean treats axiom (constant)? Thanks!

Yaël Dillies (Sep 01 2021 at 21:09):

General rule of thumb: Lean is smarter than you (the general you!). I'll let others expand, but just here your axiomatization already forgets crucial "axioms": fst (mk a b) = a and snd (mk a b) = b. It's just too easy to miss something like that.

Yaël Dillies (Sep 01 2021 at 21:11):

One way to think about inductive is that it's automation. Sure you can write all the axioms, but if you have a tool that does it right and quick, why bother? Then there also are more technical (defeqness, reduction?, ...) reasons

Reid Barton (Sep 01 2021 at 21:11):

Two reasons. With axiom, you can easily introduce inconsistency (e.g., axiom bad : false). Also, using inductive means that you get computation rules: fst (prod.mk a b) is definitionally equal to a, and likewise for snd; these cannot be replicated using axiom.

Reid Barton (Sep 01 2021 at 21:11):

Otherwise, what you wrote with axiom is basically what Lean translates the inductive declaration into internally, like @Yaël Dillies was saying.

Reid Barton (Sep 01 2021 at 21:11):

I guess that's three reasons. :upside_down:

Reid Barton (Sep 01 2021 at 21:15):

(Actually the primitive constant Lean really generates is the recursor prod.rec rather than prod.fst and prod.snd; not sure whether that makes any important difference in this case.)

Daniel Geisz (Sep 01 2021 at 21:20):

Ok, that makes sense. I suppose using axiom naively seems more natural to me, but it certainly makes sense to just let lean take the brunt of the work.

I guess maybe a follow-up then: When would be a reasonable time to use axiom instead of defining intro or elim rules for inductive types?

Eric Rodriguez (Sep 01 2021 at 21:21):

you can also use structures, which may be more like what you're used to in some ways:

structure myprod (α β : Type) : Type :=
(fst : α) (snd : β)

#print prefix myprod

#eval (myprod.mk 2 1).fst

Eric Rodriguez (Sep 01 2021 at 21:22):

and I don't think axiom is used in mathlib, if that gives you the sort of level of averse we are to axiom

Eric Rodriguez (Sep 01 2021 at 21:22):

lean core has a couple (classical.choice, funext, propext, quot.sound) but it's pretty strongly discouraged that we use it (and constant too, which IIRC is equivalent)

Daniel Geisz (Sep 01 2021 at 21:23):

Oh ok, fair enough. Certainly helpful, thanks!

Mario Carneiro (Sep 01 2021 at 21:25):

There are actually quite a few (~100) occurrences of constant (specifically meta constant) in lean core

Mario Carneiro (Sep 01 2021 at 21:26):

but since they are meta they don't interfere with logical consistency of the non-meta part

Mario Carneiro (Sep 01 2021 at 21:32):

Eric Rodriguez said:

lean core has a couple (classical.choice, funext, propext, quot.sound)

Actually funext isn't an axiom

Mario Carneiro (Sep 01 2021 at 21:32):

lean only has three axioms

Mario Carneiro (Sep 01 2021 at 21:33):

plus a big ol' axiom schema called inductive

Eric Rodriguez (Sep 01 2021 at 21:43):

wow, funext being proved through quotient.sound was not was I was expecting to read

Eric Rodriguez (Sep 01 2021 at 21:44):

and I'm assuming meta constant is stuff implemented in the c++?

Eric Rodriguez (Sep 01 2021 at 21:58):

(also, do you know what attribute [intro!] does? ctrl+fing the source code gives funext as the only result, and I can't find any intro! x that turns f = g into f x = g x)

Yakov Pechersky (Sep 01 2021 at 22:04):


Yakov Pechersky (Sep 01 2021 at 22:08):

I hoped this would work:

import tactic.ext

universe u

@[ext] structure Foo (R : Type*) :=
(func : R  R)

lemma foo_eq {R : Type*} (f g : Foo R) (h :  x : R, f.func x = g.func x) : f = g :=
  exact h _

attribute [intro!] foo_eq

variables {R : Type*} {f g : Foo R}

example : f = g :=
  intro, -- I was hoping this would work

Jason Rute (Sep 01 2021 at 23:04):

To explicitly answer your question, I can only think of one possible use of axiom. That is if you want to play around with other logical axioms. For example, you could use an axiom introducing large cardinal assumptions like in set theory. You could also use it to play around with foundations which are not as strong as the axiom of choice. But note axioms are purposely behind the scenes, so if you use them they will be available to all of your later code to use. For example, it isn’t easy to do constructive math using tactics in lean since a lot of tactics bring in one of lean’s non-constructive axioms. Also, I’m pretty sure no code using axioms would be accepted into mathlib. I think in many cases it would be better to just include the “axiom” (like a large cardinal assumption) as a hypothesis to the theorem.

Yakov Pechersky (Sep 01 2021 at 23:10):

In other words, variables is really the axiom that mathlib uses.

Sebastien Gouezel (Sep 02 2021 at 06:16):

Here is a mathlib example needing the continuum hypothesis:

theorem no_pettis_integral (Hcont : # = aleph 1) :
  ¬  (g : discrete_copy  →ᵇ ),
       (φ : (discrete_copy  →ᵇ ) L[] ),  x in Icc 0 1, φ (f Hcont x) = φ g :=

You can see that it is baked in as an assumption instead of an axiom.

Last updated: Dec 20 2023 at 11:08 UTC