chore: use match_expr in omega (#4358)
This commit is contained in:
Kim Morrison
GitHub
parent
fbb3055f82
commit
37d60fd2ec
1 changed files with 58 additions and 52 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue