matching on Finset

Stream: new members

[Simon Daniel]

Hi, im wondering on what is the most elegant way to match on a finset. what i try:

def f: ({"a", "b"}:Finset String) -> Nat
| ⟨"a", _⟩ => 1
| ⟨"b", _⟩ => 2
| _ => sorry --maybe solve by contradiction somehow?

can Lean figure out the dead branch here itself? What i rather would write is

def f': ({"a", "b"}:Finset String) -> Nat
| "a" => 1
| "b" => 2

[Eric Wieser]

Note it works fine for integers:

def f: ({11, 12}:Finset Nat) -> Nat
| ⟨11, _⟩ => 1
| ⟨12, _⟩ => 2

I think the problem is that string decidable equality is not reducible

[Aaron Liu]

It's not running any decidable equality procedure, but using dependent elimination to eliminate the remaining cases

[Aaron Liu]

I think the problem is docs#Nat.isValidChar, which has these huge numbers in it.

[Aaron Liu]

This works, but it takes a while

import Mathlib

example : ({'a', 'b'} : Finset Char) → Nat
| ⟨Char.mk (UInt32.ofBitVec 97) _, _⟩ => 1
| ⟨Char.mk (UInt32.ofBitVec 98) _, _⟩ => 2

[Aaron Liu]

It's also very bloated

import Mathlib

