extensional finite map inside inductive definition

Stream: Is there code for X?

[Ka Wing Li]

Is there any extensional finite map that I can use in an inductive definition?

[Ka Wing Li]

i.e. gmap from Rocq stdpp.

[Jakub Nowak]

Is Std.ExtTreeMap or Std.ExtHashMap what you need?
There's Std.ExtTreeMap.ext_getElem? and analogous for hash map.

[Ka Wing Li]

Let me forward the message here.
Ka Wing Li said:

I tried the following but get error "application type mismatch"

inductive tm : Type where
| nat : ℕ → tm
| var : String → tm
| abs : String → tm → tm
| app : tm → tm → tm

inductive vl : Type where
| nat : ℕ → vl
| abs : Std.ExtTreeMap String vl → tm → vl

[Ka Wing Li]

It seems Ext(D)TreeMap and Ext(D)HashMap cannot be used inside inductive definition.

[Jakub Nowak]

Std.DTreeMap.Raw

[Jakub Nowak]

Yes, they cannot, you need Raw.

[Ka Wing Li]

But it is not extensional.

[Jakub Nowak]

Hm, you're right.

[Jakub Nowak]

It would be much easier if you included what you already know in your question. :)

[Ka Wing Li]

See stdpp gmap desciption:

• It guarantees logarithmic-time lookup and partial_alter, and linear-time merge. It has a low constant factor for computation in Coq compared to other versions (see the Appel and Leroy paper for benchmarks).
• It satisfies extensional equality (∀ i, m1 !! i = m2 !! i) → m1 = m2.
• It can be used in nested recursive definitions, e.g., Inductive test := Test : gmap test → test. This is possible because we do not use a Sigma type to ensure canonical representations (a Sigma type would break Coq's strict positivity check).

[Ka Wing Li]

It would be much easier if you included what you already know in your question. :)

Sorry, it's my fault that I thought mentioning both "extensional" and "inductive definitions", as well as ExtDTreeMap in another channel, is sufficient.

[Jakub Nowak]

Ka Wing Li said:

It would be much easier if you included what you already know in your question. :)

Sorry, it's my fault that I thought mentioning both "extensional" and "inductive definitions", as well as ExtDTreeMap in another channel, is sufficient.

I think it's ok, but I haven't seen your other message in another topic. And it's my bad for not noticing that the Raw version in not extensional.

[Jakub Nowak]

Unrelated to the question, but HOAS might of interest to you. It lets you represent dsl abstraction using lean's native abstraction. https://lean-lang.org/examples/1900-1-1-parametric-higherorder-abstract-syntax/

[Jakub Nowak]

Do you need both extensionability and logarithmic operations though? You can use a type that is not extensionable for programming, and the extensionable model of it in proofs. Though, even without that requirement I couldn't find an implementation of key-value store that is both extensionable and can be used in inductives.

[Jakub Nowak]

You could write the below code. But that makes vl type harder to use and it's overly complicated. I think that we should have extensional key-value store usable in inductives. I don't think it's necessary for it to have logarithmic operations, but it would be useful to have.

import Mathlib

inductive tm : Type where
| nat : ℕ → tm
| var : String → tm
| abs : String → tm → tm
| app : tm → tm → tm

inductive vl' : Type where
| nat : ℕ → vl'
| abs : Std.TreeMap.Raw String vl' → tm → vl'

def vl'.isSetoid : Setoid vl' where
  r
  | abs ctx t, abs ctx' t' => ctx.Equiv ctx' ∧ t = t'
  | v, v' => v = v'

  iseqv.refl _ := by split <;> simp
  iseqv.symm h := by
    split at h
    · rw [Std.TreeMap.Raw.Equiv.comm]
      simp [h]
    · simp_all
  iseqv.trans {x y z} h₁ h₂ := sorry

def vl : Type := Quotient vl'.isSetoid

[Ka Wing Li]

Interesting, stdpp tries their best to avoid the need of setoid. I faced a little difficulty in proving transitivity, but figured it out anyway.

[Ka Wing Li]

logarithmic is preferable if possible as it was used for functional big step as in CakeML. Yet for proving metatheory it is still ok.

[Ka Wing Li]

Being extensional is beneficial for rewrite, like idempotent of insert and commuting fmap and insert.

lemma tmp {α β} {cmp : α → α → Ordering} [LT α] [LE α] [Std.LawfulCmp cmp] :
  ∀ (m : Std.ExtTreeMap α β cmp) (f : α → β → β) k v,
  (m |>.insert k v |>.map f) = (m |>.map f |>.insert k (f k v)) := by
  grind

[Jakub Nowak]

Non-logarithmic should be I think not too hard by using AList with additional assumption that the list is sorted.