Zulip Chat Archive

Stream: general

Topic: Issue translating Agda to Lean. Definitional equality?


view this post on Zulip SnowFox (Mar 16 2021 at 18:40):

Hello. I'm trying to translate categorical thinnings (aka order preserving embedings) from Agda to Lean. As used in Co-De-Bruijn indices. https://arxiv.org/abs/1807.04085
Just before posting this ... I thought surely mathlib has a generalization, which it does rel_embedding / order_embedding, and it seems the function I'm after is called trans.

I'm using Lean 4, though adapting this to Lean 3 resulted in "bad patterns" as I reuse k in each pattern. If Lean 4 supports this, it'd be worth a mention in the differences against Lean 3 in its manual!

Can someone help me fix the type error?

-- Equivalently (ks : List K) × BitVec ks.length → List K
inductive Thinning {K} : List K  List K  Prop
| empty                      : Thinning []     []
| skip k (ks : Thinning l r) : Thinning l      (k::r)
| keep k (ks : Thinning l r) : Thinning (k::l) (k::r)

namespace Thinning
  def comp {K} {a b c : List K} : Thinning a b  Thinning b c  Thinning a c
  | l, skip k r => skip k (comp l r)
  | skip k l, keep k r => skip k (comp l r)
  | keep k l, keep k r => keep k (comp l r)
  | empty, empty => empty
end Thinning

-- CoDeBruijn.lean:11:7: error: type mismatch
--   skip k r
-- has type
--   Thinning b (k :: ?m.826)
-- but is expected to have type
--   Thinning b c

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 19:59):

You need to include a b c in the pattern

inductive Thinning {K} : List K  List K  Prop
| empty                      : Thinning []     []
| skip k (ks : Thinning l r) : Thinning l      (k::r)
| keep k (ks : Thinning l r) : Thinning (k::l) (k::r)

namespace Thinning
  def comp {K} : {a b c : List K}  Thinning a b  Thinning b c  Thinning a c
  | _, _, _, l, skip k r => skip k (comp l r)
  | _, _, _, skip k l, keep _ r => skip k (comp l r)
  | _, _, _, keep k l, keep _ r => keep k (comp l r)
  | _, _, _, empty, empty => empty
end Thinning

view this post on Zulip SnowFox (Mar 16 2021 at 20:07):

Ah! Thanks! I tried that and got lost with the lack of Pi/Π notation now... meant to figure that out. Okay, unexpected binder syntax position.... :)

view this post on Zulip Leonardo de Moura (Mar 31 2021 at 15:59):

@SnowFox We have recently added a feature to make this kind of definition more convenient to write. Lean will add the _s for you, and you can write your example as

inductive Thinning {K} : List K  List K  Prop
| empty                      : Thinning []     []
| skip k (ks : Thinning l r) : Thinning l      (k::r)
| keep k (ks : Thinning l r) : Thinning (k::l) (k::r)

namespace Thinning
  def comp {K} {a b c : List K} : Thinning a b  Thinning b c  Thinning a c
  | l, skip k r => skip k (comp l r)
  | skip k l, keep _ r => skip k (comp l r)
  | keep k l, keep _ r => keep k (comp l r)
  | empty, empty => empty
end Thinning

You need the nightly build.


Last updated: May 11 2021 at 14:11 UTC