Basic Qq help - matching against both goal and hypothesis

Stream: metaprogramming / tactics

[Dessertion]

What would be the Lean equivalent of the following Coq tactic?

Ltac match_on_conj :=
  match goal with
  | [ H : ?P /\ ?Q |- ?P ] => apply (proj1 H)
  | [ H : ?P /\ ?Q |- ?Q ] => apply (proj2 H)
  end.

Example E1 {P Q : Prop} (H : P /\ Q) : P.
  match_on_conj.
Qed.

Example E2 {P Q : Prop} (H : P /\ Q) : Q.
  match_on_conj.
Qed.

This is my very crude attempt at a translation:

import Qq

open Qq Lean Elab Meta Tactic

elab "match_on_conj" : tactic => do
  for ldecl in ← getLCtx do
    let ⟨0, type, _⟩ := ← inferTypeQ ldecl.toExpr | continue
    match type with
    | ~q($p ∧ $q) =>
      have goalType : Q(Prop) := ← getMainTarget
      let hypName := mkIdent ldecl.userName
      if let ~q($x) := goalType then
        if ← isDefEq x p then
          evalTactic (← `(tactic| apply And.left $hypName))
        else if ← isDefEq x q then
          evalTactic (← `(tactic| apply And.right $hypName))
        else pure ()
    | _ => pure ()

example {P Q : Prop} (H : P ∧ Q) : P := by
  match_on_conj

example {P Q : Prop} (H : P ∧ Q) : Q := by
  match_on_conj

Is there a way to directly match the goal against my hypotheses as in Coq, without resorting to isDefEq? And more generally, what would be a more idiomatic way to write something like this?

[Aaron Liu]

Maybe something like this? Not sure how this generalizes to more complicated stuff though.

macro "match_on_conj" : tactic =>
  `(tactic| first | exact And.left ‹_› | exact And.right ‹_› | fail "tactic 'match_on_conj' failed")

example {P Q : Prop} (H : P ∧ Q) : P := by
  match_on_conj

example {P Q : Prop} (H : P ∧ Q) : Q := by
  match_on_conj

[Dessertion]

I suppose that does work for this toy example, but I would still like to know how one would implement this from "first principles" (vs. directly chaining pre-existing tactics).

[Aaron Liu]

Metaprogramming in Lean did not cover Qq, so I don't know how to use it. Here's my solution:

import Lean

open Lean Elab Meta Tactic

elab "match_on_conj" : tactic => do
  let goal := ← getMainGoal
  let goalType ← goal.getType'
  for ldecl in ← getLCtx do
    if ldecl.isImplementationDetail then continue
    let type ← instantiateMVars (← whnf ldecl.type)
    let some (p, q) := type.app2? ``And | continue
    if ← withReducible (isDefEq p goalType) then
      goal.assign (mkApp3 (.const ``And.left []) p q ldecl.toExpr)
    else if ← withReducible (isDefEq q goalType) then
      goal.assign (mkApp3 (.const ``And.right []) p q ldecl.toExpr)
    else
      throwTacticEx `match_on_conj goal

example {P Q : Prop} (H : P ∧ Q) : P := by
  match_on_conj

example {P Q : Prop} (H : P ∧ Q) : Q := by
  match_on_conj

[Vasilii Nesterov]

This is an example with Qq:

import Qq

open Qq Lean Elab Meta Tactic

elab "match_on_conj" : tactic => do
  for ldecl in ← getLCtx do
    if ldecl.isImplementationDetail then continue
    let ⟨u, type, expr⟩ ← inferTypeQ ldecl.toExpr
    if !(← isProp type) then continue
    have : u =QL 0 := ⟨⟩
    match type with
    | ~q($p ∧ $q) =>
      let goal ← getMainGoal
      let goalType ← getMainTarget
      if ← isDefEq goalType p then
        goal.assign q(And.left $expr)
      else if ← isDefEq goalType q then
        goal.assign q(And.right $expr)
    | _ => pure ()

example {P Q : Prop} (H : P ∧ Q) : P := by
  match_on_conj

example {P Q : Prop} (H : P ∧ Q) : Q := by
  match_on_conj

example {P Q R : Prop} (h1 : P → Q ∧ R) (h2 : P) : Q := by
  have h3 := h1 h2
  match_on_conj

Note that if we write

let ⟨0, type, _⟩ := ← inferTypeQ ldecl.toExpr | continue

instead of

let ⟨u, type, expr⟩ := ← inferTypeQ ldecl.toExpr
if !(← isProp type) then continue
have : u =QL 0 := ⟨⟩

then we lose hypotheses whose u is a metavariable and the last example fails.