## Stream: new members

### Topic: are truth tables an option?

#### James B Clifford (Dec 02 2022 at 00:08):

I was taught that (a \/ b) is only false when both a and b are false. My prof drew a truth table on the board, crossed out the row where they were both false. Then concluded that the only truthful row where a was false b was true; therefore, not a implies b. I know this is a super simple example, but does lean have a form of truth table syntax? would I use a series of axioms, or define a function that returned false if they were both false and treat the function as the table?

#### Yaël Dillies (Dec 02 2022 at 00:39):

Typically, you would use tactic#by_cases in tactic mode in a proof.

#### Yaël Dillies (Dec 02 2022 at 00:39):

But maybe docs#bor is what you're after? This is precisely defined in a truth table kind of a way.

#### Arien Malec (Dec 02 2022 at 01:19):

It can be confusing at first, but Prop isn't a boolean, and ∨ in Lean is defined as an inductive where you construct one precisely by giving a proof of either the left or right sides. Boolean or, as @Yaël Dillies notes, is easily defined via a match statement that's the normal truth table.

#### Arien Malec (Dec 02 2022 at 01:25):

I carried around the implicit belief that a Prop is analogous to boolean, and that let me astray at first.

#### Eric Rodriguez (Dec 02 2022 at 01:29):

Prop is like a boolean that you don't know the answer to; that is, p : Prop is either equal to true or to false (docs#classical.prop_complete) but you can have a Prop representing, i.e. the Riemann hypothesis. A bool is always either _literally_ true or false, if that makes sense

#### Arien Malec (Dec 02 2022 at 01:34):

I think that's misleading (or at least it mislead me). If I have a proof of something (or take it as a premise), I have hp: p where p: Prop. I can also have a proof that p → False (which is called ¬p in Lean). It turns out you need to know p ∨ ¬p only rarely.

#### Arien Malec (Dec 02 2022 at 01:35):

The earlier you just accept the Curry-Howard correspondence the better.

#### Adam Topaz (Dec 02 2022 at 01:43):

The tactic tauto! should also be mentioned (IIRC it essentially uses truth tables under the hood)

#### Adam Topaz (Dec 02 2022 at 01:43):

Not to be confused with tactic#tauto

#### Eric Wieser (Dec 02 2022 at 01:56):

