lemma from match statement

Stream: general

[Scott Viteri]

Are there any lemmas that tie the matched variables to the particular case it was matched with?

I have a term constructor, and I am trying to define a function on it as follows:

inductive term : Type
| const : string → option sort → term
| app : term → term → term

notation `clause` := list (option term)
infixl ` • ` :20  := app

@[simp] def reduce_not_and_aux : term → clause
| (const "and" _ • t₀ • (const "and" _ • t₁ • t₂)) :=
    mkNot t₀ :: mkNot t₁ :: reduce_not_and_aux t₂
| (const "and" _ • t₀ • t₁)  := [mkNot t₀, mkNot t₁]
| t := [mkNot t]

However the equation compiler fails, and when I try to set_option for additional details, emacs crashes.
I believe that lean is not inferring that t₂ is smaller than the full term. I have constructed a 'term_size' function, and I am trying to prove that it decreases.

This brings me to the original question -- can the match statement give me a lemma about what it matched?
Specifically I would like to say that if the reduce_not_and_aux takes a term t, then t =(const "and" _ • t₀ • (const "and" _ • t₁ • t₂)) in the first case.

Thank You,
Scott

[Yakov Pechersky]

A simp attribute works only on lemmas (and theorems), as far as I know.

[Scott Viteri]

woops thx

[Scott Morrison]

No, @[simp] works on definitions too.

[Scott Morrison]

It means that simp will happily unfold the definition itself. In my experience it's rarely what you want, and it's better to write custom simp lemmas yourself in nearly every circumstance.

[Scott Morrison]

The attribute @[simps] is extremely useful when defining structures: it will automatically create @[simp] lemmas for each of the projections.

[Scott Viteri]

I appreciate the comments here, but I would still be interested in an answer to the original question if possible.

[Scott Viteri]

Nevermind!

[Mario Carneiro]

Hm, there seems to be a weird bug here:

constant sort : Type

inductive term : Type
| const : string → option sort → term
| app : term → term → term
open term

def reduce_not_and_aux : term → unit
| (app _ t) := reduce_not_and_aux t
| t := ()

If you replace constant sort : Type with def sort : Type := sorry it works, which suggests somehow the noncomputable marker is interfering with the equation compiler

[Mario Carneiro]

But even after fixing that, it seems the equation compiler still has an issue with the definition, which I assume is what you are seeing. The problem has to do with the way string matches are compiled. Here's an implementation that will work:

def sort : Type := sorry

inductive term : Type
| const : string → option sort → term
| app : term → term → term
open term

notation `clause` := list (option term)
infixl ` • ` :20  := app

def mkNot : term → term := sorry

def is_and : term → bool
| (const "and" _) := tt
| _ := ff

def reduce_not_and_aux : term → clause
| t@(A1 • t₀ • (A2 • t₁ • t₂)) :=
  if is_and A1 ∧ is_and A2 then
    mkNot t₀ :: mkNot t₁ :: reduce_not_and_aux t₂
  else [mkNot t]
| t@(A1 • t₀ • t₁) :=
  if is_and A1 then [mkNot t₀, mkNot t₁]
  else [mkNot t]
| t := [mkNot t]

[Mario Carneiro]

