Require Import List.
Require Import Setoid.
Require Import Axioms.
Require Export Atoms.
Section Swap.
Variable A : AtomT.
Variable X : Set.
Record SwapT : Set := mkSwap {
swap : (A * A) -> X -> X;
swap_same : forall a x, swap (a, a) x = x;
swap_invol : forall ab x, swap ab (swap ab x) = x;
swap_distrib :
forall ab c d x,
swap ab (swap (c, d) x) =
swap (swapa A ab c, swapa A ab d) (swap ab x)
}.
Variable S : SwapT.
Lemma swap_same' :
forall a b x, a = b -> swap S (a, b) x = x.
Lemma swap_invol' :
forall a b c d x, a = c -> b = d -> swap S (a, b) (swap S (c, d) x) = x.
Lemma swap_injective : forall ab x y, swap S ab x = swap S ab y -> x = y.
Lemma swap_move_left : forall ab x y, swap S ab x = y -> x = swap S ab y.
Lemma swap_move_right : forall ab x y, x = swap S ab y -> swap S ab x = y.
Lemma swap_switch : forall a b x, swap S (a, b) x = swap S (b, a) x.
Lemma swap_switch_invol : forall a b x, swap S (a, b) (swap S (b, a) x) = x.
Lemma swap_switch_invol' :
forall a b c d x, a = d -> b = c -> swap S (a, b) (swap S (c, d) x) = x.
Lemma swap_undistrib :
forall a b cd x,
swap S (a, b) (swap S cd x) =
swap S cd (swap S (swapa A cd a, swapa A cd b) x).
End Swap.
Implicit Arguments mkSwap [A X].
Implicit Arguments swap [A X].
Implicit Arguments swap_same [A X].
Implicit Arguments swap_invol [A X].
Implicit Arguments swap_distrib [A X].
Implicit Arguments swap_same' [A X a b].
Implicit Arguments swap_invol' [A X a b c d].
Implicit Arguments swap_injective [A X S ab x y].
Implicit Arguments swap_move_left [A X].
Implicit Arguments swap_move_right [A X].
Implicit Arguments swap_switch [A X].
Implicit Arguments swap_switch_invol [A X].
Implicit Arguments swap_switch_invol' [A X a b c d].
Implicit Arguments swap_undistrib [A X].
Hint Resolve swap_same swap_invol swap_distrib : nominal.
Hint Immediate swap_injective swap_move_left swap_move_right : nominal.
Hint Resolve swap_switch swap_switch_invol swap_undistrib : nominal.
Hint Rewrite swap_same : nominal.
Hint Rewrite swap_invol : nominal.
Hint Rewrite swap_same' using congruence : nominal.
Hint Rewrite swap_invol' using congruence : nominal.
Hint Rewrite swap_switch_invol : nominal.
Hint Rewrite swap_switch_invol' using congruence : nominal.
Ltac autorewrite_swap_in_hyp :=
repeat (
match goal with
| H : context [swap ?S (?a, ?a) ?x] |- _ =>
rewrite (@swap_same _ _ S a x) in H
| H : context [swap ?S (?a, ?b) (swap ?S (?a, ?b) ?x)] |- _ =>
rewrite (@swap_switch _ _ S (a, b) x) in H
| H : context [swap ?S (?a, ?b) (swap ?S (?b, ?a) ?x)] |- _ =>
rewrite (@swap_switch_invol _ _ S a b x) in H
| H : context [swap ?S (?a, ?b) ?x] |- _ =>
rewrite (@swap_same' _ _ S a b x) in H;
[idtac | solve [congruence]]
| H : context [swap ?S (?a, ?b) (swap ?S (?c, ?d) ?x)] |- _ =>
(rewrite (@swap_invol _ _ S a b c d x) in H;
[idtac | solve [congruence] | solve [congruence]]) ||
(rewrite (@swap_switch_invol _ _ S a b c d x) in H;
[idtac | solve [congruence] | solve [congruence]])
end).
Swapping on atoms |
Section AtomSwap.
Variable A : AtomT.
Variables a b c : atom A.
Definition mkAtomSwap :=
mkSwap
(swapa A)
(@swapa_same A)
(@swapa_invol A)
(@swapa_distrib A).
Lemma atom_swap_left : swap mkAtomSwap (a, b) a = b.
Lemma atom_swap_left' : a = c -> swap mkAtomSwap (a, b) c = b.
Lemma atom_swap_right : swap mkAtomSwap (a, b) b = a.
Lemma atom_swap_right' : b = c -> swap mkAtomSwap (a, b) c = a.
Lemma atom_swap_neither : a <> c -> b <> c -> swap mkAtomSwap (a, b) c = c.
End AtomSwap.
atom_swap_simpl_once is just an auxilary tactic.
|
Ltac atom_swap_simpl_once a b c :=
(rewrite (@atom_swap_left _ a b)) ||
(rewrite (@atom_swap_left' _ a b c);
[idtac | solve [congruence]]) ||
(rewrite (@atom_swap_right _ a b)) ||
(rewrite (@atom_swap_right' _ a b c);
[idtac | solve [congruence]]) ||
(rewrite (@atom_swap_neither _ a b c);
[idtac | solve [congruence] | solve [congruence]]).
Ltac atom_swap_simpl_hyp H a b c :=
(rewrite (@atom_swap_left _ a b) in H) ||
(rewrite (@atom_swap_left' _ a b c) in H;
[idtac | solve [congruence]]) ||
(rewrite (@atom_swap_right _ a b) in H) ||
(rewrite (@atom_swap_right' _ a b c) in H;
[idtac | solve [congruence]]) ||
(rewrite (@atom_swap_neither _ a b c) in H;
[idtac | solve [congruence] | solve [congruence]]).
atom_swap_simpl performs all reductions of atom swaps (in the goal or in
the hypotheses) for which the result is inferrable from the context using
the congruence tactic.
|
Ltac atom_swap_simpl :=
repeat (
match goal with
| |- context [swap (mkAtomSwap _) (?a, ?b) ?c] =>
atom_swap_simpl_once a b c
| H : context [swap (mkAtomSwap _) (?a, ?b) ?c] |- _ =>
atom_swap_simpl_hyp H a b c
end).
atom_swap_case H1 H2 a b c will reduce all expressions of the form
atom_swap _ (a, b) c to either a, b, or c, splitting the goal
as necessary, when the relationships between a and c and between
b and c cannot be inferred from the context. H1 will be used
as the name for a newly introduced assumption about the relationship
between a and c, and respectively H2 for b and c. Also,
any additional reductions of atom swaps that are inferrable from the
context will be performed.
|
Ltac atom_swap_case H1 H2 a b c :=
atom_swap_simpl;
try match goal with
| |- context [swap (mkAtomSwap _) (a, b) c] =>
case (atom_eqdec _ a c); intro H1; try congruence;
atom_swap_simpl;
try match goal with
| |- context [swap (mkAtomSwap _) (a, b) c] =>
case (atom_eqdec _ b c); intro H2; try congruence;
atom_swap_simpl
end
end.
| The identity swap |
Section IdSwap.
Variable A : AtomT.
Variable X : Set.
Definition id_swap (s : A * A) (x : X) := x.
Lemma id_swap_same : forall a x, id_swap (a, a) x = x.
Lemma id_swap_invol : forall ab x, id_swap ab (id_swap ab x) = x.
Lemma id_swap_distrib :
forall ab c d x,
id_swap ab (id_swap (c, d) x) =
id_swap (swapa A ab c, swapa A ab d) (id_swap ab x).
Definition mkIdSwap :=
mkSwap
id_swap
id_swap_same
id_swap_invol
id_swap_distrib.
Lemma id_swap_reduce :
forall ab x,
swap mkIdSwap ab x = x.
End IdSwap.
Implicit Arguments id_swap [A X].
Implicit Arguments id_swap_same [A X].
Implicit Arguments id_swap_invol [A X].
Implicit Arguments id_swap_distrib [A X].
Implicit Arguments id_swap_reduce [A X].
Hint Resolve id_swap_same id_swap_invol id_swap_distrib : nominal.
Hint Rewrite id_swap_same id_swap_invol id_swap_reduce : nominal.
id_swap_simpl performs all reductions of id swaps (in the goal or in
the hypotheses) for which the result is inferrable from the context using
the congruence tactic.
|
Ltac id_swap_simpl :=
repeat (
match goal with
| |- context [swap (mkIdSwap _) (?a, ?b) ?x] =>
rewrite (@id_swap_reduce _ _ (a, b) x)
| H : context [swap (mkIdSwap _) (?a, ?b) ?x] |- _ =>
rewrite (@id_swap_reduce _ _ (a, b) x) in H
end).
Swapping on pairs |
Section PairSwap.
Variable A : AtomT.
Variable X : Set.
Variable XS : SwapT A X.
Variable Y : Set.
Variable YS : SwapT A Y.
Definition pair_swap (s : atom A * atom A) (p : X * Y) :=
let (x, y) := p in (swap XS s x, swap YS s y).
Lemma pair_swap_same : forall a p, pair_swap (a, a) p = p.
Lemma pair_swap_invol : forall ab p, pair_swap ab (pair_swap ab p) = p.
Lemma pair_swap_distrib :
forall ab c d p,
pair_swap ab (pair_swap (c, d) p) =
pair_swap (swapa A ab c, swapa A ab d) (pair_swap ab p).
Definition mkPairSwap :=
mkSwap
pair_swap
pair_swap_same
pair_swap_invol
pair_swap_distrib.
End PairSwap.
Implicit Arguments pair_swap [A X Y].
Implicit Arguments pair_swap_same [A X Y].
Implicit Arguments pair_swap_invol [A X Y].
Implicit Arguments pair_swap_distrib [A X Y].
Implicit Arguments mkPairSwap [A X Y].
Hint Resolve pair_swap_same pair_swap_invol pair_swap_distrib : nominal.
Hint Rewrite pair_swap_same pair_swap_distrib : nominal.
Notation "X ^* Y" := (mkPairSwap X Y) (at level 50, left associativity).
Swapping on lists |
Section ListSwap.
Variable A : AtomT.
Variable X : Set.
Variable XS : SwapT A X.
Fixpoint list_swap (s : A * A) (ls : list X) {struct ls} : list X :=
match ls with
| nil => nil
| x :: ls' => swap XS s x :: list_swap s ls'
end.
Lemma list_swap_same : forall a ls, list_swap (a, a) ls = ls.
induction ls.
simpl...
simpl; rewrite (swap_same XS); rewrite IHls...
Qed.
Lemma list_swap_invol : forall ab ls, list_swap ab (list_swap ab ls) = ls.
induction ls.
simpl...
simpl; rewrite (swap_invol XS); rewrite IHls...
Qed.
Lemma list_swap_distrib :
forall ab c d ls,
list_swap ab (list_swap (c, d) ls) =
list_swap (swapa A ab c, swapa A ab d) (list_swap ab ls).
induction ls.
simpl...
simpl; rewrite (swap_distrib XS); rewrite IHls...
Qed.
Definition mkListSwap :=
mkSwap
list_swap
list_swap_same
list_swap_invol
list_swap_distrib.
Lemma list_swap_In :
forall xs x ab,
List.In x xs <-> List.In (swap XS ab x) (list_swap ab xs).
End ListSwap.
Implicit Arguments list_swap [A X].
Implicit Arguments list_swap_same [A X].
Implicit Arguments list_swap_invol [A X].
Implicit Arguments list_swap_distrib [A X].
Implicit Arguments mkListSwap [A X].
Hint Resolve list_swap_same list_swap_invol list_swap_distrib : nominal.
Hint Rewrite list_swap_same list_swap_invol : nominal.
Swapping on functions. |
Section FunctionSwap.
Variable A : AtomT.
Variable X : Set.
Variable XS : SwapT A X.
Variable Y : Set.
Variable YS : SwapT A Y.
Definition func_swap (s : atom A * atom A) (f : X -> Y) (x : X) :=
swap YS s (f (swap XS s x)).
Lemma func_swap_same : forall a f, func_swap (a, a) f = f.
Lemma func_swap_invol : forall ab f, func_swap ab (func_swap ab f) = f.
Lemma func_swap_distrib :
forall ab c d f,
func_swap ab (func_swap (c, d) f) =
func_swap (swapa A ab c, swapa A ab d) (func_swap ab f).
Definition mkFuncSwap :=
mkSwap
func_swap
func_swap_same
func_swap_invol
func_swap_distrib.
Lemma swap_app :
forall ab f x,
swap YS ab (f x) = (swap mkFuncSwap ab f) (swap XS ab x).
Lemma swap_func :
forall ab f x,
(swap mkFuncSwap ab f) x = swap YS ab (f (swap XS ab x)).
End FunctionSwap.
Implicit Arguments func_swap [A X Y].
Implicit Arguments func_swap_same [A X Y].
Implicit Arguments func_swap_invol [A X Y].
Implicit Arguments func_swap_distrib [A X Y].
Implicit Arguments mkFuncSwap [A X Y].
Implicit Arguments swap_app [A X Y].
Implicit Arguments swap_func [A X Y].
Hint Resolve func_swap_same func_swap_invol func_swap_distrib : nominal.
Hint Rewrite func_swap_same func_swap_invol : nominal.
Hint Resolve swap_app swap_func : nomimal.
Notation "X ^-> Y" := (mkFuncSwap X Y) (at level 90, right associativity).