modular proofs?

Stream: new members

[Anthony Towns]

Hi; I've messed around with coq a little in the past and am trying to learn lean4 -- so far it's pretty cool! One thing I'm having trouble with is how to make my proofs "modular" -- ie, I'm trying to prove an algorithm works the way I think it does, but I don't want to be overly specific about the data it's operating on.

The way I've been trying to solve this is by creating a class:

class MyData (Foo : Type u) where
  relationship : Foo -> Foo -> Prop
  constraint : forall (a b : Foo), relationship a b -> not relationship b a
  Fn1 : Foo -> Int

and then for messing around, I made an Example.lean file with a @[default instance] of MyData (Prod Int Nat).

That seems to work okay, but in order to prove theorems on it and stuff, I obviously want to be general and just rely on the "relationship" and "Fn1" relationships/constraints/functions/etc. So I've written:

section specific
variable {Foo : Type u} [MyData Foo]
open MyData

But the next thing I'd like is to give myself an alias for List (List Foo)); but using def or abbrev then gives me errors when I use that alias like "don't know how to synthesise implicit argument" for Foo, presumably because it's leaving Foo as arbitrary, rather than keeping it linked to the variable I've declared.

While writing this, googling has led me to try:

section specific
set_option quotPrecheck.allowSectionVars true
variable {Foo : Type u} [MyData Foo]
open MyData
notation "SomeFoo" => List (List Foo)
```

which seems to work so far, but seems pretty obscure? Anyway, does that all seem sensible, or is there a better way?

[Kyle Miller]

Using notation like this is common in mathlib, though be sure to do local notation so that it doesn't escape the section where it makes sense.

[Kyle Miller]

If you use mathlib's notation3 command (which is notation but with some Lean-3-like extensions and a more powerful pretty printer generator), then List (List Foo) will pretty print as SomeFoo too.

[Anthony Towns]

Thanks!

Kyle Miller said:

If you use mathlib's notation3 command (which is notation but with some Lean-3-like extensions and a more powerful pretty printer generator), then List (List Foo) will pretty print as SomeFoo too.

At least in emacs/flycheck, it seems to pretty print that way already, so I guess I'll stick with this since the notation3 seems to be in a "we're not sure we'll keep this" state...