using `cons` as match_pattern

Stream: Is there code for X?

[Asei Inoue]

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

@[match_pattern]
def cons (x : α) (xs : Many α) : Many α :=
  .more x (fun () => xs)

def Many.union : Many α → Many α → Many α
  | Many.none, ys => ys
  | Many.more x xs, ys => Many.more x (fun () => union (xs ()) ys)

instance : Append (Many α) where
  append := Many.union

/- error: invalid alternative name 'cons' -/
theorem union_none (x : α) (xs : Many α) : xs ++ .none = xs := by
  induction xs with
  | none => rfl
  | cons x xs ih => sorry

[Asei Inoue]

I want to use this cons function for induction...

[Shreyas Srinivas]

Is this a lazy list?

[Shreyas Srinivas]

@loogle LazyList

[loogle]

:search: LazyList, LazyList.iota, and 66 more

[Asei Inoue]

see https://lean-lang.org/functional_programming_in_lean/monads/arithmetic.html#nondeterministic-search

[Kyle Miller]

The induction tactic doesn't use match infrastructure. The @[match_pattern] attribute doesn't apply here at all.

You could write an @[induction_eliminator] to save you from writing using myEliminatorTheorem in induction xs using myEliminatorTheorem with .... You'll have to write myEliminatorTheorem (it should copy how Many.recOn looks, but you can adjust the statement to have a cons minor hypothesis).

[Asei Inoue]

@Kyle Miller Thank you. How can I enable cons to be used in pattern matching by match? I have created a cons version of Many.casesOn, but it does not work.

[Asei Inoue]

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

@[match_pattern]
def Many.cons (x : α) (xs : Many α) : Many α :=
  .more x (fun () => xs)

@[match_pattern]
protected def Many.cons_casesOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
    (cons : (a : α) → (b : Many α) → motive (Many.cons a b)) : motive t := by
  match t with
  | .none => assumption
  | .more x xs =>
    exact cons x (xs ())

def Many.takeAll : Many α → List α
  | Many.none => []
  /-
  invalid pattern, constructor or constant marked with '[match_pattern]' expected
  -/
  | Many.cons x xs => x :: xs.takeAll

[Kyle Miller]

You can't, since fun () => xs is not a valid pattern.

def Many.takeAll : Many α → List α
  | Many.none => []
  | Many.more x (fun () => xs) => x :: xs.takeAll
--               ~~~~~~~~~~~~ invalid pattern

[Asei Inoue]

impossible? oh no... :sad:

[Kyle Miller]

(By the way, for Many.cons_casesOn, it doesn't make sense giving it @[match_pattern]. You could, if it's what you want to be the default eliminator for the cases tactic, use @[cases_eliminator] instead.)

[Kyle Miller]

All @[match_pattern] does is make it so that match will unfold a definition while processing the patterns. If the unfolded version doesn't work, then it's no use adding @[match_pattern].

[Asei Inoue]

@Kyle Miller

You could write an @[induction_eliminator] to save you from writing using myEliminatorTheorem in induction xs using myEliminatorTheorem with ....

Thank you. but I get an error:

set_option autoImplicit false

variable {α : Type}

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

@[simp]
theorem Many.fun_simp (xs : Unit → Many α) : (fun _ => xs ()) = xs := by simp

def Many.cons (x : α) (xs : Many α) : Many α :=
  .more x (fun () => xs)

/--
info: Many.recOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
  (more : (a : α) → (a_1 : Unit → Many α) → ((a : Unit) → motive (a_1 a)) → motive (Many.more a a_1)) : motive t
-/
#guard_msgs in #check Many.recOn

/-
code generator does not support recursor 'Many.rec' yet, consider using 'match ... with' and/or structural recursion
-/
@[induction_eliminator]
protected def Many.rec_casesOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
    (cons : (a : α) → (b : Many α) → (motive b) → motive (Many.cons a b)) : motive t := by
  induction t with
  | none => assumption
  | more x xs ih =>
    specialize ih ()
    replace cons := cons x <| xs ()
    specialize cons ih
    simpa [Many.cons] using cons

[Kyle Miller]

Why did you replace your definition of Many.rec_casesOn if the match expression from before worked?

[Asei Inoue]

Why did you replace your definition of Many.rec_casesOn if the match expression from before worked?

Sorry I don't understand the intension of your question. what is the "match expression from before worked"?
But I just want to try induction_eliminator, I don't expect the proof to work with it.

[Kyle Miller]

My suggestion earlier was to replace @[match_pattern] with @[cases_eliminator]. There is no need to change the body of the definition, and as you saw, using induction for the body makes it become not compilable.

@[cases_eliminator]
protected def Many.cons_casesOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
    (cons : (a : α) → (b : Many α) → motive (Many.cons a b)) : motive t := by
  match t with
  | .none => assumption
  | .more x xs =>
    exact cons x (xs ())

[Kyle Miller]

(Rephrasing "Why did you replace your definition of Many.rec_casesOn if the match expression from before worked?" in clearer language: "If it worked to use a match expression, why did you replace the definition to use induction?")

[Asei Inoue]

@Kyle Miller
why are you talking about cases_eliminator? I think we are talking about induction_eliminator.

[Kyle Miller]

By the way, the issue with using the induction or cases tactic in a def is that these make use of eliminators for the type, and eliminators do not have compiled code, leading to the "code generator does not support recursor" error.

[Kyle Miller]

I'm talking about cases_eliminator because your Many.cons_casesOn looks like a cases eliminator. It has no induction hypothesis in cons.

[Kyle Miller]

(Plus, you named it casesOn.)

[Asei Inoue]

oh... I made a huge naming mistake

[Asei Inoue]

I get an error again.

set_option autoImplicit false

variable {α : Type}

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

@[simp] theorem Many.fun_simp (xs : Unit → Many α) : (fun _ => xs ()) = xs := by simp

def Many.cons (x : α) (xs : Many α) : Many α :=
  .more x (fun () => xs)

/-
unexpected eliminator resulting type
  motive x.1
-/
@[induction_eliminator]
protected def Many.cons_recOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
    (cons : (a : α) → (b : Many α) → (motive b) → motive (Many.cons a b)) : motive t := by
  match t with
  | .none => assumption
  | .more x xs =>
    have ih := Many.cons_recOn (xs ()) (by assumption) cons
    replace cons := (cons x <| xs ()) ih
    simp [Many.cons] at cons
    assumption
    done

[Eric Wieser]

Kyle Miller said:

I'm talking about cases_eliminator because your Many.cons_casesOn looks like a cases eliminator. It has no induction hypothesis in cons.

So far in mathlib we've been using these two attributes together. On types where there is no induction going on, is this the morally correct approach?

[Eric Wieser]

Alternatively, should induction x be a lint warning if x : A × B or some other type where recOn and casesOn coincide?

[Asei Inoue]

so is it impossible to write induction_eliminator lemma for Many?

[Eric Wieser]

No, it just doesn't like the arguments in the order you have

[Eric Wieser]

Here's a working version:

@[elab_as_elim, induction_eliminator]
protected def Many.consRec.{u} {α : Type} {motive : Many α → Sort u} (none : motive Many.none)
    (cons : (a : α) → (b : Many α) → (motive b) → motive (Many.cons a b)) : (t : Many α) → motive t
  | .none => none
  | .more x xs => cons x (xs ()) (Many.consRec none cons (xs ()))

[Eric Wieser]

The only required change was moving t to be the last argument

[Asei Inoue]

@Eric Wieser Thank you!!