## Stream: Coq users

### Topic: Ltac for set-theoretical reasoning

#### João Mendes (Feb 24 2023 at 19:36):

I am trying to develop a proof-system in ND-style for set-theoretical reasoning in Coq. As the core, I am using the Library Coq.Sets.Ensembles. My idea is to implement the rules of the system using Ltac and the problem I am facing now is to implement the following rule (the elimination of intersection):
inter_elim.png

Then, what I want to do is to define a new tactic which transform a goal $x \in A$ into $x \in A \cap B$. Using common tactics, I've managed to do it this way:

  Theorem inter_elim2 : forall (x : U) (A B : Ensemble), In (Intersection A B) x ->
In A x.
Proof.
intros.
assert (H0 : In (Intersection A B) x -> In A x).
intro H1.
elim H1.
intros; auto.
apply H0.


But, when I enconde such sequence in a Ltac as the following:

 Ltac ltac_inter_elim2 B :=
match goal with
| |- In ?A ?x =>
let H := fresh "H" in
let H0 := fresh "H0" in
assert (H : In (Intersection A B) x -> In A x);
intro H0
end.


And try to use it in a theorem:

  Theorem inter_elim2' : forall (x : U) (A B : Ensemble), In (Intersection A B) x ->
In A x.
Proof.
intros.
ltac_inter_elim2 B.


The message "No product even after head-reduction." shows and I am not getting why. Can someone help me?

When I define the Ltac like this:

 Ltac ltac_inter_elim2 B :=
match goal with
| |- In ?A ?x =>
let H := fresh "H" in
let H0 := fresh "H0" in
assert (H : In (Intersection A B) x -> In A x)
end.


No error is raised, though this is not what I want of course.

#### Gaëtan Gilbert (Feb 24 2023 at 19:41):

after assert you have 2 goals: the one to prove what you asserted, and the original with an added hypothesis
the intros fails on the second goal
instead do assert (H : ...);[intros H0 | ]

#### João Mendes (Feb 24 2023 at 19:46):

It worked! Thank you for the clarification :wink:

Last updated: Jun 15 2024 at 08:01 UTC