What's needed for mutual defs?

Stream: lean4

[Arthur Paulino]

Hi! Not sure how troublesome this is but we're trying to make mutual blocks with a somewhat minimal baggage. What else do we need to make this work?

prelude

def id (A : Type) (x : A) : A := x

inductive Unit where
| unit

inductive Bar
  | hi | bye

def bar := Bar.hi

inductive MyNat
| zero : MyNat
| succ : MyNat → MyNat

structure PProd (α : Sort u) (β : Sort v) where
  fst : α
  snd : β

mutual

  def f : MyNat → MyNat
    | .zero   => .zero
  -- tactic 'cases' failed, nested error:
  -- tactic 'cases' failed, not applicable to the given hypothesis
  -- _fun_discr✝ : MyNat
  -- motive : MyNat → Sort ?u.74
  -- h_1 : Unit → motive MyNat.zero
  -- h_2 : (n : MyNat) → motive (MyNat.succ n)
  -- ⊢ motive _fun_discr✝ after processing
  --   _
  -- the dependent pattern matcher can solve the following kinds of equations
  -- - <var> = <term> and <term> = <var>
  -- - <term> = <term> where the terms are definitionally equal
  -- - <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
  --     | .succ n => (g n).succ

  def g : MyNat → MyNat
    | .zero   => .zero
    | .succ n => (f n).succ

end

[Sebastian Ullrich]

You should probably get comfortable with navigating the Lean source code if that's your goal. For example, starting at "tactic 'cases' failed, not applicable to the given hypothesis" you should soon find the next missing type.

[Arthur Paulino]

Sorry, the error message is cryptic to me :/
I can't parse that there is a missing type, so I can't parse what the missing type is

[Leonardo de Moura]

BTW, when defining your own prelude, be aware of the issue https://github.com/leanprover/lean4/issues/188

[Sebastian Ullrich]

Arthur Paulino said:

Sorry, the error message is cryptic to me :/
I can't parse that there is a missing type, so I can't parse what the missing type is

That's why I talked about navigating the codebase: if you grep for the message (preferable the second half, as the first half could be templated), you're already very close.

[Mario Carneiro]

@Leonardo de Moura Regarding lean4#188, I think lean should have something like rust's "lang items": when you declare Nat you would put a @[lang] (or @[lang = "Nat"]) attribute on it and this would use the given key / the declaration name to determine what to check about the definition

[Mario Carneiro]

This is also useful for documenting which types have extra special compiler magic on top of the usual

[Mario Carneiro]

