Proof by exhaustive checking of all Fintype values

Stream: mathlib4

[ziman]

Not sure in which channel I should put this but here goes:

I've got a theory that defines some order on permutations. I have a (concrete) permutation on 3 elements and I want to show that this permutation is not dominated by any other permutation. You just traverse all possible permutations and check that none dominates the permutation in question, given the provided definition of "dominates". Sounds easy.

One way might be doing fin_cases but in another lemma involving four nested 3-branch fin_cases, I observed that Lean was struggling a bit with the 81 goals already and everything was getting quite slow. And I expect to do more exhaustive checks on bigger sets later so I thought I'd come up with something smarter.

It also feels like a waste to bring up all those cases as Lean goals. What I would do in Agda instead is making an exhaustive check function. It's sufficient to get either yes proof or other, as it's usually a lot of hassle to prove the negative case, and we will never want that proof in the end, as our goal is to prove the _positive_ case to the type checker.

inductive Semi (P : Prop) : Type where
  | yes (pf : P) : Semi P
  | other : Semi P  -- no or unknown

def checkList
    {α : Type}
    {P : α → Prop}
    {xs : List α}
    (check : (i : α) → Semi (P i))
  : Semi (∀ i ∈ xs, P i)
  := match xs with
      | [] => (Semi.yes (by simp))
      | (List.cons x xs) => match check x, checkList check with
        | Semi.yes px , Semi.yes pxs => Semi.yes λ
          | i, List.Mem.head _ => px
          | i, List.Mem.tail _ ixs => pxs i ixs
        | _ , _ => Semi.other

Then I can make the system check the proof and accept it like in this example:

def Checked {P : Prop} (semiP : Semi P) : Prop :=
  match semiP with
  | Semi.yes _ => P
  | Semi.other => True

def checked {P : Prop} (semiP : Semi P) : Checked semiP := by
  cases semiP
  case yes => simpa
  case other => rw [Checked]; trivial

example : ∀ i ∈ [1, 2, 3], i > 0 :=
  checked (checkList (xs := [1, 2, 3]) λ i =>
    match Nat.decLt 0 i with
    | isTrue pf => Semi.yes pf
    | isFalse _ => Semi.other
  )

Now, having the above, we should be pretty much done, right? But I'm having a lot of trouble defining this function:

def exhaustively
    {α : Type} [Fintype α]
    {P : α → Prop}
    (check : (i : α) → Semi (P i))
  : Semi (∀ i, P i)
  := sorry

I can't wrap my head around the right combination of Quotient.ind to get the damn list out of the multiset given to me by Fintype and to weave it the right way around Semi. Moreover, it seems to me that I'll even have to prove that the outcome of my projection out of the quotient will respect the permutation equivalence, which I expect to be a lot of work, yet it's only incidental to what I'm trying to do here.

There is Fintype.decidableForallFintype but that's only for decidable predicates and I don't want to prove the negative cases, as that's a lot of work as well.

So I'm not sure what to do. It seems my options are these:

1. Just use fin_cases and deal with the slowness.
2. Figure out how to define exhaustively for Fintype
3. Bite the bullet and write Decidable instances for my stuff instead of just using Semi

... or something else (?)

Any advice? What's the idiomatic way of dealing with this in Lean?

[Aaron Liu]

You can probably still do this with Decidable

[Aaron Liu]

in the negative case if you don't feel like providing a proof of isFalse you can just feed it a Classical.dec instead and if the negative case isn't inspected then it doesn't really matter what you put there anyways

[ziman]

How can I get the proof of false out of Classical.dec? I can match on its result but what do I do in the isTrue branch?

[Aaron Liu]

what do you mean

[Kyle Miller]

ziman said:

Bite the bullet and write Decidable instances

A good way to do this is to write a Bool-valued function that computes the truth of the proposition then use decidable_of_iff to write the instance itself.

[Kyle Miller]

It's not fun writing Decidable values directly.

With the bool-valued function, you don't need to interleave proofs and computation. All the proofs go into proving the iff

