Classical vs constructive logic in computation

Stream: new members

[Rekkyn]

I've heard that constructive logic plays better with computation compared to classical logic. But I've also heard that all Props are erased during computation, so it wouldn't seem to matter if a Prop was created in a classical or constructive way. Is it true that constructive logic is better for computations, and if so are there any examples of that?

[Tristan Figueroa-Reid]

Rekkyn said:

I've heard that constructive logic plays better with computation compared to classical logic. But I've also heard that all Props are erased during computation, so it wouldn't seem to matter if a Prop was created in a classical or constructive way. Is it true that constructive logic is better for computations, and if so are there any examples of that?

I don't have a good example for Prop at hand, but Props aren't the only things that can be created with classical logic (the axiom of choice is part of classical logic, and is the backing axiom for the LEM by Diaconescu's theorem)

An example of how classical logic wouldn't play well with computation is graph coloring: graph coloring can be made classically.

[Tristan Figueroa-Reid]

Correction: there is no good example for Props (assuming what you mean by "Props are erased by computation" is from #tpil (at Axioms and Computations))

[Kyle Miller]

I think that's a bit different from what Rekkyn is asking. That's a noncomputable instance, and it's noncomputable because it's using choice to "construct" a list of all the colorings. (Side note: we should change that to be a Finite instance!) There was never any hope that it would be computable.

For definitions, it doesn't matter one way or another if the proofs that appear in them are proved using choice or not. It all gets erased when the function is compiled for evaluation.

If you care about defeq properties, it's possible for something like Eq.rec or Acc.rec to get stuck on a classical proof (since in reduction proofs are not erased). I've never run into this as an issue however.

Sometimes people talk about writing proofs without constructive logic so that they can be reduced to compute witnesses "for free". That's probably where "better for computations" comes from. My understanding of the situation for Lean is (1) reducing proofs is largely a non-goal so things can get unnecessarily stuck because, for example, types aren't reduced and Eq.rec can get stuck during reduction of an otherwise "computable" definition and (2) people have found that reduction of proofs is not normalizing (#general > Normalization fails in lean @ 💬 ) so perhaps it's not good to try relying on this in Lean.

In practice, rather than writing proofs of existentials, you can make definitions that compute a witness and then write theorems that prove the witnesses have certain properties.

[Kyle Miller]

It's possible to work constructively in the sense of making sure to give algorithms for everything that is meaningfully computable, without subscribing to constructive logic, which is making the proofs themselves computable in some sense too. (I think CS outside of type theory tends not to ever think about avoiding LEM in proofs about algorithms for example. That doesn't make the algorithms any less computable.)

[Aaron Liu]

Kyle Miller said:

That's a noncomputable instance, and it's noncomputable because it's using choice to "construct" a list of all the colorings. (Side note: we should change that to be a Finite instance!) There was never any hope that it would be computable.

I think you can make it computable if you add DecidableRel G.Adj. Why give up on computability?

[Rekkyn]

Kyle Miller said:

I think that's a bit different from what Rekkyn is asking. That's a noncomputable instance, and it's noncomputable because it's using choice to "construct" a list of all the colorings. (Side note: we should change that to be a Finite instance!) There was never any hope that it would be computable.

For definitions, it doesn't matter one way or another if the proofs that appear in them are proved using choice or not. It all gets erased when the function is compiled for evaluation.

If you care about defeq properties, it's possible for something like Eq.rec or Acc.rec to get stuck on a classical proof (since in reduction proofs are not erased). I've never run into this as an issue however.

Sometimes people talk about writing proofs without constructive logic so that they can be reduced to compute witnesses "for free". That's probably where "better for computations" comes from. My understanding of the situation for Lean is (1) reducing proofs is largely a non-goal so things can get unnecessarily stuck because, for example, types aren't reduced and Eq.rec can get stuck during reduction of an otherwise "computable" definition and (2) people have found that reduction of proofs is not normalizing (#general > Normalization fails in lean @ 💬 ) so perhaps it's not good to try relying on this in Lean.

In practice, rather than writing proofs of existentials, you can make definitions that compute a witness and then write theorems that prove the witnesses have certain properties.

This makes sense, thanks! I'm guessing there's no reason why someone couldn't make "computable" versions of the built-in Props like this?

inductive TypeOr (a b : Prop) : Type where
  | inl (h : a) : TypeOr a b
  | inr (h : b) : TypeOr a b

[Aaron Liu]

My understanding is, there also hasn't been any reason for anyone to do this either.

[Aaron Liu]

If you want to emulate this behavior, use docs#PLift to change the arguments from Prop to Type, then use Sum/Prod/Sigma to construct the "computable" version.

[Rekkyn]

Aaron Liu said:

If you want to emulate this behavior, use docs#PLift to change the arguments from Prop to Type, then use Sum/Prod/Sigma to construct the "computable" version.

That's useful to know, thanks!

[Kyle Miller]

If you think you can make it computable (ideally with an efficient algorithm) then go ahead @Aaron Liu!

There are two points here:

1. Noncomputable Fintype instances are useless. They should be Finite instances. This instance pre-dates Finite, otherwise I would have written it as a Finite instance.
2. It is worth having Finite instances since they do not bring in unnecessary dependence on algorithms. Inside a proof, it does not matter at all that there's some arbitrary way to make a List of all simple graphs. Mere finiteness suffices.

[Edward van de Meent]

Inside a proof, it may matter if there is a computable list: if you're working with a concrete type and you want to do case analysis using fin_cases, you need a computable Fintype instance.

[Aaron Liu]

Kyle Miller said:

If you think you can make it computable (ideally with an efficient algorithm) then go ahead Aaron Liu!

For now, it's not efficient. Maybe I'll implement an efficient algorithm later.

Code

import Mathlib.Combinatorics.SimpleGraph.Coloring

variable {V α : Type*} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [Fintype α] [DecidableRel G.Adj]

def finColoringFintype : Fintype (G.Coloring (Fin n)) := by
  refine ⟨?_, ?_⟩
  · refine (Finset.univ : Finset (V → Fin n)).filterMap ?_ ?_
    · intro color
      by_cases valid : ∀ {v w : V}, G.Adj v w → color v ≠ color w
      · exact some (SimpleGraph.Coloring.mk color valid)
      · exact none
    · intro a b c hac hbc
      ext x
      simp only [Option.mem_def, Option.dite_none_right_eq_some, Option.some.injEq] at hac hbc
      obtain ⟨ha, hab⟩ := hac
      obtain ⟨hb, rfl⟩ := hbc
      apply_fun (· x |>.val) at hab
      exact hab
  · intro x
    rw [Finset.mem_filterMap]
    use x, Finset.mem_univ _
    rw [dif_pos (@SimpleGraph.Coloring.valid V G (Fin n) x), Option.some.injEq]
    ext
    rfl

instance : Fintype (G.Coloring α) :=
  (Fintype.truncFinBijection α).recOnSubsingleton fun f ↦
    finColoringFintype.ofBijective (fun g ↦ G.recolorOfEmbedding ⟨f.val, f.prop.injective⟩ g) <| by
      constructor
      · apply Function.Embedding.injective
      · intro a
        use G.recolorOfEquiv (Equiv.ofBijective f.val f.prop).symm a
        ext v
        simp [Equiv.ofBijective_apply_symm_apply]

[Aaron Liu]

I had some time, so I made it more efficient (without tactics).

More Efficient

import Mathlib.Combinatorics.SimpleGraph.Coloring

def finColoringFintype {G : SimpleGraph (Fin n)} [DecidableRel G.Adj] :
    Fintype (G.Coloring (Fin m)) :=
  Nat.rec
    (motive := fun n ↦ ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj], Fintype (G.Coloring (Fin m)))
    (fun _ _ ↦
      ⟨{⟨Fin.elim0, fun {a} ↦ a.elim0⟩},
       fun _ ↦ Finset.mem_singleton.mpr (RelHom.ext fun a ↦ a.elim0)⟩)
    (fun n ih G _ ↦
      ⟨(@Finset.univ _ (ih _) ×ˢ Finset.univ).filterMap
        (fun p : (G.comap Fin.castSucc).Coloring (Fin m) × Fin m ↦
          if h : ∀ a, G.Adj a.castSucc (Fin.last n) → p.fst a ≠ p.snd then
          some (SimpleGraph.Coloring.mk (Fin.snoc p.fst p.snd)
            fun {v w} ↦ v.lastCases
              (Fin.snoc_last .. ▸ w.lastCases
                (fun hAdj ↦ (G.irrefl hAdj).elim)
                (fun w hAdj ↦ Fin.snoc_castSucc .. ▸ (h w hAdj.symm).symm))
              (fun v ↦ Fin.snoc_castSucc .. ▸ w.lastCases
                (Fin.snoc_last .. ▸ h v)
                (fun _ ↦ Fin.snoc_castSucc .. ▸ p.fst.valid))) else none)
        fun v w _ hbv hbw ↦
          (Option.dite_none_right_eq_some.mp (Option.mem_def.mp hbv)).elim fun _ hv ↦
          (Option.dite_none_right_eq_some.mp (Option.mem_def.mp hbw)).elim fun _ hw ↦
            Prod.ext (RelHom.ext fun x ↦
              @Fin.snoc_castSucc n (fun _ ↦ Fin m) v.snd v.fst x ▸
              @Fin.snoc_castSucc n (fun _ ↦ Fin m) w.snd w.fst x ▸
              congrArg (· x.castSucc) (Option.some.inj (hv.trans hw.symm)))
              (@Fin.snoc_last n (fun _ ↦ Fin m) v.snd v.fst ▸
               @Fin.snoc_last n (fun _ ↦ Fin m) w.snd w.fst ▸
               congrArg (· (Fin.last n)) (Option.some.inj (hv.trans hw.symm))),
      fun C ↦ (Finset.mem_filterMap _).mpr
        ⟨(SimpleGraph.Hom.comp C (SimpleGraph.Hom.comap Fin.castSucc G), C (Fin.last n)),
          Finset.mk_mem_product (Finset.mem_univ _) (Finset.mem_univ (C (Fin.last n))),
          (dif_pos fun (a : Fin n) (ha : G.Adj a.castSucc (Fin.last n)) ↦ C.valid ha).trans
          (congrArg some (RelHom.ext fun x ↦ x.lastCases
            (@Fin.snoc_last n (fun _ ↦ Fin m) (C (Fin.last n)) _)
            (@Fin.snoc_castSucc n (fun _ ↦ Fin m) (C (Fin.last n)) _)))⟩⟩) n G

variable {V α : Type*} {G : SimpleGraph V} [Fintype V] [Fintype α] [DecidableEq V] [DecidableRel G.Adj]

instance : Fintype (G.Coloring α) :=
  (Fintype.truncFinBijection α).recOnSubsingleton fun ⟨f, hf⟩ ↦
    (Fintype.truncEquivFin V).recOnSubsingleton fun e ↦
      ⟨(@Finset.univ _ finColoringFintype).map
        ⟨fun r ↦
          (SimpleGraph.Embedding.completeGraph ⟨f, hf.injective⟩).toHom.comp
            (SimpleGraph.Hom.comp r (SimpleGraph.Embedding.map e.toEmbedding G).toHom),
              fun a b hab ↦ RelHom.ext fun x ↦
                e.apply_symm_apply x ▸
                Equiv.ofBijective_symm_apply_apply f hf (a (e (e.symm x))) ▸
                Equiv.ofBijective_symm_apply_apply f hf (b (e (e.symm x))) ▸
                congrArg (fun r ↦ (Equiv.ofBijective f hf).symm (r (e.symm x))) hab⟩,
      fun r ↦ Finset.mem_map.mpr
        ⟨(SimpleGraph.Iso.completeGraph (Equiv.ofBijective f hf).symm).toHom.comp
        (SimpleGraph.Hom.comp r (SimpleGraph.Iso.map e G).symm),
        @Finset.mem_univ _ finColoringFintype _, RelHom.ext fun x ↦
          (Equiv.ofBijective_apply_symm_apply f hf (r (e.symm (e x)))).trans
          (congrArg r (e.symm_apply_apply x))⟩⟩

[Kyle Miller]

I'm not sure why it's written with all the proofs as proof terms — using tactics for proofs doesn't make definitions any less efficient, and using proof terms significantly harms readability.

Also, it's almost always better to use recursion instead of raw recursors. That motive doesn't look like it's complicated, so match ought to be able to handle the situation itself.

[Aaron Liu]

I tried match and it didn't work (not generalizing enough) (yes I tried (generalizing := true)), so I used Nat.rec directly.
I was writing it in term mode because "don't construct terms using tactics" and before I knew it, I had written the whole thing in terms.

I tried this on #eval Fintype.card ((⊤ : (SimpleGraph (Fin 8))).Coloring (Fin 7)) and this solution was 8 times faster than the other one I wrote.

[Kyle Miller]

That's fair, but if we want to include it in mathlib, we'll have to write it in a readable style. Ideally, we would factor out the key ideas into multiple definitions too. This is not an irreducibly complex computation.