explicit parameters lead to more work

Stream: general

[FR]

import algebra.order.monoid

namespace implicit

def bar (m : with_bot ℕ) : Type* := sorry

def foo' {m n : ℕ} (x : bar m) (y : bar n) : ℕ := sorry

def foo : ∀ {m n : with_bot ℕ}, bar m → bar n → ℕ
| (m' : ℕ) (n' : ℕ) := λ x y, foo' x y
| _        _        := λ _ _, 0

def mul : ∀ {m n : with_bot ℕ}, bar m → bar n → bar (m + n) := sorry

lemma h {m₁ m₂ n : ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (mul x₁ x₂) y = foo x₁ y * foo x₂ y := sorry

example {m₁ m₂ n : with_bot ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (mul x₁ x₂) y = foo x₁ y * foo x₂ y :=
begin
  cases m₁; cases m₂; cases n; simp only [foo, nat.zero_mul, nat.mul_zero],
  exact h x₁ x₂ y,
end

end implicit

namespace explicit

def bar (m : with_bot ℕ) : Type* := sorry

def foo' (m n : ℕ) (x : bar m) (y : bar n) : ℕ := sorry

def foo : ∀ (m n : with_bot ℕ), bar m → bar n → ℕ
| (m : ℕ) (n : ℕ) := λ x y, foo' m n x y
| (m : ℕ) ⊥       := λ _ _, 0
| ⊥       (n : ℕ) := λ _ _, 0
| ⊥       ⊥       := λ _ _, 0

def mul : ∀ {m n : with_bot ℕ}, bar m → bar n → bar (m + n) := sorry

lemma h {m₁ m₂ n : ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (m₁ + m₂) n (mul x₁ x₂) y = foo m₁ n x₁ y * foo m₂ n x₂ y := sorry

example {m₁ m₂ n : with_bot ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (m₁ + m₂) n (mul x₁ x₂) y = foo m₁ n x₁ y * foo m₂ n x₂ y :=
begin
  induction m₁ using with_bot.rec_bot_coe;
  induction m₂ using with_bot.rec_bot_coe;
  induction n using with_bot.rec_bot_coe;
  try { rw [with_bot.bot_add], };
  try { rw [with_bot.add_bot], };
  try { rw [← with_bot.coe_add], };
  simp only [foo, nat.zero_mul, nat.mul_zero],
  exact h x₁ x₂ y,
end

end explicit

Once I made the pattern matching argument explicit, I found I had to deal with far more problems on my own than before. Are there any better solutions?

[FR]

Oh, I did it. Just use simp !

example {m₁ m₂ n : with_bot ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (m₁ + m₂) n (mul x₁ x₂) y = foo m₁ n x₁ y * foo m₂ n x₂ y :=
begin
  cases m₁; cases m₂; cases n; simp ! only [nat.zero_mul, nat.mul_zero],
  exact h x₁ x₂ y,
end

[FR]

But it unfolds too much. Can I control it?

[Eric Wieser]

Once I made the pattern matching argument explicit

What do you mean by that? Your implicit.foo and explicit.foo contain a different number of patterns to match against; there's more difference than just (m n : with_bot ℕ) vs {m n : with_bot ℕ}

[Eric Wieser]

I suspect your question is actually "why does this get harder when I fully-expand the wildcard pattern", and the answer is something along the lines of "because now you have to do the same expansion in the proof

[FR]

import algebra.order.monoid

namespace implicit

def bar (m : with_bot ℕ) : Type* := sorry

def foo' {m n : ℕ} (x : bar m) (y : bar n) : ℕ := sorry

def foo : ∀ {m n : with_bot ℕ}, bar m → bar n → ℕ
| (m : ℕ) (n : ℕ) := λ x y, foo' x y
| _       _       := λ _ _, 0

def mul : ∀ {m n : with_bot ℕ}, bar m → bar n → bar (m + n) := sorry

lemma h {m₁ m₂ n : ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (mul x₁ x₂) y = foo x₁ y * foo x₂ y := sorry

example {m₁ m₂ n : with_bot ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (mul x₁ x₂) y = foo x₁ y * foo x₂ y :=
begin
  cases m₁; cases m₂; cases n; simp only [foo, nat.zero_mul, nat.mul_zero],
  exact h x₁ x₂ y,
end

end implicit

namespace explicit

def bar (m : with_bot ℕ) : Type* := sorry

def foo' (m n : ℕ) (x : bar m) (y : bar n) : ℕ := sorry

def foo : ∀ (m n : with_bot ℕ), bar m → bar n → ℕ
| (m : ℕ) (n : ℕ) := λ x y, foo' m n x y
| _       _       := λ _ _, 0

def mul : ∀ {m n : with_bot ℕ}, bar m → bar n → bar (m + n) := sorry

lemma h {m₁ m₂ n : ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (m₁ + m₂) n (mul x₁ x₂) y = foo m₁ n x₁ y * foo m₂ n x₂ y := sorry

example {m₁ m₂ n : with_bot ℕ}
  (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
    foo (m₁ + m₂) n (mul x₁ x₂) y = foo m₁ n x₁ y * foo m₂ n x₂ y :=
begin
  cases m₁; cases m₂; cases n; simp only [foo, nat.zero_mul, nat.mul_zero],
  exact h x₁ x₂ y,
end

end explicit

But this still fails?

[FR]

It seems that simp treats implicit parameters differently than explicit parameters.

[Eric Wieser]

Ah thanks, you're right!

[Eric Wieser]

A slightly shorter mwe:

import algebra.order.monoid

def bar (m : with_bot ℕ) : Type* := sorry
def mul : ∀ {m n : with_bot ℕ}, bar m → bar n → bar (m + n) := sorry
def foo' (m n : ℕ) (x : bar m) (y : bar n) : ℕ := sorry

namespace implicit

def foo : ∀ {m n : with_bot ℕ}, bar m → bar n → ℕ
| (m : ℕ) (n : ℕ) := λ x y, foo' _ _ x y
| _       _       := λ _ _, 0

example {m₁ m₂ n : with_bot ℕ} (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
  foo (mul x₁ x₂) y = foo x₁ y * foo x₂ y :=
begin
  cases m₁; cases m₂; cases n,
  { simp only [foo, nat.zero_mul, nat.mul_zero], },
  all_goals { sorry }
end

end implicit

namespace explicit

def foo : ∀ (m n : with_bot ℕ), bar m → bar n → ℕ
| (m : ℕ) (n : ℕ) := λ x y, foo' m n x y
| _       _       := λ _ _, 0

example {m₁ m₂ n : with_bot ℕ} (x₁ : bar m₁) (x₂ : bar m₂) (y : bar n) :
  foo _ _ (mul x₁ x₂) y = foo _ _ x₁ y * foo _ _ x₂ y :=
begin
  cases m₁; cases m₂; cases n,
  { simp only [foo, nat.zero_mul, nat.mul_zero], },
  all_goals { sorry }
end

end explicit

[FR]

How should I get lean to do the same thing in the case of explicit parameters? simp ! can unfold it but this would also unfold other things.

[Gabriel Ebner]

simp uses reducible transparency for matching. With reducible transparency, a definition like (0 : with_bot ℕ) is not unfolded to some 0 because it is only semireducible.

[Gabriel Ebner]

However, there's a big exception. Implicit arguments get "upgraded" to semireducible transparency.

[Gabriel Ebner]

In other words, the following works with the implicit version but not the explicit version, because 0 = some 0 is only defeq with semireducible transparency:

example (x y) : @foo 0 0 x y = @foo (some 0) (some 0) x y :=
by tactic.reflexivity tactic.transparency.reducible