fix: have tauto use Lean.Meta.isProp rather than Lean.Expr.isProp (#5565)

`Lean.Expr.isProp` can't handle metavariables but `Lean.Meta.isProp` can.

Bug reported by @negiizhao

Author: kmill

Mathlib/Order/Circular.lean

@@ -425,10 +425,17 @@ def Preorder.toCircularPreorder (α : Type _) [Preorder α] : CircularPreorder 
     · exact Or.inr (Or.inr ⟨hca, hab.trans hbd⟩)
   sbtw_iff_btw_not_btw {a b c} := by
     simp_rw [lt_iff_le_not_le]
-    have := le_trans a b c
-    have := le_trans b c a
-    have := le_trans c a b
-    tauto
+    have h1 := le_trans a b c
+    have h2 := le_trans b c a
+    have h3 := le_trans c a b
+    -- Porting note: was `tauto`, but this is a much faster tactic proof
+    revert h1 h2 h3
+    generalize (a ≤ b) = p1
+    generalize (b ≤ a) = p2
+    generalize (a ≤ c) = p3
+    generalize (c ≤ a) = p4
+    generalize (b ≤ c) = p5
+    by_cases p1 <;> by_cases p2 <;> by_cases p3 <;> by_cases p4 <;> by_cases p5 <;> simp [*]
 #align preorder.to_circular_preorder Preorder.toCircularPreorder
 
 /-- The circular partial order obtained from "looping around" a partial order.

Mathlib/Tactic/Tauto.lean

@@ -29,7 +29,7 @@ initialize registerTraceClass `tauto
 def distribNotOnceAt (hypFVar : Expr) (g : MVarId) : MetaM AssertAfterResult := g.withContext do
   let .fvar fvarId := hypFVar | throwError "not fvar {hypFVar}"
   let h ← fvarId.getDecl
-  let e : Q(Prop) ← (do guard (← inferType h.type).isProp; pure h.type)
+  let e : Q(Prop) ← (do guard <| ← Meta.isProp h.type; pure h.type)
   let replace (p : Expr) := g.replace h.fvarId p
   match e with
   | ~q(¬ ($a : Prop) = $b) => do
@@ -92,25 +92,25 @@ Calls `distribNotAt` on the head of `state.fvars` up to `nIters` times, returnin
 early on failure.
 -/
 partial def distribNotAt (nIters : Nat) (state : DistribNotState) : MetaM DistribNotState :=
-match nIters, state.fvars with
-| 0, _ | _, [] => pure state
-| n + 1, fv::fvs => do
-  try
-    let result ← distribNotOnceAt fv state.currentGoal
-    let newFVars := (mkFVar result.fvarId)::(fvs.map (fun x ↦ result.subst.apply x))
-    distribNotAt n ⟨newFVars, result.mvarId⟩
-  catch _ => pure state
+  match nIters, state.fvars with
+  | 0, _ | _, [] => pure state
+  | n + 1, fv::fvs => do
+    try
+      let result ← distribNotOnceAt fv state.currentGoal
+      let newFVars := mkFVar result.fvarId :: fvs.map (fun x ↦ result.subst.apply x)
+      distribNotAt n ⟨newFVars, result.mvarId⟩
+    catch _ => pure state
 
 /--
 For each fvar in `fvars`, calls `distribNotAt` and carries along the resulting
 renamings.
 -/
 partial def distribNotAux (fvars : List Expr) (g : MVarId) : MetaM MVarId :=
-match fvars with
-| [] => pure g
-| _ => do
-   let result ← distribNotAt 3 ⟨fvars, g⟩
-   distribNotAux result.fvars.tail! result.currentGoal
+  match fvars with
+  | [] => pure g
+  | _ => do
+    let result ← distribNotAt 3 ⟨fvars, g⟩
+    distribNotAux result.fvars.tail! result.currentGoal
 
 /--
 Tries to apply de-Morgan-like rules on all hypotheses.
@@ -120,7 +120,7 @@ def distribNot : TacticM Unit := withMainContext do
   let mut fvars := []
   for h in ← getLCtx do
     if !h.isImplementationDetail then
-      fvars := (mkFVar h.fvarId):: fvars
+      fvars := mkFVar h.fvarId :: fvars
   liftMetaTactic' (distribNotAux fvars)
 
 /-- Config for the `tauto` tactic. Currently empty. TODO: add `closer` option. -/
@@ -131,15 +131,17 @@ declare_config_elab elabConfig Config
 
 /-- Matches propositions where we want to apply the `constructor` tactic
 in the core loop of `tauto`. -/
-def coreConstructorMatcher (e : Q(Prop)) : MetaM Bool := match e with
+def coreConstructorMatcher (e : Q(Prop)) : MetaM Bool :=
+  match e with
   | ~q(_ ∧ _) => pure true
   | ~q(_ ↔ _) => pure true
   | ~q(True) => pure true
   | _ => pure false
 
 /-- Matches propositions where we want to apply the `cases` tactic
 in the core loop of `tauto`. -/
-def casesMatcher (e : Q(Prop)) : MetaM Bool := match e with
+def casesMatcher (e : Q(Prop)) : MetaM Bool :=
+  match e with
   | ~q(_ ∧ _) => pure true
   | ~q(_ ∨ _) => pure true
   | ~q(Exists _) => pure true
@@ -179,7 +181,8 @@ def tautoCore : TacticM Unit := do
 
 /-- Matches propositions where we want to apply the `constructor` tactic in the
 finishing stage of `tauto`. -/
-def finishingConstructorMatcher (e : Q(Prop)) : MetaM Bool := match e with
+def finishingConstructorMatcher (e : Q(Prop)) : MetaM Bool :=
+  match e with
   | ~q(_ ∧ _) => pure true
   | ~q(_ ↔ _) => pure true
   | ~q(Exists _) => pure true

test/Tauto.lean

@@ -69,6 +69,35 @@ example (p q r : Prop) (h : ¬ p = q) (h' : r = q) : p ↔ ¬ r := by tauto
 example (p : Prop) : p → ¬ (p → ¬ p) := by tauto
 example (p : Prop) (em : p ∨ ¬ p) : ¬ (p ↔ ¬ p) := by tauto
 
+-- reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/weird.20tactic.20bug/near/370505747
+open Classical in
+example (hp : p) (hq : q) : (if p ∧ q then 1 else 0) = 1 := by
+  -- split_ifs creates a hypothesis with a type that's a metavariable
+  split_ifs
+  · rfl
+  · tauto
+
+example (hp : p) (hq : q) (h : ¬ (p ∧ q)) : False := by
+  -- causes `h'` to have a type that's a metavariable:
+  have h' := h
+  clear h
+  tauto
+
+example (p : Prop) (h : False) : p := by
+  -- causes `h'` to have a type that's a metavariable:
+  have h' := h
+  clear h
+  tauto
+
+example (hp : p) (hq : q) : p ∧ q := by
+  -- causes goal to have a type that's a metavariable:
+  suffices h : ?foo by exact h
+  tauto
+
+-- Checking `tauto` can deal with annotations:
+example (hp : ¬ p) (hq : ¬ (q ↔ p) := by sorry) : q := by
+  tauto
+
 example (P : Nat → Prop) (n : Nat) : P n → n = 7 ∨ n = 0 ∨ ¬ (n = 7 ∨ n = 0) ∧ P n :=
 by tauto