blob: 915f58df9e18e7bfa3472479072ec68d9dbddfb7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B)
:= fun x y => match x, y with
| inl x', inl y' => RA x' y'
| inr x', inr y' => RB x' y'
| _, _ => False
end.
Global Instance Equivalence_sumwise {A B} {RA:relation A} {RB:relation B}
{RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB}
: Equivalence (sumwise RA RB).
Proof.
split; repeat intros [?|?]; simpl; trivial; destruct RA_equiv, RB_equiv; try tauto; eauto.
Qed.
Arguments sumwise {A B} _ _ _ _.
Ltac congruence_sum_step :=
match goal with
| [ H : inl _ = inr _ |- _ ] => solve [ inversion H ]
| [ H : inr _ = inl _ |- _ ] => solve [ inversion H ]
| [ H : inl _ = inl _ |- _ ] => inversion H; clear H
| [ H : inr _ = inr _ |- _ ] => inversion H; clear H
end.
Ltac congruence_sum := repeat congruence_sum_step.
|
