Dependent inductive parameter

Stream: Is there code for X?

[Ka Wing Li]

I am looking for a way to represent the following Rocq code in Lean4.

Local Open Scope positive_scope.

Local Notation "P ~ 0" := (λ p, P p~0) : function_scope.
Local Notation "P ~ 1" := (λ p, P p~1) : function_scope.

Inductive gmap_dep_ne (A : Type) (P : positive → Prop) :=
  | GNode001 : gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode010 : P 1 → A → gmap_dep_ne A P
  | GNode011 : P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode100 : gmap_dep_ne A P~0 → gmap_dep_ne A P
  | GNode101 : gmap_dep_ne A P~0 → gmap_dep_ne A P~1 → gmap_dep_ne A P
  | GNode110 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P
  | GNode111 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P.

Variant gmap_dep (A : Type) (P : positive → Prop) :=
  | GEmpty : gmap_dep A P
  | GNodes : gmap_dep_ne A P → gmap_dep A P.

[Ka Wing Li]

I tried the following

import Mathlib

postfix:arg (priority := high) "~0" => fun P p => P (PosNum.bit0 p)
postfix:arg (priority := high) "~1" => fun P p => P (PosNum.bit1 p)

inductive gmap_dep_ne (A : Type) (P : PosNum → Prop) : Type where
| GNode001 : gmap_dep_ne A P~1 → gmap_dep_ne A P
| GNode010 : P 1 → A → gmap_dep_ne A P
| GNode011 : P 1 → A → gmap_dep_ne A (P~1) → gmap_dep_ne A P
| GNode100 : gmap_dep_ne A P~0 → gmap_dep_ne A P
| GNode101 : gmap_dep_ne A P~0 → gmap_dep_ne A P~1 → gmap_dep_ne A P
| GNode110 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P
| GNode111 : gmap_dep_ne A P~0 → P 1 → A → gmap_dep_ne A P~1 → gmap_dep_ne A P

inductive gmap_dep (A : Type) (P : PosNum → Prop) where
| GEmpty : gmap_dep A P
| GNodes : gmap_dep_ne A P → gmap_dep A P

[Ka Wing Li]

Yet get some cryptic error

Mismatched inductive type parameter in
  gmap_dep_ne A ((fun P p ↦ P p.bit1) P)
The provided argument
  (fun P p ↦ P p.bit1) P
is not definitionally equal to the expected parameter
  P

[Aaron Liu]

it works when you make it

inductive gmap_dep_ne (A : Type) : (P : PosNum → Prop) → Type where

[Ka Wing Li]

I tried that, but encounter problem when writing a recursive function traversing the gmap.

[Aaron Liu]

can you show the problem

[Ka Wing Li]

Yep, I am extracting the code of the problem

[Ka Wing Li]

I am not sure if this is okay

instance [DecidableEq A] : (∀ i (x y : P i), x = y) → DecidableEq (gmap_dep_ne A P) := by
  unfold DecidableEq
  intros t₁ t₂
  let rec go (t₁ t₂ : gmap_dep_ne A P) : Decidable (t₁ = t₂) :=
  match t₁, t₂ with
  | .GNode001 r1, .GNode001 r2 => if (go r1 r2) then isTrue _ else isFalse _
  | .GNode010 _ x1, .GNode010 _ x2 => sorry
  | .GNode011 _ x1 r1, .GNode011 _ x2 r2 => sorry
  | .GNode100 l1, .GNode100 l2 => sorry
  | .GNode101 l1 r1, .GNode101 l2 r2 => sorry
  | .GNode110 l1 _ x1, .GNode110 l2 _ x2 => sorry
  | .GNode111 l1 _ x1 r1, .GNode111 l2 _ x2 r2 => sorry
  | _, _ => isFalse _

[Ka Wing Li]

error at (go r1 r2)

[Ka Wing Li]

Application type mismatch: The argument
  r1
has type
  gmap_dep_ne A ((fun P p ↦ P p.bit1) P)
but is expected to have type
  gmap_dep_ne A P
in the application
  go r1

[Aaron Liu]

(∀ i (x y : P i), x = y) is weird

[Aaron Liu]

I can fill it in with fun _ _ _ => rfl

[Ka Wing Li]

It is from Rocq (∀ i, ProofIrrel (P i)), probably should not be used here.

[Aaron Liu]

Ka Wing Li said:

Application type mismatch: The argument
  r1
has type
  gmap_dep_ne A ((fun P p ↦ P p.bit1) P)
but is expected to have type
  gmap_dep_ne A P
in the application
  go r1

isn't go just the original function again

[Aaron Liu]

if you give the instance a name you can call it recursively

[Ka Wing Li]

what do you mean?

[Aaron Liu]

instance decEq [DecidableEq A] : DecidableEq (gmap_dep_ne A P) := fun t₁ t₂ =>

[Aaron Liu]

and then you call decEq recursively

[Ka Wing Li]

You mean the following?

instance dec [DecidableEq A] : DecidableEq (gmap_dep_ne A P) :=
  fun t₁ t₂ ↦
  match t₁, t₂ with
  | .GNode001 r1, .GNode001 r2 => if (dec r1 r2).decide then isTrue (by sorry) else isFalse (by sorry)
  | _, _ => isFalse (by sorry)

[Ka Wing Li]

let me try

[Ka Wing Li]

It's working! Thanks.

[Ka Wing Li]

Sometimes helper functions cause weird problems and inlining works.

[Ka Wing Li]

That's another story.

[Aaron Liu]

by the way you can deriving DecidableEq for your gmap_dep_ne

[Ka Wing Li]

... why I am doing this

[Ka Wing Li]

Excuse me, another similar question:

def GNode (ml : gmap_dep A P~0) (mx : Option (P 1 × A)) (mr : gmap_dep A P~1) : gmap_dep A P :=
  match ml, mx, mr with
  | .GNodes l, some (p, x), .GNodes r => .GNodes (.GNode111 l p x r)
  | _, _, _ => sorry

I got problem for P 1 in type.

Type mismatch
  P 1
has type
  Prop
of sort `Type` but is expected to have type
  Type ?u.27678
of sort `Type (?u.27678 + 1)`

[Ka Wing Li]

Tried to change P 1 to Prop or Type will result in p being P 1 instead of others.

[Aaron Liu]

you can make it (mx : Option (P 1 ×' A))

[Ka Wing Li]

? What’s that?

[Aaron Liu]

docs#PProd

[Ka Wing Li]

Ahh, interesting

[Aaron Liu]

and then the pattern will be | .GNodes l, some ⟨p, x⟩, .GNodes r => .GNodes (.GNode111 l p x r), with the angle brackets ⟨⟩ instead of parentheses ()

[Ka Wing Li]

?!

[Aaron Liu]

the (a, b) notation gives you Prod.mk a b, so it's specific to docs#Prod

[Aaron Liu]

so if you use docs#PProd that won't work

[Aaron Liu]

instead you need to do PProd.mk a b explicitly, or you can use the anonymous constructor notation ⟨a, b⟩ which works on any inductive type with only one constructor

[Ka Wing Li]

Angle bracket is building record, right?

[Ka Wing Li]

Okay, that make sense now

[Ka Wing Li]

One day I’m going to understand the universe in Lean

[Ka Wing Li]

I need some doc about the similarities and differences of universe in lean and rocq

[Ka Wing Li]

Thanks for the help btw!