Another basic question: prove equality of inductive type arg

Stream: new members

[Alcides Fonseca]

inductive K : ℕ → Prop
| rule1 : K 1

theorem this_is_a_test {n}:
    K n → n = 1 :=
begin
    intro n_k,
    sorry,
end

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?

[Chris Hughes]

Continue induction n_k, refl.

[Chris Hughes]

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

[Alcides Fonseca]

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

[Alcides Fonseca]

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 = ⋆ :=
begin
    intro n_k,
    induction n_k,
    refl,
end

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
state:
Γ : Context,
k : Kind,
n_k : CheckKind Γ Ty.Integer k
⊢ k = ⋆

I can provide the full file if required.

[Kevin Buzzard]

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

[Alcides Fonseca]

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 :=
begin
    intro n_k,
    induction n_k, <-- error
    refl,
end

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

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Mario Carneiro]

inductive th := t0, t1, t2

Oh wow that page is old

[Andrew Ashworth]

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

[Alcides Fonseca]

@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!

[Mario Carneiro]

(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.)