From c1ad8c34be7c6fd323fc5eff5ce337fd23a72e04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 9 May 2018 18:34:06 +0200 Subject: [PATCH] - --- src/simp_loop/monotone_elim.lean | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/src/simp_loop/monotone_elim.lean b/src/simp_loop/monotone_elim.lean index 88ae4d2..2e03f00 100644 --- a/src/simp_loop/monotone_elim.lean +++ b/src/simp_loop/monotone_elim.lean @@ -289,8 +289,8 @@ candidates ← disjs.mmap (λconjs, do (ps, e, ss) ← return xs, (rel, l, r) ← parse_rel e, return $ - (if l ∈ vs ∧ ¬ l.occurs r ∧ ¬ l.occurs rel ∧ (ps ++ ss).all (λe, ¬ l.occurs e) then [l] else []) ++ - (if r ∈ vs ∧ ¬ r.occurs l ∧ ¬ r.occurs rel ∧ (ps ++ ss).all (λe, ¬ r.occurs e) then [r] else [])) + (if l ∈ vs ∧ (r :: rel :: ps ++ ss).all (λe, ¬ l.occurs e) then [l] else []) ++ + (if r ∈ vs ∧ (l :: rel :: ps ++ ss).all (λe, ¬ r.occurs e) then [r] else [])) <|> return []), return candidates.join), let candidates := vs.filter $ λv, candidates.all $ λcs, v ∈ cs, @@ -314,6 +314,29 @@ l ← analyse_connection_aux ls vs lhs rhs, r ← analyse_connection_aux ls vs rhs lhs, return (l.map (λp, (ff, p)) ++ r.map (λp, (tt, p))) +meta def ors (c : conv unit) : conv unit := do +`(_ ∨ _) ← lhs | c, +congr_core (congr_core skip ors) ors, +skip + +meta def ands (c : conv unit) : conv unit := do +`(_ ∧ _) ← lhs | c, +congr_core (congr_core skip ands) ands, +skip + +meta def local_eq (v₀ v₁ : expr) : bool := +v₀.is_local_constant ∧ v₁.is_local_constant ∧ v₀.local_uniq_name = v₁.local_uniq_name + +meta def term_focus (l : list (name × bool × pattern)) (v : expr) : conv unit := +l.mfirst $ assume ⟨n, symm, pat⟩, do + ([], [t]) ← match_pattern pat, + guard $ v.occurs t, + (if symm then apply_const n else fail "symmetric apply not supported yet"), + ors (ands $ (do + l ← lhs, + (_, l, r) ← lift_tactic $ parse_rel l, + guard ((v.occurs l ∧ ¬ local_eq l v) ∨ (v.occurs r ∧ ¬ local_eq r v)), + term_focus) <|> skip) end analyse