I have a puzzling situation in Coq where I'm working with relations and ensembles. I have defined coercions between them and a tactic to solve membership goals:
Require Import Lia Reals Lra Classical_sets List Ensembles Relations_1.
Import ListNotations.
Notation "x ∈ A" := (In _ A x) (at level 40).
Notation "A ⋃ B" := (Union _ A B) (at level 30).
Notation "⦃⦄" := (Empty_set _).
Notation ℝ := R.
Fixpoint list_to_ensemble {U : Type} (l : list U) : Ensemble U :=
match l with
| [] => ⦃⦄
| x :: xs => Union U (Singleton U x) (list_to_ensemble xs)
end.
Notation "⦃ x ⦄" := (Singleton _ x).
Notation "⦃ x , y , .. , z ⦄" :=
(@list_to_ensemble _ (cons x (cons y .. (cons z nil) ..)))
(format "⦃ x , y , .. , z ⦄").
Lemma In_Union_def : forall (U : Type) (A B : Ensemble U) (x : U),
x ∈ (A ⋃ B) <-> x ∈ A \/ x ∈ B.
Proof.
intros; split; [apply Union_inv | intros [H1 | H1]; [apply Union_introl; auto | apply Union_intror; auto]].
Qed.
Coercion rel_to_ens {A} (R : Relation A) : Ensemble (A * A) :=
fun p => R (fst p) (snd p).
Coercion ens_to_rel {A} (E : Ensemble (A * A)) : Relation A :=
fun x y => E (x,y).
Lemma x_y_In_implies_rel : forall A (R : Relation A) x y, (x, y) ∈ R <-> R x y.
Proof.
intros; split; auto.
Qed.
Ltac solve_in_Union :=
simpl; auto;
match goal with
| [ |- ?x ∈ Singleton _ _ ] =>
apply Singleton_intro; (try reflexivity; try nia; try nra)
| [ |- ?x ∈ Union _ ?A ?B ] =>
apply In_Union_def; solve [ left; solve_in_Union | right; solve_in_Union ]
| [ |- ?G ] => fail "Goal not solvable"
end.
When proving a simple membership property:
Section Example.
Open Scope R_scope.
Let R : Relation ℝ := ⦃ (1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6) ⦄.
Lemma lemma_example : R 1 1.
Proof.
apply x_y_In_implies_rel. unfold R. try solve_in_Union.
assert ((1, 1) ∈ ⦃ (1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6) ⦄) as H1 by solve_in_Union.
auto.
Qed.
End Example.
When I try to solve the goal with try solve_in_Union, my goal is exactly:
(1, 1) ∈ ⦃(1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6)⦄
Strangely, using solve_in_Union directly on this goal fails. However, if I assert exactly the same goal text and try to prove it with solve_in_Union, it works:
Even more puzzling, if I pattern match the goal and print it:
match goal with
| [ |- ?G ] => idtac G
end.
It shows exactly the same text that works in the assertion. Why does solve_in_Union fail on the original goal but succeed on an assertion of the identical goal? What's the fundamental difference between these two seemingly identical situations?
As for the Coq version I am using, when I type coqc -v into the terminal I get
coqc -v The Coq Proof Assistant, version 8.19.2 compiled with OCaml 5.2.0
Doing Set Printing All. and take a sharp look at the goal we see
that in the first (non-working) case, the goal is
In (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
(@rel_to_ens RbaseSymbolsImpl.R
(@ens_to_rel RbaseSymbolsImpl.R
(@list_to_ensemble (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
(@cons (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
(@pair RbaseSymbolsImpl.R RbaseSymbolsImpl.R
(IZR (Zpos xH)) (IZR (Zpos xH)))
....
and in the second (working) case the goal is
In (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
(@list_to_ensemble (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
(@cons (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
(@pair RbaseSymbolsImpl.R RbaseSymbolsImpl.R (IZR (Zpos xH))
(IZR (Zpos xH)))
so it seems like somehow the coercions ens_to_rel and rel_to_ens get in the way of the unfolding that is needed for the matching to work.
Actually all that is quite a mouthful, and when we have spotted the problem it is better to just do Set Printing Coercions.
So the R is a Relation with a coercion, but the term in your assert is an Ensemble.
Definition your_R : Relation R := ⦃ (1,1), (1,2) ⦄.
Definition your_assert := ⦃ (1,1), (1,2) ⦄.
Set Printing All.
Print X.
Print Y.
prints
X = ens_to_rel ⦃(1, 1),(1, 2)⦄
: Relation ℝ
Y = ⦃(1, 1),(1, 2)⦄
: Ensemble (ℝ * ℝ)
There is no rule that matches the former which is why the Ltac solve_in_Union fails.
In particular, your goal is like
(1, 1) ∈ rel_to_ens (ens_to_rel ⦃(1, 1),(1, 2)⦄)
which cannot be simplified because the two coercions are not definitionally inverses. They are partially applied functions and cannot be further reduced.