fact: Definition solve_tauto : forall {P:Prop}, ttac P := mfix1 solve_tauto (P : Prop) : M _ := mmatch P in Prop as P' return ttac P' with | True => apply I | [? Q1 Q2] Q1 /\ Q2 => apply (@conj _ _) <**> solve_tauto Q1 <**> solve_tauto Q2 | [? Q1 Q2] Q1 \/ Q2 => mtry q1 <- apply (@or_introl _ _) <**> solve_tauto Q1; mif has_open_subgoals q1 then raise TautoFail else ret q1 with TautoFail => apply (@or_intror _ _) <**> solve_tauto Q2 end | [? (Q1 Q2 : Prop)] Q1 -> Q2 => tintro (fun x:Q1=> solve_tauto Q2) | [? X (Q : X -> Prop)] (exists x : X, Q x) => x <- M.evar X; q <- apply (@ex_intro _ _ _) <**> solve_tauto (Q x); promote_uninst_evar x q | _ => TT.use (T.try T.assumption) end.
imports: Mtac2(Mtac2 Ttactics Sorts) Coq(List)