Zulip Chat Archive

Stream: new members

Topic: Help trying to prove that something is inside a Map.

Felipe GS (Jun 12 2022 at 21:46):

I'm trying to prove that some thing is inside a map. But I'm having problems with the pattern matching of Prop...

inductive MapImpl : Type u  Type v  Type (max u v + 1)
    | empty : MapImpl α β
    | node  : MapImpl α β  α  β  MapImpl α β  MapImpl α β
    deriving Repr

 inductive MapImpl.Member [LT α]: α  (MapImpl α β) -> Prop
    | here    : Member k (MapImpl.node l k v r)
    | inLeft  : Member k l  (k < c)  Member k (MapImpl.node l c v r)
    | inRight : Member k r  (k > c)  Member k (MapImpl.node l c v r)

def MapImpl.find [DecidableEq α] [LT α] [DecidableRel (@LT.lt α _)] [Ord α] : (s: MapImpl α β)  (k: α)  MapImpl.Member k s  β
    | MapImpl.empty,        key, proof => nomatch proof
    | MapImpl.node l k v r, key, proof =>
      match (decEq k key) with
      | Decidable.isTrue  _ => v
      | Decidable.isFalse _ =>
          dite (LT.lt key k) sorry sorry

Last updated: Dec 20 2023 at 11:08 UTC