DCOIOmega.conv
Require Import imports par geq.
Module Type conv_sig
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax)
(Import ieq : geq_sig lattice syntax).
Definition iconv Ξ ℓ a b := exists c0 c1, a ⇒* c0 /\ b ⇒* c1 /\ IEq Ξ ℓ c0 c1.
Definition conv Ξ a b := exists ℓ, iconv Ξ ℓ a b.
End conv_sig.
Module conv_facts
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax)
(Import ieq : geq_sig lattice syntax)
(Import conv : conv_sig lattice syntax par ieq).
Module pfacts := par_facts lattice syntax par.
Module ifacts := geq_facts lattice syntax ieq.
Import pfacts.
Import ifacts.
Lemma ieq_iconv Ξ ℓ a b : IEq Ξ ℓ a b -> iconv Ξ ℓ a b.
Proof. sfirstorder use:rtc_refl unfold:iconv. Qed.
Lemma iok_preservation Ξ ℓ a (h : IOk Ξ ℓ a) : forall b, a ⇒ b -> IOk Ξ ℓ b.
Proof.
elim : Ξ ℓ a / h; try qauto inv:Par ctrs:IOk.
(* App *)
- move => Ξ ℓ a ℓ0 b ha iha hb ihb b0.
elim /Par_inv=>//.
+ hauto lq:on ctrs:IOk.
+ move => _ a0 a1 b1 b2 ℓ1 ha0 hb1 [*]. subst.
apply : iok_subst; eauto.
have /iha : tAbs ℓ0 a0 ⇒ tAbs ℓ0 a1 by eauto with par.
by inversion 1.
(* Let *)
- move => Ξ ℓ ℓ0 ℓ1 a b ? ha iha hb ihb ?.
elim /Par_inv=>//_.
+ hauto lq:on ctrs:IOk.
+ move => ? ℓ2 a0 b0 c0 a1 b1 c1 ? ? ? [*]. subst.
apply : iok_morphing; eauto.
have /iha {}iha : tPack ℓ0 a0 b0 ⇒ tPack ℓ0 a1 b1 by eauto with par.
hauto lq:on use:iok_subst_cons, iok_subst_id inv:IOk.
(* Ind *)
- move => Ξ ℓ ℓ0 a b c ? ha iha hb ihb hc ihc b0.
elim /Par_inv=>//_.
+ hauto lq:on ctrs:IOk.
+ move => ℓ1 a0 a1 b1 ? [*]. subst.
eauto using iok_subsumption.
+ move => ℓ1 a0 a1 b1 b2 c0 c1 ha' hb' hc' [*] [:tr0]. subst.
apply : iok_morphing; eauto.
by eauto using iok_subsumption.
apply iok_subst_cons; eauto.
apply iok_subst_cons.
apply iok_subst_id.
abstract : tr0.
have : tSuc c0 ⇒ tSuc c1 by eauto with par.
qauto l:on inv:IOk.
hauto q:on ctrs:IOk use:meet_idempotent.
Qed.
Lemma iok_preservation_star Ξ ℓ a (h : IOk Ξ ℓ a) : forall b, a ⇒* b -> IOk Ξ ℓ b.
Proof. induction 1; sfirstorder use:iok_preservation. Qed.
Lemma simulation : forall Ξ ℓ,
(forall a b, IEq Ξ ℓ a b ->
forall a', Par a a' ->
exists b', Par b b' /\ IEq Ξ ℓ a' b') /\
(forall ℓ0 a b, GIEq Ξ ℓ ℓ0 a b ->
forall a', Par a a' ->
exists b', Par b b' /\ GIEq Ξ ℓ ℓ0 a' b').
Proof.
apply IEq_mutual; try qauto ctrs:IEq, Par, GIEq inv:Par.
- hauto lq:on ctrs:IEq, Par inv:Par, IEq.
- move => Ξ ℓ ℓ0 a0 a1 h0 ih0 a'.
elim /Par_inv => // h1 ℓ1 a2 a3 h2 [*]; subst.
case /ih0 : (h2) => a2 h.
exists (tAbs ℓ0 a2).
hauto lq:on ctrs:IEq, Par use:Par_refl.
- move => Ξ ℓ a0 a1 ℓ0 b0 b1 h0 ih0 h1 ih1 a'.
elim /Par_inv => //.
+ hauto lq:on ctrs:Par, IEq.
+ move => hp a2 a3 b2 b3 ℓ1 h2 h3 [*]; subst.
case /ih1 : h3 => b4 [h30 h31].
elim /IEq_inv : h0 => // _ ℓ1 a0 a4 he [*]. subst.
have /ih0 : tAbs ℓ0 a2 ⇒ tAbs ℓ0 a3 by eauto with par.
move => [? []].
elim /Par_inv => // _ ℓ1 a0 a1 ? [? ? ?]. subst.
elim /IEq_inv => // _ ℓ1 a0 a5 ?[? ?][? ?]. subst.
exists (a1[b4..]). split.
by auto using Par_refl with par.
sfirstorder use:ieq_morphing_mutual, ieq_subst_cons, ieq_subst_id.
- hauto lq:on ctrs:IEq inv:Par use:Par_refl.
- move => Ξ ℓ ℓ0 a0 a1 b0 b1 ? ha iha hb ihb ?.
elim /Par_inv=>// _ ? ? ? a2 b2 + + [*]. subst.
move /iha => {iha} [a1' ha1'].
move /ihb => {ihb} [b1' hb1'].
exists (tEq ℓ0 a1' b1').
hauto lq:on ctrs:Par, IEq use:Par_refl.
- move => Ξ ℓ ℓp t0 t1 p0 p1 ? ? ht ? hp p.
elim /Par_inv=>// _.
+ move => ? ? ? t2 p2 + + [*]. subst.
move /ht => {}ht.
move /hp => {}hp.
move : ht => [t']?.
move : hp => [p']?.
exists (tJ ℓp t' p').
hauto lq:on ctrs:IEq, Par use:Par_refl.
+ move => ℓp0 t2 t3 + [*]. subst.
have ? : p1 = tRefl by qauto l:on inv:IEq. subst.
hauto l:on ctrs:Par, IEq.
- hauto lq:on ctrs:IEq, Par inv:Par, IEq.
- hauto lq:on ctrs:IEq, Par inv:Par, IEq.
- move => Ξ ℓ ℓ0 ℓ1 a0 b0 a1 b1 ? ha iha hb ihb a'.
elim /Par_inv => //= _.
+ hauto lq:on ctrs:IEq, Par.
+ move => ? ? a2 b2 c0 a3 b3 c1 ? ? hbc [*]. subst.
elim /IEq_inv : ha=>//= hp ℓ2 a0 b4 a4 b5 ? ? [*]. subst.
have /iha : tPack ℓ0 a2 b2 ⇒ tPack ℓ0 a3 b3 by auto using P_Pack.
move => [b'][hp'].
elim /IEq_inv=>//= _ ℓ2 a0 b4 a1 b6 ? ? [*]. subst.
move /ihb : hbc.
have {hp}[? ?] : a4 ⇒ a1 /\ b5 ⇒ b6 by inversion hp'.
move => [b'][?]?.
exists (b'[b6.:a1..]).
split. by eauto using P_LetPack.
eapply ieq_morphing_mutual; eauto.
case => [|i]//=.
* rewrite /elookup => //=.
move => ℓ2 [*]. subst.
case : (lprop.sub_eqdec ℓ2 ℓ) => ?;
by eauto with ieq.
* move => ℓ2.
rewrite /elookup//=.
case : i=>[|i]//=.
scongruence.
case : (lprop.sub_eqdec ℓ2 ℓ) => ?;
by eauto with ieq.
- hauto q:on ctrs:Par, IEq inv:Par, IEq.
- move => Ξ ℓ ℓ0 a0 b0 c0 a1 b1 c1 ? ha iha hb ihb hc ihc a'.
elim/Par_inv=>//=_.
+ hauto lq:on ctrs:IEq, Par.
+ move => ℓ1 a2 a3 b2 ? [*]. subst.
inversion hc; subst. hauto lq:on ctrs:Par, IEq.
+ move => ℓ1 a2 a3 b2 b3 c2 c3 +++ [*]. subst.
elim /IEq_inv : hc => //=_ a2 a4 ha24 [?]?. subst.
move /iha => {iha} [a1'][ha1]ha1'.
move /ihb => {ihb} [b1'][hb1]hb1'.
move /P_Suc /ihc => {ihc} [c1'][hc1]hc1'.
elim /Par_inv : hc1 => //= _ a2 b2 ? [*]. subst.
elim /IEq_inv : hc1' => //= _ a2 a5 ? [?][?]. subst.
eexists.
split. eauto with par.
eapply ieq_morphing_mutual; eauto.
case => [|i]//=.
hauto lq:on ctrs:GIEq, IEq unfold:elookup.
move => ℓ1; rewrite /elookup //=.
case : i => [|i]//=.
hauto lq:on ctrs:GIEq, IEq unfold:elookup.
move => ?. apply ieq_gieq. move => *.
apply : I_Var; eauto.
- move => Ξ ℓ ℓ0 a0 a1 b0 b1 ? ha iha hb ihb u.
elim /Par_inv=>//=_.
+ hauto lq:on ctrs:Par,IEq.
+ move => ℓ1 b2 b3 ? [*]. subst.
have ? : a1 = tTT by inversion ha. subst.
hauto lq:on ctrs:IEq, Par.
- hauto l:on ctrs:Par use:Par_refl.
Qed.
(* Lemma 3.2 (Simulation) *)
Lemma simulation_star Ξ ℓ a b a' (h : IEq Ξ ℓ a b) (h0 : a ⇒* a') :
exists b', b ⇒* b' /\ IEq Ξ ℓ a' b'.
Proof.
move : b h.
elim : a a' / h0.
- sfirstorder.
- move => a a0 a1 ha ha0 ih b hab.
suff : exists b0,Par b b0 /\ IEq Ξ ℓ a0 b0; hauto lq:on use:simulation ctrs:rtc.
Qed.
Lemma conv_refl Ξ ℓ a : IOk Ξ ℓ a -> conv Ξ a a.
Proof.
move /iok_ieq /(_ ℓ ltac:(by rewrite meet_idempotent)) /ieq_iconv => h /ltac:(exists ℓ) //.
Qed.
Lemma iconv_sym Ξ ℓ a b : iconv Ξ ℓ a b -> iconv Ξ ℓ b a.
Proof. hauto lq:on use:ieq_sym_mutual unfold:conv, iconv. Qed.
Lemma conv_sym Ξ a b : conv Ξ a b -> conv Ξ b a.
Proof. hauto lq:on use:iconv_sym unfold:conv. Qed.
Lemma iconv_rpar Ξ ℓ a b a0 :
iconv Ξ ℓ a b -> a0 ⇒ a -> iconv Ξ ℓ a0 b.
Proof. hauto lq:on ctrs:rtc unfold:iconv. Qed.
Lemma conv_rpar Ξ a b a0 :
conv Ξ a b -> a0 ⇒ a -> conv Ξ a0 b.
Proof. hauto use:iconv_rpar unfold:conv. Qed.
Lemma iconv_par Ξ ℓ a b a0 :
iconv Ξ ℓ a b -> a ⇒ a0 -> iconv Ξ ℓ a0 b.
Proof.
rewrite /iconv.
move => [c0][c1][h0][h1]h2 h3.
apply rtc_once in h3.
move : Pars_confluent (h0) (h3). repeat move/[apply].
move => [ca][h5]h6.
move : simulation_star (h2) (h5). repeat move/[apply].
move /ieq_sym in h2.
move => [c1' [h7 h8]].
exists ca, c1'.
hauto l:on use:rtc_transitive.
Qed.
Lemma conv_par Ξ a b a0 :
conv Ξ a b -> a ⇒ a0 -> conv Ξ a0 b.
Proof.
hauto lq:on use:iconv_par unfold:conv.
Qed.
Lemma iconv_par2 Ξ ℓ a b a0 b0 :
iconv Ξ ℓ a b -> a ⇒ a0 -> b ⇒ b0 -> iconv Ξ ℓ a0 b0.
Proof. hauto lq:on use:iconv_par, iconv_sym. Qed.
Lemma ieq_trans_heterogeneous Ξ ℓ ℓ0 a b c :
IEq Ξ ℓ a b ->
IEq Ξ ℓ0 b c ->
IEq Ξ (ℓ ∩ ℓ0) a c.
Proof.
move => h0 h1.
apply ieq_trans with (B := b).
- apply ieq_sym_mutual.
apply ieq_sym_mutual in h0.
eapply ieq_downgrade_mutual; eauto.
- apply ieq_sym_mutual in h0.
rewrite meet_commutative.
eapply ieq_downgrade_mutual; eauto.
Qed.
Lemma ieq_trans_heterogeneous_leq Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
IEq Ξ ℓ a b ->
IEq Ξ ℓ0 b c ->
IEq Ξ ℓ a c.
Proof.
hauto l:on drew:off use:ieq_trans_heterogeneous, meet_commutative.
Qed.
Lemma ieq_trans_heterogeneous_leq' Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
IEq Ξ ℓ0 a b ->
IEq Ξ ℓ b c ->
IEq Ξ ℓ a c.
Proof.
move => h.
move /ieq_trans_heterogeneous /[apply].
rewrite meet_commutative. congruence.
Qed.
Lemma iconv_trans_heterogeneous Ξ ℓ0 ℓ1 a b c :
iconv Ξ ℓ0 a b -> iconv Ξ ℓ1 b c -> iconv Ξ (ℓ0 ∩ ℓ1) a c.
Proof.
rewrite /iconv.
move => [a0 [b0 [h0 [h1 h2]]]].
move => [b1 [c0 [h3 [h4 h5]]]].
move : Pars_confluent (h1) (h3). repeat move/[apply].
move => [q [h6 h7]].
move /ieq_sym in h2.
move : simulation_star (h2) (h6). repeat move/[apply].
move => [p0][? ?].
move : simulation_star (h5) (h7). repeat move/[apply].
move => [p1][? ?].
exists p0, p1. hauto lq:on use:ieq_sym, ieq_trans_heterogeneous, rtc_transitive.
Qed.
Lemma iconv_trans_heterogeneous_leq Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
iconv Ξ ℓ a b ->
iconv Ξ ℓ0 b c ->
iconv Ξ ℓ a c.
Proof.
hauto l:on drew:off use:iconv_trans_heterogeneous, meet_commutative.
Qed.
Lemma iconv_trans_heterogeneous_leq' Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
iconv Ξ ℓ0 a b ->
iconv Ξ ℓ b c ->
iconv Ξ ℓ a c.
Proof.
move => h.
move /iconv_trans_heterogeneous /[apply].
rewrite meet_commutative. congruence.
Qed.
Lemma iconv_trans Ξ ℓ a b c :
iconv Ξ ℓ a b -> iconv Ξ ℓ b c -> iconv Ξ ℓ a c.
Proof.
hauto l:on use:iconv_trans_heterogeneous_leq, meet_idempotent.
Qed.
(* Lemma 4.3 (Transitivity of Equality) *)
Lemma conv_trans Ξ a b c : conv Ξ a b -> conv Ξ b c -> conv Ξ a c.
Proof.
hauto lq:on use:iconv_trans_heterogeneous unfold:conv.
Qed.
Lemma iconv_subst Ξ ℓ Δ ρ (h : iok_subst_ok ρ Ξ Δ) a b (h0 : iconv Ξ ℓ a b) :
iconv Δ ℓ a[ρ] b[ρ].
Proof.
rewrite /iconv in h0 *.
move : h0 => [c0][c1][h0][h1]h2.
exists c0[ρ], c1[ρ].
sfirstorder use:ieq_morphing_iok, Par_subst_star.
Qed.
Lemma conv_subst Ξ Δ ρ (h : iok_subst_ok ρ Ξ Δ) a b (h0 : conv Ξ a b) :
conv Δ a[ρ] b[ρ].
Proof. hauto lq:on use:iconv_subst unfold:conv. Qed.
Lemma ieq_conv Ξ ℓ a b : IEq Ξ ℓ a b -> conv Ξ a b.
Proof. rewrite /conv; eauto using ieq_iconv. Qed.
Lemma conv_univ_inj Ξ i j : conv Ξ (tUniv i) (tUniv j) -> i = j.
Proof.
rewrite /conv/iconv.
move => [ℓ][c0][c1][/Pars_univ_inv h0][/Pars_univ_inv h1]h2. subst.
by inversion h2; subst.
Qed.
Lemma iconv_pi_inj Ξ ℓ ℓ0 A0 B0 ℓ1 A1 B1 :
iconv Ξ ℓ (tPi ℓ0 A0 B0) (tPi ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
iconv Ξ ℓ A0 A1 /\
iconv (ℓ0 :: Ξ) ℓ B0 B1.
Proof.
rewrite /iconv.
move => [c0][c1][hPi0][hPi1]heq.
move /Pars_pi_inv : hPi0 => [A0'][B0'][h0][h1]h2.
move /Pars_pi_inv : hPi1 => [A1'][B1'][h3][h4]h5.
subst.
hauto lq:on inv:IEq.
Qed.
Lemma iconv_sig_inj Ξ ℓ ℓ0 A0 B0 ℓ1 A1 B1 :
iconv Ξ ℓ (tSig ℓ0 A0 B0) (tSig ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
iconv Ξ ℓ A0 A1 /\
iconv (ℓ0 :: Ξ) ℓ B0 B1.
Proof.
rewrite /iconv.
move => [c0][c1][hPi0][hPi1]heq.
move /Pars_sig_inv : hPi0 => [A0'][B0'][h0][h1]h2.
move /Pars_sig_inv : hPi1 => [A1'][B1'][h3][h4]h5.
subst.
hauto lq:on inv:IEq.
Qed.
Lemma conv_pi_inj Ξ ℓ0 A0 B0 ℓ1 A1 B1 :
conv Ξ (tPi ℓ0 A0 B0) (tPi ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
conv Ξ A0 A1 /\
conv (ℓ0 :: Ξ) B0 B1.
Proof. rewrite/conv; hauto lq:on use:iconv_pi_inj. Qed.
Lemma conv_sig_inj Ξ ℓ0 A0 B0 ℓ1 A1 B1 :
conv Ξ (tSig ℓ0 A0 B0) (tSig ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
conv Ξ A0 A1 /\
conv (ℓ0 :: Ξ) B0 B1.
Proof. rewrite/conv; hauto lq:on use:iconv_sig_inj. Qed.
Lemma conv_eq_inj Ξ ℓ0 a0 b0 ℓ1 a1 b1 : conv Ξ (tEq ℓ0 a0 b0) (tEq ℓ1 a1 b1) -> ℓ0 = ℓ1 /\ exists ℓ, ℓ0 ⊆ ℓ /\ iconv Ξ ℓ a0 a1 /\ iconv Ξ ℓ b0 b1.
Proof.
rewrite /conv/iconv.
move => [ℓ][c0][c1][h0][h1]h2.
move /Pars_eq_inv : h0 => [a0'][b0'][h3][h4]h5. subst.
move /Pars_eq_inv : h1 => [a1'][b1'][h6][h7]h8. subst.
elim /IEq_inv : h2 => // _ ℓ2 a2 a3 b2 b3 ? ? ? [? ? ?] [? ? ?]. subst.
sfirstorder.
Qed.
Lemma iconv_iok_downgrade Ξ ℓ0 ℓ1 a b :
IOk Ξ ℓ0 a -> iconv Ξ ℓ1 a b -> iconv Ξ (ℓ0 ∩ ℓ1) a b.
Proof.
rewrite /iconv.
move => ha [a'][b'][h0][h1]h2.
exists a', b'.
repeat split => //.
suff /iok_ieq /(_ ℓ0) /(_ ltac:(by rewrite meet_idempotent)) : IOk Ξ ℓ0 a'.
rewrite meet_commutative.
sfirstorder use:ieq_downgrade_mutual.
eauto using iok_preservation_star.
Qed.
Lemma iconv_renaming : forall Ξ ℓ a b,
iconv Ξ ℓ a b ->
forall ξ Δ, iok_ren_ok ξ Ξ Δ ->
iconv Δ ℓ (ren_tm ξ a) (ren_tm ξ b).
Proof.
hauto lq:on use:Pars_renaming, ieq_weakening_mutual unfold:iconv.
Qed.
Lemma conv_renaming : forall Ξ a b,
conv Ξ a b ->
forall ξ Δ, iok_ren_ok ξ Ξ Δ ->
conv Δ (ren_tm ξ a) (ren_tm ξ b).
Proof. hauto lq:on use:iconv_renaming unfold:conv. Qed.
Lemma iconv_conv Ξ ℓ a b : iconv Ξ ℓ a b -> conv Ξ a b.
Proof. sfirstorder unfold:conv. Qed.
Lemma iconv_par_star Ξ ℓ a b a0 :
iconv Ξ ℓ a b -> a ⇒* a0 -> iconv Ξ ℓ a0 b.
Proof.
move => h h0.
move : Ξ b h.
induction h0;
hauto lq:on use:iconv_par unfold:conv.
Qed.
Lemma iconv_par_star2 Ξ ℓ a b a0 b0 :
iconv Ξ ℓ a b -> a ⇒* a0 -> b ⇒* b0 -> iconv Ξ ℓ a0 b0.
Proof. hauto lq:on use:iconv_par_star, iconv_sym. Qed.
Lemma conv_par_star2 Ξ a b a0 b0 :
conv Ξ a b -> a ⇒* a0 -> b ⇒* b0 -> conv Ξ a0 b0.
Proof. hauto lq:on use:iconv_par_star2, iconv_conv. Qed.
End conv_facts.
Module Type conv_sig
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax)
(Import ieq : geq_sig lattice syntax).
Definition iconv Ξ ℓ a b := exists c0 c1, a ⇒* c0 /\ b ⇒* c1 /\ IEq Ξ ℓ c0 c1.
Definition conv Ξ a b := exists ℓ, iconv Ξ ℓ a b.
End conv_sig.
Module conv_facts
(Import lattice : Lattice)
(Import syntax : syntax_sig lattice)
(Import par : par_sig lattice syntax)
(Import ieq : geq_sig lattice syntax)
(Import conv : conv_sig lattice syntax par ieq).
Module pfacts := par_facts lattice syntax par.
Module ifacts := geq_facts lattice syntax ieq.
Import pfacts.
Import ifacts.
Lemma ieq_iconv Ξ ℓ a b : IEq Ξ ℓ a b -> iconv Ξ ℓ a b.
Proof. sfirstorder use:rtc_refl unfold:iconv. Qed.
Lemma iok_preservation Ξ ℓ a (h : IOk Ξ ℓ a) : forall b, a ⇒ b -> IOk Ξ ℓ b.
Proof.
elim : Ξ ℓ a / h; try qauto inv:Par ctrs:IOk.
(* App *)
- move => Ξ ℓ a ℓ0 b ha iha hb ihb b0.
elim /Par_inv=>//.
+ hauto lq:on ctrs:IOk.
+ move => _ a0 a1 b1 b2 ℓ1 ha0 hb1 [*]. subst.
apply : iok_subst; eauto.
have /iha : tAbs ℓ0 a0 ⇒ tAbs ℓ0 a1 by eauto with par.
by inversion 1.
(* Let *)
- move => Ξ ℓ ℓ0 ℓ1 a b ? ha iha hb ihb ?.
elim /Par_inv=>//_.
+ hauto lq:on ctrs:IOk.
+ move => ? ℓ2 a0 b0 c0 a1 b1 c1 ? ? ? [*]. subst.
apply : iok_morphing; eauto.
have /iha {}iha : tPack ℓ0 a0 b0 ⇒ tPack ℓ0 a1 b1 by eauto with par.
hauto lq:on use:iok_subst_cons, iok_subst_id inv:IOk.
(* Ind *)
- move => Ξ ℓ ℓ0 a b c ? ha iha hb ihb hc ihc b0.
elim /Par_inv=>//_.
+ hauto lq:on ctrs:IOk.
+ move => ℓ1 a0 a1 b1 ? [*]. subst.
eauto using iok_subsumption.
+ move => ℓ1 a0 a1 b1 b2 c0 c1 ha' hb' hc' [*] [:tr0]. subst.
apply : iok_morphing; eauto.
by eauto using iok_subsumption.
apply iok_subst_cons; eauto.
apply iok_subst_cons.
apply iok_subst_id.
abstract : tr0.
have : tSuc c0 ⇒ tSuc c1 by eauto with par.
qauto l:on inv:IOk.
hauto q:on ctrs:IOk use:meet_idempotent.
Qed.
Lemma iok_preservation_star Ξ ℓ a (h : IOk Ξ ℓ a) : forall b, a ⇒* b -> IOk Ξ ℓ b.
Proof. induction 1; sfirstorder use:iok_preservation. Qed.
Lemma simulation : forall Ξ ℓ,
(forall a b, IEq Ξ ℓ a b ->
forall a', Par a a' ->
exists b', Par b b' /\ IEq Ξ ℓ a' b') /\
(forall ℓ0 a b, GIEq Ξ ℓ ℓ0 a b ->
forall a', Par a a' ->
exists b', Par b b' /\ GIEq Ξ ℓ ℓ0 a' b').
Proof.
apply IEq_mutual; try qauto ctrs:IEq, Par, GIEq inv:Par.
- hauto lq:on ctrs:IEq, Par inv:Par, IEq.
- move => Ξ ℓ ℓ0 a0 a1 h0 ih0 a'.
elim /Par_inv => // h1 ℓ1 a2 a3 h2 [*]; subst.
case /ih0 : (h2) => a2 h.
exists (tAbs ℓ0 a2).
hauto lq:on ctrs:IEq, Par use:Par_refl.
- move => Ξ ℓ a0 a1 ℓ0 b0 b1 h0 ih0 h1 ih1 a'.
elim /Par_inv => //.
+ hauto lq:on ctrs:Par, IEq.
+ move => hp a2 a3 b2 b3 ℓ1 h2 h3 [*]; subst.
case /ih1 : h3 => b4 [h30 h31].
elim /IEq_inv : h0 => // _ ℓ1 a0 a4 he [*]. subst.
have /ih0 : tAbs ℓ0 a2 ⇒ tAbs ℓ0 a3 by eauto with par.
move => [? []].
elim /Par_inv => // _ ℓ1 a0 a1 ? [? ? ?]. subst.
elim /IEq_inv => // _ ℓ1 a0 a5 ?[? ?][? ?]. subst.
exists (a1[b4..]). split.
by auto using Par_refl with par.
sfirstorder use:ieq_morphing_mutual, ieq_subst_cons, ieq_subst_id.
- hauto lq:on ctrs:IEq inv:Par use:Par_refl.
- move => Ξ ℓ ℓ0 a0 a1 b0 b1 ? ha iha hb ihb ?.
elim /Par_inv=>// _ ? ? ? a2 b2 + + [*]. subst.
move /iha => {iha} [a1' ha1'].
move /ihb => {ihb} [b1' hb1'].
exists (tEq ℓ0 a1' b1').
hauto lq:on ctrs:Par, IEq use:Par_refl.
- move => Ξ ℓ ℓp t0 t1 p0 p1 ? ? ht ? hp p.
elim /Par_inv=>// _.
+ move => ? ? ? t2 p2 + + [*]. subst.
move /ht => {}ht.
move /hp => {}hp.
move : ht => [t']?.
move : hp => [p']?.
exists (tJ ℓp t' p').
hauto lq:on ctrs:IEq, Par use:Par_refl.
+ move => ℓp0 t2 t3 + [*]. subst.
have ? : p1 = tRefl by qauto l:on inv:IEq. subst.
hauto l:on ctrs:Par, IEq.
- hauto lq:on ctrs:IEq, Par inv:Par, IEq.
- hauto lq:on ctrs:IEq, Par inv:Par, IEq.
- move => Ξ ℓ ℓ0 ℓ1 a0 b0 a1 b1 ? ha iha hb ihb a'.
elim /Par_inv => //= _.
+ hauto lq:on ctrs:IEq, Par.
+ move => ? ? a2 b2 c0 a3 b3 c1 ? ? hbc [*]. subst.
elim /IEq_inv : ha=>//= hp ℓ2 a0 b4 a4 b5 ? ? [*]. subst.
have /iha : tPack ℓ0 a2 b2 ⇒ tPack ℓ0 a3 b3 by auto using P_Pack.
move => [b'][hp'].
elim /IEq_inv=>//= _ ℓ2 a0 b4 a1 b6 ? ? [*]. subst.
move /ihb : hbc.
have {hp}[? ?] : a4 ⇒ a1 /\ b5 ⇒ b6 by inversion hp'.
move => [b'][?]?.
exists (b'[b6.:a1..]).
split. by eauto using P_LetPack.
eapply ieq_morphing_mutual; eauto.
case => [|i]//=.
* rewrite /elookup => //=.
move => ℓ2 [*]. subst.
case : (lprop.sub_eqdec ℓ2 ℓ) => ?;
by eauto with ieq.
* move => ℓ2.
rewrite /elookup//=.
case : i=>[|i]//=.
scongruence.
case : (lprop.sub_eqdec ℓ2 ℓ) => ?;
by eauto with ieq.
- hauto q:on ctrs:Par, IEq inv:Par, IEq.
- move => Ξ ℓ ℓ0 a0 b0 c0 a1 b1 c1 ? ha iha hb ihb hc ihc a'.
elim/Par_inv=>//=_.
+ hauto lq:on ctrs:IEq, Par.
+ move => ℓ1 a2 a3 b2 ? [*]. subst.
inversion hc; subst. hauto lq:on ctrs:Par, IEq.
+ move => ℓ1 a2 a3 b2 b3 c2 c3 +++ [*]. subst.
elim /IEq_inv : hc => //=_ a2 a4 ha24 [?]?. subst.
move /iha => {iha} [a1'][ha1]ha1'.
move /ihb => {ihb} [b1'][hb1]hb1'.
move /P_Suc /ihc => {ihc} [c1'][hc1]hc1'.
elim /Par_inv : hc1 => //= _ a2 b2 ? [*]. subst.
elim /IEq_inv : hc1' => //= _ a2 a5 ? [?][?]. subst.
eexists.
split. eauto with par.
eapply ieq_morphing_mutual; eauto.
case => [|i]//=.
hauto lq:on ctrs:GIEq, IEq unfold:elookup.
move => ℓ1; rewrite /elookup //=.
case : i => [|i]//=.
hauto lq:on ctrs:GIEq, IEq unfold:elookup.
move => ?. apply ieq_gieq. move => *.
apply : I_Var; eauto.
- move => Ξ ℓ ℓ0 a0 a1 b0 b1 ? ha iha hb ihb u.
elim /Par_inv=>//=_.
+ hauto lq:on ctrs:Par,IEq.
+ move => ℓ1 b2 b3 ? [*]. subst.
have ? : a1 = tTT by inversion ha. subst.
hauto lq:on ctrs:IEq, Par.
- hauto l:on ctrs:Par use:Par_refl.
Qed.
(* Lemma 3.2 (Simulation) *)
Lemma simulation_star Ξ ℓ a b a' (h : IEq Ξ ℓ a b) (h0 : a ⇒* a') :
exists b', b ⇒* b' /\ IEq Ξ ℓ a' b'.
Proof.
move : b h.
elim : a a' / h0.
- sfirstorder.
- move => a a0 a1 ha ha0 ih b hab.
suff : exists b0,Par b b0 /\ IEq Ξ ℓ a0 b0; hauto lq:on use:simulation ctrs:rtc.
Qed.
Lemma conv_refl Ξ ℓ a : IOk Ξ ℓ a -> conv Ξ a a.
Proof.
move /iok_ieq /(_ ℓ ltac:(by rewrite meet_idempotent)) /ieq_iconv => h /ltac:(exists ℓ) //.
Qed.
Lemma iconv_sym Ξ ℓ a b : iconv Ξ ℓ a b -> iconv Ξ ℓ b a.
Proof. hauto lq:on use:ieq_sym_mutual unfold:conv, iconv. Qed.
Lemma conv_sym Ξ a b : conv Ξ a b -> conv Ξ b a.
Proof. hauto lq:on use:iconv_sym unfold:conv. Qed.
Lemma iconv_rpar Ξ ℓ a b a0 :
iconv Ξ ℓ a b -> a0 ⇒ a -> iconv Ξ ℓ a0 b.
Proof. hauto lq:on ctrs:rtc unfold:iconv. Qed.
Lemma conv_rpar Ξ a b a0 :
conv Ξ a b -> a0 ⇒ a -> conv Ξ a0 b.
Proof. hauto use:iconv_rpar unfold:conv. Qed.
Lemma iconv_par Ξ ℓ a b a0 :
iconv Ξ ℓ a b -> a ⇒ a0 -> iconv Ξ ℓ a0 b.
Proof.
rewrite /iconv.
move => [c0][c1][h0][h1]h2 h3.
apply rtc_once in h3.
move : Pars_confluent (h0) (h3). repeat move/[apply].
move => [ca][h5]h6.
move : simulation_star (h2) (h5). repeat move/[apply].
move /ieq_sym in h2.
move => [c1' [h7 h8]].
exists ca, c1'.
hauto l:on use:rtc_transitive.
Qed.
Lemma conv_par Ξ a b a0 :
conv Ξ a b -> a ⇒ a0 -> conv Ξ a0 b.
Proof.
hauto lq:on use:iconv_par unfold:conv.
Qed.
Lemma iconv_par2 Ξ ℓ a b a0 b0 :
iconv Ξ ℓ a b -> a ⇒ a0 -> b ⇒ b0 -> iconv Ξ ℓ a0 b0.
Proof. hauto lq:on use:iconv_par, iconv_sym. Qed.
Lemma ieq_trans_heterogeneous Ξ ℓ ℓ0 a b c :
IEq Ξ ℓ a b ->
IEq Ξ ℓ0 b c ->
IEq Ξ (ℓ ∩ ℓ0) a c.
Proof.
move => h0 h1.
apply ieq_trans with (B := b).
- apply ieq_sym_mutual.
apply ieq_sym_mutual in h0.
eapply ieq_downgrade_mutual; eauto.
- apply ieq_sym_mutual in h0.
rewrite meet_commutative.
eapply ieq_downgrade_mutual; eauto.
Qed.
Lemma ieq_trans_heterogeneous_leq Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
IEq Ξ ℓ a b ->
IEq Ξ ℓ0 b c ->
IEq Ξ ℓ a c.
Proof.
hauto l:on drew:off use:ieq_trans_heterogeneous, meet_commutative.
Qed.
Lemma ieq_trans_heterogeneous_leq' Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
IEq Ξ ℓ0 a b ->
IEq Ξ ℓ b c ->
IEq Ξ ℓ a c.
Proof.
move => h.
move /ieq_trans_heterogeneous /[apply].
rewrite meet_commutative. congruence.
Qed.
Lemma iconv_trans_heterogeneous Ξ ℓ0 ℓ1 a b c :
iconv Ξ ℓ0 a b -> iconv Ξ ℓ1 b c -> iconv Ξ (ℓ0 ∩ ℓ1) a c.
Proof.
rewrite /iconv.
move => [a0 [b0 [h0 [h1 h2]]]].
move => [b1 [c0 [h3 [h4 h5]]]].
move : Pars_confluent (h1) (h3). repeat move/[apply].
move => [q [h6 h7]].
move /ieq_sym in h2.
move : simulation_star (h2) (h6). repeat move/[apply].
move => [p0][? ?].
move : simulation_star (h5) (h7). repeat move/[apply].
move => [p1][? ?].
exists p0, p1. hauto lq:on use:ieq_sym, ieq_trans_heterogeneous, rtc_transitive.
Qed.
Lemma iconv_trans_heterogeneous_leq Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
iconv Ξ ℓ a b ->
iconv Ξ ℓ0 b c ->
iconv Ξ ℓ a c.
Proof.
hauto l:on drew:off use:iconv_trans_heterogeneous, meet_commutative.
Qed.
Lemma iconv_trans_heterogeneous_leq' Ξ ℓ ℓ0 a b c :
ℓ ⊆ ℓ0 ->
iconv Ξ ℓ0 a b ->
iconv Ξ ℓ b c ->
iconv Ξ ℓ a c.
Proof.
move => h.
move /iconv_trans_heterogeneous /[apply].
rewrite meet_commutative. congruence.
Qed.
Lemma iconv_trans Ξ ℓ a b c :
iconv Ξ ℓ a b -> iconv Ξ ℓ b c -> iconv Ξ ℓ a c.
Proof.
hauto l:on use:iconv_trans_heterogeneous_leq, meet_idempotent.
Qed.
(* Lemma 4.3 (Transitivity of Equality) *)
Lemma conv_trans Ξ a b c : conv Ξ a b -> conv Ξ b c -> conv Ξ a c.
Proof.
hauto lq:on use:iconv_trans_heterogeneous unfold:conv.
Qed.
Lemma iconv_subst Ξ ℓ Δ ρ (h : iok_subst_ok ρ Ξ Δ) a b (h0 : iconv Ξ ℓ a b) :
iconv Δ ℓ a[ρ] b[ρ].
Proof.
rewrite /iconv in h0 *.
move : h0 => [c0][c1][h0][h1]h2.
exists c0[ρ], c1[ρ].
sfirstorder use:ieq_morphing_iok, Par_subst_star.
Qed.
Lemma conv_subst Ξ Δ ρ (h : iok_subst_ok ρ Ξ Δ) a b (h0 : conv Ξ a b) :
conv Δ a[ρ] b[ρ].
Proof. hauto lq:on use:iconv_subst unfold:conv. Qed.
Lemma ieq_conv Ξ ℓ a b : IEq Ξ ℓ a b -> conv Ξ a b.
Proof. rewrite /conv; eauto using ieq_iconv. Qed.
Lemma conv_univ_inj Ξ i j : conv Ξ (tUniv i) (tUniv j) -> i = j.
Proof.
rewrite /conv/iconv.
move => [ℓ][c0][c1][/Pars_univ_inv h0][/Pars_univ_inv h1]h2. subst.
by inversion h2; subst.
Qed.
Lemma iconv_pi_inj Ξ ℓ ℓ0 A0 B0 ℓ1 A1 B1 :
iconv Ξ ℓ (tPi ℓ0 A0 B0) (tPi ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
iconv Ξ ℓ A0 A1 /\
iconv (ℓ0 :: Ξ) ℓ B0 B1.
Proof.
rewrite /iconv.
move => [c0][c1][hPi0][hPi1]heq.
move /Pars_pi_inv : hPi0 => [A0'][B0'][h0][h1]h2.
move /Pars_pi_inv : hPi1 => [A1'][B1'][h3][h4]h5.
subst.
hauto lq:on inv:IEq.
Qed.
Lemma iconv_sig_inj Ξ ℓ ℓ0 A0 B0 ℓ1 A1 B1 :
iconv Ξ ℓ (tSig ℓ0 A0 B0) (tSig ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
iconv Ξ ℓ A0 A1 /\
iconv (ℓ0 :: Ξ) ℓ B0 B1.
Proof.
rewrite /iconv.
move => [c0][c1][hPi0][hPi1]heq.
move /Pars_sig_inv : hPi0 => [A0'][B0'][h0][h1]h2.
move /Pars_sig_inv : hPi1 => [A1'][B1'][h3][h4]h5.
subst.
hauto lq:on inv:IEq.
Qed.
Lemma conv_pi_inj Ξ ℓ0 A0 B0 ℓ1 A1 B1 :
conv Ξ (tPi ℓ0 A0 B0) (tPi ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
conv Ξ A0 A1 /\
conv (ℓ0 :: Ξ) B0 B1.
Proof. rewrite/conv; hauto lq:on use:iconv_pi_inj. Qed.
Lemma conv_sig_inj Ξ ℓ0 A0 B0 ℓ1 A1 B1 :
conv Ξ (tSig ℓ0 A0 B0) (tSig ℓ1 A1 B1) ->
ℓ0 = ℓ1 /\
conv Ξ A0 A1 /\
conv (ℓ0 :: Ξ) B0 B1.
Proof. rewrite/conv; hauto lq:on use:iconv_sig_inj. Qed.
Lemma conv_eq_inj Ξ ℓ0 a0 b0 ℓ1 a1 b1 : conv Ξ (tEq ℓ0 a0 b0) (tEq ℓ1 a1 b1) -> ℓ0 = ℓ1 /\ exists ℓ, ℓ0 ⊆ ℓ /\ iconv Ξ ℓ a0 a1 /\ iconv Ξ ℓ b0 b1.
Proof.
rewrite /conv/iconv.
move => [ℓ][c0][c1][h0][h1]h2.
move /Pars_eq_inv : h0 => [a0'][b0'][h3][h4]h5. subst.
move /Pars_eq_inv : h1 => [a1'][b1'][h6][h7]h8. subst.
elim /IEq_inv : h2 => // _ ℓ2 a2 a3 b2 b3 ? ? ? [? ? ?] [? ? ?]. subst.
sfirstorder.
Qed.
Lemma iconv_iok_downgrade Ξ ℓ0 ℓ1 a b :
IOk Ξ ℓ0 a -> iconv Ξ ℓ1 a b -> iconv Ξ (ℓ0 ∩ ℓ1) a b.
Proof.
rewrite /iconv.
move => ha [a'][b'][h0][h1]h2.
exists a', b'.
repeat split => //.
suff /iok_ieq /(_ ℓ0) /(_ ltac:(by rewrite meet_idempotent)) : IOk Ξ ℓ0 a'.
rewrite meet_commutative.
sfirstorder use:ieq_downgrade_mutual.
eauto using iok_preservation_star.
Qed.
Lemma iconv_renaming : forall Ξ ℓ a b,
iconv Ξ ℓ a b ->
forall ξ Δ, iok_ren_ok ξ Ξ Δ ->
iconv Δ ℓ (ren_tm ξ a) (ren_tm ξ b).
Proof.
hauto lq:on use:Pars_renaming, ieq_weakening_mutual unfold:iconv.
Qed.
Lemma conv_renaming : forall Ξ a b,
conv Ξ a b ->
forall ξ Δ, iok_ren_ok ξ Ξ Δ ->
conv Δ (ren_tm ξ a) (ren_tm ξ b).
Proof. hauto lq:on use:iconv_renaming unfold:conv. Qed.
Lemma iconv_conv Ξ ℓ a b : iconv Ξ ℓ a b -> conv Ξ a b.
Proof. sfirstorder unfold:conv. Qed.
Lemma iconv_par_star Ξ ℓ a b a0 :
iconv Ξ ℓ a b -> a ⇒* a0 -> iconv Ξ ℓ a0 b.
Proof.
move => h h0.
move : Ξ b h.
induction h0;
hauto lq:on use:iconv_par unfold:conv.
Qed.
Lemma iconv_par_star2 Ξ ℓ a b a0 b0 :
iconv Ξ ℓ a b -> a ⇒* a0 -> b ⇒* b0 -> iconv Ξ ℓ a0 b0.
Proof. hauto lq:on use:iconv_par_star, iconv_sym. Qed.
Lemma conv_par_star2 Ξ a b a0 b0 :
conv Ξ a b -> a ⇒* a0 -> b ⇒* b0 -> conv Ξ a0 b0.
Proof. hauto lq:on use:iconv_par_star2, iconv_conv. Qed.
End conv_facts.