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.