# Library CoindTactic

The coind tactic again (very slightly improved). See CoindStart for an explanation how this works.

Lemma exists_forall_impl : forall A (P : A -> Prop) (Q : Prop),
((exists x, P x) -> Q) -> forall x : A, P x -> Q.
Proof. firstorder. Qed.

Tactic Notation "if" tactic(t) "then" tactic(t1) "else" tactic(t2) :=
first [ t; first [ t1 | fail 2 ] | t2 ].

Tactic Notation "if_is_not_var" tactic(t) "then" tactic(t1) :=
if (is_var t) then idtac else t1.

Ltac step1_arity2 :=
match goal with
| [|- ?P ?s ?s] => remember s in * |- * at 1
| [|- ?P ?s1 ?s2] =>
(if_is_not_var s1 then remember s1);
(if_is_not_var s2 then remember s2)
end.

Ltac step1_arity1 :=
match goal with
| [|- ?P ?s] =>
if_is_not_var s then remember s
end.

Ltac step2conjn :=
match goal with
| [H : ?P |- ?R] =>
match type of P with
| Prop =>
match R with
| ?Q -> ?R =>
let J := fresh "J" in
intro J; cut (P /\ Q); [clear H J | tauto]
| _ => generalize dependent H
end
| _ => fail
end
end.

Ltac step2exn_arity2 :=
match goal with
| [s1 : _, s2 : _, x : ?T |- ?Q -> ?P ?s1 ?s2] =>
generalize dependent x; apply exists_forall_impl
| [s1 : _, s2 : _, x : ?T |- ?P ?s1 ?s2] =>
clear x
end.

Ltac step2exn_arity1 :=
match goal with
| [s : _, x : ?T |- ?Q -> ?P ?s] =>
generalize dependent x; apply exists_forall_impl
| [s : _, x : ?T |- ?P ?s] =>
clear x
end.

Ltac step2_arity2 :=
repeat step2conjn; repeat step2exn_arity2.

Ltac step2_arity1 :=
repeat step2conjn; repeat step2exn_arity1.

Ltac step3_arity2 X :=
match goal with
| [|- ?Q -> ?P ?s1 ?s2] =>
generalize dependent s2; generalize dependent s1;
apply X
| [|- ?P ?s1 ?s2] =>
generalize dependent s2; generalize dependent s1;
apply X
end.

Ltac step3_arity1 X :=
match goal with
| [|- ?Q -> ?P ?s] => generalize dependent s; apply X
| [|- ?P ?s] => generalize dependent s; apply X
end.

Ltac destrs :=
match goal with
| [H : exists x, _ |- _] => destruct H
| [H : _ /\ _ |- _] => destruct H
| [H : True |- _] => destruct H
end.

Ltac post := intros; repeat destrs; subst; simpl in *.

Tactic Notation "coind2" "using" constr(X) :=
intros; step1_arity2; step2_arity2; step3_arity2 X; post.

Tactic Notation "coind1" "using" constr(X) :=
intros; step1_arity1; step2_arity1; step3_arity1 X; post.

(* guess the arity of the co-inductive predicate *)
Tactic Notation "coind" "using" constr(X) :=
intros; match goal with
| [|- ?P ?x ?y] => coind2 using X
| [|- ?P ?x] => coind1 using X
end.