Library deBruijn_Isomorphism
This file provides a connection between the generic level
and many concrete type systems based on some isomorphisms.
A concrete type system TT is isomorphic to the type representation RR when there is an isomorphism between TT and Interpret RR.
A concrete type system TT is isomorphic to the type representation RR when there is an isomorphism between TT and Interpret RR.
Open Scope type_scope.
The following section collects all the functions and predicates
which can be defined and handled generically.
The section can be extended when new concept is created generically.
Isomorphisms between a representation and a concrete types/terms.
Function injectivity
Given a type TT and a representation type RR,
- From : TT -> Interpret RR, an one-to-one function
- To : Interpret RR -> TT, an one-to-one functioen when restricted to Image of From
- To (From x) = x, hence
- From (To (From x)) = From x
Module Type Iso_partial.
Parameter TT : Type.
Parameter RR : Rep.
Parameter From : TT -> Interpret RR.
Parameter From_inj : fun_inj From.
Parameter To : Interpret RR -> TT.
Parameter To_From : forall (T:TT), To (From T) = T.
Definition ISO : Iso TT (Interpret RR) := (From, To).
Hint Rewrite To_From : isorew.
Hint Resolve To_From.
End Iso_partial.
If there are variables, then From and To build a real
isomorphism between TT and Interpret RR.
- From and To are one-to-one and onto.
- To (From} x) = x.
Module Type Iso_full.
Include Type Iso_partial.
Parameter From_To : forall (T:Interpret RR), From (To T) = T.
Parameter To_inj : fun_inj To.
Hint Rewrite From_To : isorew.
Hint Resolve From_To.
End Iso_full.
Isomorphism for nat will be the basic for other isomorphisms.
Module Iso_nat.
Definition TT := nat.
Definition RR :=
PLUS
UNIT
REC.
Fixpoint From (T: TT) : Interpret RR :=
match T with
| O => Term (InL _ Unit)
| S n => Term (InR _ (Rec (From n)))
end.
The following definition using a garbage for never-appearing cases
is simpler than other, more accurate variations.
Fixpoint To_ (T : InterpretRep RR RR) : TT :=
match T return _ with
| InL _ _ Unit => 0
| InR _ _ (Rec U) => S (To U)
| _ => 0
end
with To (T:Interpret RR) : TT :=
match T with
| Var _ => 0
| Term U => To_ U
end.
Lemma To_From : forall (T:TT), To (From T) = T.
Proof.
intro T; induction T; simpl; f_equal; auto.
Qed.
End Iso_nat.
For automation
Lemma Iso_nat_REC : Iso_nat.RR <> REC.
Proof.
unfold Iso_nat.RR; congruence.
Qed.
Hint Resolve Iso_nat_REC.
Hint Resolve Iso_nat.To_From.
Hint Rewrite Iso_nat.To_From : iso_module.
specialized tactics for the proof of From_To.
Ltac from_to_Rep T H :=
dependent destruction T;
destruct T;
try discriminate;
repeat (
match goal with
| [H : InterpretRep _ _ |- _] => destruct H; try discriminate
end);
simpl;
match goal with
| H : PLUS _ _ = _ |- _ => inversion H; subst
end;
try (
match goal with
| q : QQ |- _ => destruct q
end);
match goal with
| H : JMeq _ _ |- _ => rewrite <- (JMeq_eq H); simpl
end;
try repeat rewrite H; auto;
try autorewrite with iso_module; auto.
Ltac from_to T H:=
let v := fresh "v" in
destruct T as [v | ]; simpl;
[destruct v | idtac]; auto using H.