IR check failed

Stream: lean4

[Henrik Böving]

I broke something again \o/, #mwe

abbrev shrinkFn (α : Type u) [sz : SizeOf α] := (x : α) → List { y : α // sz.sizeOf y < sz.sizeOf x }

class Sampleable (α : Type u) where
  [wf : SizeOf α]
  shrink : @shrinkFn α wf := λ _ => []

attribute [instance] Sampleable.wf

def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := λ ⟨fst, snd⟩ => []

instance [Sampleable α] [Sampleable β] : Sampleable (Prod α β) where
  shrink := Prod.shrink Sampleable.shrink Sampleable.shrink

error: IR check failed at 'instSampleableProd._rarg', error: unknown declaration 'Prod._sizeOf_inst'

but Prod._sizeOf_inst is very much a thing, version is latest nightly

[Leonardo de Moura]

We do not generate code for SizeOf instances, and we will not change that in the near future. We only use them in proofs to justify termination.
If you are building more infrastructure to justify termination. You can add noncomputable to your instance.

[Henrik Böving]

I see...but why exactly does it even try to generate executable code for sizeOf here? I didn't call it anywhere did I?

[Leonardo de Moura]

Your Sampleable depends on SizeOf. Try the following, and you will find the sizeOf instance there.

noncomputable instance ex [Sampleable α] [Sampleable β] : Sampleable (Prod α β) where
  shrink := Prod.shrink Sampleable.shrink Sampleable.shrink

set_option pp.explicit true
#print ex

[Henrik Böving]

Ah indeed there it is, I see, notabug then^^

[Notification Bot]

Henrik Böving has marked this topic as resolved.

[Notification Bot]

Henrik Böving has marked this topic as unresolved.

[Henrik Böving]

While I got this Sampleable code here, I did define Prod.shrink to be:

def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := λ ⟨fst, snd⟩ =>
  let shrink1 := shrA fst |>.map $ λ ⟨x, h⟩ => ⟨Prod.mk x snd, (by
    simp only [SizeOf.sizeOf, Prod._sizeOf_1]
    rw [Nat.add_assoc, Nat.add_assoc]
    apply Nat.add_lt_add_left
    apply Nat.add_lt_add_right
    exact h
  )⟩
  let shrink2 := shrB snd |>.map $ λ ⟨x, h⟩ => ⟨Prod.mk fst x, (by
    simp only [SizeOf.sizeOf, Prod._sizeOf_1]
    rw [Nat.add_assoc, Nat.add_assoc]
    apply Nat.add_lt_add_left
    apply Nat.add_lt_add_left
    exact h
  )⟩
  shrink1 ++ shrink2

And I basically have two issues with this, the first being that I'm mentioning this Prod._sizeOf_1 explicitly but its an autogenerated name so I should probably do something different? And the second is the way I'm rewriting here with applying associativity, then canceling the 1, then canceling the other part, that feels very manual, do we have automation for this type of stuff yet?

[Simon Hudon]

Making most Sampleable instances noncomputable is going to throw a wrench in the plan of using it to generate test cases for Lean code. Changing the class declaration to this should get around that issue:

class Sampleable (α : Type u) [wf : SizeOf α] where
  shrink : @shrinkFn α wf := λ _ => []

[Henrik Böving]

Thaaat will in turn mess up Sampleable.lift quite a lot though since that one relies on explicit specification of this parameter....

[Henrik Böving]

I guess I'll get it to work somehow^^

[Simon Hudon]

You're going to need to give it type:

def sampleable.lift (α : Type u) {β : Type u} [sizeof α] [sizeof β] [sampleable α] (f : α → β) (g : β → α)
  (h : ∀ (a : α), sizeof (g (f a)) ≤ sizeof a) : sampleable β :=

and it won't be producing its own definition of sizeof β

[Leonardo de Moura]

@Henrik Böving Your example above helped me to fix problems with the arith simplifier. I pushed some fixes, and you can now write the example above as follows

abbrev shrinkFn (α : Type u) [sz : SizeOf α] := (x : α) → List { y : α // sz.sizeOf y < sz.sizeOf x }

class Sampleable (α : Type u) [SizeOf α] where
  shrink : shrinkFn α := fun _ => []

def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := fun (fst, snd) =>
  let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨(x, snd), by simp_all_arith⟩
  let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨(fst, x), by simp_all_arith⟩
  shrink1 ++ shrink2

[Henrik Böving]

Simon Hudon said:

You're going to need to give it type:

def sampleable.lift (α : Type u) {β : Type u} [sizeof α] [sizeof β] [sampleable α] (f : α → β) (g : β → α)
  (h : ∀ (a : α), sizeof (g (f a)) ≤ sizeof a) : sampleable β :=

and it won't be producing its own definition of sizeof β

Yeah I did that already and sorried out the correctness proof, it will cause stuff like this FIn.sampleable instance to break due to the same SizeOf noncomputable issue again :(

[Henrik Böving]

Namely like this:

abbrev shrinkFn (α : Type u) [sz : SizeOf α] := (x : α) → List { y : α // sz.sizeOf y < sz.sizeOf x }

class Sampleable (α : Type u) [wf : SizeOf α] where
  shrink : @shrinkFn α wf := λ _ => []

def Nat.shrink (n : Nat) : List { y : Nat // sizeOf y < sizeOf n } :=
  if h : 0 < n then
    let m := n/2
    have h : m < n := by sorry
    let rest := shrink m
    ⟨m, h⟩ :: rest.map (λ x => {x with property := Nat.lt_trans x.property h})
  else
    []

instance Nat.sampleable : Sampleable Nat where
  shrink := Nat.shrink

def Sampleable.lift (α : Type u) {β : Type u} [SizeOf α] [SizeOf β] [Sampleable α] (f : α → β) (g : β → α) (h : ∀ a , sizeOf (g (f a)) ≤ sizeOf a) : Sampleable β :=
  {
    shrink := λ x =>
      have : ∀ (a : α), sizeOf a < sizeOf (g x) → sizeOf (f a) < sizeOf x := by
        intro a h
        sorry
      shrink (g x) |>.map λ ⟨p, h⟩ => ⟨f p, sorry⟩
  }

instance Fin.sampleable {n : Nat} : Sampleable (Fin (n.succ)) :=
  Sampleable.lift Nat Fin.ofNat Fin.val (λ a => Nat.mod_le _ _)

[Henrik Böving]

I have some more IR checks failed!

abbrev TupleNTyp : Nat → Type 1
  | 0 => Type
  | n + 1 => Type → (TupleNTyp n)

abbrev TupleN : (n : Fin 1) → (TupleNTyp n.val)
  | 0 => Unit
--  | 1 => Solo
--  | 2 => Prod
--  | 3 => fun a b c => Prod a (Prod b c)

IR check failed at 'TupleN', error: unexpected type '◾', object expected

1. Quite the confusing message, the fuck is that square?
2. I feel like this should work?

[Mario Carneiro]

the square is the "neutral object" aka "erased thing" which takes the place of universes and propositions (types that are erased)

[Mario Carneiro]

It sounds like lean is having trouble deciding whether TupleNTyp n.val should be erased or not