type depending on an `if`

Stream: lean4

[Scott Morrison]

I worry I'm confused about something basic here. Suppose I want to fill in:

example (P : Prop) [Decidable P] {a b : α} {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) := ...

Here is one answer:

import Mathlib.Tactic.SplitIfs
set_option autoImplicit true

def yuck (P : Prop) [Decidable P] {a b : α} {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) := by
  split_ifs
  · exact x
  · exact y

(If you wonder why I named it yuck, try #print yuck.)

Alternatively we can:

def yum (P : Prop) [i : Decidable P] {a b : α} {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) :=
  match i with
  | isTrue _ => x
  | isFalse _ => y

But:

1. I had to name the Decidable instance, which is a bit smelly.
2. Having to do this feels like it rather spoils the point of if syntax.

[Scott Morrison]

Is it really not possible to make

def mmmm (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) :=
  if P then x else y      -- application type mismatch

work somehow?

[Marcus Rossel]

You can do this:

def mmmm (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) :=
  if h : P then if_pos h ▸ x else if_neg h ▸ y

[Scott Morrison]

But then my term has nasty Eq.recs. It's barely better than yuck.

[Scott Morrison]

I think what I am hoping for an answer to mmmm is redefining the syntax for if, so that both if statements are actually match statements. Note that

def mmmm! (P : Prop) [i : Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (match i with | isTrue _ => a | isFalse _ => b) :=
  match i with | isTrue _ => x | isFalse _ => y

works just fine, so this is plausible.

[Scott Morrison]

Alternatively

def mmmm! (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (match (inferInstance : Decidable P) with | isTrue _ => a | isFalse _ => b) :=
  match (inferInstance : Decidable P) with | isTrue _ => x | isFalse _ => y

avoids needing to name the instance, and still works fine.

[Scott Morrison]

Or even nicer:

def mmmm! (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (match decide P with | true => a | false => b) :=
  match decide P with | true => x | false => y

[Scott Morrison]

Indeed, one can override the syntax:

macro_rules
  | `(if $c then $t else $e) => do
    let mvar ← Lean.withRef c `(?m)
    `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; match decide $mvar with | true => $t | false => $e)

def mmmm!! (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) :=
  if P then x else y

[Scott Morrison]

So the question becomes: why don't do we this already?

[Scott Morrison]

It seems much nicer, and the terms are better. But presumably even if there is no obstruction, it is the mother of all refactors to implement.

[Scott Morrison]

I suspect changing if to mean match rather than casesOn will also help with reduction of terms, given our recent experiences there.

[Scott Morrison]

Two potential problems:

1. run_cmd do if false then pure 3 else pure 7 now fails with auxiliary declaration cannot be created when declaration name is not available, but maybe we could just allow that?
2. I suspect that this breaks the lazy evaluation of branches of the if statement. Can anyone suggest either an easy test for this, and assuming it fails, any ideas for a solution?

[Eric Wieser]

I don't see why you called it yuck:

set_option pp.proofs.withType false in
#print yuck
/--
def yuck.{u_1, u_2} : {α : Sort u_1} →
  (P : Prop) → [inst : Decidable P] → {a b : α} → {C : α → Sort u_2} → C a → C b → C (if P then a else b) :=
fun {α} P [Decidable P] {a b} {C} x y => if h : P then Eq.mpr _ x else Eq.mpr _ y
-/

A single Eq.mpr in each branch doesn't seem too surprising for a dependent if

[Kyle Miller]

The match expressions are hiding some of the complexity since they pretty print so nicely. Just like the Eq recursor, there's a motive, which is how the match expression is able to let the type become specialized depending on the discriminant.

set_option autoImplicit true

def mmmm! (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (match decide P with | true => a | false => b) :=
  match decide P with | true => x | false => y

set_option pp.match false
#print mmmm!
/-
def mmmm!.{u_1, u_2} : {α : Sort u_1} → {a b : α} → (P : Prop) → [inst : Decidable P] →
    {C : α → Sort u_2} →
    C a → C b → C (mmmm!.match_1 (fun x ↦ α) (decide P) (fun _ ↦ a) fun _ ↦ b) :=
fun {α} {a b} P [Decidable P] {C} x y ↦
  mmmm!.match_1 (fun x ↦ C (mmmm!.match_1 (fun x ↦ α) x (fun _ ↦ a) fun _ ↦ b))
    (decide P)
    (fun _ ↦ x)
    (fun _ ↦ y)
-/

[Kyle Miller]

It's interesting having if be able to specialize decide P to different values in the target type, which is what match enables. I wonder if it would be more useful to be able to specialize P itself, rather than decide P.

For example, this doesn't work (nor does using match decide P with | true => x | false => y), but I might expect being able to use if P then x else y in the body.

def mmmm! (P : Prop) [i : Decidable P] {C : Prop → Sort _} (x : C True) (y : C False) : C P :=
  match i with
  | isTrue _ => x
  | isFalse _ => y

[Kyle Miller]

I was just exploring a bit -- maybe if could be notation that figures out how to apply fancyIfImpl. This lets you simultaneously swap out P for True/False, the decidable instance for instDecidableTrue/instDecidableFalse, and decide P for true/false.

def fancyIfImpl (motive : (P : Prop) → [Decidable P] → Bool → Sort _)
    (P : Prop) [Decidable P]
    (ifTrue : Unit → motive True true)
    (ifFalse : Unit → motive False false) :
    motive P (decide P) :=
  match h : decide P with
  | true => by convert eq_true_of_decide h ▸ ifTrue (); simpa using h
  | false => by convert eq_false_of_decide h ▸ ifFalse (); simpa using h

def test1 (P : Prop) [Decidable P] {C : Prop → Sort _} (x : C True) (y : C False) :
    C P :=
  fancyIfImpl (fun P _ _ => C P)
    P
    (fun _ => x)
    (fun _ => y)

def test2 (P : Prop) [Decidable P] {C : α → Sort _} (x : C a) (y : C b) :
    C (if P then a else b) :=
  fancyIfImpl (fun P _ _ => C (if P then a else b))
    P
    (fun _ => x)
    (fun _ => y)