## Stream: new members

### Topic: resource for mutual lemmas

#### Vincent Siles (Oct 07 2019 at 12:53):

Using the doc I managed to define a simple value type

inductive value : Type
| VBoolean : bool -> value
| VInteger : int -> value
| VString : string -> value
| VSequence : list value -> value
| VNone : value


and a boolean equality on it (by mutually defining val_eqb and val_list_eqb). Now I'm trying to prove some facts about it (my ultimate goal would be to provide an instance of decidable_eq), but I'm struggling to define mutual lemmas. So far I tried:

mutual theorem val_eqb_eq, val_list_eqb_eq
with val_eqb_eq: ∀ v0 v1, val_eqb v0 v1 = tt ↔ v0 = v1  :=
begin
sorry,
end
with val_list_eqb_eq : ∀ l0 l1, val_list_eqb l0 l1 = tt ↔ l0 = l1


which has several issues:
invalid equations, must be followed by a command, '.', 'with', doc-string or EOF on the := and invalid mutual declaration, 'val_list_eqb_eq' expected on the end.

I can't find much on https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#mutual-recursion, but maybe there are other resources ?

#### Rob Lewis (Oct 07 2019 at 13:42):

I think you have to use pattern matching notation in mutual declarations, e.g.

mutual theorem val_eqb_eq, val_list_eqb_eq
with val_eqb_eq: ∀ v0 v1, val_eqb v0 v1 = tt ↔ v0 = v1
| v0 v1 := sorry
with val_list_eqb_eq : ∀ l0 l1, val_list_eqb l0 l1 = tt ↔ l0 = l1
| l0 l1 := sorry


But note that nested inductives (VSequence : list value -> value) are not one of the strong points of Lean 3. There's limited support for this and you'll get frustrated quickly.

#### Vincent Siles (Oct 07 2019 at 13:55):

Damned... and I was thinking I could get away from Coq for that reason :D Thanks for the insight

#### Scott Morrison (Oct 08 2019 at 00:50):

My advice would be to avoid the mutual keyword entirely, and roll your own "all-at-once" object defined recursively, then define projectors pulling out the bits you want.

#### Vincent Siles (Oct 08 2019 at 06:56):

I tried something like that, but I found that it was as annoying as doing it in Coq, so I'll stick with what I know for the moment

#### Mario Carneiro (Oct 08 2019 at 07:16):

@Vincent Siles Lean implements nested inductives using regular inductives, and you can roll your own without too much difficulty. We're working on a more general framework for nested inductives, but lean's built in inductives have a decent behavior as is

#### Mario Carneiro (Oct 08 2019 at 07:18):

Lean's built in compilation for nested inductives is... half baked

#### Vincent Siles (Oct 08 2019 at 07:20):

I'll definitenly check it out, but right now I have some time constraints, so I'll stick to what I know :p

#### Mario Carneiro (Oct 08 2019 at 07:20):

In the case of the value type, I don't even see why a nested inductive is necessary. Can't you just do:

inductive value : Type
| VBoolean : bool -> value
| VInteger : int -> value
| VString : string -> value
| VNil : value
| VCons : value -> value -> value
| VNone : value


#### Vincent Siles (Oct 08 2019 at 07:21):

It's less easy, I can't directly reuse the list library . What you propose is the usual solution to deal with nested. But you loose all benefits of actual lists

#### Mario Carneiro (Oct 08 2019 at 07:22):

you won't really be able to reuse the list library anyway, because you will have lots of induction constraints

#### Mario Carneiro (Oct 08 2019 at 07:22):

unless you are using it nonrecursively, in which case it's easy to build an isomorphism

#### Vincent Siles (Oct 08 2019 at 07:23):

indeed. That's my current solution with Coq

#### Vincent Siles (Oct 08 2019 at 07:23):

(the isomorphism / coercion)

#### Mario Carneiro (Oct 08 2019 at 07:25):

I think that no matter how you cut it it won't be as nice as a true nested inductive because it's not really a list constructor, it's only a shim over the basic inductive. If you are willing to put meta it will act like the "real thing"

#### Vincent Siles (Oct 08 2019 at 07:26):

I don't know about meta. I'll read about it when I'll arrive at the office, thanks

#### Mario Carneiro (Oct 08 2019 at 07:28):

This basically means "I don't care about proving things, pretend this is Haskell". It lifts the well foundedness restrictions on recursion and basically all constraints on inductives (positivity, nestedness, etc), meaning that the logic becomes unsound but it still has an operational semantics and you can use it like a programming language

#### Kevin Buzzard (Oct 08 2019 at 09:32):

That's a really nice way of thinking about meta -- it should be called haskell.

Last updated: May 10 2021 at 23:11 UTC