are truth tables an option?

Stream: new members

[James B Clifford]

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]

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

[Yaël Dillies]

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

[Arien Malec]

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]

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

[Eric Rodriguez]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

Not to be confused with tactic#tauto

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Rodriguez]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

You can, that's the absurd function

[Mario Carneiro]

or Not.elim I suppose

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

[Arien Malec]

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]

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

[Arien Malec]

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

[Jireh Loreaux]

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

[Arien Malec]

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]

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

[Yaël Dillies]

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

[Jireh Loreaux]

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]

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

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

[Yaël Dillies]

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

[Jireh Loreaux]

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

[Mario Carneiro]

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]

and hnp is a function, of type Prop?

[Mario Carneiro]

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

[Mario Carneiro]

hnp is not of type Prop

[Arien Malec]

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]

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]

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