To the documentation, tauto and tauto! are the same tactic... (docs#tactic.interactive.tauto)

#### Eric Wieser (Dec 02 2022 at 01:57):

... and I broke the rendering somehow, image.png (https://github.com/leanprover-community/lean/issues/789)

#### Eric Rodriguez (Dec 02 2022 at 10:08):

Arien Malec said:

I think that's misleading (or at least it mislead me). If I have a proof of something (or take it as a premise), I have hp: p where p: Prop. I can also have a proof that p → False (which is called ¬p in Lean). It turns out you need to know p ∨ ¬p only rarely.

This is just a proof by contradiction, however. One of those terms cannot exist if Lean is sound; that is, it would have no constructors (but it's obviously hard to decide which one it is!)

#### Arien Malec (Dec 02 2022 at 16:59):

All I'm saying is that I carried around a mistaken belief that Prop was like a boolean and it helped (me at least) to drop that and just follow the types

#### Mario Carneiro (Dec 02 2022 at 17:34):

I'm not sure I would characterize that belief as mistaken

#### Mario Carneiro (Dec 02 2022 at 17:35):

it's more natural to reason about propositions in natural deduction style, but there really are only two of them: docs4#Classical.prop_complete

#### Arien Malec (Dec 02 2022 at 20:19):

The kinds of issues that got me into trouble initially was thinking that in a function of typep -> q I could pass a hypothesis of ¬p on the analogy of type Bool -> Bool

#### Arien Malec (Dec 02 2022 at 20:20):

Which is what I was used to in a non-dependent-type world.

#### Mario Carneiro (Dec 02 2022 at 20:21):

You can, that's the absurd function

#### Mario Carneiro (Dec 02 2022 at 20:22):

or Not.elim I suppose

import Std.Logic
example {p q : Prop} (h1 : ¬p) : p → q := h1.elim


#### Arien Malec (Dec 02 2022 at 20:32):

my brain hurts.

variable {p q: Prop}
def imp : p → q → p := fun hp: p => fun _ => hp

def err: ¬p → q → ¬p := fun hnp: ¬p => imp hnp


#### Mario Carneiro (Dec 02 2022 at 20:34):

FYI p → q → p means p → (q → p). It says that if p and q are true then p is true

#### Arien Malec (Dec 02 2022 at 20:36):

where my brain hurt was when I expected imp hnp to fail with a type error

#### Jireh Loreaux (Dec 02 2022 at 21:06):

why would you think it would do that? (honest question)

#### Arien Malec (Dec 02 2022 at 21:39):

I've got a function of p → False and I'm feeding it into a function of p → q → p? So maybe I can reason that imp takes p and turns it into p which then leads to a return of a function p → False?

#### Kevin Buzzard (Dec 02 2022 at 21:40):

You're feeding it into a function of type p' -> q -> p' so it just lets p' be not p.

#### Yaël Dillies (Dec 02 2022 at 21:40):

What's confusing is that both p don't mean the same thing.

#### Jireh Loreaux (Dec 02 2022 at 22:00):

Yeah, the key point is that when you do variable {p q : Prop} then these are (universally quantified, and implicit!) variables in the forthcoming declarations. So imp says, for any propositions pand q, p → q → p. Now, if p is a proposition, so is ¬p and hence we can plug it in instead, to get ¬p → q → ¬p (i.e., err := @imp ¬p q).

Perhaps Arien what you were trying to say is that you can't do this in reverse? That is, you can't go from err to imp in the same trivial way? (of course, you can after rewriting ¬¬p to p, but that requires classical axioms)

#### Arien Malec (Dec 02 2022 at 22:05):

"Now, if p is a proposition, so is ¬p" is where I get confused. I thought ¬p was a function, not a Prop

#### Jireh Loreaux (Dec 02 2022 at 22:06):

Remember, Lean has impredicative Prop, so a Pi type (i.e., edit: type of functions) from Prop ends up in Prop.

#### Yaël Dillies (Dec 02 2022 at 22:06):

Those are non contradictory statements. ¬ p is a function, but functions have a type too! And the type of ¬ p is Prop.

#### Jireh Loreaux (Dec 02 2022 at 22:06):

p : Prop, but also p → False : Prop.

#### Mario Carneiro (Dec 02 2022 at 22:27):

Functions don't have the type Prop, but ¬p is not a function, it is a type of functions, that is p -> False, the type of all functions from p to False. p -> False is not itself a function, it is a type, and the type of a type is a universe, in this case Prop.

#### Arien Malec (Dec 02 2022 at 22:50):

and hnp is a function, of type Prop?

#### Mario Carneiro (Dec 02 2022 at 22:51):

hnp is a function, of type ¬p / p -> False

#### Mario Carneiro (Dec 02 2022 at 22:52):

hnp is not of type Prop

#### Arien Malec (Dec 02 2022 at 22:57):

hmm. So then I get confused again by imp hnp -- is my reasoning, that imp hnp works by resolving imp p to pto produce p -> False on the right track?

#### Mario Carneiro (Dec 02 2022 at 23:19):

The implicit arguments are doing you a disservice here. Here is your example again without them:

def imp : ∀ (p q: Prop), p → q → p := fun p => fun q => fun hp: p => fun _hq: q => hp

def err: ∀ (p q: Prop), ¬p → q → ¬p := fun p => fun q => fun hnp: ¬p => imp (¬p) q hnp


#### Mario Carneiro (Dec 02 2022 at 23:22):

imp is actually a function that takes four arguments: two propositions p and q, and then a proof of that p and q. Depending on what propositions you pass for the first two arguments, the rest of the theorem can say different things. If you pass (¬p) and q to imp, that's two arguments down and the remaining two arguments should be proofs of (¬p) and q respectively

Last updated: Dec 20 2023 at 11:08 UTC