Library FSetWeakNotin

Lemmas and tactics for working with and solving goals related to non-membership in finite sets. The main tactic of interest here is solve_notin.

Implicit arguments are declared by default in this library.

Original authors: Brian Aydemir and Arthur Chargu'eraud.





Require Import FSetInterface.

Implementation





Module Notin (Import X : FSetInterface.WS).

Facts about set non-membership





Lemma notin_empty : forall x,

  ~ In x empty.




Lemma notin_union : forall x E F,

  ~ In x E -> ~ In x F -> ~ In x (union E F).




Lemma elim_notin_union : forall x E F,

  ~ In x (union E F) -> (~ In x E) /\ (~ In x F).






Lemma notin_singleton : forall x y,

  ~ E.eq x y -> ~ In x (singleton y).






Lemma elim_notin_singleton : forall x y,

  ~ In x (singleton y) -> ~ E.eq x y.






Lemma elim_notin_singleton' : forall x y,

  ~ In x (singleton y) -> x <> y.








Lemma notin_add : forall x y F,

  ~ E.eq y x -> ~ In x F -> ~ In x (add y F).






Lemma elim_notin_add : forall x y F,

  ~ In x (add y F) -> ~ E.eq y x /\ ~ In x F.






Lemma elim_notin_add' : forall x y F,

  ~ In x (add y F) -> y <> x /\ ~ In x F.

Tactics

The tactic destruct_notin destructs all hypotheses of the form (~ In x E), where E is built using only empty, add, union, and singleton.





Ltac destruct_notin :=

  match goal with

    | H: In ?x ?E -> False |- _ =>

      change (~ In x E) in H;

      destruct_notin

    | H: ~ In _ empty |- _ =>

      clear H;

      destruct_notin

    | H: ~ In ?x (union ?E ?F) |- _ =>

      destruct (@elim_notin_union x E F H);

      clear H;

      destruct_notin

    | H: ~ In ?x (singleton ?y) |- _ =>

      let F1 := fresh in

      let F2 := fresh in

      assert (F1 := @elim_notin_singleton x y H);

      assert (F2 := @elim_notin_singleton' x y H);

      clear H;

      destruct_notin

    | H: ~ In ?x (add ?y ?F) |- _ =>

      destruct (@elim_notin_add x y F H);

      destruct (@elim_notin_add' x y F H);

      clear H;

      destruct_notin

    | _ =>

      idtac

  end.

The tactic solve_notin solves goals of them form (x <> y) and (~ In x E) that are provable from hypotheses of the form destructed by destruct_notin.





Ltac solve_notin :=

  destruct_notin;

  repeat (progress (  apply notin_empty

                   || apply notin_union

                   || apply notin_singleton

                   || apply notin_add));

  solve [ trivial | congruence | intuition auto ].

Examples and test cases

These examples and test cases are not meant to be exhaustive.





Lemma test_solve_notin_1 : forall x E F G,

  ~ In x (union E F) -> ~ In x G -> ~ In x (union E G).






Lemma test_solve_notin_2 : forall x y E F G,

  ~ In x (union E (union (singleton y) F)) -> ~ In x G ->

  ~ In x (singleton y) /\ ~ In y (singleton x).






Lemma test_solve_notin_3 : forall x y,

  ~ E.eq x y -> ~ In x (singleton y) /\ ~ In y (singleton x).






Lemma test_solve_notin_4 : forall x y E F G,

  ~ In x (union E (union (singleton x) F)) -> ~ In y G.






Lemma test_solve_notin_5 : forall x y E F,

  ~ In x (union E (union (singleton y) F)) -> ~ In y E ->

  ~ E.eq y x /\ ~ E.eq x y.






Lemma test_solve_notin_6 : forall x y E,

  ~ In x (add y E) -> ~ E.eq x y /\ ~ In x E.






End Notin.

This page has been generated by coqdoc