Zulip Chat Archive

Stream: new members

Topic: resource for mutual lemmas


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 08 2019 at 07:18):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 08 2019 at 07:22):

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

view this post on Zulip Vincent Siles (Oct 08 2019 at 07:23):

indeed. That's my current solution with Coq

view this post on Zulip Vincent Siles (Oct 08 2019 at 07:23):

(the isomorphism / coercion)

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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