[Kyle Miller]

Do you have a #mwe ? It'd be easier to give a more concrete example if there's a single code block I can pop into my editor.

[ziman]

Sure, I'll adapt the above to make one. Thanks!

[Kyle Miller]

I guess I could also point you to this: #new members > Proof by reflection @ 💬

[ziman]

Kyle Miller said:

Do you have a #mwe ? It'd be easier to give a more concrete example if there's a single code block I can pop into my editor.

Here's a minimal example: https://gist.github.com/ziman/3912b5a507d61aa3478943c2772d3159
It's a bit contrived but should demonstrate the idea well, I hope.

[Aaron Liu]

import Mathlib.Data.Fintype.Defs

set_option autoImplicit false

inductive Semi (P : Prop) : Type where
  | yes (pf : P) : Semi P
  | other : Semi P  -- no or unknown

def checkList
    {α : Type}
    {P : α → Prop}
    {xs : List α}
    (check : (i : α) → Semi (P i))
  : Semi (∀ i ∈ xs, P i)
  := match xs with
      | [] => (Semi.yes (by simp))
      | (List.cons x xs) => match check x, checkList check with
        | Semi.yes px , Semi.yes pxs => Semi.yes λ
          | i, List.Mem.head _ => px
          | i, List.Mem.tail _ ixs => pxs i ixs
        | _ , _ => Semi.other

def Checked {P : Prop} (semiP : Semi P) : Prop :=
  match semiP with
  | Semi.yes _ => P
  | Semi.other => True

def checked {P : Prop} (semiP : Semi P) : Checked semiP := by
  cases semiP
  case yes => simpa
  case other => rw [Checked]; trivial

example : ∀ i ∈ [1, 2, 3], i > 0 :=
  checked (checkList (xs := [1, 2, 3]) λ i =>
    match Nat.decLt 0 i with
    | isTrue pf => Semi.yes pf
    | isFalse _ => Semi.other
  )

-- (a bit contrived) example:

def Dominates (xs ys : Vector (Fin 4) 4) : Prop := xs.sum > ys.sum

-- the zero vector is undominated
example : ∀ ys, ¬Dominates ys #v[0, 0, 0, 0] :=
  sorry

[ziman]

Aaron Liu said:

what do you mean

I cannot just use Classical.dec in the negative branch because it could return either proof of true or proof of false, and I need the proof of false.

[Aaron Liu]

I thought you said you didn't need them

ziman said:

It also feels like a waste to bring up all those cases as Lean goals. What I would do in Agda instead is making an exhaustive check function. It's sufficient to get either yes proof or other, as it's usually a lot of hassle to prove the negative case, and we will never want that proof in the end, as our goal is to prove the _positive_ case to the type checker.

[ziman]

I don't but Lean won't let me get away without them, since in the meantime they're going to be represented as Decidable :)

[ziman]

I could probably just use sorry or axiomatise them away, since -- as you say -- i don't care what's there, but there ought to be a cleaner way :)

[ziman]

Apologies, the definition of Dominates should use < instead of >, otherwise the example is false.

[Aaron Liu]

so do you need the proof of false or do you not

[ziman]

I don't need it. That's why I'm trying to avoid using Decidable, so that Lean does not need it, either.

[Aaron Liu]

so if you don't need it then replace isFalse ⋯ everywhere by (Classical.dec _)

[ziman]

Oh, I see!

[ziman]

Okay, that's... sly :D And I think it should work because we'll never end up in the negative branch so it should not block reduction.

[Aaron Liu]

yeah that's the point

[Kyle Miller]

I see, you're asking for a semidecision, to avoid proving the iff.

Usually it's better to develop out the full decision procedures, but in case it's interesting, here's some Semi theory developed out for this:

import Mathlib

set_option autoImplicit false

inductive Semi (P : Prop) : Type where
  | yes (pf : P) : Semi P
  | other : Semi P  -- no or unknown

def Semi.decide {p : Prop} [inst : Decidable p] : Semi p :=
  match inst with
  | isTrue pf => .yes pf
  | _ => .other

