logical connectives vs inductive definitions

Stream: general

[Billy Price]

This is a pretty general question. The first time I formalised something in Lean, I made fairly frequent use of logical connectives in my definitions, but after returning to do something else, I noticed that I could essentially eliminate all uses of disjunctions, conjunctions and existentials by defining it inductively. For example, if I have a property foo in mind of objects a of type A which holds if bar a or baz a, my old instinct would be something like

def foo : A -> Prop := bar a ∨ baz a

but now I tend to do something like this

inductive foo : A -> Prop
| foo.bar  {a} : bar a -> foo a
| foo.baz {a} : baz a -> foo a

Similarly, I could define something using an existential, or I could do it inductively with the existential argument as an argument to the constructor. Conjunctions can also be removed by currying if they are a hypothesis to a constructor and by splitting into two constructors if it's a conclusion.

Is this a well understood phenomena, and is there any important difference between these two different ways of defining things? I have an intuition that the difference between | foo.bar {a} : (∃ b, bar a b) -> foo a and | foo.bar {a} (b) : bar a b -> foo a has some computability significance, though I'm not sure.

I think I just picked up this habit implicitly from read other people's Lean code, and I have a feeling that this is the "better" way to define things in lean, and leads to cleaner tactic proofs, but I don't really know enough to confirm that.

[Damiano Testa]

I believe that, internally, and and or are defined as inductive types. Thus, what you seem to be doing is to bypass a step and go straight to the "correct" form.

[Billy Price]

That's a good point! same for the existential right?

[Horatiu Cheval]

I would say the second variant (the one without exists) is more common and easier to work with since it's more straightforward to partially apply foo.bar to b and so on. Plus I think the second version is nicer because it can be written the same way even if your inductive is not Prop valued, while with the first you might need to change the existential into something else.

[Horatiu Cheval]

And I don't think there's any computationally significant difference between the two if you are defining Props, which by definition carry no computational meaning

[Yakov Pechersky]

A counterpoint is that "and", "or", "exists" have many helper lemmas proved about them, like or.comm. Of course one could prove the equivalent for your bespoke type, or might not need them, but there is a usefulness to the commonality of the logical structure, if your proofs involve conversion and manipulation of the terms.

[Alex J. Best]

An example of @Yakov Pechersky's point:

import tactic

inductive is_zero_or_one_mod_four : ℕ -> Prop
| zero (n) : n % 4 = 0 → is_zero_or_one_mod_four n
| one (n) : n % 4 = 1 → is_zero_or_one_mod_four n

example : is_zero_or_one_mod_four 9 :=
begin
  have : 9 % 4 = 1 := rfl,
  simp [this], -- fails, need to explicitly apply our constructors
end

@[simp]
def is_zero_or_one_mod_four' : ℕ -> Prop := λ n, n % 4 = 0 ∨ n % 4 = 1

example : is_zero_or_one_mod_four' 9 :=
begin
  have : 9 % 4 = 1 := rfl,
  simp,
  simp [this], -- LOL
end

with the inductive definition we don't get access to the simplifier for free.

Side question: Does anyone know why simp [this] doesn't work for the second example, is this a known bug?

[Horatiu Cheval]

I think another thing against using logical connectives, not really applicable to the examples here but to more complicated inductives with recursive constructors, is that iirc lean might not work very well with nested inductives. I remember trying to define a constructor of the form foo.bar (a b) : foo a \/ foo b -> foo (baz a b) where lean would reject it with some unexpected nested inductive error, so I had no choice than to break up the disjunction into two constructors.

[Horatiu Cheval]

Slightly off-topic, but I think this fits into a more general "inductive predicates vs recursive functions" discussion. Is there a mathlib standard approach to this? I think I've seen several times the pattern of defining an inductive predicate and then defining a recursive function equivalent to it, so that you can move between the approaches and get the benefits of both.

[Kyle Miller]

Yakov Pechersky said:

A counterpoint is that "and", "or", "exists" have many helper lemmas proved about them, like or.comm. Of course one could prove the equivalent for your bespoke type, or might not need them, but there is a usefulness to the commonality of the logical structure, if your proofs involve conversion and manipulation of the terms.

I've wondered before about having some mechanism that could convert things to the "canonical" generic equivalents, like sigmas, exists, products, sums, ands, ors, etc. so that generic lemmas might apply. Maybe one implementation of it would be an attribute you could apply to certain inductive types to generate an equivalence to the generic version.

[Yakov Pechersky]

More contributions into making the transport tactic stronger could be one direction. The derive handler is also powerful, and could be extended to provide such lemmas.

[Mario Carneiro]

Yes, I would like to have a derive handler similar to haskell's deriving Generic that would reduce everything to W-types and prove equivalence. That could be used to power other derive handlers like derive fintype, derive subsingleton, derive countable, derive encodable

[Yakov Pechersky]

How close is the delta derive handler?

[Mario Carneiro]

delta derive only handles straight unfolding of def foo := bar, it doesn't work on inductive types

[Mario Carneiro]

I mean to take an arbitrary inductive type and write down an equivalent combination of sum, prod, W (there is a chapter on this in my thesis)

[Eric Wieser]

We have docs#mk_iff_of_inductive_prop_cmd which I think glues over between inductive types and and/or

[Eric Wieser]

Which I think works via @[mk_iff]

[Kyle Miller]

Indeed (using @Alex J. Best's example):

import tactic

@[mk_iff] inductive is_zero_or_one_mod_four : ℕ -> Prop
| zero (n) : n % 4 = 0 → is_zero_or_one_mod_four n
| one (n) : n % 4 = 1 → is_zero_or_one_mod_four n

attribute [simp] is_zero_or_one_mod_four_iff

example : is_zero_or_one_mod_four 9 :=
begin
  have : 9 % 4 = 1 := rfl,
  simp [this],
end

[Alex J. Best]

(deleted)

[Alex J. Best]

Wow I didn't know about this (clearly! lol). It looks like this is only used about 10 times in mathlib, what do people think, should we be adding it to more inductive Props like docs#is_solvable_by_rad?

[Mario Carneiro]

I don't think it works for recursive predicates (or at least, the result isn't particularly useful as a definition)

[Mario Carneiro]

is_solvable_by_rad needs to be an inductive predicate because it is inductively generated by clauses