accessing current and previous patterns

Stream: new members

[Etienne Laurin]

Is it possible to prove h?

example : ℕ → ℕ
| (_ + 2) := 0
| (a + 1) := by { suffices h : a = 0; sorry }
| _ := 0

[Bryan Gin-ge Chen]

No, it's not. Could you say more about what you're trying to do?

[Mario Carneiro]

You would have to write that function like this:

example : ℕ → ℕ
| (n + 2) := 0
| 1 := by { let a := 0; sorry }
| 0 := 0

The a := 0 is trivial of course in this version

[Etienne Laurin]

I'm porting some code from Haskell, I was trying to use pattern matching instead of dite.

[Etienne Laurin]

I'm trying to write a tactic that keeps a pattern match witness, but I'm getting stuck implementing has_reflect. What am I missing here?

meta structure equation :=
(witness : option name) (pattern : pexpr) (body : pexpr)

meta instance equation.reflect : has_reflect equation
| ⟨witness, pattern, body⟩
:= `(equation.mk %%(reflect witness) %%(reflect pattern) %%(reflect body))
-- equation type mismatch, term has type
--   expr
-- but is expected to have type
--   reflected {witness := witness, pattern := pattern, body := body}

#reduce λ x : equation, reflected x
-- λ (x : equation), expr

[Mario Carneiro]

I think you can just do this:

@[derive has_reflect]
meta structure equation :=
(witness : option name) (pattern : pexpr) (body : pexpr)

[Mario Carneiro]

You have to use some messy methods to get around the typing otherwise:

meta def dont_tell_me_what_I_cant_do {α} {a : α} : expr → reflected a :=
by delta reflected; exact id

meta instance equation.reflect : has_reflect equation
| ⟨witness, pattern, body⟩ := dont_tell_me_what_I_cant_do
  `(equation.mk %%(reflect witness) %%(reflect pattern) %%(reflect body))

[Mario Carneiro]

If you don't construct the term yourself but let lean do it, it is more agreeable:

meta instance equation.reflect : has_reflect equation
| ⟨witness, pattern, body⟩ := `(_)

[Etienne Laurin]

Splendid, the attribute does work.

[Etienne Laurin]

_ seems dodgy.. I have two terms variables of the same type I don't know which one it would pick.

[Mario Carneiro]

The type is reflect a so lean knows exactly what to put there

[Mario Carneiro]

The value is reflected in the type of the goal

[Mario Carneiro]

You only need the brute force methods if you want to lie to lean about what the reflected value is

[Mario Carneiro]

for example

meta instance equation.reflect : has_reflect equation
| ⟨witness, pattern, body⟩ := dont_tell_me_what_I_cant_do `(0 : ℕ)

[Etienne Laurin]

What magic makes _ work? If I change the pattern match into a let, it fails "to synthesize type class instance"

| eqn := let witness := eqn.witness, body := eqn.body, pattern := eqn.pattern in `(_)

[Mario Carneiro]

If you don't pattern match on eqn, the goal is reflect eqn, and then lean's automatic mechanism for deriving reflect instances will use the has_reflect equations instance to synthesize this goal. This fails because we're in the middle of building the instance

[Mario Carneiro]

The magic that makes `(_) produce a reflect instance is... magic, it is built into lean's elaborator