Is this automatic type rewriting?

Stream: new members

[Johannes C. Mayer]

This is a bit puzzling for me. Here I proved that band is commutative. Doing this seems to require that for every case, of what the constructor can be, I need to provide a term of type x && y = y && x. The strange thing is that I have done so without referencing x and y at all.

variables x y : bool

theorem and_comm' : x && y = y && x :=
bool.cases_on x (bool.cases_on y
    (refl (band ff ff))
    (refl (band ff tt)))
  (bool.cases_on y
    (refl (band tt ff))
    (refl (band tt tt)))

Is the correct way to think about this, that LEAN knowns that, for example, in the first term, x = ff and y = ff. Then when I provide (refl (band ff ff)) which is of type ff && ff = ff && ff LEAN automatically rewrites the type appropriately, using x = ff and y = ff, such that we get (refl (band ff ff)) : x && y = y && x?

[Mario Carneiro]

you did reference x and y, in the bool.cases_on. The four subproofs are not about x and y, they have types like ff && tt = tt && ff

[Mario Carneiro]

bool.cases_on says something like "in order to prove \forall x : bool, P(x) it suffices to prove P(true) and P(false)". In the subgoals P(true) and P(false), x is no longer present

[Mario Carneiro]

Now, there is still some funny business going on, because if you think about it (refl (band ff tt)) should have the type ff && tt = ff && tt and not ff && tt = tt && ff which, as you can check, is the expected type reported by lean for that subterm

[Mario Carneiro]

and what's actually happening is that lean evaluates the definition of band to find that ff && tt and tt && ff both normalize to the same thing, namely ff

[Johannes C. Mayer]

Ah, ok. So I guess the behavior for cases is actually an inference rule in type theory (at least it does not seem to be defined in LEAN itself). And lean can reduce the applied && because the arguments are sufficient to know the result of the bool.cases_on in the definition of &&.

[Mario Carneiro]

No, bool.cases_on is a regular function, try #print bool.cases_on to see its type and proof

[Mario Carneiro]

the part of this function that can be called "term rewriting" is in the clever choice of the "motive", the first (implicit) argument to bool.cases_on. You can see what it chose for the motives like this:

set_option pp.generalized_field_notation false
set_option pp.implicit true
#print and_comm'

theorem and_comm' : ∀ (x y : bool), x && y = y && x :=
λ (x y : bool),
  @bool.cases_on (λ (_x : bool), _x && y = y && _x) x
    (@bool.cases_on (λ (_x : bool), ff && _x = _x && ff) y
       (@refl bool (@eq bool)
          (@is_preorder.to_is_refl bool (@eq bool) (@is_equiv.to_is_preorder bool (@eq bool) (eq_is_equiv bool)))
          (ff && ff))
       (@refl bool (@eq bool)
          (@is_preorder.to_is_refl bool (@eq bool) (@is_equiv.to_is_preorder bool (@eq bool) (eq_is_equiv bool)))
          (ff && tt)))
    (@bool.cases_on (λ (_x : bool), tt && _x = _x && tt) y
       (@refl bool (@eq bool)
          (@is_preorder.to_is_refl bool (@eq bool) (@is_equiv.to_is_preorder bool (@eq bool) (eq_is_equiv bool)))
          (tt && ff))
       (@refl bool (@eq bool)
          (@is_preorder.to_is_refl bool (@eq bool) (@is_equiv.to_is_preorder bool (@eq bool) (eq_is_equiv bool)))
          (tt && tt)))

[Mario Carneiro]

the key part here is (λ (_x : bool), _x && y = y && _x), which is what we instantiate for "P" in my proof sketch. When you apply x to this, you get x && y = y && x, which is the goal, and when you apply ff to this you get ff && y = y && ff which is the first subgoal (and similarly for the second)

[Johannes C. Mayer]

Ah, I was confused because it is generated automatically. But bool.cases_on is defined in terms of bool.rec and #print tells me that the definition of bool.rec starts with protected eliminator bool.rec .... Does this mean that bool.rec is a regular function? Because it does not use def like bool.cases_on but eliminator.

[Mario Carneiro]

Indeed, while bool.cases_on is derived, it is not far from the axioms; bool.rec comes right out of the axiomatic construction for inductive types so that is "rock bottom" as far as lean is concerned

[Mario Carneiro]

Basically inductive is a schema that comes with a rule for constructing a list of axioms for each inductive type, and there is a proof on paper that those axioms can't be used to derive a contradiction

[Johannes C. Mayer]

So is a scheme basically a template that says, that if there is an object that fits into the template (i.e. it has certain properties), that then you have some new axioms (that would normally depend on the object)?

So in this case it would be that the scheme says that you have and can use the rec, and then LEAN automatically adds the rec each time we declare a new inductive type.

[Mario Carneiro]

Yes, that's exactly correct. inductive has some preconditions on it, but if the preconditions are violated then the declaration itself is rejected. If you pass the preconditions then you get a pile of axioms and can do what you like with them

[Mario Carneiro]

here's an example of an invalid inductive declaration btw:

inductive foo : Type
| mk : (foo → false) → foo
-- arg #1 of 'foo.mk' has a non positive occurrence of the datatypes being declared

[Johannes C. Mayer]

So is one of the conditions, that the type of the constructor can't contain functions 'arguments' that take in as the first parameter the type that is being declared?

[Mario Carneiro]

Yes, that's called "strict positivity". The type to be declared can't appear on the left of the left of an arrow

[Johannes C. Mayer]

ok, thanks.