From 37d60fd2ecf82bf1fd031d63b471893821d90f20 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 5 Jun 2024 07:53:45 +0100 Subject: [PATCH] chore: use match_expr in omega (#4358) --- src/Lean/Elab/Tactic/Omega/Frontend.lean | 110 ++++++++++++----------- 1 file changed, 58 insertions(+), 52 deletions(-) diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 986ce1ab38..11b810d59d 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -217,8 +217,10 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × match groundInt? b with | some _ => rewrite e (mkApp2 (.const ``Int.pow_succ []) b k') | none => mkAtomLinearCombo e - | (``Nat.cast, #[.const ``Int [], i, n]) => - handleNatCast e i n + | (``Nat.cast, #[α, i, n]) => + match_expr α with + | Int => handleNatCast e i n + | _ => mkAtomLinearCombo e | (``Prod.fst, #[α, β, p]) => match p with | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y => rewrite e (mkApp4 (.const ``Prod.fst_mk [u, v]) α x β y) @@ -423,65 +425,69 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) : else return (p, 0) | .app _ _ => - match t.getAppFnArgs with - | (``Eq, #[.const ``Int [], x, y]) => - match y.int? with - | some 0 => pure (← p.addIntEquality h x, 1) - | _ => p.addFact (mkApp3 (.const ``Int.sub_eq_zero_of_eq []) x y h) - | (``LE.le, #[.const ``Int [], _, x, y]) => - match x.int? with - | some 0 => pure (← p.addIntInequality h y, 1) - | _ => p.addFact (mkApp3 (.const ``Int.sub_nonneg_of_le []) y x h) - | (``LT.lt, #[.const ``Int [], _, x, y]) => - p.addFact (mkApp3 (.const ``Int.add_one_le_of_lt []) x y h) - | (``GT.gt, #[.const ``Int [], _, x, y]) => - p.addFact (mkApp3 (.const ``Int.lt_of_gt []) x y h) - | (``GE.ge, #[.const ``Int [], _, x, y]) => - p.addFact (mkApp3 (.const ``Int.le_of_ge []) x y h) - | (``GT.gt, #[.const ``Nat [], _, x, y]) => - p.addFact (mkApp3 (.const ``Nat.lt_of_gt []) x y h) - | (``GE.ge, #[.const ``Nat [], _, x, y]) => - p.addFact (mkApp3 (.const ``Nat.le_of_ge []) x y h) - | (``Ne, #[.const ``Nat [], x, y]) => - p.addFact (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h) - | (``Not, #[P]) => match ← pushNot h P with + match_expr t with + | Eq α x y => + match_expr α with + | Int => + match y.int? with + | some 0 => pure (← p.addIntEquality h x, 1) + | _ => p.addFact (mkApp3 (.const ``Int.sub_eq_zero_of_eq []) x y h) + | Nat => p.addFact (mkApp3 (.const ``Int.ofNat_congr []) x y h) + | Fin n => p.addFact (mkApp4 (.const ``Fin.val_congr []) n x y h) + | _ => pure (p, 0) + | LE.le α _ x y => + match_expr α with + | Int => + match x.int? with + | some 0 => pure (← p.addIntInequality h y, 1) + | _ => p.addFact (mkApp3 (.const ``Int.sub_nonneg_of_le []) y x h) + | Nat => p.addFact (mkApp3 (.const ``Int.ofNat_le_of_le []) x y h) + | Fin n => p.addFact (mkApp4 (.const ``Fin.val_le_of_le []) n x y h) + | _ => pure (p, 0) + | LT.lt α _ x y => + match_expr α with + | Int => p.addFact (mkApp3 (.const ``Int.add_one_le_of_lt []) x y h) + | Nat => p.addFact (mkApp3 (.const ``Int.ofNat_lt_of_lt []) x y h) + | Fin n => p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_lt []) n x y h) + | _ => pure (p, 0) + | GT.gt α _ x y => + match_expr α with + | Int => p.addFact (mkApp3 (.const ``Int.lt_of_gt []) x y h) + | Nat => p.addFact (mkApp3 (.const ``Nat.lt_of_gt []) x y h) + | Fin n => p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_gt []) n x y h) + | _ => pure (p, 0) + | GE.ge α _ x y => + match_expr α with + | Int => p.addFact (mkApp3 (.const ``Int.le_of_ge []) x y h) + | Nat => p.addFact (mkApp3 (.const ``Nat.le_of_ge []) x y h) + | Fin n => p.addFact (mkApp4 (.const ``Fin.val_le_of_ge []) n x y h) + | _ => pure (p, 0) + | Ne α x y => + match_expr α with + | Int => p.addFact (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h) + | Nat => p.addFact (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h) + | _ => pure (p, 0) + | Dvd.dvd α _ k x => + match_expr α with + | Int => p.addFact (mkApp3 (.const ``Int.emod_eq_zero_of_dvd []) k x h) + | Nat => p.addFact (mkApp3 (.const ``Nat.mod_eq_zero_of_dvd []) k x h) + | _ => pure (p, 0) + | Not P => match ← pushNot h P with | none => return (p, 0) | some h' => p.addFact h' - | (``Eq, #[.const ``Nat [], x, y]) => - p.addFact (mkApp3 (.const ``Int.ofNat_congr []) x y h) - | (``LT.lt, #[.const ``Nat [], _, x, y]) => - p.addFact (mkApp3 (.const ``Int.ofNat_lt_of_lt []) x y h) - | (``LE.le, #[.const ``Nat [], _, x, y]) => - p.addFact (mkApp3 (.const ``Int.ofNat_le_of_le []) x y h) - | (``Ne, #[.const ``Int [], x, y]) => - p.addFact (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h) - | (``Prod.Lex, _) => p.addFact (← mkAppM ``Prod.of_lex #[h]) - | (``Dvd.dvd, #[.const ``Nat [], _, k, x]) => - p.addFact (mkApp3 (.const ``Nat.mod_eq_zero_of_dvd []) k x h) - | (``Dvd.dvd, #[.const ``Int [], _, k, x]) => - p.addFact (mkApp3 (.const ``Int.emod_eq_zero_of_dvd []) k x h) - | (``Eq, #[.app (.const ``Fin []) n, x, y]) => - p.addFact (mkApp4 (.const ``Fin.val_congr []) n x y h) - | (``LE.le, #[.app (.const ``Fin []) n, _, x, y]) => - p.addFact (mkApp4 (.const ``Fin.val_le_of_le []) n x y h) - | (``LT.lt, #[.app (.const ``Fin []) n, _, x, y]) => - p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_lt []) n x y h) - | (``GE.ge, #[.app (.const ``Fin []) n, _, x, y]) => - p.addFact (mkApp4 (.const ``Fin.val_le_of_ge []) n x y h) - | (``GT.gt, #[.app (.const ``Fin []) n, _, x, y]) => - p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_gt []) n x y h) - | (``And, #[t₁, t₂]) => do + | Prod.Lex _ _ _ _ _ _ => p.addFact (← mkAppM ``Prod.of_lex #[h]) + | And t₁ t₂ => do let (p₁, n₁) ← p.addFact (mkApp3 (.const ``And.left []) t₁ t₂ h) let (p₂, n₂) ← p₁.addFact (mkApp3 (.const ``And.right []) t₁ t₂ h) return (p₂, n₁ + n₂) - | (``Exists, #[α, P]) => + | Exists α P => p.addFact (mkApp3 (.const ``Exists.choose_spec [← getLevel α]) α P h) - | (``Subtype, #[α, P]) => + | Subtype α P => p.addFact (mkApp3 (.const ``Subtype.property [← getLevel α]) α P h) - | (``Iff, #[P₁, P₂]) => + | Iff P₁ P₂ => p.addFact (mkApp4 (.const ``Decidable.and_or_not_and_not_of_iff []) P₁ P₂ (.app (.const ``Classical.propDecidable []) P₂) h) - | (``Or, #[_, _]) => + | Or _ _ => if (← cfg).splitDisjunctions then return ({ p with disjunctions := p.disjunctions.insert h }, 1) else