Autosubst.Autosubst_MMap
Apply a function to all instances of a type A occuring in a type B.
This is used to implement term structures with containers, e.g.
Inductive term := C (xs : list term)
By default we provide mmap instances for option, list, pair and
the codomain of a function. For additional inductive types, there is
a derive tactic to generate new mmap instances.
Require Import Autosubst_Basics.
Class MMap (A B: Type) := mmap : (A -> A) -> B -> B.
Arguments mmap {A B _} f !s /.
Class MMap (A B: Type) := mmap : (A -> A) -> B -> B.
Arguments mmap {A B _} f !s /.
Extensionality for mmap. This Lemma is uninteresting, as it is implied by
functional extensionality. However, instances of this class should be
transparent and take the proof of [forall t, f t = gt] as a non-recursive
argument. This is sufficient to allow the fixpoint checker to lift proofs
over mmap.
Class MMapExt (A B : Type) `{MMap A B} :=
mmap_ext : forall f g,
(forall t, f t = g t) -> forall s, mmap f s = mmap g s.
Arguments mmap_ext {A B _ _ f g} H s.
Class MMapLemmas (A B : Type) `{MMap A B} := {
mmap_id x : mmap id x = x;
mmap_comp f g x : mmap f (mmap g x) = mmap (g >>> f) x
}.
mmap_ext : forall f g,
(forall t, f t = g t) -> forall s, mmap f s = mmap g s.
Arguments mmap_ext {A B _ _ f g} H s.
Class MMapLemmas (A B : Type) `{MMap A B} := {
mmap_id x : mmap id x = x;
mmap_comp f g x : mmap f (mmap g x) = mmap (g >>> f) x
}.
MMap Lemmas
Section LemmasForMMap.
Context {A B : Type}.
Context {MMap_Inst : MMap A B} {MMapLemmas_Inst : MMapLemmas A B}.
Lemma mmap_idX : mmap id = id.
Proof. f_ext. exact mmap_id. Qed.
Lemma mmap_compX f g : mmap f >>> mmap g = mmap (f >>> g).
Proof. f_ext. apply mmap_comp. Qed.
Lemma mmap_compR {C} f g (h : _ -> C) :
mmap f >>> mmap g >>> h = mmap (f >>> g) >>> h.
Proof. now rewrite <- mmap_compX. Qed.
End LemmasForMMap.
Identity Instance
Section MMapId.
Context {A : Type}.
Global Instance MMap_refl : MMap A A := id.
Global Instance MMapLemmas_refl : MMapLemmas A A. now constructor. Qed.
Global Instance MMapExt_refl : MMapExt A A. hnf. tauto. Defined.
End MMapId.
Arguments MMap_refl _ _ f /.
Lemma mmap_id_instE {A} f : @mmap _ _ (@MMap_refl A) f = f. reflexivity. Qed.
Constant Instance: mmap f x just ignores f and leaves x unchanged.
This instance has low priority so that it is just used if there is
no alternative.
Section MMapConst.
Context {A B: Type}.
Global Instance MMap_const : MMap A B | 100 := fun _ => id.
Global Instance MMapLemmas_const : MMapLemmas A A. now constructor. Qed.
Global Instance MMapExt_const : MMapExt A A. hnf. tauto. Defined.
End MMapConst.
Arguments MMap_const _ _ f x /.
Lemma mmap_const_instE {A B} f x : @mmap _ _ (@MMap_const A B) f x = x. reflexivity. Qed.
Simplify mmap expressions
Ltac mmap_typeclass_normalize :=
repeat match goal with
| [|- appcontext[@mmap ?A ?B _ ?f]] =>
let s := constr:(@mmap A B _ f) in progress change (@mmap A B _ f) with s
end.
Ltac mmap_typeclass_normalizeH H :=
repeat match typeof H with
| appcontext[@mmap ?A ?B _ ?f] =>
let s := constr:(@mmap A B _ f) in progress change (@mmap A B _ f) with s
end.
Hint Rewrite @mmap_id_instE @mmap_const_instE : mmap.
Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR
using exact _ : mmap.
Hint Rewrite @mmap_id_instE @mmap_const_instE : autosubst.
Hint Rewrite @mmap_id @mmap_comp @mmap_idX @mmap_compX @mmap_compR
using exact _ : autosubst.
Ltac msimpl :=
mmap_typeclass_normalize;
repeat first
[ solve [trivial]
| progress (simpl; autorewrite with mmap)
| fold_id].
Ltac msimplH H :=
mmap_typeclass_normalizeH H;
repeat first
[ solve [trivial]
| progress (simpl; autorewrite with mmap in H)
| fold_id in H].
Tactic Notation "msimpl" "in" ident(H) := msimplH H.
Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl.
Deriving Instances
Ltac derive_MMap :=
hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] =>
intros f; fix map 1; intros xs; change (annot B xs); destruct xs;
match goal with
| [ |- annot _ ?ys ] =>
let rec tmap xs :=
(match xs with
| ?s1 ?s2 =>
let s1 := tmap s1 in
let T := typeof s2 in
let s2 :=
match T with
| A => constr:(f s2)
| B => constr:(map s2)
| _ => constr:(mmap f s2)
end in
constr:(s1 s2)
| _ => xs
end) in
let ys := tmap ys in exact ys
end
end.
Hint Extern 0 (MMap _ _) => derive_MMap : derive.
Ltac derive_MMapLemmas := constructor;
[ induction 0; simpl; f_equal; trivial; apply mmap_id
| intros f g; induction 0; simpl; f_equal; trivial; apply mmap_comp ].
Hint Extern 0 (MMapLemmas _ _) => derive_MMapLemmas : derive.
Ltac derive_MMapExt :=
intros ???; fix 1; destruct 0; simpl; f_equal; auto using mmap_ext.
Hint Extern 0 (MMapExt _ _) => derive_MMapExt : derive.
(* Local Variables: *)
(* coq-load-path: (("." "Autosubst")) *)
(* End: *)