The Coq Proof Assistant

# Library Coq.Init.Tauto

# The tauto and intuition tactics

Require Import Notations.
Require Import Ltac.
Require Import Datatypes.
Require Import Logic.
Local Ltac not_dep_intros :=
repeat match goal with
| |- (forall (_: ?X1), ?X2) => intro
| |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
end.
Local Ltac axioms flags :=
match reverse goal with
| |- ?X1 => is_unit_or_eq flags X1; constructor 1
| H:?X1 |- _ => is_empty flags X1; elim H
| _ => assumption
end.
Local Ltac simplif flags :=
not_dep_intros;
repeat
(match reverse goal with
| id: ?X1 |- _ => is_conj flags X1; elim id; do 2 intro; clear id
| id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
| id: (Coq.Init.Logic.not _) |- _ => red in id
| id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id
| _ =>
find_cut ltac:(fun id0 id1 X2 =>
assert X2; [exact (id0 id1) | clear id0]
)
| id: forall (_ : ?X1), ?X2|- _ =>
is_unit_or_eq flags X1; cut X2;
[ intro; clear id
|
cut X1; [exact id| constructor 1; fail]
]
| id: forall (_ : ?X1), ?X2|- _ =>
flatten_contravariant_conj flags X1 X2 id
| id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ =>
assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3)
by (do 2 intro; apply id; split; assumption);
clear id
| id: forall (_:?X1), ?X2|- _ =>
flatten_contravariant_disj flags X1 X2 id
| |- ?X1 => is_conj flags X1; split
| |- (Coq.Init.Logic.iff _ _) => split
| |- (Coq.Init.Logic.not _) => red
end;
not_dep_intros).
Local Ltac tauto_intuit flags t_reduce t_solver :=
let rec t_tauto_intuit :=
(simplif flags; axioms flags
|| match reverse goal with
| id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
cut X3;
[ intro; clear id; t_tauto_intuit
| cut (forall (_: X1), X2);
[ exact id
| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
solve [ t_tauto_intuit ]]]
| id:forall (_:not ?X1), ?X3|- _ =>
cut X3;
[ intro; clear id; t_tauto_intuit
| cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]]
| |- ?X1 =>
is_disj flags X1; solve [left;t_tauto_intuit | right;t_tauto_intuit]
end
||
match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit
| |- _ => t_reduce;t_solver
end
||
t_solver
) in t_tauto_intuit.
Local Ltac intuition_gen flags solver := tauto_intuit flags reduction_not_iff solver.
Local Ltac tauto_intuitionistic flags := intuition_gen flags fail || fail "tauto failed".
Local Ltac tauto_classical flags :=
(apply_nnpp || fail "tauto failed"); (tauto_intuitionistic flags || fail "Classical tauto failed").
Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flags.
Ltac tauto := with_uniform_flags ltac:(fun flags => tauto_gen flags).
Ltac dtauto := with_power_flags ltac:(fun flags => tauto_gen flags).
Ltac intuition_solver :=
first [solve [auto]
| tryif solve [auto with *] then warn_auto_with_star else idtac].
Local Ltac intuition_then tac := with_uniform_flags ltac:(fun flags => intuition_gen flags tac).
Ltac intuition := intuition_then ltac:(idtac;intuition_solver).
Local Ltac dintuition_then tac := with_power_flags ltac:(fun flags => intuition_gen flags tac).
Ltac dintuition := dintuition_then ltac:(idtac;intuition_solver).
Tactic Notation "intuition" := intuition.
Tactic Notation "intuition" tactic(t) := intuition_then t.
Tactic Notation "dintuition" := dintuition.
Tactic Notation "dintuition" tactic(t) := dintuition_then t.