Zulip Chat Archive

Stream: new members

Topic: Another basic question: prove equality of inductive type arg

view this post on Zulip Alcides Fonseca (Jun 09 2020 at 20:33):

inductive K :   Prop
| rule1 : K 1

theorem this_is_a_test {n}:
    K n  n = 1 :=
    intro n_k,

I have reduced my problem to this simple case. I want to prove that n can only be 1 due to the inductive structure of K that has no other value. In my real-world example, there are plenty of rules with multiple arguments, but the gist of it is this case, which I cannot prove. Any tips?

view this post on Zulip Chris Hughes (Jun 09 2020 at 20:36):

Continue induction n_k, refl.

view this post on Zulip Chris Hughes (Jun 09 2020 at 20:37):

induction is what you should use to prove things about inductive predicates.

view this post on Zulip Alcides Fonseca (Jun 09 2020 at 20:39):

Thank you! This works on this small problem, but not on the original problem. Let me see if I can figure out the difference.

view this post on Zulip Alcides Fonseca (Jun 09 2020 at 20:46):

A more realist example, in which that solution does not work:

import syntax

mutual inductive K, CheckKind
with K :     Prop
| rule1 {y} : K y 2

with CheckKind : Context  Ty  Kind  Prop
| K_Int {Γ} :
    CheckKind Γ Ty.Integer 

| K_Bool {Γ} :
    CheckKind Γ Ty.Boolean 

theorem this_is_a_test {Γ k}:
    CheckKind Γ Ty.Integer k  k =  :=
    intro n_k,
    induction n_k,

The error is:

test.lean:22:4: error
induction tactic failed, argument #2 of major premise type
  CheckKind Γ Ty.Integer k
is not a variable
Γ : Context,
k : Kind,
n_k : CheckKind Γ Ty.Integer k
 k = 

I can provide the full file if required.

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 21:04):

Mutual inductives are somehow compiled down to regular inductives in an arcane way. You could try cases n_k and if that doesn't work either then you might want to start looking at the output of #print prefix CheckKind to find out what's actually going on

view this post on Zulip Alcides Fonseca (Jun 09 2020 at 21:08):

The problem was indeed related with mutual induction. A more simple example would be:

mutual inductive K, K2
with K :       Prop
| rule1 {y} : K y 1 2

with K2 : Prop
| rule2 : K2

theorem this_is_another_test {y n}:
    K y 1 n  n = 2 :=
    intro n_k,
    induction n_k, <-- error

Using cases indeed worked. Thank you very much to both!

view this post on Zulip Mario Carneiro (Jun 10 2020 at 02:40):

The compilation of mutual inductives to regular inductives is not that arcane, at least on paper, and in fact because of the limitations of Lean's implementation I often just do this compilation process manually by writing the underlying inductive type myself (and depending on the application I might just use the new composite inductive type directly rather than defining the two mutual inductive types and all the translation machinery).

The idea is simple: Take all the indices of all elements of the mutual inductive and compress them into one "index inductive" with one constructor for each mutual inductive. (You can use either a new inductive or just use sums and products if you are too lazy to give this inductive a name.) For example, in your mutual inductive the first inductive is K : ℕ → ℕ → Prop and the second is CheckKind : Context → Ty → Kind → Prop, so the index inductive is essentially ℕ × ℕ ⊕ Context × Ty × Kind, or as an inductive:

inductive Ty | Integer | Boolean
def Context : Type := sorry
inductive Kind | star
notation `` := Kind.star

inductive K_Kind : Type
| K :     K_Kind
| CheckKind : Context  Ty  Kind  K_Kind

The actual inductive we are writing will have type T : K_Kind -> Prop, with the old K m n being expressed as T (K_Kind.K m n) and the old CheckKind Γ A k being T (K_Kind.CheckKind Γ A k). Then we just write down the constructors:

open K_Kind
inductive T : K_Kind  Prop
| rule1 {y} : T (K y 2)
| K_Int {Γ} : T (CheckKind Γ Ty.Integer )
| K_Bool {Γ} : T (CheckKind Γ Ty.Boolean )

Since this example has been significantly golfed already, the mutual inductive is not very interesting because there are no cross-recursions, and this could just be two separate inductive types. But we can easily use either type in any constructor.

The big advantage of writing things like this instead of using lean's mutual inductive is that you can do proper structural mutual recursion. Currently lean fakes it with well founded recursion and it's not too hard to find the limitations; the recursion principle that is generated is also wrong so it doesn't allow you to manually write structural recursions. This composite inductive's recursor yields the correct mutual recursion principle.

view this post on Zulip Mario Carneiro (Jun 10 2020 at 02:43):

There is also a wiki page on the MS lean repo Compiling mutually inductive declarations that describes this process.

view this post on Zulip Mario Carneiro (Jun 10 2020 at 02:44):

inductive th := t0, t1, t2

Oh wow that page is old

view this post on Zulip Andrew Ashworth (Jun 10 2020 at 04:07):

This explanation might well also belong on the community wiki. Mutual inductives are a sore point in Lean.

view this post on Zulip Alcides Fonseca (Jun 10 2020 at 08:06):

@Mario Carneiro Thank you for the explanation. Because I am having other errors (related to missing well-founded recursion) I might have to move to the "manually compiled" version. And yes, I have a few cross-recursions, thus the need for mutual inductive types. So this was actually very helpful!

view this post on Zulip Mario Carneiro (Jun 10 2020 at 08:07):

(I assumed you did, else why use a mutual inductive? But your example was a bit too abstract to demonstrate all the interesting aspects of mutual inductives.)

Last updated: May 13 2021 at 18:26 UTC