Rocoma.Recipes_logrel
Fixpoint logrel P U : recipe -> Prop :=
match U with
| Void => P
| Arr U V =>
fun s => forall t, closed t -> [ ⊢ t :- U ] ->
(forall ξ, strongly (logrel P U) t.|[ren ξ]) ->
logrel P V (App s t)
| TArr V => fun s => forall T, logrel P V (TApp s T)
end.
Inductive stack_rel P : type -> stack -> Prop :=
| stack_rel_nil :
stack_rel P Void [::]
| stack_rel_term t l U :
stack_rel P U l ->
stack_rel P (TArr U) (T t :: l)
| stack_rel_recipe s l U V :
(forall ξ, strongly (logrel P U) s.|[ren ξ]) ->
stack_rel P V l ->
stack_rel P (Arr U V) (R s :: l).
TOPLAS Lemma 3.1. If P is an n-ary logical relation and (s1,…,sn) are closed recipes of
the same type, then P holds on (s1,…,sn) if and only if P holds on any
tuple of complete applications (s1∘l,…∘l,sn∘l) such that P holds
strongly on (l1,…,ln).
Lemma logical_relation_lemma P U s :
(* closed s -> *)
[ ⊢ s :- U ] ->
logrel P U s <-> (forall l, stack_rel P U l ->
closed_stack l ->
[ ⊨ l :- U ] ->
P (s ∘ l)).
Proof.
move=> ht.
split.
{ elim: U s ht=>//=.
- by move=> s ht h l hl hcl hlt; inv hlt.
- move=> U _ V hV s hty h l hl hcl hlt.
inv hlt=>/=. inv hl=>/=. inv hcl.
apply hV=>//.
+ by apply ty_app with U.
+ by apply h.
- move=> V hV s hty h l hl hcl hlt.
inv hl=>/=. inv hlt. inv hcl.
apply hV=>//.
+ by constructor. }
{ elim: U s ht=>/=.
- move=> s ht hl.
by apply (hl [::]); constructor.
- move=> U hU V hV s hty hl t hct htyt hst.
apply hV.
+ by apply ty_app with U.
+ move=> l hl2 hcl2 hl3.
have->: App s t ∘ l = s ∘ (R t :: l) by [].
by apply hl; constructor.
- move=> V hV s ht hl S.
apply hV.
+ by constructor=>//; apply fv_plage_eq.
+ move=> l hl2 hcl2 hl3.
have->: TApp s S ∘ l = s ∘ (T S :: l) by [].
apply hl.
* by constructor.
* by constructor.
* by constructor=>//; apply fv_plage_eq. }
Qed.
Corollary logical_relation_lemma_proj1 P U s :
logrel P U s ->
forall l,
[ ⊢ s :- U ] ->
stack_rel P U l -> closed_stack l -> [ ⊨ l :- U ] ->
P (s ∘ l).
Proof.
move=> h4 l h2.
move: h2 h4 l.
apply logical_relation_lemma.
Qed.
Corollary logical_relation_lemma_proj2 P U s :
(forall l,
stack_rel P U l -> closed_stack l -> [ ⊨ l :- U ] ->
P (s ∘ l)) ->
[ ⊢ s :- U ] ->
logrel P U s.
Proof.
move=> h4 h2.
move: h2 h4.
apply logical_relation_lemma.
Qed.
Definition aligned l U :=
closed_stack l /\ [ ⊨ l :- U ].
Lemma aligned_type_void l U :
aligned l U ->
forall Γ s,
[ Γ, 0, 0 ⊢ s :- U ] ->
[ Γ, 0, 0 ⊢ s ∘ l :- Void ].
Proof.
move=> [hc ht].
elim: ht hc.
- by move=> _ > ?.
- move=> c ll V hfv ht ih hcl Γ s hs /=.
inv hcl.
apply ih=>//.
by constructor.
- move=> c W ll V hty ht ih hcl Γ s hs /=.
inv hcl.
apply ih=>//.
apply ty_app with W=>//.
by apply closed_has_ty_weak.
Qed.
Lemma aligned_complete l U s :
aligned l U ->
[ ⊢ s :- U ] ->
closed s ->
complete (s ∘ l).
Proof.
move=> [??] ht hc.
split.
- by apply closed_appl.
- by apply aligned_type_void with U.
Qed.
Lemma aligned_cons_r r l W V :
closed_stack (R r :: l) ->
[ ⊨ R r :: l :- Arr W V ] ->
aligned l V.
Proof.
move=> hc h.
by split; [inv hc|inv h].
Qed.
Lemma aligned_cons_t t l V :
closed_stack (T t :: l) ->
[ ⊨ T t :: l :- TArr V ] ->
aligned l V.
Proof.
move=> hc h.
by split; [inv hc|inv h].
Qed.
Lemma aligned_neu l U :
aligned l U ->
aligned (neu_stack l) U.
Proof.
elim: l U=>// -[] ? l ih U h /=.
- inv h. inv H0. inv H.
have hl: aligned l V by [].
destruct (ih _ hl) as [h1 h2].
by split; constructor.
- inv h. inv H0. inv H.
have hl: aligned l V by [].
destruct (ih _ hl) as [h1 h2].
split; constructor=>//.
+ by apply closed_sneu.
+ by apply has_type_neu.
Qed.
Lemma aligned_hsubst θ l U :
aligned l U ->
aligned (stack_hsubst θ l) U.
Proof.
move=> [??].
split; by [apply closed_stack_hsubst|apply stack_has_type_hsubst].
Qed.
Lemma in_aligned_arg l W s :
aligned l W ->
List.In (R s) l ->
exists U, arg_of U W /\ [ ⊢ s :- U ].
Proof.
elim: W l=> [|U _ ? ih|? ih] l hl hin;
move: l hl hin=> [|[?|r] ?] [hc h] hin; try by inv h.
- have hl := aligned_cons_r hc h.
move: hin=> [e|hin].
+ move: e=> [?].
subst r.
exists U.
split; first by constructor.
by inv h.
+ have [U2 [h1 h2]] := ih _ hl hin.
exists U2.
split=>//.
by constructor.
- have hl := aligned_cons_t hc h.
move: hin=> [//|hin].
have [U2 [h1 h2]] := ih _ hl hin.
exists U2.
split=>//.
by constructor.
Qed.
(* TODO: discuss dependant type alternative:
logrel (n: nat) (R: recipe^n -> Prop) (U: type) : recipes^n -> Prop
or metaprogramming ideas... *)
(* Fixpoint logreln P U : recipe^n -> Prop :=
match U with
| Void => P
| Arr U V =>
fun ss => forall ts,
(forall ti, closed ti /\ ⊢ ti :- U ) ->
stronglyn (logreln P U) ts ->
logreln P V (map (i => App^~ ti) ss)
| TArr V =>
...
end. *)
(* closed s -> *)
[ ⊢ s :- U ] ->
logrel P U s <-> (forall l, stack_rel P U l ->
closed_stack l ->
[ ⊨ l :- U ] ->
P (s ∘ l)).
Proof.
move=> ht.
split.
{ elim: U s ht=>//=.
- by move=> s ht h l hl hcl hlt; inv hlt.
- move=> U _ V hV s hty h l hl hcl hlt.
inv hlt=>/=. inv hl=>/=. inv hcl.
apply hV=>//.
+ by apply ty_app with U.
+ by apply h.
- move=> V hV s hty h l hl hcl hlt.
inv hl=>/=. inv hlt. inv hcl.
apply hV=>//.
+ by constructor. }
{ elim: U s ht=>/=.
- move=> s ht hl.
by apply (hl [::]); constructor.
- move=> U hU V hV s hty hl t hct htyt hst.
apply hV.
+ by apply ty_app with U.
+ move=> l hl2 hcl2 hl3.
have->: App s t ∘ l = s ∘ (R t :: l) by [].
by apply hl; constructor.
- move=> V hV s ht hl S.
apply hV.
+ by constructor=>//; apply fv_plage_eq.
+ move=> l hl2 hcl2 hl3.
have->: TApp s S ∘ l = s ∘ (T S :: l) by [].
apply hl.
* by constructor.
* by constructor.
* by constructor=>//; apply fv_plage_eq. }
Qed.
Corollary logical_relation_lemma_proj1 P U s :
logrel P U s ->
forall l,
[ ⊢ s :- U ] ->
stack_rel P U l -> closed_stack l -> [ ⊨ l :- U ] ->
P (s ∘ l).
Proof.
move=> h4 l h2.
move: h2 h4 l.
apply logical_relation_lemma.
Qed.
Corollary logical_relation_lemma_proj2 P U s :
(forall l,
stack_rel P U l -> closed_stack l -> [ ⊨ l :- U ] ->
P (s ∘ l)) ->
[ ⊢ s :- U ] ->
logrel P U s.
Proof.
move=> h4 h2.
move: h2 h4.
apply logical_relation_lemma.
Qed.
Definition aligned l U :=
closed_stack l /\ [ ⊨ l :- U ].
Lemma aligned_type_void l U :
aligned l U ->
forall Γ s,
[ Γ, 0, 0 ⊢ s :- U ] ->
[ Γ, 0, 0 ⊢ s ∘ l :- Void ].
Proof.
move=> [hc ht].
elim: ht hc.
- by move=> _ > ?.
- move=> c ll V hfv ht ih hcl Γ s hs /=.
inv hcl.
apply ih=>//.
by constructor.
- move=> c W ll V hty ht ih hcl Γ s hs /=.
inv hcl.
apply ih=>//.
apply ty_app with W=>//.
by apply closed_has_ty_weak.
Qed.
Lemma aligned_complete l U s :
aligned l U ->
[ ⊢ s :- U ] ->
closed s ->
complete (s ∘ l).
Proof.
move=> [??] ht hc.
split.
- by apply closed_appl.
- by apply aligned_type_void with U.
Qed.
Lemma aligned_cons_r r l W V :
closed_stack (R r :: l) ->
[ ⊨ R r :: l :- Arr W V ] ->
aligned l V.
Proof.
move=> hc h.
by split; [inv hc|inv h].
Qed.
Lemma aligned_cons_t t l V :
closed_stack (T t :: l) ->
[ ⊨ T t :: l :- TArr V ] ->
aligned l V.
Proof.
move=> hc h.
by split; [inv hc|inv h].
Qed.
Lemma aligned_neu l U :
aligned l U ->
aligned (neu_stack l) U.
Proof.
elim: l U=>// -[] ? l ih U h /=.
- inv h. inv H0. inv H.
have hl: aligned l V by [].
destruct (ih _ hl) as [h1 h2].
by split; constructor.
- inv h. inv H0. inv H.
have hl: aligned l V by [].
destruct (ih _ hl) as [h1 h2].
split; constructor=>//.
+ by apply closed_sneu.
+ by apply has_type_neu.
Qed.
Lemma aligned_hsubst θ l U :
aligned l U ->
aligned (stack_hsubst θ l) U.
Proof.
move=> [??].
split; by [apply closed_stack_hsubst|apply stack_has_type_hsubst].
Qed.
Lemma in_aligned_arg l W s :
aligned l W ->
List.In (R s) l ->
exists U, arg_of U W /\ [ ⊢ s :- U ].
Proof.
elim: W l=> [|U _ ? ih|? ih] l hl hin;
move: l hl hin=> [|[?|r] ?] [hc h] hin; try by inv h.
- have hl := aligned_cons_r hc h.
move: hin=> [e|hin].
+ move: e=> [?].
subst r.
exists U.
split; first by constructor.
by inv h.
+ have [U2 [h1 h2]] := ih _ hl hin.
exists U2.
split=>//.
by constructor.
- have hl := aligned_cons_t hc h.
move: hin=> [//|hin].
have [U2 [h1 h2]] := ih _ hl hin.
exists U2.
split=>//.
by constructor.
Qed.
(* TODO: discuss dependant type alternative:
logrel (n: nat) (R: recipe^n -> Prop) (U: type) : recipes^n -> Prop
or metaprogramming ideas... *)
(* Fixpoint logreln P U : recipe^n -> Prop :=
match U with
| Void => P
| Arr U V =>
fun ss => forall ts,
(forall ti, closed ti /\ ⊢ ti :- U ) ->
stronglyn (logreln P U) ts ->
logreln P V (map (i => App^~ ti) ss)
| TArr V =>
...
end. *)
Redefinitions of logical relation related lemmas,
applied to a couple of recipes.
Fixpoint logrel2 P U : recipe -> recipe -> Prop :=
match U with
| Void => P
| Arr U V =>
fun s1 s2 => forall t1 t2,
closed t1 -> [ ⊢ t1 :- U ] ->
closed t2 -> [ ⊢ t2 :- U ] ->
(forall ξ, strongly2 (logrel2 P U) t1.|[ren ξ] t2.|[ren ξ]) ->
logrel2 P V (App s1 t1) (App s2 t2)
| TArr V =>
fun s1 s2 => forall T,
logrel2 P V (TApp s1 T) (TApp s2 T)
end.
Inductive stack_rel2 P : type -> stack -> stack -> Prop :=
| stack_rel2_nil :
stack_rel2 P Void [::] [::]
| stack_rel2_term t l1 l2 U :
stack_rel2 P U l1 l2 ->
stack_rel2 P (TArr U) (T t :: l1) (T t :: l2)
| stack_rel2_recipe s t l1 l2 U V :
(forall ξ, strongly2 (logrel2 P U) s.|[ren ξ] t.|[ren ξ]) ->
stack_rel2 P V l1 l2 ->
stack_rel2 P (Arr U V) (R s :: l1) (R t :: l2).
Lemma logical_relation_lemma2 P U s t :
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
logrel2 P U s t <-> (forall l1 l2, stack_rel2 P U l1 l2 ->
aligned l1 U -> aligned l2 U ->
P (s ∘ l1) (t ∘ l2)).
Proof.
move=> hc1 ht1 hc2 ht2.
rewrite /aligned.
split.
{ elim: U s t hc1 ht1 hc2 ht2.
- by move=> > ???? /= ? > hl [??] [??]; inv hl.
- move=> U h1 V h2 > ???? /= h ?? hl [ha1 hb1] [ha2 hb2].
inv hl=>/=. inv ha1. inv hb1. inv ha2. inv hb2.
apply h2=>//;
first [ by apply closed_app; split
| by apply ty_app with U
| by apply h
| by split
| idtac ].
- move=> V h2 > ???? /= h ?? hl [ha1 hb1] [ha2 hb2].
inv hl=>/=. inv ha1. inv hb1. inv ha2. inv hb2.
apply h2=>//;
first [ by apply closed_tapp
| by constructor=>//; apply fv_plage_eq
| by apply h
| by split
| idtac ]. }
{ elim: U s t hc1 ht1 hc2 ht2.
- move=> > ???? h.
apply: (h [::] [::]).
+ by constructor.
+ by split; constructor.
+ by split; constructor.
- move=> U h1 V h2 s t ???? h /= u v ???? hst.
apply h2;
first [ by apply closed_app; split
| by apply ty_app with U
| idtac ].
move=> l1 l2 hl [??] [??].
have->: App s u ∘ l1 = s ∘ (R u :: l1) by [].
have->: App t v ∘ l2 = t ∘ (R v :: l2) by [].
apply h.
+ by constructor.
+ by split; constructor.
+ by split; constructor.
- move=> V h2 s t ???? h /= S.
apply h2=>//;
first [ by apply closed_tapp
| by constructor=>//; apply fv_plage_eq
| idtac ].
move=> l1 l2 hl [??] [??].
have->: TApp s S ∘ l1 = s ∘ (T S :: l1) by [].
have->: TApp t S ∘ l2 = t ∘ (T S :: l2) by [].
apply h.
+ by constructor.
+ by split; constructor=>//; apply fv_plage_eq.
+ by split; constructor=>//; apply fv_plage_eq. }
Qed.
Corollary logical_relation_lemma2_proj1 P U s t :
logrel2 P U s t ->
forall l1 l2,
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
stack_rel2 P U l1 l2 -> aligned l1 U -> aligned l2 U ->
P (s ∘ l1) (t ∘ l2).
Proof.
move=> h7 l1 l2 h1 h3 h4 h6.
move: h1 h3 h4 h6 h7 l1 l2.
by apply logical_relation_lemma2.
Qed.
Corollary logical_relation_lemma2_proj2 P U s t :
(forall l1 l2, stack_rel2 P U l1 l2 -> aligned l1 U -> aligned l2 U ->
P (s ∘ l1) (t ∘ l2)) ->
closed s -> [ ⊢ s :- U ] ->
closed t -> [ ⊢ t :- U ] ->
logrel2 P U s t.
Proof.
move=> h7 h1 h3 h4 h6.
move: h1 h3 h4 h6 h7.
by apply logical_relation_lemma2.
Qed.
(* TODO: question de JCF à réfléchir *)
(* Definition lr (P : recipe -> Prop) U := logrel2 (fun s1 _=> P s1) U ^~ Top.
Lemma ttt P U s : lr P U s = logrel P U s.
elim: U s=>//=.
- move=> U h1 V h2 s. rewrite /lr/=. *)
Lemma aligned_closed_appl2 U s l1 l2 :
closed s ->
aligned l1 U -> aligned l2 U ->
closed (s ∘ l1) /\
closed (s ∘ l2).
Proof.
move=> hs [??] [??].
by split; apply closed_appl.
Qed.
Lemma aligned_type_void2 U s l1 l2 :
[ ⊢ s :- U ] ->
aligned l1 U -> aligned l2 U ->
[ ⊢ s ∘ l1 :- Void ] /\
[ ⊢ s ∘ l2 :- Void ].
Proof.
move=> hs ha1 ha2.
by split; apply aligned_type_void with U.
Qed.