OpSemProofs.chain
A chain (elsewhere called a type-aligned list) is like a list, but with
dependent types that must link between consequetive pairs. If a list is a
free monoid, maybe this is a free category? Anyway, it's a useful way to
represent a typed context since it's composable on both the inside and the
outside.
Inductive chain {X} {P : X -> X -> Type} : X -> X -> Type :=
| chain_nil {A : X} : chain A A
| chain_cons {A B C : X} :
P A B -> chain B C -> chain A C
.
| chain_nil {A : X} : chain A A
| chain_cons {A B C : X} :
P A B -> chain B C -> chain A C
.
Most definitions and lemmas in this file will mirror that of list
Arguments chain {X} P _ _.
Infix ":::" := chain_cons (at level 60, right associativity).
Fixpoint chain_app {X} {P : X -> X -> Type} {A B C}
(c : chain P A B) (c' : chain P B C) : chain P A C :=
match c in (chain _ A' B') return (B = B' -> chain P A' C) with
| chain_nil => fun HB => rew [fun B => chain P B C] HB in c'
| x ::: xs =>
fun HB =>
x ::: chain_app xs (rew [fun B => chain P B C] HB in c')
end eq_refl.
Infix "+++" := chain_app (right associativity, at level 60).
Theorem chain_app_nil_r {X} {P : X -> X -> Type} {A B}
(c : chain P A B) :
c +++ chain_nil = c.
Proof.
induction c; auto.
cbn.
rewrite IHc.
auto.
Qed.
Theorem chain_app_assoc {X} {P : X -> X -> Type} {A B C D : X}
(c0 : chain P A B) (c1 : chain P B C) (c2 : chain P C D) :
c0 +++ (c1 +++ c2) = (c0 +++ c1) +++ c2.
Proof.
induction c0; auto.
cbn.
rewrite IHc0.
auto.
Qed.
Definition chain_snoc {X} {P : X -> X -> Type} {A B C : X} :
chain P A B -> P B C -> chain P A C :=
fun c x => c +++ x ::: chain_nil.
Definition chain_fold_right {X} {P : X -> X -> Type}
{F : X -> Type}
(f : forall {A B : X}, P A B -> F B -> F A)
{B : X}
(b : F B)
: forall {A : X}, chain P A B -> F A :=
fix chain_fold_right {A} c :=
match c in (chain _ A' B') return (B = B' -> F A') with
| chain_nil => fun HB => rew [F] HB in b
| x ::: c' =>
fun HB =>
f x (chain_fold_right (rew <- [chain P _] HB in c'))
end eq_refl.
Definition chain_fold_left {X} {P : X -> X -> Type}
{F : X -> Type}
(f : forall {A B : X}, F A -> P A B -> F B)
: forall {A B : X}, F A -> chain P A B -> F B :=
fix chain_fold_left {A B} a c :=
match c in (chain _ A' B') return (A = A' -> F B') with
| chain_nil => fun HA => rew [F] HA in a
| x ::: c' =>
fun HA =>
chain_fold_left (f a (rew <-[fun a => P a _] HA in x)) c'
end eq_refl.
Infix ":::" := chain_cons (at level 60, right associativity).
Fixpoint chain_app {X} {P : X -> X -> Type} {A B C}
(c : chain P A B) (c' : chain P B C) : chain P A C :=
match c in (chain _ A' B') return (B = B' -> chain P A' C) with
| chain_nil => fun HB => rew [fun B => chain P B C] HB in c'
| x ::: xs =>
fun HB =>
x ::: chain_app xs (rew [fun B => chain P B C] HB in c')
end eq_refl.
Infix "+++" := chain_app (right associativity, at level 60).
Theorem chain_app_nil_r {X} {P : X -> X -> Type} {A B}
(c : chain P A B) :
c +++ chain_nil = c.
Proof.
induction c; auto.
cbn.
rewrite IHc.
auto.
Qed.
Theorem chain_app_assoc {X} {P : X -> X -> Type} {A B C D : X}
(c0 : chain P A B) (c1 : chain P B C) (c2 : chain P C D) :
c0 +++ (c1 +++ c2) = (c0 +++ c1) +++ c2.
Proof.
induction c0; auto.
cbn.
rewrite IHc0.
auto.
Qed.
Definition chain_snoc {X} {P : X -> X -> Type} {A B C : X} :
chain P A B -> P B C -> chain P A C :=
fun c x => c +++ x ::: chain_nil.
Definition chain_fold_right {X} {P : X -> X -> Type}
{F : X -> Type}
(f : forall {A B : X}, P A B -> F B -> F A)
{B : X}
(b : F B)
: forall {A : X}, chain P A B -> F A :=
fix chain_fold_right {A} c :=
match c in (chain _ A' B') return (B = B' -> F A') with
| chain_nil => fun HB => rew [F] HB in b
| x ::: c' =>
fun HB =>
f x (chain_fold_right (rew <- [chain P _] HB in c'))
end eq_refl.
Definition chain_fold_left {X} {P : X -> X -> Type}
{F : X -> Type}
(f : forall {A B : X}, F A -> P A B -> F B)
: forall {A B : X}, F A -> chain P A B -> F B :=
fix chain_fold_left {A B} a c :=
match c in (chain _ A' B') return (A = A' -> F B') with
| chain_nil => fun HA => rew [F] HA in a
| x ::: c' =>
fun HA =>
chain_fold_left (f a (rew <-[fun a => P a _] HA in x)) c'
end eq_refl.
this could be expressed in terms of fold_right, but intermediate steps in
computation look nicer if it's spelled out as a fixpoint.
Definition chain_to_list {X} {P : X -> X -> Type}
{L : Type}
(f : forall {A B : X}, P A B -> L)
: forall {A B : X}, chain P A B -> list L :=
fix chain_to_list {A B} c :=
match c with
| chain_nil => nil
| x ::: c' =>
cons (f x) (chain_to_list c')
end.
{L : Type}
(f : forall {A B : X}, P A B -> L)
: forall {A B : X}, chain P A B -> list L :=
fix chain_to_list {A B} c :=
match c with
| chain_nil => nil
| x ::: c' =>
cons (f x) (chain_to_list c')
end.
A bichain is just a chain on a product, but it makes a lot of things easier
to spell it out.
Definition bicurry {A B C D E} (f : A -> B -> C -> D -> E)
: (A * B) -> (C * D) -> E :=
fun ab cd => f (fst ab) (snd ab) (fst cd) (snd cd).
Definition bichain {X Y} (P : X -> Y -> X -> Y -> Type)
(xA : X) (yA : Y) (xB : X) (yB : Y)
: Type := @chain (X * Y) (bicurry P) (xA, yA) (xB, yB).
Definition bichain_cons {X Y} {P : X -> Y -> X -> Y -> Type} {xA yA xB yB xC yC} :
P xA yA xB yB -> bichain P xB yB xC yC -> bichain P xA yA xC yC
:= @chain_cons (X * Y) (bicurry P) (xA, yA) (xB, yB) (xC, yC).
(* Note to self: get more creative with notation *)
Infix "::::" := bichain_cons (at level 60, right associativity).
Definition bichain_fold_right {X Y} {P : X -> Y -> X -> Y -> Type}
{F : X -> Y -> Type}
(f : forall {xA yA xB yB}, P xA yA xB yB -> F xB yB -> F xA yA)
{xB yB}
(b : F xB yB)
{xA : X} {yA : Y}
(c : bichain P xA yA xB yB)
: F xA yA.
Proof.
refine
(@chain_fold_right
(X * Y)
(bicurry P)
(prod_curry F)
_
(xB, yB)
b
(xA, yA)
c).
intros [? ?] [? ?] ? ?.
exact (f _ _ _ _ X0 X1).
Defined.
Definition bichain_to_list {X Y} {P : X -> Y -> X -> Y -> Type}
{L : Type}
(f : forall {xA yA xB yB}, P xA yA xB yB -> L)
{xA yA xB yB} (c : bichain P xA yA xB yB) : list L.
Proof.
refine (chain_to_list _ c).
intros [? ?] [? ?] ?.
eapply f; eauto.
Defined.
Lemma bichain_rect X Y (P : X -> Y -> X -> Y -> Type)
(motive : forall {xA xB yA yB}, bichain P xA xB yA yB -> Type)
(case_nil : forall {x y}, @motive x y x y chain_nil)
(case_cons : forall {xA yA xB yB xC yC}
(x : P xA yA xB yB)
(xs : bichain P xB yB xC yC),
motive xs -> motive (x :::: xs)) :
forall {xA yA xB yB} (c : bichain P xA yA xB yB), motive c.
Proof.
intros.
(* "transparent assert" from https://sympa.inria.fr/sympa/arc/coq-club/2015-10/msg00047.html *)
simple refine (let motive' : forall A B : X * Y, chain (bicurry P) A B -> Type := _ in _). {
intros [? ?] [? ?].
apply motive.
}
change (motive' _ _ c).
apply (chain_rect (X * Y) (bicurry P));
subst motive';
repeat intros [? ?];
eauto.
Qed.