Multually defined inductive type and function

Stream: new members

[Eric Wieser]

Is it possible to use mutual inductive where one branch is a type and the other is a def? Or does that question not make sense?

[Chris B]

More the latter, but can you post an example of what you'd like to do?

[Scott Olson]

I know for sure this is possible in Agda, but Lean's mutual syntax seems less flexible in these examples: https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#mutual-recursion

[Scott Olson]

The Agda docs have a TypeCode/Interpretation example: https://agda.readthedocs.io/en/v2.6.1/language/mutual-recursion.html#mutual-recursion

[Eric Wieser]

Here's my best attempt:

mutual inductive blade_new, blade_is_perp
with blade : nat → Type u
| scalar : G₀ → blade_new 0
| vector : G₁ → blade 1
-- takes a vector, n+1 blade, and a proof that the vector and n+1 blade are perpendicular
| graded {n : ℕ} : Π (v : G₁) (b : blade_new (n + 1)), (blade_is_perp v b) → blade_new (n + 2)

-- a proof of perpendicularity is either
with blade_is_perp : Π  {n : ℕ}, ∀ (v : G₁) (b : blade_new (n + 1)), sorry : sorry
-- a proof that `v` is perpendicular to the sole element of `blade_new.vector`
-- a proof that both:
--   `v` is perpendicular to the v argument of `blade_new.graded`
--   `v` is perpendicular to the b argument of `blade_new.graded`

[Eric Wieser]

I'm not really sure how to write the type of blade_is_perp

[Reid Barton]

This makes sense (it's called induction-recursion) but Lean doesn't support it.

[Reid Barton]

(are blade and blade_new supposed to be the same thing?)

[Eric Wieser]

I suppose a perhaps simpler example of my problem is constructing a list along with a proof that a relation is satisfied between every pair of elements

[Reid Barton]

You can emulate induction-recursion in Lean in various ways, but the easiest to work with in a case like this will just be to build it directly as {l : list A // l.pairwise r} -- or whatever the actual name is.

[Chris B]

Kind of a reiteration of what he said, but often you can state the definition you want in a more general way than you actually plan to use it, then declare the inductive such that it uses the specialized form of the definition. Mario Carneiro helped me with similar solution a little while back, where IFunc gets declared with a type parameter (A) that then gets filled in as the inductive : https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lea%28r%29n.20you.20a.20scheme/near/190326502

[Patrick Massot]

To be honest, I've always had the impression that people interested in those things should play with Agda instead of Lean. This part part of Lean seems broken and completely orthogonal to what works great in Lean.

[Reid Barton]

In this case the "workaround" of using a list + separately defined property is also more convenient in practice anyways.

[Eric Wieser]

@Reid Barton, is it generally better to reuse existing inductive types like list instead of defining my own?

[Johan Commelin]

Depends on what you want to do. If you reuse stuff, you can also reuse a lot of lemmas.

[Johan Commelin]

And sometimes "a lot" means > 4000 lines of code.

[Eric Wieser]

And can I use pairwise on vector instead of list?

[Johan Commelin]

Well, a vector is defined in terms of lists, so "yes".

[Kevin Buzzard]

you could easily make vector.pairwise

[Johan Commelin]

But you might need to extract the listy part out of the vector

[Eric Wieser]

@Reid Barton: I don't fully understand the syntax you have, mind giving me a really simple #check command that I can put that into?

[Eric Wieser]

parameters (l : nat)
#check (l : list nat // l.pairwise eq)

is giving me "invalid expression"

[Kevin Buzzard]

you have two l's?

[Reid Barton]

{}, not ()

[Kevin Buzzard]

#check {l : list ℕ // l.pairwise eq}

[Johan Commelin]

@Gabriel Ebner Can we rip parameter out of core? [/joking]

[Johan Commelin]

@Eric Wieser (Note that parameters will be gone in lean 4.)

[Johan Commelin]

In general, it's advised to use variables instead.

[Eric Wieser]

Oh, I assumed the {} was an argument declaration like ()

[Eric Wieser]

But here it's part of the type itself. I haven't seen this type of Type before - is there somewhere in the docs I can read about the syntax?

[Kevin Buzzard]

It's notation for subtype

[Reid Barton]

You could also just make a custom structure.

[Reid Barton]

Reuse of list lemmas is one advantage, but this style is also just easier to work with than a fancy inductive-recursive definition, at least when the inductive-recursive definition isn't buying you any additional expressive power.

[Kevin Buzzard]

I'm not sure it's easy to see the {x : X // p x} notation for @subtype X p defined in Lean, it might be baked in somehow?

[Reid Barton]

For example, you can replace the list by a propositionally equal one and then transport the proof of the property without having to rebuild the entire inductive structure.

[Eric Wieser]

Johan Commelin said:

But you might need to extract the listy part out of the vector

How do I do that?

[Eric Wieser]

(v : list ℕ) didn't work, so I guess there's no coe defined?

[Reid Barton]

There is for subtype itself, but if you introduced a def for it then there isn't for your def.

[Reid Barton]

v.val or v.1 or add a has_coe instance defined to be one of these.

[Eric Wieser]

Is there any way to get autocomplete to help me there?

[Eric Wieser]

Hitting tab after the dot gave me a massive list

[Reid Barton]

Yes, define your own structure instead of reusing subtype :upside_down:

[Reid Barton]

Otherwise, there is nothing for autocomplete to know (it isn't smart enough to unfold definitions).

[Eric Wieser]

What is the structure equivalent to {x : X // p x}?

[Kevin Buzzard]

subtype p

[Johan Commelin]

structure foo :=
(l : list X)
(p : l.pairwise eq)

[Johan Commelin]

(modulo typos)

[Eric Wieser]

Thanks, that now seems obvious

[Eric Wieser]

I was trying to work out how I could constrain the l field

[Kevin Buzzard]

oh you mean rolling your own?

[Kevin Buzzard]

the joys of dependent types

[Eric Wieser]

But obviously that's not necessary, if you pass an l that doesn't satisfy the pairwise requirement, then you just get stuck producing a p

[Scott Olson]

This is the actual definition of subtype in Lean for reference: https://github.com/leanprover-community/lean/blob/de6c873a57fda86c20dc93f4660ab257ef8e8995/library/init/core.lean#L270-L271

[Reid Barton]

By the way, note that vector is defined in the Lean core library as a subtype and not an inductive family indexed on nat, even though Lean supports those just fine, for the same reason: it's easier to use.

[Johan Commelin]

@Eric Wieser Why are you actually interested in lists of which all elements are pairwise equal? They don't seem very interesting to me...

[Eric Wieser]

@Johan Commelin: That was a contrived example, what I actually care about is list where elements have a pairwise dot product of zero

[Johan Commelin]

Ok, that sounds a lot more interesting :wink: