Zulip Chat Archive
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: Dec 20 2023 at 11:08 UTC