(The @[lang = "Nat"] form would allow decoupling lang items from their names, so that for example you could declare it to have the name nat instead in a custom prelude. But this would require plumbing the name lookups everywhere instead of hardcoding names like `Nat.add around and personally I don't think it's worth it.)

[Arthur Paulino]

Sebastian Ullrich said:

grep for the message

Ah, now I understood the idea. Thanks!

[Arthur Paulino]

So, apparently this match is falling in the "anything else" case, which means that casesOn is not being found in the environment. However, I couldn't find a casesOn type that I could add to my prelude file :sad:

[Arthur Paulino]

I tried another approach: copy increasingly longer bits of Prelude.lean until it works.
Apparently no more types are missing, but I don't have what's needed to allow Lean to prove terminations by itself. How does that work?

[Arthur Paulino]

This is the #mwe:

prelude

universe u v w

@[inline] def id {α : Sort u} (a : α) : α := a

@[inline] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=
  fun x => f (g x)

@[inline] def Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
  fun x => a

set_option checkBinderAnnotations false in
@[reducible] def inferInstance {α : Sort u} [i : α] : α := i
set_option checkBinderAnnotations false in
@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive PUnit : Sort u where
  | unit : PUnit

/-- An abbreviation for `PUnit.{0}`, its most common instantiation.
    This Type should be preferred over `PUnit` where possible to avoid
    unnecessary universe parameters. -/
abbrev Unit : Type := PUnit

@[matchPattern] abbrev Unit.unit : Unit := PUnit.unit

/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/
unsafe axiom lcProof {α : Prop} : α

/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/
unsafe axiom lcUnreachable {α : Sort u} : α

inductive True : Prop where
  | intro : True

inductive False : Prop

inductive Empty : Type

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive PEmpty : Sort u where

def Not (a : Prop) : Prop := a → False

@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
  False.rec (fun _ => C) h

@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
  False.elim (h₂ h₁)

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

@[simp] abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
  Eq.rec (motive := fun α _ => motive α) m h

@[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a

@[simp] theorem id_eq (a : α) : Eq (id a) a := rfl

theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b :=
  Eq.ndrec h₂ h₁

theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
  h ▸ rfl

theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=
  h₂ ▸ h₁

@[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
  Eq.rec (motive := fun α _ => α) a h

theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
  h ▸ rfl

theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : Eq f₁ f₂) (h₂ : Eq a₁ a₂) : Eq (f₁ a₁) (f₂ a₂) :=
  h₁ ▸ h₂ ▸ rfl

theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) →  β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
  h ▸ rfl

init_quot

inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
  | refl (a : α) : HEq a a

@[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
  HEq.refl a

theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
  have : (α β : Sort u) → (a : α) → (b : β) → HEq a b → (h : Eq α β) → Eq (cast h a) b :=
    fun α β a b h₁ =>
      HEq.rec (motive := fun {β} (b : β) (h : HEq a b) => (h₂ : Eq α β) → Eq (cast h₂ a) b)
        (fun (h₂ : Eq α α) => rfl)
        h₁
  this α α a a' h rfl

structure Prod (α : Type u) (β : Type v) where
  fst : α
  snd : β

attribute [unbox] Prod

/-- Similar to `Prod`, but `α` and `β` can be propositions.
   We use this Type internally to automatically generate the brecOn recursor. -/
structure PProd (α : Sort u) (β : Sort v) where
  fst : α
  snd : β

structure And (a b : Prop) : Prop where
  intro :: (left : a) (right : b)

inductive PSum (α : Sort u) (β : Sort v) where
  | inl (val : α) : PSum α β
  | inr (val : β) : PSum α β

inductive Bar
  | hi | bye

def bar := Bar.hi

inductive MyNat
| zero : MyNat
| succ : MyNat → MyNat

mutual

  def f : MyNat → MyNat
    | .zero   => .zero
    | .succ n => (g n).succ

  def g : MyNat → MyNat
    | .zero   => .zero
    | .succ n => (f n).succ

end

[Henrik Böving]

When I check your example with ordinary nats:

mutual

  def f : Nat → Nat
    | .zero   => .zero
    | .succ n => (g n).succ

  def g : Nat → Nat
    | .zero   => .zero
    | .succ n => (f n).succ

end

And print what they elaborate to:

def f : Nat → Nat :=
fun x => f._mutual (PSum.inl x)

There is this magical _mutual declaration which if you print it is quite huge and among other things requires WellFounded recursion and the corresponding instances for well founded relation etc.

So I would imagine you need at least parts of Init.WF and maybe also Init.WFTactics

[Henrik Böving]

(Which as you can see in doc-gen adds up to a whole lot of files because these already make use of quite a few imports)

[Arthur Paulino]

Alright, thanks!!
I will try another route then :sweat_smile:

[Henrik Böving]

I don't really think you can avoid well founded recursion here though, mutual just always seems to involve using well founded recursion to show termination so you won't be able to get around it. How much of it you need for your trivial examples is a completely different question though

[Arthur Paulino]

Yeah turns out my plan to end up with a very small environment was slipping through my fingers

[Henrik Böving]

Why exactly are you doing this btw?

[Arthur Paulino]

Long story short, we're trying to achieve some kind of "translation" of the Lean environment through metaprogramming. And I'm trying to test our method to translate mutual definitions

[Henrik Böving]

But if you were to just translate every declaration that is in a regular Environment right now things would just work out by themselves no? After all in a regular one all of this stuff is in place.

[Arthur Paulino]

Yeah but the environment is HUGE, so I was looking for a small and controlled environment

[Henrik Böving]

It definitley is yes, but e.g. before I started to try and obtain all of the equational lemmata for doc-gen (which requires running additional meta code with tactics for every def because they are calculated dynamically) doc-gen did actually run through an environment with a fully loaded mathlib quite quickly, pretty printing and analyzing every declaration and even now it is in the minute span at most so processing large environments in short time definitley is possible.

[Henrik Böving]

ah it is not a timing concern i see.

[Henrik Böving]

In that case maybe you could use the regular environment and write some code that recursively figures out what declarations a certain other declaration depends on so you can make a list of things for your mutual example and only translate all the declarations that are required for it?

[Arthur Paulino]

Yeah that's precisely what I'm trying right now

[John Burnham]

Arthur Paulino said:

Long story short, we're trying to achieve some kind of "translation" of the Lean environment through metaprogramming. And I'm trying to test our method to translate mutual definitions

A slightly longer version of the story is that we're trying to transform a Lean.Environment which is a map keyed on names, to a map keyed on cryptographic hashes of a name-irrelevant representation of the constants (vaguely similar to the hashing of https://www.unison-lang.org/). This lets us content-address any constant in a way that bypasses the hierarchical namespace. So

def id1 (A : Type) (x: A) : A := x
def id2 (B : Type) (y: B) : B := y

which are identical except for names, would hash to the same anonymous constant.

Anyway, to do this for mutual blocks is complicated (since you can't hash a cyclic reference graph in the same way you would an acyclic one), so we're trying to create some simple test cases to try our solution against

[Henrik Böving]

A this is a thing I've been wondering for a while: Why exactly is this desirable? :D

[Henrik Böving]

I get that it has a certain "technical beauty" appeal but i never understood why people actually want this.

[John Burnham]

Well, there are a lot of potential benefits to content addressing (like for build systems etc). But the concrete use-case our Yatima project (https://github.com/yatima-inc/yatima-lang/wiki) needs this for is that we're compiling Lean to the Lurk language for recursive zkSNARKs (https://github.com/lurk-lang), so that we can have lightweight cryptographic certificates that myProof : myTheorem validly checks (which can be verified in constant time without re-running a kernel)

Having nameless content-addressing allows us to compose any such certificate of proof1 : Theorem1 with any other certificate ofproof2 : Theorem2 irrespective of their use of the hierarchical namespace (like if they rely on two different constants both with the same name). This greatly improves certificate generation performance

[John Burnham]

I know there have been threads around Unison-style content-addressing for Lean (or lake) here in the past, and totally open to generalizing Yatima's content-addressing schema if that's of interest. But we're implementing this for a very domain-specific reason, which may have different constraints.

One thing though is that our content-addressing uses https://ipld.io/, which will let you composably share Lean constants and environments over IPFS (https://ipfs.io/), which is kinda neat

[Mac]

Henrik Böving said:

A this is a thing I've been wondering for a while: Why exactly is this desirable? :D

Outside of a concrete use cases like John mentioned there are two other notable general advantages: it eliminates code bloat caused by cross-package code duplication and it allows for easy, transparent aliasing of definitions (ie.g., nat, Nat, natural, Natural can all resolve to the same thing). The later feature is general to any language that decouples names from unit identifiers .