CODEWITHSUNDEEP
coqcoq-tacticcoqide
HouseCorgi
HouseCorgi

Reputation: 21

How to match implication without prior intros?

I am trying to write a tactic to check if my goal is an implication without having to introduce anything beforehand.

Furthermore I would like this tactic to be compatible with any amount of variables such that, for example, forall A B C D, (A/\B)->(C\/D) would still be considered as a valid form.

Ltac is_implication term :=
  match term with
  | ?A -> ?B => idtac term "is an implication"
  | _ => idtac term "is not an implication"; fail 1
  end.


Ltac universal_implication :=
  match goal with
  | [ |- forall _ , ?G]=>is_implication G
  | _=>idtac "Goal is not an universally quantified implication";fail 1
end.


Lemma toto: forall A B:Prop ,A->B.
universal_implication.

(*returns "Goal is not an universally quantified implication
Tactic failure".*)

Upvotes: 1

Views: 50

Answers (0)

Related Questions