# 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 `axiom`

s

#### 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 :=
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 (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