force decidability

Stream: new members

[RustyYato]

Hi! Some background before my question:
This is my first stab at Lean. I have a very minimal experience with Coq in the past, but I wanted to try out alternative theorem provers to see if there were others I liked more. And Lean is a lot more user-friendly (esp around induction and recursion!)
I'm trying to create a general framework for proving numbers are prime from first principles to get a handle on how to prove things in Lean .
I know this is probably not how you would normally use Lean, but I'm new to theorem proving in general so it seems like a natural place to start.

NOTE: I've defined natural numbers like this:

inductive nat where
  | zero : nat
  | inc : nat -> nat

I've gotten to the point where I have a function to check if a number is prime or not

def nat.check_prime (n: nat) : Decidable (nat.prime n) := ...

This is implemented and it works well, the following gives the result

#eval nat.check_prime (nat.inc (nat.inc nat.zero))

isTrue _

Nice! Now I have a problem, I want to use this function to prove that 2 is prime
However, I can't figure out how to ignore to isFalse case automatically since that's impossible, and Lean seems to know that it's impossible given the eval seen above.

theorem two_is_prime : nat.prime (nat.inc (nat.inc nat.zero)) :=

How would I automatically ignore the isFalse case given this is a very concrete term

[RustyYato]

Here's as far as I was able to get

theorem two_is_prime : nat.prime (nat.inc (nat.inc nat.zero)) :=
  match nat.check_prime nat.zero.inc.inc with
  | Decidable.isTrue d => d
   -- no idea what to do here, and Lean doesn't let me ignore it like in other cases where a match branch is impossible
  | Decidable.isFalse d => admit

[RustyYato]

I was able to prove that two is prime without using this more general check_prime function, however I thought it should be possible to automatically detect if a number is prime, which led me down this rabbit hole

[Mario Carneiro]

RustyYato said:

I know this is probably not how you would normally use Lean, but I'm new to theorem proving in general so it seems like a natural place to start.

I take it you haven't seen #nng then. :) Reinventing the natural numbers is such a common way to start that it's now a popular pastime

[Mario Carneiro]

The idiomatic way to use Decidable instances to prove things is by decide:

theorem two_is_prime : nat.prime (nat.inc (nat.inc nat.zero)) := by decide

[Mario Carneiro]

The way it works is to use an auxiliary definition which forces the check_prime function to be evaluated for the term to typecheck

[Mario Carneiro]

Here's an implementation of the proof strategy from scratch:

def AsTrue (dec : Decidable p) : Prop :=
  match dec with
  | .isTrue d => True
  | .isFalse d => False

theorem of_asTrue (dec : Decidable p) : AsTrue dec → p :=
  match dec with
  | .isTrue h => fun _ => h
  | .isFalse _ => False.elim

theorem two_is_prime : nat.prime (nat.inc (nat.inc nat.zero)) :=
  of_asTrue (nat.check_prime nat.zero.inc.inc) trivial

The trick is in the trivial at the end. trivial is a proof of True, but the type that is expected is AsTrue (nat.check_prime nat.zero.inc.inc), so to make this typecheck lean will first unfold AsTrue, then see the match, then unfold nat.check_prime to get it to evaluate to isTrue of something.

[Mario Carneiro]

@RustyYato

[RustyYato]

Mario Carneiro said:

RustyYato said:

I know this is probably not how you would normally use Lean, but I'm new to theorem proving in general so it seems like a natural place to start.

I take it you haven't seen #nng then. :) Reinventing the natural numbers is such a common way to start that it's now a popular pastime

Oh wow, that's great! I'll definitely have to take a look at that.

[RustyYato]

Mario Carneiro said:

The idiomatic way to use Decidable instances to prove things is by decide:

theorem two_is_prime : nat.prime (nat.inc (nat.inc nat.zero)) := by decide

I see, this was the missing piece for me, thanks! And the manual implementation is super helpful, using AsTrue to force evaluation wasn't something I thought about. Seems like a nice tool for other similar situations.

Thanks a lot for the help!

[RustyYato]

So I tried this out, but I ran into this problem

failed to reduce to 'true'
  Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h) prime_is_decidable

with this instance

instance prime_is_decidable : Decidable (nat.prime n) := nat.check_prime n

So I tried out the manual approach you showed and got

application type mismatch
  of_asTrue (nat.check_prime (nat.inc (nat.inc nat.zero))) trivial
argument
  trivial
has type
  True : Prop
but is expected to have type
  AsTrue (nat.check_prime (nat.inc (nat.inc nat.zero))) : Prop

Which looks like lean isn't able to reduce check_prime for some reason. At first I thought it was because I used well-founded recursion in by implementation of division, because of the docs for the decide tactic say that it may not work in the presence of well-founded recursion. So I went ahead and reimplemented it without well-founded recursion, and decide still doesn't work. I've tried everything I could think of and I still don't know why it's not evaluating.

Here's the entire project so far: https://github.com/RustyYato/lean-root2
Here's the definition of two is prime: https://github.com/RustyYato/lean-root2/blob/71e8179556aef1635301df3d721d72b7d89584c3/Root2/Prime/Concrete.lean#L15-L16

[RustyYato]

Wow, that took a while, but the reason why it wasn't reducing was because of how I was comparing equality of my natural numbers
After copying the implementation from the std lib, it worked.
Now to understand why

[RustyYato]

before I had equality defined like so

def nat.compare_eq (a b: nat) : Decidable (a = b) :=

  match a with
  | nat.zero => match b with
    | nat.zero => Decidable.isTrue rfl
    | nat.inc _ => Decidable.isFalse (by intro; contradiction)
  | nat.inc a₀ => match b with
    | nat.zero => Decidable.isFalse (by intro; contradiction)
    | nat.inc b₀ =>
      by rw [@nat.eq_inc_irr a₀ b₀]; exact (nat.compare_eq a₀ b₀)

where eq_inc_irr : (inc a = inc b) = (a = b). I guess that lean doesn't like wrapping and unwrapping Decidable and gives up

[RustyYato]

But I have less than and less or equal comparisons defined in a similar way, and they get evaluated just fine. So I'm not sure why this one change made the difference