if statements and less than or equal for nat.

Stream: new members

[Justin Pearson]

I am not using lean as a programming language, but I'm proving things about functions that look like the sort of functions that you would write in a programming language (if that confuses you then ignore it). I'm quite happy doing things with lists, trees etc, but I realise that there is something fundamental that I don't understand.

What is going on with the following piece of code?

def blug (x : ℕ) (y : ℕ) : ℕ  :=
  if x < y then 42 else 0
example : blug 1 2 = 42  :=  rfl
example : blug 2 1 ≠ 42 := dec_trivial

blug is the sort of function that a programmer might write. So how come the two proofs just work? I found dec_trivial by using library search. Looking at the definition it is something to do with decidable propositions, which is something that I don't really understand yet.
Is there some magic that is going provides the required proofs with you use if (or ite)?

I'm sorry if my question is vague, it is difficult for me to understand what I don't understand.

[Johan Commelin]

A proposition is decidable if there is an algorithm that can be run to find out whether it's true or not.

[Johan Commelin]

So the things that programmers write in their if .. then .. else statements had better be decidable. And indeed this is the case for (in)equalities of natural numbers.

[Johan Commelin]

dec_trivial signals to Lean that it should run that algorithm. Along the way, if P then a else b gets reduced to a or b, as Lean figures out whether P is true or not.

[Eric Wieser]

reading the implementation of src#ite might explain why the rfl proof works

[Johan Commelin]

However, if you cheat, and you use classical.decidable_* stuff, then you can make it look like propositions are decidable, even though they are not. In such cases ite will not reduce nicely. So for programming purposes all the classical stuff is best avoided.

[Justin Pearson]

It would be nice to have some mechanism that lets you mark something as classical free with some sort of check.

[Mario Carneiro]

for programming purposes, the mechanism already exists, it is the noncomputable modifier

[Mario Carneiro]

for axiom hawks there is no mechanism available yet, although it's a relatively simple attribute to write

[Justin Pearson]

For the next person that gets here, stepping through the tactic states

begin
 unfold blug , unfold ite  ,
 rw  [nat.decidable_lt] ,
 dsimp [nat.decidable_le] , refl
end

and looking at the definition of nat.decidable was really helpful.

[Kyle Miller]

Regarding decidability and what it is, here's a CS-inclined mathematician's understanding. Mathematical truth is represented by propositions in Prop. As we know, every proposition is equal to true : Prop or false : Prop, but there's no general algorithm that evaluates a proposition to one of these values -- usually you've got to write a proof.

There's also bool truth, represented by tt or ff. In Lean, every function that returns a bool (unless it's marked noncomputable) will eventually evaluate to one of these values. This is more restrictive that Prop truth, but you can count on getting an answer.

It would be inconvenient having parallel Prop-valued and bool-valued theories. For example, having both a < that evaluates to a bool when things are computable (like for ℕ) and a < that evaluates to a Prop when things aren't necessarily computable. Prop is the more general one, and the one we'd like to have well-developed since everything (or so it seems) we'd want to prove can be encoded as a proposition, but, again, its limitation is that propositions can't be evaluated in general.

A solution to this is decidable and the typeclass system. When you ask for a decidable p instance, what is essentially happening is that p is being recompiled into a bool expression. Well, a variant of a bool where the values remember a proof of the proposition they're translating, since that's a convenient piece of extra information for things like docs#dite. This lets you write (certain) propositions in contexts that need to be able to evaluate a Prop to true or false.

The sub-language of Prop that's recompilable to these bool-like expressions is ad hoc, underspecified, and constantly changing, but at least it's all in the open -- every decidable instance is listed in the dropdown under docs#decidable.

What dec_trivial does is invoke this recompiler (by asking for the Prop's decidable instance) and then extract its proof if it could be recompiled.

(Disclaimer: I write these messages to consolidate my understanding as I learn Lean. The above seems to be a workable model, but it could be incorrect.)