Top.Util.FSetNotin

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

Authors: Arthur Charguéraud and Brian Aydemir.

Implementation

Module Notin (X : FSetInterface.S).

Facts about set (non-)membership

Lemma in_singleton : ∀ x,
  In x (singleton x).

Lemma notin_empty : ∀ x,
  ¬ In x empty.

Lemma notin_union : ∀ x E F,
  ¬ In x E → ¬ In x F → ¬ In x (union E F).

Lemma elim_notin_union : ∀ x E F,
  ¬ In x (union E F) → (¬ In x E) ∧ (¬ In x F).

Lemma notin_singleton : ∀ x y,
  ¬ E.eq x y → ¬ In x (singleton y).

Lemma elim_notin_singleton : ∀ x y,
  ¬ In x (singleton y) → ¬ E.eq x y.

Lemma elim_notin_singleton' : ∀ x y,
  ¬ In x (singleton y) → x ≠ y.

Lemma notin_singleton_swap : ∀ x y,
  ¬ In x (singleton y) → ¬ In y (singleton x).

Rewriting non-membership facts

Lemma notin_singleton_rw : ∀ x y,
  ¬ In x (singleton y) ↔ ¬ E.eq x y.

Tactics

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

The tactic notin_solve solves goals of them form (x ≠ y) and (~ In x E) that are provable from hypotheses of the form destructed by notin_simpl_hyps.

Examples and test cases

Lemma test_notin_solve_1 : ∀ x E F G,
  ¬ In x (union E F) → ¬ In x G → ¬ In x (union E G).

Lemma test_notin_solve_2 : ∀ 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_notin_solve_3 : ∀ x y,
  ¬ E.eq x y → ¬ In x (singleton y) ∧ ¬ In y (singleton x).

Lemma test_notin_solve_4 : ∀ x y E F G,
  ¬ In x (union E (union (singleton x) F)) → ¬ In y G.

Lemma test_notin_solve_5 : ∀ x y E F,
  ¬ In x (union E (union (singleton y) F)) → ¬ In y E →
  ¬ E.eq y x ∧ ¬ E.eq x y.

End Notin.