how to use Qq library

Stream: general

[Kim Morrison]

@Eric Wieser, any interest in continuing with this PR? I just ran into the same problem. (Trying to answer https://proofassistants.stackexchange.com/questions/5360/what-is-the-standard-equivalent-of-an-ltac-match-in-lean4/5368#5368)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Kim Morrison you could make that marginally more readable with match_expr. Is that reasonable to recommend to newcomers? It's unfortunate that it doesn't support nested expressions.

elab "match_assoc" : tactic => do
  for ldecl in (← getLCtx) do
    match_expr ldecl.type with
    | Eq _ lhs _ =>
      match_expr lhs with
      | And a _ =>
        let_expr And _ _ := a | continue
        evalTactic (← `(tactic| rw [and_assoc] at $(mkIdent ldecl.userName):ident))
      | Or e _ =>
        let_expr Or _ _ := e | continue
        evalTactic (← `(tactic| rw [or_assoc] at $(mkIdent ldecl.userName):ident))
      | _ => pure ()
    | _ => pure ()

[Aaron Liu]

Don't we have ~q(...) matching?

[Kim Morrison]

Yes, I failed to get ~q(...) to work here as I kept running into the issue above.

[Aaron Liu]

Looks like you want to have a : Q(Prop) := a instead of let

[Aaron Liu]

oh yeah that's what Eric said

[Aaron Liu]

what's the problem then?

[Aaron Liu]

Does the solution not work?

[Jakub Nowak]

Kim Morrison said:

Eric Wieser, any interest in continuing with this PR? I just ran into the same problem. (Trying to answer https://proofassistants.stackexchange.com/questions/5360/what-is-the-standard-equivalent-of-an-ltac-match-in-lean4/5368#5368)

Offtopic about that SE question, isn't the standard way in Lean to try applying the theorem and just let it succeed or fail?

[Kim Morrison]

Aaron Liu said:

Does the solution not work?

I couldn't get it to work. I wrote what looked like the right code, but the matches never obtained.

[Aaron Liu]

Can you give a #mwe

[Kim Morrison]

Sorry, insufficiently interested in Qq. :-)