def Semi.of_imp (p : Prop) {q : Prop} (h : p → q) (s : Semi p) : Semi q :=
  match s with
  | .yes pf => .yes (h pf)
  | .other => .other

def Semi.isYes {p : Prop} (s : Semi p) : Bool := s matches .yes ..

theorem true_of_isYes {p : Prop} (s : Semi p) (h : s.isYes) : p :=
  match s, h with
  | .yes pf, _ => pf

def checkList
    {α : Type}
    {P : α → Prop}
    {xs : List α}
    (check : (i : α) → Semi (P i))
  : Semi (∀ i ∈ xs, P i)
  := match xs with
      | [] => (Semi.yes (by simp))
      | (List.cons x xs) => match check x, checkList check with
        | Semi.yes px , Semi.yes pxs => Semi.yes λ
          | i, List.Mem.head _ => px
          | i, List.Mem.tail _ ixs => pxs i ixs
        | _ , _ => Semi.other

example : ∀ i ∈ [1, 2, 3], i > 0 :=
  true_of_isYes (checkList (fun _ => Semi.decide)) rfl

[Kyle Miller]

You don't actually need to do any work though:

import Mathlib

set_option autoImplicit false

def Dominates (xs ys : Vector (Fin 4) 4) : Prop := xs.sum < ys.sum
deriving Decidable

example : ∀ ys, ¬Dominates ys #v[0, 0, 0, 0] := by decide

[Kyle Miller]

Mathlib already has the decision procedures for you :-)

[Kyle Miller]

If you want to speed it up and do the reduction only in the kernel, not the kernel+elaborator, you can do

example : ∀ ys, ¬Dominates ys #v[0, 0, 0, 0] := by decide +kernel

[ziman]

Ah, too bad that deriving will work only in the minimal example with the simple Dominates predicate. :)
But I didn't know Lean had deriving, that's great, and I'll surely use it elsewhere.

[ziman]

And all the other tricks you're showing me :)

[Kyle Miller]

What this deriving does is unfold the def and use the instance for the body of the definition.

[ziman]

That's a lot of magic. :) So the decide tactic can somehow figure out that the domain of the predicate is a Fintype and check all the values? Or why does it work?

I suppose I could make a decision procedure for this and use Aaron's trick in the negative branches. And then use the decide tactic.

[Kyle Miller]

It's because there are some Decidable instances available already for universal/existential quantifiers over Fintypes

[Aaron Liu]

decide uses typeclass synthesis to infer a Decidable instance

[ziman]

Right, I see.

[ziman]

Alright, I'll try this. Thank you both!

[Kyle Miller]

Just got around to rewriting checkList using the Semi API:

def checkList
    {α : Type}
    {P : α → Prop}
    {xs : List α}
    (check : (i : α) → Semi (P i))
  : Semi (∀ i ∈ xs, P i) :=
  Semi.of_imp (xs.Forall fun i => (check i).isYes)
    (by simp [List.forall_iff_forall_mem]; intro h x hx; specialize h x hx; exact true_of_isYes _ h)
    Semi.decide

Using Semi.decide you can pull in decision procedures.

(I used xs.Forall because it had some more simp lemmas, instead of List.all, which would feel more natural. There's a Decidable instance for it already, so it's fine. I didn't check, but I expect it to use List.all in the end.)

[ziman]

I'd be really curious to see how one could port Fintype.decidableForallFintype to Semi instead of Decidable.

But thanks to your help, I think I should have a way forward without it, too.

[Kyle Miller]

Take a look at its definition: it uses decidable_of_iff. You'd use the Semi.of_imp analogue, and work through the different instances until it gets down to, effectively, checkList. It's some work.

Maybe you can cheat a bit using Aaron's Classical.dec trick to extend a Semi to a Decidable, and then use Semi.decide with this instance. You'll have to mark the instance noncomputable though, but that doesn't stop reduction, so long as the computation stays inside the Semi.yes part.