Zulip Chat Archive

Stream: new members

Topic: accessing current and previous patterns


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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))

view this post on Zulip 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 := `(_)

view this post on Zulip Etienne Laurin (Jan 13 2020 at 19:38):

Splendid, the attribute does work.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 13 2020 at 19:40):

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

view this post on Zulip Mario Carneiro (Jan 13 2020 at 19:41):

The value is reflected in the type of the goal

view this post on Zulip 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

view this post on Zulip 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 : )

view this post on Zulip 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 `(_)

view this post on Zulip 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

view this post on Zulip 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