## Stream: new members

### Topic: accessing current and previous patterns

#### Etienne Laurin (Jan 13 2020 at 00:26):

Is it possible to prove h?

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


#### Bryan Gin-ge Chen (Jan 13 2020 at 00:57):

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

#### Mario Carneiro (Jan 13 2020 at 02:43):

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 (Jan 13 2020 at 08:32):

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

#### Etienne Laurin (Jan 13 2020 at 19:04):

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 (Jan 13 2020 at 19:33):

I think you can just do this:

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


#### Mario Carneiro (Jan 13 2020 at 19:36):

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 (Jan 13 2020 at 19:38):

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 (Jan 13 2020 at 19:38):

Splendid, the attribute does work.

#### Etienne Laurin (Jan 13 2020 at 19:40):

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

#### Mario Carneiro (Jan 13 2020 at 19:40):

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

#### Mario Carneiro (Jan 13 2020 at 19:41):

The value is reflected in the type of the goal

#### Mario Carneiro (Jan 13 2020 at 19:41):

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

#### Mario Carneiro (Jan 13 2020 at 19:42):

for example

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


#### Etienne Laurin (Jan 13 2020 at 19:48):

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 (Jan 13 2020 at 23:03):

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 (Jan 13 2020 at 23:03):

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

Last updated: May 14 2021 at 00:42 UTC