resource for mutual lemmas

Stream: new members

[Vincent Siles]

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]

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]

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

[Scott Morrison]

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]

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]

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

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

[Vincent Siles]

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]

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]

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]

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

[Mario Carneiro]

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

[Vincent Siles]

indeed. That's my current solution with Coq

[Vincent Siles]

(the isomorphism / coercion)

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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