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: Oct 04 2023 at 23:01 UTC