Trouble with a String Matching Function

Stream: new members

[Colin Jones ⚛️]

How do I get this to work?

def mwe := { s : String // s.length == 2 && s.dropWhile "AB".toList.contains == ""}

def AA : mwe := ⟨"AA", by rfl⟩
def AB : mwe := ⟨"AB", by rfl⟩
def BA : mwe := ⟨"BA", by rfl⟩
def BB : mwe := ⟨"BB", by rfl⟩

def matcher (s : mwe) :=
  match s with
  | AA => "1"
  | AB => "2"
#eval matcher AA
#eval matcher AB

I want the s variable to match with the AB I defined earlier not with the type itself.

[Colin Jones ⚛️]

I want #eval matcher AB to output 2 not 1.

[Daniel Weber]

Is

def matcher (s : mwe) :=
  match s with
  | ⟨"AA", _⟩ => "1"
  | ⟨"AB", _⟩ => "2"
  | _ => ""
#eval matcher AA
#eval matcher AB

good, or are you looking for something else?

[Tomas Skrivan]

I think adding @[match_pattern] to definitions of AA and AB will make your original code work.

[Colin Jones ⚛️]

Sorry for responding so late. Thank you both for replying. For the first one, is there a way I can prove that there are no other mwes other than "AB", "AA", "BB", "BA" so I don't have to include the miscellaneous case | _ => ""? Something like this:

def matcher (s : mwe) :=
  match s with
  | ⟨"AA", _⟩ => "1"
  | ⟨"AB", _⟩ => "2"
  | ⟨"BB", _⟩ => "3"
  | ⟨"BA", _⟩ => "4"

Also @[match_pattern] does work too:

@[match_pattern]
def AA : mwe := ⟨"AA", by rfl⟩
@[match_pattern]
def AB : mwe := ⟨"AB", by rfl⟩
@[match_pattern]
def BA : mwe := ⟨"BA", by rfl⟩
@[match_pattern]
def BB : mwe := ⟨"BB", by rfl⟩

def matcher' (s : mwe) :=
  match s with
  | AA => "1"
  | AB => "2"
  | _ => ""

[Kevin Buzzard]

You can prove there are no other mwes but then you'd still have to include what you call the miscellaneous case, you would just insert your proof there to show that it doesn't need to be dealt with.

[Colin Jones ⚛️]

Would it be possible to prove that AA does not equal AB e.g.

def mwe := { s : String // s.length == 2 && s.dropWhile "AB".toList.contains == ""}

@[match_pattern]
def AA : mwe := ⟨"AA", by rfl⟩
@[match_pattern]
def AB : mwe := ⟨"AB", by rfl⟩

example : AA ≠ AB := by
  simp only [ne_eq, AB, AA, String.toList, ↓Char.isValue]
  sorry

[Colin Jones ⚛️]

Would proving this even be possible? I can't separate the string part from the proof part

[Daniel Weber]

You can do this:

example : AA ≠ AB := by
  intro h
  simpa [AA, AB] using congrArg Subtype.val h

[Colin Jones ⚛️]

Thank you I would've spend decades trying to find this. Speaking of how did you find that solution so fast?

[Daniel Weber]

Using Mathlib tactics a simpler solution (which I also found first) is:

import Mathlib.Tactic.ApplyFun

example : AA ≠ AB := by
  apply_fun Subtype.val
  simp [AA, AB]

which essentially says "these values aren't equal because their Subtype.val is different" and then simp is capable of showing that.
Now that apply_fun can be replaced by "assume AA = AB, then by docs#congrArg we have AA.val = AB.val"

[Colin Jones ⚛️]

Thank you

[Daniel Weber]

This can also be written as

example : AA ≠ AB := by
  apply mt (congrArg Subtype.val)
  simp [AA, AB]

to more directly replicate apply_fun

[Notification Bot]

10 messages were moved from this topic to #new members > Faster Way to prove all possible elements in a set by Eric Wieser.