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.

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 | ]`

It worked! Thank you for the clarification :wink:

Last updated: Jun 15 2024 at 08:01 UTC