/-
[result]
def f (x_1 : u32) : obj :=
  let x_2 : obj := UInt32.toNat x_1;
  let x_3 : obj := 0;
  let x_4 : obj := 1;
  let x_5 : obj := Nat.sub x_2 x_4;
  dec x_2;
  let x_6 : obj := Nat.sub x_5 x_4;
  dec x_5;
  let x_7 : obj := Nat.sub x_6 x_4;
  dec x_6;
  let x_8 : obj := Nat.sub x_7 x_4;
  dec x_7;
  let x_9 : obj := Nat.sub x_8 x_4;
  dec x_8;
  let x_10 : obj := Nat.sub x_9 x_4;
  dec x_9;
  let x_11 : obj := Nat.sub x_10 x_4;
  dec x_10;
  let x_12 : obj := Nat.sub x_11 x_4;
  dec x_11;
  let x_13 : obj := Nat.sub x_12 x_4;
  dec x_12;
  let x_14 : obj := Nat.sub x_13 x_4;
  dec x_13;
  let x_15 : obj := Nat.sub x_14 x_4;
  dec x_14;
  let x_16 : obj := Nat.sub x_15 x_4;
  dec x_15;
  let x_17 : obj := Nat.sub x_16 x_4;
  dec x_16;
  let x_18 : obj := Nat.sub x_17 x_4;
  dec x_17;
  let x_19 : obj := Nat.sub x_18 x_4;
  dec x_18;
  let x_20 : obj := Nat.sub x_19 x_4;
  dec x_19;
  let x_21 : obj := Nat.sub x_20 x_4;
  dec x_20;
  let x_22 : obj := Nat.sub x_21 x_4;
  dec x_21;
  let x_23 : obj := Nat.sub x_22 x_4;
  dec x_22;
  let x_24 : obj := Nat.sub x_23 x_4;
  dec x_23;
  let x_25 : obj := Nat.sub x_24 x_4;
  dec x_24;
  let x_26 : obj := Nat.sub x_25 x_4;
  dec x_25;
  let x_27 : obj := Nat.sub x_26 x_4;
  dec x_26;
  let x_28 : obj := Nat.sub x_27 x_4;
  dec x_27;
  let x_29 : obj := Nat.sub x_28 x_4;
  dec x_28;
  let x_30 : obj := Nat.sub x_29 x_4;
  dec x_29;
  let x_31 : obj := Nat.sub x_30 x_4;
  dec x_30;
  let x_32 : obj := Nat.sub x_31 x_4;
  dec x_31;
  let x_33 : obj := Nat.sub x_32 x_4;
  dec x_32;
  let x_34 : obj := Nat.sub x_33 x_4;
  dec x_33;
  let x_35 : obj := Nat.sub x_34 x_4;
  dec x_34;
  let x_36 : obj := Nat.sub x_35 x_4;
  dec x_35;
  let x_37 : obj := Nat.sub x_36 x_4;
  dec x_36;
  let x_38 : obj := Nat.sub x_37 x_4;
  dec x_37;
  let x_39 : obj := Nat.sub x_38 x_4;
  dec x_38;
  let x_40 : obj := Nat.sub x_39 x_4;
  dec x_39;
  let x_41 : obj := Nat.sub x_40 x_4;
  dec x_40;
  let x_42 : obj := Nat.sub x_41 x_4;
  dec x_41;
  let x_43 : obj := Nat.sub x_42 x_4;
  dec x_42;
  let x_44 : obj := Nat.sub x_43 x_4;
  dec x_43;
  let x_45 : obj := Nat.sub x_44 x_4;
  dec x_44;
  let x_46 : obj := Nat.sub x_45 x_4;
  dec x_45;
  let x_47 : obj := Nat.sub x_46 x_4;
  dec x_46;
  let x_48 : obj := Nat.sub x_47 x_4;
  dec x_47;
  let x_49 : obj := Nat.sub x_48 x_4;
  dec x_48;
  let x_50 : obj := Nat.sub x_49 x_4;
  dec x_49;
  let x_51 : obj := Nat.sub x_50 x_4;
  dec x_50;
  let x_52 : obj := Nat.sub x_51 x_4;
  dec x_51;
  let x_53 : obj := Nat.sub x_52 x_4;
  dec x_52;
  let x_54 : obj := Nat.sub x_53 x_4;
  dec x_53;
  let x_55 : obj := Nat.sub x_54 x_4;
  dec x_54;
  let x_56 : obj := Nat.sub x_55 x_4;
  dec x_55;
  let x_57 : obj := Nat.sub x_56 x_4;
  dec x_56;
  let x_58 : obj := Nat.sub x_57 x_4;
  dec x_57;
  let x_59 : obj := Nat.sub x_58 x_4;
  dec x_58;
  let x_60 : obj := Nat.sub x_59 x_4;
  dec x_59;
  let x_61 : obj := Nat.sub x_60 x_4;
  dec x_60;
  let x_62 : obj := Nat.sub x_61 x_4;
  dec x_61;
  let x_63 : obj := Nat.sub x_62 x_4;
  dec x_62;
  let x_64 : obj := Nat.sub x_63 x_4;
  dec x_63;
  let x_65 : obj := Nat.sub x_64 x_4;
  dec x_64;
  let x_66 : obj := Nat.sub x_65 x_4;
  dec x_65;
  let x_67 : obj := Nat.sub x_66 x_4;
  dec x_66;
  let x_68 : obj := Nat.sub x_67 x_4;
  dec x_67;
  let x_69 : obj := Nat.sub x_68 x_4;
  dec x_68;
  let x_70 : obj := Nat.sub x_69 x_4;
  dec x_69;
  let x_71 : obj := Nat.sub x_70 x_4;
  dec x_70;
  let x_72 : obj := Nat.sub x_71 x_4;
  dec x_71;
  let x_73 : obj := Nat.sub x_72 x_4;
  dec x_72;
  let x_74 : obj := Nat.sub x_73 x_4;
  dec x_73;
  let x_75 : obj := Nat.sub x_74 x_4;
  dec x_74;
  let x_76 : obj := Nat.sub x_75 x_4;
  dec x_75;
  let x_77 : obj := Nat.sub x_76 x_4;
  dec x_76;
  let x_78 : obj := Nat.sub x_77 x_4;
  dec x_77;
  let x_79 : obj := Nat.sub x_78 x_4;
  dec x_78;
  let x_80 : obj := Nat.sub x_79 x_4;
  dec x_79;
  let x_81 : obj := Nat.sub x_80 x_4;
  dec x_80;
  let x_82 : obj := Nat.sub x_81 x_4;
  dec x_81;
  let x_83 : obj := Nat.sub x_82 x_4;
  dec x_82;
  let x_84 : obj := Nat.sub x_83 x_4;
  dec x_83;
  let x_85 : obj := Nat.sub x_84 x_4;
  dec x_84;
  let x_86 : obj := Nat.sub x_85 x_4;
  dec x_85;
  let x_87 : obj := Nat.sub x_86 x_4;
  dec x_86;
  let x_88 : obj := Nat.sub x_87 x_4;
  dec x_87;
  let x_89 : obj := Nat.sub x_88 x_4;
  dec x_88;
  let x_90 : obj := Nat.sub x_89 x_4;
  dec x_89;
  let x_91 : obj := Nat.sub x_90 x_4;
  dec x_90;
  let x_92 : obj := Nat.sub x_91 x_4;
  dec x_91;
  let x_93 : obj := Nat.sub x_92 x_4;
  dec x_92;
  let x_94 : obj := Nat.sub x_93 x_4;
  dec x_93;
  let x_95 : obj := Nat.sub x_94 x_4;
  dec x_94;
  let x_96 : obj := Nat.sub x_95 x_4;
  dec x_95;
  let x_97 : obj := Nat.sub x_96 x_4;
  dec x_96;
  let x_98 : obj := Nat.sub x_97 x_4;
  dec x_97;
  let x_99 : obj := Nat.sub x_98 x_4;
  dec x_98;
  let x_100 : obj := Nat.sub x_99 x_4;
  dec x_99;
  let x_101 : obj := Nat.sub x_100 x_4;
  dec x_100;
  let x_102 : u8 := Nat.decEq x_101 x_3;
  dec x_101;
  case x_102 : u8 of
  Bool.false →
    let x_103 : obj := 2;
    ret x_103
  Bool.true →
    let x_104 : obj := 1;
    ret x_104
