fact: Definition solve_tauto : tactic := mfix0 solve_tauto : gtactic _ := (match_goal with | [[ |- True ] ] => ret I | [[? Q1 Q2 |- Q1 /\ Q2 ] ] => TT.apply (@conj _ _) <**> TT.by' solve_tauto <**> TT.by' solve_tauto | [[? Q1 Q2 |- Q1 \/ Q2 ] ] => mtry TT.apply (@or_introl _ _) <**> TT.by' solve_tauto with | TautoFail => TT.apply (@or_intror _ _) <**> TT.by' solve_tauto end | [[? (Q1 Q2 : Prop) |- Q1 -> Q2 ] ] => TT.by' (T.introsn 1 &> solve_tauto) | [[? X (Q : X -> Prop) |- (exists x : X, Q x)] ] => TT.by' (T.eexists &> [m: solve_tauto | T.idtac]) | [[? P | (p : P) |- P ] ] => TT.apply p | [[? G |- G ] ] => raise TautoFail end )%TT%MC.
imports: Mtac2(Mtac2 Ttactics Sorts) Coq(List)