## Stream: general

### Topic: Issue translating Agda to Lean. Definitional equality?

#### 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


#### 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


#### 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.... :)

#### 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