(it's about now that I wish lean had pattern guards)

[Mario Carneiro]

If you are doing meta code, then the original version will work fine:

meta def reduce_not_and_aux : term → clause
| (const "and" _ • t₀ • (const "and" _ • t₁ • t₂)) :=
  mkNot t₀ :: mkNot t₁ :: reduce_not_and_aux t₂
| (const "and" _ • t₀ • t₁) := [mkNot t₀, mkNot t₁]
| t := [mkNot t]

[Scott Viteri]

Thanks Mario!
I had written the full definitions using term.rec_on to unblock myself, but this is much nicer.

On a separate note, is there a way to pattern match using functions?
In other places I have definitions like

def reduce_iff_aux : term → nat → clause
| (const "iff" _ • t₀ • t₁) 0 := [mkNot t₀, t₁]
| (const "iff" _ • t₀ • t₁) 1 := [t₀, mkNot t₁]
| _           _ := [option.none]
 ```
But I would much rather define something like

def iff (t₁ t₂ : term) : term := const "iff" _ • t₁ • t₂
def reduce_iff_aux : term → nat → clause
| (iff • t₀ • t₁) 0 := [mkNot t₀, t₁]
| (iff • t₀ • t₁) 1 := [t₀, mkNot t₁]
| _ _ := [option.none]

[Reid Barton]

Try putting @[pattern] before def iff

[Scott Viteri]

that worked, thanks!

[Scott Viteri]

Investigating the cause of the string pattern match issue, I find that
#reduce (string.has_decidable_eq "hi" "hi")
yields

619:1: excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

[Scott Viteri]

The same statement with #eval works correctly.
Digging a bit deeper, I receive the same error with

#reduce (list.has_dec_eq "hi".data "hi".data)

[Scott Viteri]

(side note: why are the has_dec_eq statements named inconsistently?)

[Bryan Gin-ge Chen]

#reduce doesn't work well with strings, see e.g. this thread and this thread.

[Scott Viteri]

Ok, but then what is the reason that Mario's is_and function works?

def is_and : term → bool
| (const "and" _) := tt
| _ := ff

[Scott Viteri]

#reduce (is_and (const "and" boolsort))
works fine

[Reid Barton]

The kernel can see that "and" = "and" without doing much work

[Reid Barton]

in particular, without computing the entire normal form of "and"

[Scott Viteri]

so pattern matching uses the kernel to check string equality?

[Reid Barton]

#reduce uses the kernel to reduce things to normal form

[Reid Barton]

in this case, that thing is whatever the equation compiler turned is_and into, applied to its argument

[Scott Viteri]

is the issue with normal form on natural numbers that the normal form is written in unary representation or something?

[Reid Barton]

yes but it's worse than that: the proof that 'a' is a valid Unicode character is also encoded in unary

[Scott Viteri]

where does this notation come from?
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)

[Scott Viteri]

namely the hexadecimal

[Reid Barton]

I would presume it's built-in just like ordinary decimal numeric literals.

[Scott Viteri]

When I write #check 123 should I think of that as a unary nat?

[Reid Barton]

I would think of it as 123

[Scott Viteri]

Because it infers the type is nat

[Reid Barton]

the representation and whether you care what the representation is depends on the context

[Reid Barton]

the inferred type also depends on the context, but with no context it's indeed nat

[Scott Viteri]

oh really

[Scott Viteri]

so there is some code to do this context inference somewhere in the c++?

[Reid Barton]

Writing #check 2000000000000000 works fine, so obviously in this situation Lean did not build a unary representation of the number behind the scenes

[Scott Viteri]

haha right

[Scott Viteri]

It can't be so hard to rewrite char using hexadecimal nat explicitly written as an inductive datatype, no?

[Reid Barton]

It would be possible but there's no real application I can think of

[Reid Barton]

and it would complicate making #eval treat them efficiently

[Reid Barton]

for syntax trees you shouldn't really be using string in the first place--make an inductive type with the values you care about

[Scott Viteri]

In this context I want to simulate an open type

[Scott Viteri]

I'm adding smt theories dynamically

[Scott Viteri]

I really don't want support them all in one big inductive term/sort datastructure, and then edit any def that uses them upon each addition

[Scott Viteri]

Now I could replace string matching with nat here, but that will make things more difficult to read

[Reid Barton]

or use a type variable

[Reid Barton]

but I agree this is a bit more complicated

[Scott Viteri]

do you mean if I set the different sorts up as types?

[Scott Viteri]

and pattern match on which type

[Scott Viteri]

Actually I am unsure what you mean

[Reid Barton]

well, I'd have to think about it more but I'm pretty sure there is always a better option than string

[Scott Viteri]

fair enough

[Scott Viteri]

this is the kind of example that I am looking at

def sortof_aux : term → option sort
| (const str s) :=
  match str with
  | "bot" := boolsort
  | "not" := (arrow boolsort boolsort)
  | "or"  := (arrow boolsort (arrow boolsort boolsort))
  | "and"  := (arrow boolsort (arrow boolsort boolsort))
  | "implies"  := (arrow boolsort (arrow boolsort boolsort))
  | "xor"  := (arrow boolsort (arrow boolsort boolsort))
  | "iff"  := (arrow boolsort (arrow boolsort boolsort))
  | _      := s
  end
| (const str (option.some constructor) • t₁ • t₂) :=
  if str = "eq" then
    do s₁ ← sortof_aux t₁, s₂ ← sortof_aux t₂,
      if s₁ = s₂ then boolsort else option.none
  else option.none
| (const str (option.some constructor) • t₁ • t₂ • t₃) :=
  if str = "f_ite" then
    (do s₁ ← sortof_aux t₁, s₂ ← sortof_aux t₂, s₃ ← sortof_aux t₂,
        if s₁ = boolsort ∧ s₂ = s₃ then s₂ else option.none)
  else option.none
| (f • t)  :=
  do sf ← sortof_aux f, s ← sortof_aux t,
    match sf with
    | (arrow s1 s2) := if s1 = s then s2 else option.none
    | _ := option.none
    end

def sortof : option term → option sort :=
 (flip option.bind) sortof_aux

def x₁ := const "x₁" boolsort
#reduce (sortof x₁) -- recursion error

[Scott Viteri]

doesn't work because comparing strings

[Reid Barton]

does #eval work?

[Scott Viteri]

yes

[Scott Viteri]

#eval (sortof x₁) -- (some bool)

[Mario Carneiro]

Another option to represent an "open type" would be num

[Mario Carneiro]

just define bot := 0 and not := 1 and so on

[Mario Carneiro]

You should be able to handle at least a few thousand constructors that way in the kernel

[Scott Viteri]

Ok I'm looking at num now

[Scott Viteri]

it is zero or pos, and if pos seems to have a binary encoding of nat

[Scott Viteri]

why is this better than using nat

[Scott Viteri]

efficiency?

[Mario Carneiro]

Yes, you can #reduce (200000000000000 : num) in the kernel without too much trouble

[Scott Viteri]

I could use a map from strings to their corresponding nums to make it more readable, but I feel like this runs into the same issues as before

[Mario Carneiro]

actually I lied, lean can only go up to about (20000 : num), although this is farther than you can go on nat

[Mario Carneiro]

In Coq it's pretty common to use pos_num for maps and things in the kernel

[Scott Viteri]

I mean 20000 is good enough

[Mario Carneiro]

basically you should think of a function out of pos_num as an infinite binary tree

[Mario Carneiro]

whereas a function out of nat is more like a list

[Mario Carneiro]

so it is easier to store more data, more easily accessible, on the tree representation

[Reid Barton]

can you pattern match on num?

[Scott Viteri]

I don't see why not

[Scott Viteri]

it will be a nested pattern match if it is pos

[Scott Viteri]

does pattern match not work on all inductive types?

[Reid Barton]

right, I guess it should work fine

[Reid Barton]

in that case, you don't need to make a fancy map or anything, you can just write @[pattern] def bot : num = 1 like Mario suggested

[Scott Viteri]

Oh

[Scott Viteri]

I didn't understand the suggestion

[Scott Viteri]

that makes total sense

[Scott Viteri]

Thanks!

[Mario Carneiro]

actually pos_num is better than num for this

[Mario Carneiro]

you don't need 0 here so the pure tree structure is simpler

[Scott Viteri]

yeah