TPIL4: Propositions as types

Stream: new members

[Krishna Padmasola]

Hello friends, in the section Working with Propositions as Types, a proof of p → q → p is given as follows:

variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

I was trying to to create a proof for p → q in a similar fashion, but the following does not work

example : p → q := fun hp : p => fun hq : q => hq

Lean complains that the types don't match, but I am not able to figure out an expression that would make them match.
What am I doing wrong?

[Alex Mobius]

Well, that's because you cannot really prove p -> q for arbitrary propositions p, q.

[Alex Mobius]

Here, writng an implication as a function would be writing a function to provide a proof of arbitrary q given a proof of arbitrary p. You cannot provide that, because p and q are not really related.
In the first example, what you're proving is p -> (q -> p), i.e. "given knowledge that p is true, p follows from anything", which is provable.

[Krishna Padmasola]

Thanks @Alex Mobius that makes sense now.
Another thing I'm trying to wrap my head around is Prop vs Bool.
Why are there 2 types for the same thing?

[Edward van de Meent]

because for one, you get excluded middle by construction.

[Edward van de Meent]

(sort of)

[Edward van de Meent]

for example:

example (x : Bool) : x = false ∨ x = true:= Bool.rec (Or.inl rfl) (Or.inr rfl) x

[Alex Mobius]

Bool is a truth that's only known a runtime, Prop is a truth that is known at type-checking type. There's a type class called Decidable which bridges the two.
Prop is a type of many possible types (propositions) that have either 1 or 0 elements - its only element is the proof of the proposition if the proposition is correct. Therefore, the type checker can check if an element of that type can be constructed given known theorems. Bool is a type that has 2 elements, they are also 1 and 0, but they're just numbers with special arithmetic instead of "amount of proofs"

[Alex Mobius]

I hope this makes sense!

[Krishna Padmasola]

@Edward van de Meent thanks, I think I need to read up on recursors and axiom of choice (?) to have a deeper understanding of your answer.

@Alex Mobius type-checking time vs runtime is an interesting observation. Does that mean we cannot create any propositions that involve runtime computation?

When you say Decidable does the bridging, does that mean we can use Prop in place of Bool, for example in if expressions?

I tried the following but it did not work

def z : Prop := 2 = 2
set_option diagnostics true
#eval if z then 10 else 20

I get the error message failed to synthesize Decidable z

[Krishna Padmasola]

also tried this, which does not work

def z : Prop := 2 = 2
theorem zth : z := rfl
#check zth
set_option diagnostics true
#eval if zth then 10 else 20

but this works, not sure why, because the proof is not supplied

#eval if 2 = 2 then 10 else 20

[Kyle Miller]

failed to synthesize Decidable z means that it couldn't automatically do the bridging.

The issue is that Decidable synthesis won't unfold definitions unless they are reducible. If you change it to abbrev z it will work, since this marks the definition as being reducible. Definitions are "semi-reducible" by default.

[Kyle Miller]

if zth then 10 else 20 is a type error because zth is a proof, not a proposition

[Krishna Padmasola]

thanks @Kyle Miller so in if 2 = 2 then ... Lean is able to prove that the proposition is true by itself? Is that what is meant by synthesizing Decidableor bridging?

[Kyle Miller]

Yes, it synthesizes a Decidable (2 = 2) instance there

[Kyle Miller]

Even though Decidable z is definitionally equal to Decidable (2 = 2), typeclass synthesis won't unfold z. (This is intentional, to let people create type synonym with properties that are different from the old type.)

[Kyle Miller]

By the way, Decidable p is pretty much Bool, but its versions of true and false contain either a proof or disproof of p. This is how the bridging is done.

[Alex Mobius]

If you need to, you would do it like that:

instance: Decidable z := by unfold z; infer_impl

[Kyle Miller]

or instance : Decidable z := inferInstanceAs <| Decidable (2 = 2)

[Kyle Miller]

(do you mean infer_instance @Alex Mobius ?)

[Krishna Padmasola]

Since @Alex Mobius pointed out in the thread above that we cannot prove p -> q for arbitrary p and q (it makes sense now that I think about it), I tried to prove for specific p and q

The following code type checks, but I think I am doing something wrong:

-- define x to be 2
def x : Nat := 2

-- define a proposition that x is equal to 2
def p : Prop := x = 2

-- define y to be 3
def y : Nat := 3

-- define a proposition that y is equal to x + 1
def q : Prop := y = x + 1

-- proof that the proposition (x = 2) is True
example : p := Eq.refl _

-- given a proof that (x = 2) is True, return a proof that (y = x + 1) is True
theorem t : p -> q :=
  fun hp : p =>
    match hp with
    -- proof of hp using refl
    -- assuming _ matches x in the proof below,
    -- return proof of y = x + 1
    | Eq.refl _ => Eq.refl (Nat.succ _)

The reason I am suspicious is that the above type checks even when I replace | Eq.refl _ => Eq.refl (Nat.succ _) with | Eq.refl _ => Eq.refl _
Can someone help me understand what I am doing wrong here? What would be a correct way to prove that p -> q in this specific case?

[Daniel Weber]

In this case q is unconditionally true, so one can just do fun _ => rfl

[Chris Bailey]

theorem t : p -> q := fun _ => rfl

In this case it's definitionally true, you can just prove it by computation with rfl. A "more explicit" proof might be

example : p -> q := by
  simp only [p, q, y]
  intro hp
  rw [hp]
  done

There's still a large amount of complexity being hidden by the elaborator here even though the procedure is perhaps a bit more explicit, but that's kind of the point of a proof assistant.

[Chris Bailey]

Fwiw the substitution part is done using the recursor for the Eq type, but I would suggest continuing to develop an intuitive sense for how stuff moves around in the vernacular before digging into that.

[Alex Mobius]

Maybe try your hand at something like

variable (x y z: Nat)
def p := y = x + 1 /\ z = y + 1
def q := z = x + 2

example: p -> q := sorry

[Krishna Padmasola]

Thanks friends, sorry I could not respond earlier, I was trying to understand the responses, which caused me explore previously unexplored chapters in TPIL. I think I'll need to spend some time and read the rest of the chapters because it all seems linked.

I am new to theorem proving, so I was trying to come up with ways to prove without using tactics, because tactics seem like magic to me at this point (I don't understand how they are proving it behind the scenes). The way I'd like to understand is to be able to clearly see the step by step reasoning (using only terms, not tactics). I realize that would not scale for complex proofs, but would like to be able to reduce it to a step by step term based proof at least partially just to be able to build the intuition for equivalence of term based and tactic based proofs.