Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
open tactic.interactive ( casesm constructor_matching )
find all assumptions of the shape `¬ (p ∧ q)` or `¬ (p ∨ q)` and
replace them using de Morgan's law.
meta def distrib_not : tactic unit :=
do h ← get_local h.local_pp_name,
| `(¬ _ = _) := replace h.local_pp_name ``(mt iff.to_eq %%h)
| `(_ ≠ _) := replace h.local_pp_name ``(mt iff.to_eq %%h)
| `(_ = _) := replace h.local_pp_name ``(eq.to_iff %%h)
| `(¬ (_ ∧ _)) := replace h.local_pp_name ``(decidable.not_and_distrib'.mp %%h) <|>
replace h.local_pp_name ``(decidable.not_and_distrib.mp %%h)
| `(¬ (_ ∨ _)) := replace h.local_pp_name ``(not_or_distrib.mp %%h)
| `(¬ ¬ _) := replace h.local_pp_name ``(decidable.of_not_not %%h)
| `(¬ (_ → (_ : Prop))) := replace h.local_pp_name ``(decidable.not_imp.mp %%h)
| `(¬ (_ ↔ _)) := replace h.local_pp_name ``(decidable.not_iff.mp %%h)
| `(_ ↔ _) := replace h.local_pp_name ``(decidable.iff_iff_and_or_not_and_not.mp %%h) <|>
``(decidable.iff_iff_and_or_not_and_not.mp (%%h).symm) <|>
| `(_ → _) := replace h.local_pp_name ``(decidable.not_or_of_imp %%h)
The following definitions maintain a path compression datastructure, i.e. a forest such that:
- every node is the type of a hypothesis
- there is a edge between two nodes only if they are provably equivalent
- every edge is labelled with a proof of equivalence for its vertices
- edges are added when normalizing propositions.
meta def tauto_state := ref $ expr_map (option (expr × expr))
meta def modify_ref {α : Type} (r : ref α) (f : α → α) :=read_ref r >>= write_ref r ∘ f
meta def add_refl (r : tauto_state) (e : expr) : tactic (expr × expr) :=
p ← mk_mapp `rfl [none,e],
write_ref r $ m.insert e none,
If there exists a symmetry lemma that can be applied to the hypothesis `e`,
meta def add_symm_proof (r : tauto_state) (e : expr) : tactic (expr × expr) :=
let rel := e.get_app_fn.const_name,
some symm ← pure $ environment.symm_for env rel
(do e' ← mk_meta_var `(Prop),
iff_t ← to_expr ``(%%e = %%e'),
(applyc `iff.to_eq ; () <$ split ; applyc symm),
e' ← instantiate_mvars e',
write_ref r $ (m.insert e (e',p)).insert e' none,
meta def add_edge (r : tauto_state) (x y p : expr) : tactic unit :=
modify_ref r $ λ m, m.insert x (y,p)
Retrieve the root of the hypothesis `e` from the proof forest.
If `e` has not been internalized, add it to the proof forest.
meta def root (r : tauto_state) : expr → tactic (expr × expr) | e :=
let record_e : tactic (expr × expr) :=
(do (e,p) ← get_assignment v >>= root,
some e' ← pure $ m.find e | record_e,
p'' ← mk_app `eq.trans [p',p''],
| none := prod.mk e <$> mk_mapp `rfl [none,some e]
Given hypotheses `a` and `b`, build a proof that `a` is equivalent to `b`,
applying congruence and recursing into arguments if `a` and `b`
are applications of function symbols.
meta def symm_eq (r : tauto_state) : expr → expr → tactic expr | a b :=
(unify a' b' >> add_refl r a' *> mk_mapp `rfl [none,a]) <|>
do p ← match (a', b') with
| (`(¬ %%a₀), `(¬ %%b₀)) :=
p' ← mk_app `congr_arg [`(not),p],
| (`(%%a₀ ∧ %%a₁), `(%%b₀ ∧ %%b₁)) :=
p' ← to_expr ``(congr (congr_arg and %%p₀) %%p₁),
| (`(%%a₀ ∨ %%a₁), `(%%b₀ ∨ %%b₁)) :=
p' ← to_expr ``(congr (congr_arg or %%p₀) %%p₁),
| (`(%%a₀ ↔ %%a₁), `(%%b₀ ↔ %%b₁)) :=
p' ← to_expr ``(congr (congr_arg iff %%p₀) %%p₁),
p' ← to_expr ``(eq.trans (congr (congr_arg iff %%p₀) %%p₁)
| (`(%%a₀ → %%a₁), `(%%b₀ → %%b₁)) :=
if ¬ a₁.has_var ∧ ¬ b₁.has_var then
p' ← mk_app `congr_arg [`(implies),p₀,p₁],
else unify a' b' >> add_refl r a' *> mk_mapp `rfl [none,a]
(do guard $ a'.get_app_fn.is_constant ∧
a'.get_app_fn.const_name = b'.get_app_fn.const_name,
(a'',pa') ← add_symm_proof r a',
mk_eq_symm pb >>= mk_eq_trans p'
meta def find_eq_type (r : tauto_state) : expr → list expr → tactic (expr × expr)
(prod.mk H <$> symm_eq r e t) <|> find_eq_type e Hs
private meta def contra_p_not_p (r : tauto_state) : list expr → list expr → tactic unit
do t ← (extract_opt_auto_param <$> infer_type H1) >>= whnf,
(H2,p) ← find_eq_type r a Hs,
H2 ← to_expr ``( (%%p).mpr %%H2 ),
pr ← mk_app `absurd [tgt, H2, H1],
meta def contradiction_with (r : tauto_state) : tactic unit :=
meta def contradiction_symm :=
using_new_ref (native.rb_map.mk _ _) contradiction_with
meta def assumption_with (r : tauto_state) : tactic unit :=
do { ctx ← local_context, (H,p) ← find_eq_type r t ctx,
mk_eq_mpr p H >>= tactic.exact }
<|> fail "assumption tactic failed"
meta def assumption_symm :=
using_new_ref (native.rb_map.mk _ _) assumption_with
Configuration options for `tauto`.
If `classical` is `tt`, runs `classical` before the rest of `tauto`.
`closer` is run on any remaining subgoals left by `tauto_core; basic_tauto_tacs`.
meta structure tauto_cfg :=
(closer : tactic unit := pure ())
meta def tautology (cfg : tauto_cfg := {}) : tactic unit := focus1 $ let basic_tauto_tacs : list (tactic unit) :=
[reflexivity, solve_by_elim,
constructor_matching none [``(_ ∧ _),``(_ ↔ _),``(Exists _),``(true)]],
tauto_core (r : tauto_state) : tactic unit :=
do try (contradiction_with r);
repeat (() <$ tactic.intro1);
casesm (some ()) [``(_ ∧ _),``(_ ∨ _),``(Exists _),``(false)];
try (contradiction_with r);
try (target >>= match_or >> refine ``( or_iff_not_imp_left.mpr _));
try (target >>= match_or >> refine ``( or_iff_not_imp_right.mpr _));
repeat (() <$ tactic.intro1);
constructor_matching (some ()) [``(_ ∧ _),``(_ ↔ _),``(true)];
do when cfg.classical classical,
using_new_ref (expr_map.mk _) tauto_core;
repeat (first basic_tauto_tacs); cfg.closer, done
local postfix `?`:9001 := optional
`tautology` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`.
This is a finishing tactic: it either closes the goal or raises an error.
The variant `tautology!` uses the law of excluded middle.
`tautology {closer := tac}` will use `tac` on any subgoals created by `tautology`that it is unable to solve before failing.
meta def tautology (c : parse $ (tk "!")?) (cfg : tactic.tauto_cfg := {}) :=tactic.tautology $ { classical := c.is_some, ..cfg }-- Now define a shorter name for the tactic `tautology`.
`tauto` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`.
This is a finishing tactic: it either closes the goal or raises an error.
The variant `tauto!` uses the law of excluded middle.
`tauto {closer := tac}` will use `tac` on any subgoals created by `tauto`that it is unable to solve before failing.
meta def tauto (c : parse $ (tk "!")?) (cfg : tactic.tauto_cfg := {}) : tactic unit :=This tactic (with shorthand `tauto`) breaks down assumptions of the form
`_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`. This is a finishing tactic: it
either closes the goal or raises an error.
The variants `tautology!` and `tauto!` use the law of excluded middle.
For instance, one can write:
example (p q r : Prop) [decidable p] [decidable r] : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (r ∨ p ∨ r) := by tauto
and the decidability assumptions can be dropped if `tauto!` is used
`tauto {closer := tac}` will use `tac` on any subgoals created by `tauto`that it is unable to solve before failing.
category := doc_category.tactic,
decl_names := [`tactic.interactive.tautology, `tactic.interactive.tauto],
tags := ["logic", "decision procedure"] }