def f._boxed (x_1 : obj) : obj :=
  let x_2 : u32 := unbox x_1;
  dec x_1;
  let x_3 : obj := f x_2
-/
set_option trace.compiler.ir.result true in
def f : ({'a', 'b'} : Finset Char) → Nat
| ⟨Char.mk (UInt32.ofBitVec 97) _, _⟩ => 1
| ⟨Char.mk (UInt32.ofBitVec 98) _, _⟩ => 2

/-
function size: 365
matcher size: 2739221
-/
run_cmd do
  let f ← Lean.getConstInfo ``f
  let matcher ← Lean.getConstInfo ``f.match_1
  Lean.logInfo m!"function size: {f.value!.size}\nmatcher size: {matcher.value!.size}"

[Aaron Liu]

In contrast, this is not bloat:

import Mathlib

/-
[result]
def f (x_1 : u32) : obj :=
  let x_2 : u32 := 97;
  let x_3 : u8 := UInt32.decEq x_1 x_2;
  case x_3 : u8 of
  Bool.false →
    let x_4 : obj := 2;
    ret x_4
  Bool.true →
    let x_5 : obj := 1;
    ret x_5
def f._boxed (x_1 : obj) : obj :=
  let x_2 : u32 := unbox x_1;
  dec x_1;
  let x_3 : obj := f x_2;
  ret x_3
-/
set_option trace.compiler.ir.result true in
def f (x : ({'a', 'b'} : Finset Char)) : Nat :=
  if ha : x = 'a' then 1
  else if hb : x = 'b' then 2
  else False.elim <| by
    fin_cases x <;> contradiction

/-
function size: 605
proof size: 43185
-/
run_cmd do
  let f ← Lean.getConstInfo ``f
  let prf ← Lean.getConstInfo ``f.proof_1
  Lean.logInfo m!"function size: {f.value!.size}\nproof size: {prf.value!.size}"

[Aaron Liu]

I imagine this works for Finset String as well

[Eric Wieser]

Aaron Liu said:

It's not running any decidable equality procedure, but using dependent elimination to eliminate the remaining cases

{a, b} invokes decidable equality of a and b to reduce to a constructor, so I think decidability is still to blame