Tealeaves.Examples.STLC.Language
From Tealeaves Require Export
Singlesorted.Theory.Product
LN.Leaf LN.Atom LN.AtomSet LN.AssocList
LN.Singlesorted.Operations
Singlesorted.Classes.DecoratedTraversableModule.
Export List.ListNotations.
Open Scope list_scope.
Export DecoratedTraversableMonad.Notations.
Open Scope tealeaves_scope.
Export LN.AtomSet.Notations.
Open Scope set_scope.
Export LN.AssocList.Notations.
Set Implicit Arguments.
Singlesorted.Theory.Product
LN.Leaf LN.Atom LN.AtomSet LN.AssocList
LN.Singlesorted.Operations
Singlesorted.Classes.DecoratedTraversableModule.
Export List.ListNotations.
Open Scope list_scope.
Export DecoratedTraversableMonad.Notations.
Open Scope tealeaves_scope.
Export LN.AtomSet.Notations.
Open Scope set_scope.
Export LN.AssocList.Notations.
Set Implicit Arguments.
Parameter base_typ : Type.
Inductive typ :=
| base : base_typ -> typ
| arr : typ -> typ -> typ.
Coercion base : base_typ >-> typ.
(* we suggest more informative names for Lam's arguments
than Coq otherwise infers *)
Inductive term (A : Type) :=
| Var : A -> term A
| Lam : forall (X : typ) (t : term A), term A
| Ap : term A -> term A -> term A.
Inductive typ :=
| base : base_typ -> typ
| arr : typ -> typ -> typ.
Coercion base : base_typ >-> typ.
(* we suggest more informative names for Lam's arguments
than Coq otherwise infers *)
Inductive term (A : Type) :=
| Var : A -> term A
| Lam : forall (X : typ) (t : term A), term A
| Ap : term A -> term A -> term A.
Module Notations.
Notation "'λ' X ⋅ body" := (Lam X body) (at level 45).
Notation "[ t1 ] [ t2 ]" := (Ap t1 t2) (at level 40).
Notation "A ⟹ B" := (arr A B) (at level 40).
End Notations.
Ltac basic t :=
induction t;
[ reflexivity |
simpl; match goal with H : _ |- _ => rewrite H end; reflexivity |
simpl; do 2 match goal with H : _ |- _ => rewrite H end; reflexivity ].
Notation "'λ' X ⋅ body" := (Lam X body) (at level 45).
Notation "[ t1 ] [ t2 ]" := (Ap t1 t2) (at level 40).
Notation "A ⟹ B" := (arr A B) (at level 40).
End Notations.
Ltac basic t :=
induction t;
[ reflexivity |
simpl; match goal with H : _ |- _ => rewrite H end; reflexivity |
simpl; do 2 match goal with H : _ |- _ => rewrite H end; reflexivity ].
Fixpoint fmap_term {A B : Type} (f : A -> B) (t : term A) : term B :=
match t with
| Var a => Var (f a)
| Lam X t => Lam X (fmap_term f t)
| Ap t1 t2 => Ap (fmap_term f t1) (fmap_term f t2)
end.
Instance Fmap_term : Fmap term := @fmap_term.
Theorem fmap_id : forall A, fmap term id = @id (term A).
Proof.
intros. ext t. unfold transparent tcs. basic t.
Qed.
Theorem fmap_fmap : forall A B C (f : A -> B) (g : B -> C),
fmap term g ∘ fmap term f = fmap term (g ∘ f).
Proof.
intros. ext t. unfold transparent tcs.
unfold compose. basic t.
Qed.
Instance Functor_term : Functor term :=
{| fun_fmap_id := @fmap_id;
fun_fmap_fmap := @fmap_fmap;
|}.
match t with
| Var a => Var (f a)
| Lam X t => Lam X (fmap_term f t)
| Ap t1 t2 => Ap (fmap_term f t1) (fmap_term f t2)
end.
Instance Fmap_term : Fmap term := @fmap_term.
Theorem fmap_id : forall A, fmap term id = @id (term A).
Proof.
intros. ext t. unfold transparent tcs. basic t.
Qed.
Theorem fmap_fmap : forall A B C (f : A -> B) (g : B -> C),
fmap term g ∘ fmap term f = fmap term (g ∘ f).
Proof.
intros. ext t. unfold transparent tcs.
unfold compose. basic t.
Qed.
Instance Functor_term : Functor term :=
{| fun_fmap_id := @fmap_id;
fun_fmap_fmap := @fmap_fmap;
|}.
Section fmap_term_rewrite.
Context
`{f : A -> B}.
Lemma fmap_term_ap : forall (t1 t2 : term A),
fmap term f (@Ap A t1 t2) = @Ap B (fmap term f t1) (fmap term f t2).
Proof.
reflexivity.
Qed.
End fmap_term_rewrite.
Context
`{f : A -> B}.
Lemma fmap_term_ap : forall (t1 t2 : term A),
fmap term f (@Ap A t1 t2) = @Ap B (fmap term f t1) (fmap term f t2).
Proof.
reflexivity.
Qed.
End fmap_term_rewrite.
Definition ret_term {A} : A -> term A := fun a => Var a.
Fixpoint join_term {A : Type} (t : term (term A)) : term A :=
match t with
| Var t' => t'
| Lam X t => Lam X (join_term t)
| Ap t1 t2 => Ap (join_term t1) (join_term t2)
end.
Instance Ret_term : Return term := @ret_term.
Instance Join_term : Join term := @join_term.
Theorem join_natural : forall A B (f : A -> B),
fmap term f ∘ join term = join term ∘ fmap term (fmap term f).
Proof.
intros. ext t. unfold transparent tcs.
unfold compose. basic t.
Qed.
Instance: Natural (@join term _).
Proof.
constructor.
- apply Functor_compose.
- typeclasses eauto.
- apply join_natural.
Qed.
Theorem ret_natural : forall A B (f : A -> B),
fmap term f ∘ ret term = ret term ∘ f.
Proof.
reflexivity.
Qed.
Instance: Natural (@ret term _).
Proof.
constructor; try typeclasses eauto.
apply ret_natural.
Qed.
Theorem join_ret : forall A,
join term ∘ ret term = @id (term A).
Proof.
reflexivity.
Qed.
Theorem join_fmap_ret : forall A,
join term ∘ fmap term (ret term) = @id (term A).
Proof.
intros. unfold compose. unfold transparent tcs.
ext t. basic t.
Qed.
Theorem join_join : forall A,
join term ∘ join term = join term (A := A) ∘ fmap term (join term).
Proof.
intros. unfold compose. unfold transparent tcs.
ext t. basic t.
Qed.
Instance Monad_term : Monad term :=
{| mon_join_ret := join_ret;
mon_join_fmap_ret := join_fmap_ret;
mon_join_join := join_join |}.
Fixpoint join_term {A : Type} (t : term (term A)) : term A :=
match t with
| Var t' => t'
| Lam X t => Lam X (join_term t)
| Ap t1 t2 => Ap (join_term t1) (join_term t2)
end.
Instance Ret_term : Return term := @ret_term.
Instance Join_term : Join term := @join_term.
Theorem join_natural : forall A B (f : A -> B),
fmap term f ∘ join term = join term ∘ fmap term (fmap term f).
Proof.
intros. ext t. unfold transparent tcs.
unfold compose. basic t.
Qed.
Instance: Natural (@join term _).
Proof.
constructor.
- apply Functor_compose.
- typeclasses eauto.
- apply join_natural.
Qed.
Theorem ret_natural : forall A B (f : A -> B),
fmap term f ∘ ret term = ret term ∘ f.
Proof.
reflexivity.
Qed.
Instance: Natural (@ret term _).
Proof.
constructor; try typeclasses eauto.
apply ret_natural.
Qed.
Theorem join_ret : forall A,
join term ∘ ret term = @id (term A).
Proof.
reflexivity.
Qed.
Theorem join_fmap_ret : forall A,
join term ∘ fmap term (ret term) = @id (term A).
Proof.
intros. unfold compose. unfold transparent tcs.
ext t. basic t.
Qed.
Theorem join_join : forall A,
join term ∘ join term = join term (A := A) ∘ fmap term (join term).
Proof.
intros. unfold compose. unfold transparent tcs.
ext t. basic t.
Qed.
Instance Monad_term : Monad term :=
{| mon_join_ret := join_ret;
mon_join_fmap_ret := join_fmap_ret;
mon_join_join := join_join |}.
Fixpoint dec_term {A} (t : term A) : term (nat * A) :=
match t with
| Var a => Var (Ƶ, a)
| Lam τ t => Lam τ (shift term (1, dec_term t))
| Ap t1 t2 => Ap (dec_term t1) (dec_term t2)
end.
Instance Decorate_term : Decorate nat term := @dec_term.
Theorem dec_natural : forall A B (f : A -> B),
fmap term (fmap (prod nat) f) ∘ dec term = dec term ∘ fmap term f.
Proof.
intros. unfold compose. ext t. induction t.
- now cbn.
- cbn -[shift]. fequal. now rewrite dec_helper_1.
- cbn. now fequal.
Qed.
Instance: Natural (@dec nat term _).
Proof.
constructor.
- typeclasses eauto.
- apply Functor_compose.
- apply dec_natural.
Qed.
Theorem dec_extract : forall A,
fmap term (extract (prod nat)) ∘ dec term = @id (term A).
Proof.
intros. unfold compose. ext t. induction t.
- reflexivity.
- cbn -[shift]. now rewrite dec_helper_2.
- unfold id. cbn. now fequal.
Qed.
Theorem dec_dec : forall A,
dec term ∘ dec term = fmap term (cojoin (prod nat)) ∘ dec term (A := A).
Proof.
intros. unfold compose. ext t. induction t.
- reflexivity.
- cbn -[shift]. fequal. now rewrite dec_helper_3.
- cbn. fequal; auto.
Qed.
Instance DecoratedFunctor_term : DecoratedFunctor nat term.
Proof.
constructor.
- typeclasses eauto.
- apply Monoid_Nat.
- typeclasses eauto.
- apply dec_dec.
- apply dec_extract.
Qed.
Theorem dec_ret : forall A,
dec term ∘ ret term (A := A) = ret term ∘ pair Ƶ.
Proof.
reflexivity.
Qed.
Theorem dec_join : forall A,
dec term ∘ join term (A := A) =
join term ∘ fmap term (shift term) ∘ dec term ∘ fmap term (dec term).
Proof.
intros. unfold compose. ext t. induction t.
- cbn -[shift]. now rewrite shift_zero.
- cbn -[shift]. fequal. now rewrite (dec_helper_4).
- cbn. fequal; auto.
Qed.
Instance DecoratedMonad_term : DecoratedMonad nat term.
Proof.
constructor.
- typeclasses eauto.
- typeclasses eauto.
- typeclasses eauto.
- apply dec_ret.
- apply dec_join.
Qed.
match t with
| Var a => Var (Ƶ, a)
| Lam τ t => Lam τ (shift term (1, dec_term t))
| Ap t1 t2 => Ap (dec_term t1) (dec_term t2)
end.
Instance Decorate_term : Decorate nat term := @dec_term.
Theorem dec_natural : forall A B (f : A -> B),
fmap term (fmap (prod nat) f) ∘ dec term = dec term ∘ fmap term f.
Proof.
intros. unfold compose. ext t. induction t.
- now cbn.
- cbn -[shift]. fequal. now rewrite dec_helper_1.
- cbn. now fequal.
Qed.
Instance: Natural (@dec nat term _).
Proof.
constructor.
- typeclasses eauto.
- apply Functor_compose.
- apply dec_natural.
Qed.
Theorem dec_extract : forall A,
fmap term (extract (prod nat)) ∘ dec term = @id (term A).
Proof.
intros. unfold compose. ext t. induction t.
- reflexivity.
- cbn -[shift]. now rewrite dec_helper_2.
- unfold id. cbn. now fequal.
Qed.
Theorem dec_dec : forall A,
dec term ∘ dec term = fmap term (cojoin (prod nat)) ∘ dec term (A := A).
Proof.
intros. unfold compose. ext t. induction t.
- reflexivity.
- cbn -[shift]. fequal. now rewrite dec_helper_3.
- cbn. fequal; auto.
Qed.
Instance DecoratedFunctor_term : DecoratedFunctor nat term.
Proof.
constructor.
- typeclasses eauto.
- apply Monoid_Nat.
- typeclasses eauto.
- apply dec_dec.
- apply dec_extract.
Qed.
Theorem dec_ret : forall A,
dec term ∘ ret term (A := A) = ret term ∘ pair Ƶ.
Proof.
reflexivity.
Qed.
Theorem dec_join : forall A,
dec term ∘ join term (A := A) =
join term ∘ fmap term (shift term) ∘ dec term ∘ fmap term (dec term).
Proof.
intros. unfold compose. ext t. induction t.
- cbn -[shift]. now rewrite shift_zero.
- cbn -[shift]. fequal. now rewrite (dec_helper_4).
- cbn. fequal; auto.
Qed.
Instance DecoratedMonad_term : DecoratedMonad nat term.
Proof.
constructor.
- typeclasses eauto.
- typeclasses eauto.
- typeclasses eauto.
- apply dec_ret.
- apply dec_join.
Qed.
Section dec_term_rewrite.
Context
`{f : A -> B}.
Lemma dec_term_lam1 : forall (X : typ) (t : term A),
dec term (Lam X t) = shift term (1, Lam X (dec term t)).
Proof.
reflexivity.
Qed.
Lemma dec_term_lam2 : forall (X : typ) (t : term A),
dec term (Lam X t) = Lam X (shift term (1, dec term t)).
Proof.
reflexivity.
Qed.
End dec_term_rewrite.
Context
`{f : A -> B}.
Lemma dec_term_lam1 : forall (X : typ) (t : term A),
dec term (Lam X t) = shift term (1, Lam X (dec term t)).
Proof.
reflexivity.
Qed.
Lemma dec_term_lam2 : forall (X : typ) (t : term A),
dec term (Lam X t) = Lam X (shift term (1, dec term t)).
Proof.
reflexivity.
Qed.
End dec_term_rewrite.
Import Applicative.Notations.
Fixpoint dist_term `{Fmap F} `{Pure F} `{Mult F} {A : Type}
(t : term (F A)) : F (term A) :=
match t with
| Var a => fmap F (@Var A) a
| Lam X t => fmap F (Lam X) (dist_term t)
| Ap t1 t2 => (pure F (@Ap A))
<⋆> dist_term t1
<⋆> dist_term t2
end.
Instance: Dist term := @dist_term.
Fixpoint dist_term `{Fmap F} `{Pure F} `{Mult F} {A : Type}
(t : term (F A)) : F (term A) :=
match t with
| Var a => fmap F (@Var A) a
| Lam X t => fmap F (Lam X) (dist_term t)
| Ap t1 t2 => (pure F (@Ap A))
<⋆> dist_term t1
<⋆> dist_term t2
end.
Instance: Dist term := @dist_term.
Section term_dist_rewrite.
Context
`{Applicative G}.
Variable (A : Type).
Lemma dist_term_var_1 : forall (x : G A),
dist term G (@Var (G A) x) = pure G (@Var A) <⋆> x.
Proof.
intros. cbn. now rewrite fmap_to_ap.
Qed.
Lemma dist_term_var_2 : forall (x : G A),
dist term G (@Var (G A) x) = fmap G (@Var A) x.
Proof.
reflexivity.
Qed.
Lemma dist_term_lam_1 : forall (X : typ) (t : term (G A)),
dist term G (Lam X t) = pure G (Lam X) <⋆> (dist term G t).
Proof.
intros. cbn. now rewrite fmap_to_ap.
Qed.
Lemma dist_term_lam_2 : forall (X : typ) (t : term (G A)),
dist term G (Lam X t) = fmap G (Lam X) (dist term G t).
Proof.
reflexivity.
Qed.
Lemma dist_term_ap_1 : forall (t1 t2 : term (G A)),
dist term G (Ap t1 t2) =
(pure G (@Ap A))
<⋆> dist term G t1
<⋆> dist term G t2.
Proof.
reflexivity.
Qed.
Lemma dist_term_ap_2 : forall (t1 t2 : term (G A)),
dist term G (Ap t1 t2) =
(fmap G (@Ap A) (dist term G t1)
<⋆> dist term G t2).
Proof.
intros. rewrite dist_term_ap_1.
now rewrite fmap_to_ap.
Qed.
End term_dist_rewrite.
Section dist_term_properties.
Context
`{Applicative G}.
Lemma dist_natural_term : forall `(f : A -> B),
fmap (G ∘ term) f ∘ dist term G =
dist term G ∘ fmap (term ∘ G) f.
Proof.
intros; cbn. ext t.
unfold_ops @Fmap_compose. unfold compose. induction t.
+ cbn. compose near a. now rewrite 2(fun_fmap_fmap G).
+ cbn. rewrite <- IHt.
compose near (dist term G t).
now rewrite 2(fun_fmap_fmap G).
+ rewrite (dist_term_ap_2).
rewrite (fmap_term_ap).
rewrite (dist_term_ap_2).
rewrite <- IHt1, <- IHt2.
rewrite <- ap7.
rewrite ap6. fequal.
compose near (dist term G t1).
rewrite (fun_fmap_fmap G).
rewrite (fun_fmap_fmap G).
compose near (dist term G t1) on right.
rewrite (fun_fmap_fmap G).
reflexivity.
Qed.
Lemma dist_morph_term : forall `{ApplicativeMorphism G1 G2 ϕ} A,
dist term G2 ∘ fmap term (ϕ A) = ϕ (term A) ∘ dist term G1.
Proof.
intros. ext t. unfold compose. induction t.
- cbn. now rewrite <- (appmor_natural G1 G2).
- cbn. rewrite IHt.
now rewrite (appmor_natural G1 G2).
- rewrite fmap_term_ap. inversion H9.
rewrite dist_term_ap_2.
rewrite IHt1. rewrite IHt2.
rewrite dist_term_ap_2. rewrite (ap_morphism_1).
fequal. now rewrite <- (appmor_natural).
Qed.
Lemma dist_unit_term : forall (A : Type),
dist term (fun A => A) = @id (term A).
Proof.
intros. ext t. induction t.
- reflexivity.
- cbn. rewrite IHt. reflexivity.
- cbn. rewrite IHt1, IHt2.
reflexivity.
Qed.
#[local] Set Keyed Unification.
Lemma dist_linear_term : forall `{Applicative G1} `{Applicative G2} (A : Type),
dist term (G1 ∘ G2) =
fmap G1 (dist term G2) ∘ dist term G1 (A := G2 A).
Proof.
intros. unfold compose. ext t. induction t.
- cbn. compose near a on right. now rewrite (fun_fmap_fmap G1).
- cbn. rewrite IHt. compose near (dist term G1 t).
change (fmap (G1 ○ G2) (Lam X)) with (fmap G1 (fmap G2 (@Lam A X))).
rewrite (fun_fmap_fmap G1).
now rewrite (fun_fmap_fmap G1).
- rewrite dist_term_ap_2.
rewrite (dist_term_ap_2 (G := G1 ○ G2)).
rewrite ap6.
compose near ((dist term G1 t1)).
rewrite (fun_fmap_fmap G1).
rewrite (ap_compose_3 G2 G1).
rewrite IHt1, IHt2.
rewrite <- ap7. fequal.
repeat (compose near (dist term G1 t1) on left;
rewrite (fun_fmap_fmap G1)).
fequal. ext s1 s2. unfold compose; cbn.
unfold precompose. now rewrite (fmap_to_ap).
Qed.
#[local] Unset Keyed Unification.
Theorem trvmon_ret_term `{Applicative G} :
`(dist term G ∘ ret term (A := G A) = fmap G (ret term)).
Proof.
intros. ext x. reflexivity.
Qed.
#[local] Set Keyed Unification.
Theorem trvmon_join_term :
`(dist term G ∘ join term = fmap G (join term) ∘ dist (term ∘ term) G (A := A)).
Proof.
intros. ext t. unfold compose. induction t.
- cbn. compose near (dist term G a).
rewrite (fun_fmap_fmap G).
replace (join term ∘ Var (A := term A)) with (@id (term A)).
now rewrite (fun_fmap_id G).
apply (join_ret).
- cbn. rewrite IHt.
unfold_ops @Dist_compose. unfold compose.
compose near (dist term G (fmap term (dist term G) t)).
rewrite (fun_fmap_fmap G).
rewrite (fun_fmap_fmap G).
reflexivity.
- cbn. rewrite IHt1, IHt2.
unfold_ops @Dist_compose. unfold compose.
rewrite <- fmap_to_ap.
rewrite <- fmap_to_ap.
rewrite <- ap7. rewrite ap6.
fequal. compose near ((dist term G (fmap term (dist term G) t1))).
repeat rewrite (fun_fmap_fmap G).
compose near ((dist term G (fmap term (dist term G) t1))) on left.
rewrite (fun_fmap_fmap G).
fequal.
Qed.
#[local] Set Keyed Unification.
End dist_term_properties.
Instance TraversableFunctor_term : TraversableFunctor term :=
{| dist_natural := @dist_natural_term;
dist_morph := @dist_morph_term;
dist_linear := @dist_linear_term;
dist_unit := @dist_unit_term;
|}.
Instance TraversableMonad_term : TraversableMonad term :=
{| trvmon_ret := @trvmon_ret_term;
trvmon_join := @trvmon_join_term;
|}.
Context
`{Applicative G}.
Variable (A : Type).
Lemma dist_term_var_1 : forall (x : G A),
dist term G (@Var (G A) x) = pure G (@Var A) <⋆> x.
Proof.
intros. cbn. now rewrite fmap_to_ap.
Qed.
Lemma dist_term_var_2 : forall (x : G A),
dist term G (@Var (G A) x) = fmap G (@Var A) x.
Proof.
reflexivity.
Qed.
Lemma dist_term_lam_1 : forall (X : typ) (t : term (G A)),
dist term G (Lam X t) = pure G (Lam X) <⋆> (dist term G t).
Proof.
intros. cbn. now rewrite fmap_to_ap.
Qed.
Lemma dist_term_lam_2 : forall (X : typ) (t : term (G A)),
dist term G (Lam X t) = fmap G (Lam X) (dist term G t).
Proof.
reflexivity.
Qed.
Lemma dist_term_ap_1 : forall (t1 t2 : term (G A)),
dist term G (Ap t1 t2) =
(pure G (@Ap A))
<⋆> dist term G t1
<⋆> dist term G t2.
Proof.
reflexivity.
Qed.
Lemma dist_term_ap_2 : forall (t1 t2 : term (G A)),
dist term G (Ap t1 t2) =
(fmap G (@Ap A) (dist term G t1)
<⋆> dist term G t2).
Proof.
intros. rewrite dist_term_ap_1.
now rewrite fmap_to_ap.
Qed.
End term_dist_rewrite.
Section dist_term_properties.
Context
`{Applicative G}.
Lemma dist_natural_term : forall `(f : A -> B),
fmap (G ∘ term) f ∘ dist term G =
dist term G ∘ fmap (term ∘ G) f.
Proof.
intros; cbn. ext t.
unfold_ops @Fmap_compose. unfold compose. induction t.
+ cbn. compose near a. now rewrite 2(fun_fmap_fmap G).
+ cbn. rewrite <- IHt.
compose near (dist term G t).
now rewrite 2(fun_fmap_fmap G).
+ rewrite (dist_term_ap_2).
rewrite (fmap_term_ap).
rewrite (dist_term_ap_2).
rewrite <- IHt1, <- IHt2.
rewrite <- ap7.
rewrite ap6. fequal.
compose near (dist term G t1).
rewrite (fun_fmap_fmap G).
rewrite (fun_fmap_fmap G).
compose near (dist term G t1) on right.
rewrite (fun_fmap_fmap G).
reflexivity.
Qed.
Lemma dist_morph_term : forall `{ApplicativeMorphism G1 G2 ϕ} A,
dist term G2 ∘ fmap term (ϕ A) = ϕ (term A) ∘ dist term G1.
Proof.
intros. ext t. unfold compose. induction t.
- cbn. now rewrite <- (appmor_natural G1 G2).
- cbn. rewrite IHt.
now rewrite (appmor_natural G1 G2).
- rewrite fmap_term_ap. inversion H9.
rewrite dist_term_ap_2.
rewrite IHt1. rewrite IHt2.
rewrite dist_term_ap_2. rewrite (ap_morphism_1).
fequal. now rewrite <- (appmor_natural).
Qed.
Lemma dist_unit_term : forall (A : Type),
dist term (fun A => A) = @id (term A).
Proof.
intros. ext t. induction t.
- reflexivity.
- cbn. rewrite IHt. reflexivity.
- cbn. rewrite IHt1, IHt2.
reflexivity.
Qed.
#[local] Set Keyed Unification.
Lemma dist_linear_term : forall `{Applicative G1} `{Applicative G2} (A : Type),
dist term (G1 ∘ G2) =
fmap G1 (dist term G2) ∘ dist term G1 (A := G2 A).
Proof.
intros. unfold compose. ext t. induction t.
- cbn. compose near a on right. now rewrite (fun_fmap_fmap G1).
- cbn. rewrite IHt. compose near (dist term G1 t).
change (fmap (G1 ○ G2) (Lam X)) with (fmap G1 (fmap G2 (@Lam A X))).
rewrite (fun_fmap_fmap G1).
now rewrite (fun_fmap_fmap G1).
- rewrite dist_term_ap_2.
rewrite (dist_term_ap_2 (G := G1 ○ G2)).
rewrite ap6.
compose near ((dist term G1 t1)).
rewrite (fun_fmap_fmap G1).
rewrite (ap_compose_3 G2 G1).
rewrite IHt1, IHt2.
rewrite <- ap7. fequal.
repeat (compose near (dist term G1 t1) on left;
rewrite (fun_fmap_fmap G1)).
fequal. ext s1 s2. unfold compose; cbn.
unfold precompose. now rewrite (fmap_to_ap).
Qed.
#[local] Unset Keyed Unification.
Theorem trvmon_ret_term `{Applicative G} :
`(dist term G ∘ ret term (A := G A) = fmap G (ret term)).
Proof.
intros. ext x. reflexivity.
Qed.
#[local] Set Keyed Unification.
Theorem trvmon_join_term :
`(dist term G ∘ join term = fmap G (join term) ∘ dist (term ∘ term) G (A := A)).
Proof.
intros. ext t. unfold compose. induction t.
- cbn. compose near (dist term G a).
rewrite (fun_fmap_fmap G).
replace (join term ∘ Var (A := term A)) with (@id (term A)).
now rewrite (fun_fmap_id G).
apply (join_ret).
- cbn. rewrite IHt.
unfold_ops @Dist_compose. unfold compose.
compose near (dist term G (fmap term (dist term G) t)).
rewrite (fun_fmap_fmap G).
rewrite (fun_fmap_fmap G).
reflexivity.
- cbn. rewrite IHt1, IHt2.
unfold_ops @Dist_compose. unfold compose.
rewrite <- fmap_to_ap.
rewrite <- fmap_to_ap.
rewrite <- ap7. rewrite ap6.
fequal. compose near ((dist term G (fmap term (dist term G) t1))).
repeat rewrite (fun_fmap_fmap G).
compose near ((dist term G (fmap term (dist term G) t1))) on left.
rewrite (fun_fmap_fmap G).
fequal.
Qed.
#[local] Set Keyed Unification.
End dist_term_properties.
Instance TraversableFunctor_term : TraversableFunctor term :=
{| dist_natural := @dist_natural_term;
dist_morph := @dist_morph_term;
dist_linear := @dist_linear_term;
dist_unit := @dist_unit_term;
|}.
Instance TraversableMonad_term : TraversableMonad term :=
{| trvmon_ret := @trvmon_ret_term;
trvmon_join := @trvmon_join_term;
|}.
Fixpoint tolist_term {A} (t : term A) : list A :=
match t with
| Var a => [ a ]
| Lam X t => tolist_term t
| Ap t1 t2 => tolist_term t1 ++ tolist_term t2
end.
Instance Tolist_term : Tolist term := @tolist_term.
Theorem tolist_natural : forall (A B : Type) (f : A -> B),
fmap list f ∘ tolist term = tolist term ∘ fmap term f.
Proof.
intros. unfold compose. ext t. induction t.
- reflexivity.
- cbn. now rewrite IHt.
- cbn. rewrite <- IHt1, <- IHt2.
now autorewrite with tea_list.
Qed.
Instance: Natural (@tolist _ _).
Proof.
constructor; try typeclasses eauto.
apply tolist_natural.
Qed.
match t with
| Var a => [ a ]
| Lam X t => tolist_term t
| Ap t1 t2 => tolist_term t1 ++ tolist_term t2
end.
Instance Tolist_term : Tolist term := @tolist_term.
Theorem tolist_natural : forall (A B : Type) (f : A -> B),
fmap list f ∘ tolist term = tolist term ∘ fmap term f.
Proof.
intros. unfold compose. ext t. induction t.
- reflexivity.
- cbn. now rewrite IHt.
- cbn. rewrite <- IHt1, <- IHt2.
now autorewrite with tea_list.
Qed.
Instance: Natural (@tolist _ _).
Proof.
constructor; try typeclasses eauto.
apply tolist_natural.
Qed.
Theorem tolist_equal : forall {A B : Type} {f g : A -> B} (t : term A),
List.map f (tolist term t) = List.map g (tolist term t) ->
fmap term f t = fmap term g t.
Proof.
intros.
induction t.
- cbn in *. inversion H. reflexivity.
- cbn in *. f_equal; auto.
- cbn in *. apply List.fmap_app_inv in H. destruct H.
f_equal; auto.
Qed.
Theorem shapeliness_term : forall {A : Type} (t1 t2 : term A),
shape term t1 = shape term t2 /\
tolist term t1 = tolist term t2 ->
t1 = t2.
Proof.
introv [Hyp1 Hyp2]. generalize dependent t2.
induction t1; intros t2; destruct t2; try discriminate; intros.
- now preprocess.
- preprocess. erewrite IHt1; eauto.
- preprocess. cbn in *.
assert (t1_1 = t2_1).
{ apply IHt1_1; auto. eauto using (shape_l term). }
assert (t1_2 = t2_2).
{ apply IHt1_2; auto. eauto using (shape_r term). }
now subst.
Qed.
Instance ListableFunctor_term : ListableFunctor term :=
{| lfun_shapeliness := @shapeliness_term; |}.
Theorem tolist_ret : forall (A : Type),
tolist term ∘ ret term (A := A) = one.
Proof.
reflexivity.
Qed.
Theorem tolist_join : forall (A : Type),
tolist term ∘ join term =
join list (A := A) ∘ tolist term ∘ fmap term (tolist term).
Proof.
intros. unfold compose. ext t. induction t.
- cbn. auto with datatypes.
- cbn. now rewrite IHt.
- cbn. rewrite IHt1, IHt2.
now autorewrite with tea_list.
Qed.
Instance ListableMonad_term : ListableMonad term :=
{| lmon_ret := tolist_ret;
lmon_join := tolist_join; |}.
List.map f (tolist term t) = List.map g (tolist term t) ->
fmap term f t = fmap term g t.
Proof.
intros.
induction t.
- cbn in *. inversion H. reflexivity.
- cbn in *. f_equal; auto.
- cbn in *. apply List.fmap_app_inv in H. destruct H.
f_equal; auto.
Qed.
Theorem shapeliness_term : forall {A : Type} (t1 t2 : term A),
shape term t1 = shape term t2 /\
tolist term t1 = tolist term t2 ->
t1 = t2.
Proof.
introv [Hyp1 Hyp2]. generalize dependent t2.
induction t1; intros t2; destruct t2; try discriminate; intros.
- now preprocess.
- preprocess. erewrite IHt1; eauto.
- preprocess. cbn in *.
assert (t1_1 = t2_1).
{ apply IHt1_1; auto. eauto using (shape_l term). }
assert (t1_2 = t2_2).
{ apply IHt1_2; auto. eauto using (shape_r term). }
now subst.
Qed.
Instance ListableFunctor_term : ListableFunctor term :=
{| lfun_shapeliness := @shapeliness_term; |}.
Theorem tolist_ret : forall (A : Type),
tolist term ∘ ret term (A := A) = one.
Proof.
reflexivity.
Qed.
Theorem tolist_join : forall (A : Type),
tolist term ∘ join term =
join list (A := A) ∘ tolist term ∘ fmap term (tolist term).
Proof.
intros. unfold compose. ext t. induction t.
- cbn. auto with datatypes.
- cbn. now rewrite IHt.
- cbn. rewrite IHt1, IHt2.
now autorewrite with tea_list.
Qed.
Instance ListableMonad_term : ListableMonad term :=
{| lmon_ret := tolist_ret;
lmon_join := tolist_join; |}.
Lemma dtfun_compat_term1 : forall `{Applicative G} (X : typ) {A},
fmap G (dec term ∘ Lam X) ∘ δ term G (A := A) =
fmap G (curry (shift term) 1 ∘ Lam X) ∘ fmap G (dec term) ∘ δ term G.
Proof.
intros. rewrite (fun_fmap_fmap G). reflexivity.
Qed.
Theorem dtfun_compat_term :
`(forall {A : Type} `{Applicative G},
dist term G ∘ fmap term (strength G) ∘ dec term (A := G A) =
fmap G (dec term) ∘ dist term G).
Proof.
intros. ext t. unfold compose. induction t.
- cbn. compose near a. now rewrite 2(fun_fmap_fmap G).
- cbn. do 2 (compose near (dec term t) on left;
rewrite (fun_fmap_fmap term)).
reassociate <-. rewrite (strength_shift_1).
rewrite <- (fun_fmap_fmap term); unfold compose.
change (fmap term (fmap G ?f)) with (fmap (term ∘ G) f).
compose near ((fmap term (σ G) (dec term t))).
rewrite <- (dist_natural term); unfold compose.
rewrite IHt. compose near (δ term G t).
rewrite (fun_fmap_fmap G).
compose near (δ term G t) on left.
unfold_ops @Fmap_compose; rewrite 2(fun_fmap_fmap G).
fequal. ext t'; unfold compose; cbn.
compose near (dec term t') on right; now rewrite (fun_fmap_fmap term).
- cbn. rewrite IHt1, IHt2. rewrite ap6. rewrite ap6.
rewrite ap5. rewrite <- ap7.
rewrite (app_pure_natural G). rewrite <- (fmap_to_ap).
compose near (δ term G t1) on left. rewrite (fun_fmap_fmap G).
reflexivity.
Qed.
Instance : DecoratedTraversableFunctor nat term :=
{| dtfun_compat := @dtfun_compat_term |}.
Instance : DecoratedTraversableMonad nat term := {}.
Existing Instance RightAction_Join.
Instance : DecoratedTraversableModule nat term term
:= DecoratedTraversableModule_Monad term.
fmap G (dec term ∘ Lam X) ∘ δ term G (A := A) =
fmap G (curry (shift term) 1 ∘ Lam X) ∘ fmap G (dec term) ∘ δ term G.
Proof.
intros. rewrite (fun_fmap_fmap G). reflexivity.
Qed.
Theorem dtfun_compat_term :
`(forall {A : Type} `{Applicative G},
dist term G ∘ fmap term (strength G) ∘ dec term (A := G A) =
fmap G (dec term) ∘ dist term G).
Proof.
intros. ext t. unfold compose. induction t.
- cbn. compose near a. now rewrite 2(fun_fmap_fmap G).
- cbn. do 2 (compose near (dec term t) on left;
rewrite (fun_fmap_fmap term)).
reassociate <-. rewrite (strength_shift_1).
rewrite <- (fun_fmap_fmap term); unfold compose.
change (fmap term (fmap G ?f)) with (fmap (term ∘ G) f).
compose near ((fmap term (σ G) (dec term t))).
rewrite <- (dist_natural term); unfold compose.
rewrite IHt. compose near (δ term G t).
rewrite (fun_fmap_fmap G).
compose near (δ term G t) on left.
unfold_ops @Fmap_compose; rewrite 2(fun_fmap_fmap G).
fequal. ext t'; unfold compose; cbn.
compose near (dec term t') on right; now rewrite (fun_fmap_fmap term).
- cbn. rewrite IHt1, IHt2. rewrite ap6. rewrite ap6.
rewrite ap5. rewrite <- ap7.
rewrite (app_pure_natural G). rewrite <- (fmap_to_ap).
compose near (δ term G t1) on left. rewrite (fun_fmap_fmap G).
reflexivity.
Qed.
Instance : DecoratedTraversableFunctor nat term :=
{| dtfun_compat := @dtfun_compat_term |}.
Instance : DecoratedTraversableMonad nat term := {}.
Existing Instance RightAction_Join.
Instance : DecoratedTraversableModule nat term term
:= DecoratedTraversableModule_Monad term.
Import Notations.
Import LN.Singlesorted.Operations.Notations.
Definition Vb x := Var (Bd x) : term leaf.
Definition Vf n := Var (Fr n) : term leaf.
Coercion Vb : nat >-> term.
Coercion Vf : atom >-> term.
Section test_notations.
Context
(x y z : atom)
(X : typ).
Check 1.
Check (Vb 1 : term leaf).
Check Vb 1.
Check (λ X ⋅ Vb 1).
Check (λ X ⋅ (Vb 1 : term leaf)).
Check (λ X ⋅ 1).
Check (λ X ⋅ x).
Check [λ X ⋅ x][0].
Check (λ X ⋅ [x][0]).
Check [λ X ⋅ [0] [y]] [2].
Check [λ X ⋅ x ][λ X ⋅ 0 ].
Check [ x ][ λ X ⋅ 0 ].
Check [ λ X ⋅ [y][2] ][ λ X ⋅ 1 ].
Check [1][x].
Check (λ X ⋅ [1][x]).
Check [λ X ⋅ 0][λ X ⋅ [1][x]].
Check (λ X ⋅ 0) '{x ~> (λ X ⋅ x)}.
(* Fail Timeout 1 Check (λ X ⋅ 0) '( Fr x ).
Fail Timeout 1 Check (λ X ⋅ 0) '( x ). *)
Check (λ X ⋅ 0) '( Var (Fr x) ).
Check (λ X ⋅ 0) '( Vf x ).
Check (λ X ⋅ 0) '( λ X ⋅ x ).
Compute (λ X ⋅ 0).
Check (λ X ⋅ 0) '{x ~> (λ X ⋅ x)}.
Compute (λ X ⋅ 0) '{x ~> (λ X ⋅ x)}.
Compute (λ X ⋅ x) '{x ~> (λ X ⋅ [1][y])}.
Goal (λ X ⋅ x) '{x ~> (λ X ⋅ [1][y])} = (λ X ⋅ λ X ⋅ [1][y]).
Proof.
cbn. compare values x and x.
Qed.
Compute (λ X ⋅ 0).
Check (λ X ⋅ 0) '(λ X ⋅ x).
Compute (λ X ⋅ 0) '(λ X ⋅ x).
Compute (λ X ⋅ 1) '(λ X ⋅ x).
Compute (λ X ⋅ 2) '(λ X ⋅ x).
Compute (λ X ⋅ x) '(λ X ⋅ [1][y]).
Compute ([0] [λ X ⋅ [x][1]]) '(λ X ⋅ z).
Compute ([0] [λ X ⋅ [x][0]]) '(λ X ⋅ z).
Compute ('[x] λ X ⋅ x).
Compute ('[x] λ X ⋅ y).
Goal ('[x] (Var (Fr x)) = Var (Bd 0) ).
Proof. cbn. unfold compose. cbn. compare values x and x. Qed.
Goal ( ('[x] λ X ⋅ x) = (λ X ⋅ 1)).
Proof. cbn. unfold compose. simpl. compare values x and x. Qed.
Goal (x <> y -> ('[x] λ X ⋅ y) = (λ X ⋅ y)).
Proof. intro. cbn. unfold compose. simpl. compare values x and y. Qed.
End test_notations.
Import LN.Singlesorted.Operations.Notations.
Definition Vb x := Var (Bd x) : term leaf.
Definition Vf n := Var (Fr n) : term leaf.
Coercion Vb : nat >-> term.
Coercion Vf : atom >-> term.
Section test_notations.
Context
(x y z : atom)
(X : typ).
Check 1.
Check (Vb 1 : term leaf).
Check Vb 1.
Check (λ X ⋅ Vb 1).
Check (λ X ⋅ (Vb 1 : term leaf)).
Check (λ X ⋅ 1).
Check (λ X ⋅ x).
Check [λ X ⋅ x][0].
Check (λ X ⋅ [x][0]).
Check [λ X ⋅ [0] [y]] [2].
Check [λ X ⋅ x ][λ X ⋅ 0 ].
Check [ x ][ λ X ⋅ 0 ].
Check [ λ X ⋅ [y][2] ][ λ X ⋅ 1 ].
Check [1][x].
Check (λ X ⋅ [1][x]).
Check [λ X ⋅ 0][λ X ⋅ [1][x]].
Check (λ X ⋅ 0) '{x ~> (λ X ⋅ x)}.
(* Fail Timeout 1 Check (λ X ⋅ 0) '( Fr x ).
Fail Timeout 1 Check (λ X ⋅ 0) '( x ). *)
Check (λ X ⋅ 0) '( Var (Fr x) ).
Check (λ X ⋅ 0) '( Vf x ).
Check (λ X ⋅ 0) '( λ X ⋅ x ).
Compute (λ X ⋅ 0).
Check (λ X ⋅ 0) '{x ~> (λ X ⋅ x)}.
Compute (λ X ⋅ 0) '{x ~> (λ X ⋅ x)}.
Compute (λ X ⋅ x) '{x ~> (λ X ⋅ [1][y])}.
Goal (λ X ⋅ x) '{x ~> (λ X ⋅ [1][y])} = (λ X ⋅ λ X ⋅ [1][y]).
Proof.
cbn. compare values x and x.
Qed.
Compute (λ X ⋅ 0).
Check (λ X ⋅ 0) '(λ X ⋅ x).
Compute (λ X ⋅ 0) '(λ X ⋅ x).
Compute (λ X ⋅ 1) '(λ X ⋅ x).
Compute (λ X ⋅ 2) '(λ X ⋅ x).
Compute (λ X ⋅ x) '(λ X ⋅ [1][y]).
Compute ([0] [λ X ⋅ [x][1]]) '(λ X ⋅ z).
Compute ([0] [λ X ⋅ [x][0]]) '(λ X ⋅ z).
Compute ('[x] λ X ⋅ x).
Compute ('[x] λ X ⋅ y).
Goal ('[x] (Var (Fr x)) = Var (Bd 0) ).
Proof. cbn. unfold compose. cbn. compare values x and x. Qed.
Goal ( ('[x] λ X ⋅ x) = (λ X ⋅ 1)).
Proof. cbn. unfold compose. simpl. compare values x and x. Qed.
Goal (x <> y -> ('[x] λ X ⋅ y) = (λ X ⋅ y)).
Proof. intro. cbn. unfold compose. simpl. compare values x and y. Qed.
End test_notations.
Definition ctx := list (atom * typ).
Reserved Notation "Γ ⊢ t : S" (at level 90, t at level 99).
Inductive Judgment : ctx -> term leaf -> typ -> Prop :=
| j_var :
forall Γ (x : atom) (A : typ),
uniq Γ ->
(x, A) ∈ Γ ->
Γ ⊢ Var (Fr x) : A
| j_abs :
forall (L : AtomSet.t) Γ (A B : typ) (t : term leaf),
(forall x : atom, ~ AtomSet.In x L -> Γ ++ x ~ A ⊢ t '(Var (Fr x)) : B) ->
Γ ⊢ λ A ⋅ t : A ⟹ B
| j_app :
forall Γ (t1 t2 : term leaf) (A B : typ),
Γ ⊢ t1 : A ⟹ B ->
Γ ⊢ t2 : A ->
Γ ⊢ [t1][t2] : B
where "Γ ⊢ t : A" := (Judgment Γ t A).
Reserved Notation "Γ ⊢ t : S" (at level 90, t at level 99).
Inductive Judgment : ctx -> term leaf -> typ -> Prop :=
| j_var :
forall Γ (x : atom) (A : typ),
uniq Γ ->
(x, A) ∈ Γ ->
Γ ⊢ Var (Fr x) : A
| j_abs :
forall (L : AtomSet.t) Γ (A B : typ) (t : term leaf),
(forall x : atom, ~ AtomSet.In x L -> Γ ++ x ~ A ⊢ t '(Var (Fr x)) : B) ->
Γ ⊢ λ A ⋅ t : A ⟹ B
| j_app :
forall Γ (t1 t2 : term leaf) (A B : typ),
Γ ⊢ t1 : A ⟹ B ->
Γ ⊢ t2 : A ->
Γ ⊢ [t1][t2] : B
where "Γ ⊢ t : A" := (Judgment Γ t A).