Axioms vs Inductive Types

Stream: general

[Daniel Geisz]

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]

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]

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]

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]

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

[Reid Barton]

I guess that's three reasons. :upside_down:

[Reid Barton]

(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]

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]

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]

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]

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]

Oh ok, fair enough. Certainly helpful, thanks!

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

Eric Rodriguez said:

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

Actually funext isn't an axiom

[Mario Carneiro]

lean only has three axioms

[Mario Carneiro]

plus a big ol' axiom schema called inductive

[Eric Rodriguez]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

(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]

src#funext

[Yakov Pechersky]

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 :=
begin
  ext,
  exact h _
end

attribute [intro!] foo_eq

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

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

[Jason Rute]

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]

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

[Sebastien Gouezel]

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.