From af517fda090e933c7e72536fd2aa9cbe4436ebf6 Mon Sep 17 00:00:00 2001 From: Gabriele Cecilia Date: Sun, 28 Jul 2024 15:51:17 +0200 Subject: [PATCH 1/2] added harmony-lemma-formalization --- .../1_definitions.bel | 107 +++ .../2_input_rewriting.bel | 72 ++ .../3_free_output_rewriting.bel | 70 ++ .../4_bound_output_rewriting.bel | 85 +++ .../5_theorem1.bel | 216 ++++++ .../6_stepcong_lemma.bel | 657 ++++++++++++++++++ .../7_reduction_rewriting.bel | 74 ++ .../8_theorem2.bel | 29 + .../harmony-lemma-formalization/README.md | 68 ++ .../harmony-lemma-formalization/all.cfg | 8 + 10 files changed, 1386 insertions(+) create mode 100644 case-studies/harmony-lemma-formalization/1_definitions.bel create mode 100644 case-studies/harmony-lemma-formalization/2_input_rewriting.bel create mode 100644 case-studies/harmony-lemma-formalization/3_free_output_rewriting.bel create mode 100644 case-studies/harmony-lemma-formalization/4_bound_output_rewriting.bel create mode 100644 case-studies/harmony-lemma-formalization/5_theorem1.bel create mode 100644 case-studies/harmony-lemma-formalization/6_stepcong_lemma.bel create mode 100644 case-studies/harmony-lemma-formalization/7_reduction_rewriting.bel create mode 100644 case-studies/harmony-lemma-formalization/8_theorem2.bel create mode 100644 case-studies/harmony-lemma-formalization/README.md create mode 100644 case-studies/harmony-lemma-formalization/all.cfg diff --git a/case-studies/harmony-lemma-formalization/1_definitions.bel b/case-studies/harmony-lemma-formalization/1_definitions.bel new file mode 100644 index 000000000..d944ab3c3 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/1_definitions.bel @@ -0,0 +1,107 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%% Definitions %%% + +% Set of Channel Names +LF names: type = +; + +% Processes +% In order to encode input and restriction processes, which both bind names, we exploit higher order abstract syntax +% and use higher-order functions from names to proc. +% In this way we don't need to give an explicit name to bound names and deal with alpha-renaming or substitution. +LF proc: type = + | p_zero: proc % 0 + | p_in: names → (names → proc) → proc % x(y).P(y), where x(y) is an input of the name y through channel x + | p_out: names → names → proc → proc % x(u).P, where x(u) is an output of the name u through channel x + | p_par: proc → proc → proc % P|Q, where P and Q are processes + | p_res: (names → proc) → proc % (nu x) P, where x is a name and P is a process +; +--infix p_par 11 left. + +% Contexts +schema ctx = names; + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%% Reduction Semantics %%% + +% Structural Congruence +LF cong: proc → proc → type = +% Abelian Monoid Laws for Parallel Composition + | par_assoc: cong (P p_par (Q p_par R)) ((P p_par Q) p_par R) + | par_unit: cong (P p_par p_zero) P + | par_comm: cong (P p_par Q) (Q p_par P) +% Scope Extension Laws + | sc_ext_zero: cong (p_res \x.p_zero) p_zero + | sc_ext_par: cong ((p_res P) p_par Q) (p_res \x.((P x) p_par Q)) + | sc_ext_res: cong (p_res \x.(p_res \y.(P x y))) (p_res \y.(p_res \x.(P x y))) +% Compatibility Laws + | c_in: ({y:names} cong (P y) (Q y)) → cong (p_in X P) (p_in X Q) + | c_out: cong P Q → cong (p_out X Y P) (p_out X Y Q) + | c_par: cong P P' → cong (P p_par Q) (P' p_par Q) + | c_res: ({x:names} cong (P x) (Q x)) → cong (p_res P) (p_res Q) +% Equivalence Relation Laws + | c_ref: cong P P + | c_sym: cong P Q → cong Q P + | c_trans: cong P Q → cong Q R → cong P R +; +--infix cong 11 left. + +% Reduction +LF red: proc → proc → type = + | r_com: red ((p_out X Y P) p_par (p_in X Q)) (P p_par (Q Y)) + | r_par: red P Q → red (P p_par R) (Q p_par R) + | r_res: ({x:names} red (P x) (Q x)) → red (p_res P) (p_res Q) + | r_str: P cong P' → red P' Q' → Q' cong Q → red P Q +; +--infix red 11 left. + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%% LTS Semantics %%% +% We follow "Pi-Calculus in (Co)Inductive Type Theory" [Honsell et al. 2001] for the encoding of late LTS semantics. +% We define two different types for free/bound actions, and two different relations for transitions via free/bound actions. +% The result of a free transition is a process, while the result of a bound transition is a function from names to processes: +% instead of stating the bound name involved in the transition explicitly, that name is the argument of the aforementioned function. + +% Free Actions +LF f_act: type = + | f_tau: f_act + | f_out: names → names → f_act +; + +% Bound Actions +LF b_act: type = + | b_in: names → b_act + | b_out: names → b_act +; + + +% Transition Relation +LF fstep: proc → f_act → proc → type = + | fs_out: fstep (p_out X Y P) (f_out X Y) P + | fs_par1: fstep P A P' → fstep (P p_par Q) A (P' p_par Q) + | fs_par2: fstep Q A Q' → fstep (P p_par Q) A (P p_par Q') + | fs_com1: fstep P (f_out X Y) P' → bstep Q (b_in X) Q' + → fstep (P p_par Q) f_tau (P' p_par (Q' Y)) + | fs_com2: bstep P (b_in X) P' → fstep Q (f_out X Y) Q' + → fstep (P p_par Q) f_tau ((P' Y) p_par Q') + | fs_res: ({z:names} fstep (P z) A (P' z)) + → fstep (p_res P) A (p_res P') + | fs_close1: bstep P (b_out X) P' → bstep Q (b_in X) Q' + → fstep (P p_par Q) f_tau (p_res \z.((P' z) p_par (Q' z))) + | fs_close2: bstep P (b_in X) P' → bstep Q (b_out X) Q' + → fstep (P p_par Q) f_tau (p_res \z.((P' z) p_par (Q' z))) + +and bstep: proc → b_act → (names → proc) → type = + | bs_in: bstep (p_in X P) (b_in X) P + | bs_par1: bstep P A P' → bstep (P p_par Q) A \x.((P' x) p_par Q) + | bs_par2: bstep Q A Q' → bstep (P p_par Q) A \x.(P p_par (Q' x)) + | bs_res: ({z:names} bstep (P z) A (P' z)) + → bstep (p_res P) A \x.(p_res \z.(P' z x)) + | bs_open: ({z:names} fstep (P z) (f_out X z) (P' z)) + → bstep (p_res P) (b_out X) P' +; \ No newline at end of file diff --git a/case-studies/harmony-lemma-formalization/2_input_rewriting.bel b/case-studies/harmony-lemma-formalization/2_input_rewriting.bel new file mode 100644 index 000000000..7fb36d9e3 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/2_input_rewriting.bel @@ -0,0 +1,72 @@ +% Predicate about syntactic equivalence of processes involved in input transitions: +% ex_inp_rew Q X Q' holds iff there exist R, S, x_1,...,x_n such that Q cong (nu x_1)...(nu x_n)((p_in X R) p_par S) and +% (Q' y) cong (nu x_1)...(nu x_n)((R Y) p_par S). +% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case +% in which Q cong (nu x)P and Q' cong (nu x)P', where ex_inp_rew P X P' holds inductively. + +LF ex_inp_rew: proc → names → (names → proc) → type = + | inp_base: Q cong ((p_in X R) p_par S) + → ({y:names} (Q' y) cong ((R y) p_par S)) → ex_inp_rew Q X Q' + | inp_ind: Q cong (p_res P) → ({y:names} (Q' y) cong (p_res (P' y))) + → ({w:names} ex_inp_rew (P w) X \y.(P' y w)) → ex_inp_rew Q X Q' +; + + +% We prove the lemma which states that processes involved in input transitions (bstep Q (b_in X) Q') +% can be rewritten (up to congruence) in a canonic way (ex_inp_rew Q X Q'). +% Before, we need three additional lemmas which prove the result in particular cases. + +rec bs_in_rew_par1: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_inp_rew Q X \y.Q'[..,y]] + → [g ⊢ ex_inp_rew (Q p_par R) X \y.(Q'[..,y] p_par R[..])] = +/ total d (bs_in_rew_par1 _ _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ inp_base C1 \y.C2[..,y]] ⇒ [g ⊢ inp_base (c_trans (c_par C1) + (c_sym par_assoc)) \y.(c_trans (c_par C2[..,y]) (c_sym par_assoc))] + | [g ⊢ inp_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ + let [g,w:names ⊢ D2[..,w]] = bs_in_rew_par1 [g,w:names ⊢ R[..]] + [g,w:names ⊢ D1[..,w]] in [g ⊢ inp_ind (c_trans (c_par C1) + sc_ext_par) (\y.(c_trans (c_par C2[..,y]) sc_ext_par)) (\w.D2[..,w])] +; + +rec bs_in_rew_par2: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_inp_rew Q X \y.Q'[..,y]] + → [g ⊢ ex_inp_rew (R p_par Q) X \y.(R[..] p_par Q'[..,y])] = +/ total d (bs_in_rew_par2 _ _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ inp_base C1 \y.C2[..,y]] ⇒ + [g ⊢ inp_base (c_trans par_comm (c_trans (c_par C1) (c_sym par_assoc))) + \y.(c_trans par_comm (c_trans (c_par C2[..,y]) (c_sym par_assoc)))] + | [g ⊢ inp_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ + let [g,w:names ⊢ D2[..,w]] = bs_in_rew_par2 [g,w:names ⊢ R[..]] + [g, w:names ⊢ D1[..,w]] in [g ⊢ inp_ind (c_trans par_comm (c_trans (c_par C1) + (c_trans sc_ext_par (c_res \z.par_comm)))) (\y.(c_trans par_comm (c_trans + (c_par C2[..,y]) (c_trans sc_ext_par (c_res \z.par_comm))))) (\w.D2[..,w])] +; + +rec bs_in_rew_res: (g:ctx) [g,z:names ⊢ ex_inp_rew Q[..,z] X[..] \y.Q'[..,z,y]] + → [g ⊢ ex_inp_rew (p_res \z.Q[..,z]) X \y.(p_res \z.Q'[..,z,y])] = +/ total d (bs_in_rew_res _ _ _ _ d) / +fn d ⇒ case d of + | [g,z:names ⊢ inp_base C1[..,z] \y.C2[..,z,y]] ⇒ + [g ⊢ inp_ind (c_res \z.C1[..,z]) (\y.(c_res \z.C2[..,z,y])) + (\w.(inp_base c_ref \y.c_ref))] + | [g,z:names ⊢ inp_ind C1[..,z] (\y.C2[..,z,y]) (\w.D1[..,z,w])] ⇒ + let [g,z:names ⊢ D2[..,z]] = bs_in_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in + [g ⊢ inp_ind (c_res \z.C1[..,z]) (\y.(c_res \z.C2[..,z,y])) (\z.D2[..,z])] +; + + +rec bs_in_rew: (g:ctx) [g ⊢ bstep Q (b_in X) \y.Q'[..,y]] + → [g ⊢ ex_inp_rew Q X \y.Q'[..,y]] = +/ total b (bs_in_rew _ _ _ _ b) / +fn b ⇒ case b of + | [g ⊢ bs_in] ⇒ [g ⊢ inp_base (c_sym par_unit) \y.(c_sym par_unit)] + | [g ⊢ bs_par1 B1]:[g ⊢ bstep (P p_par R) (b_in X) \y.(P' p_par (R[..]))] ⇒ + let [g ⊢ D1] = bs_in_rew [g ⊢ B1] in + let [g ⊢ D2] = bs_in_rew_par1 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ bs_par2 B2]:[g ⊢ bstep (R p_par P) (b_in X) \y.((R[..]) p_par P')] ⇒ + let [g ⊢ D1] = bs_in_rew [g ⊢ B2] in + let [g ⊢ D2] = bs_in_rew_par2 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ bs_res \y.B[..,y]] ⇒ + let [g,y:names ⊢ D1[..,y]] = bs_in_rew [g,y:names ⊢ B[..,y]] in + let [g ⊢ D2] = bs_in_rew_res [g,y:names ⊢ D1[..,y]] in [g ⊢ D2] +; \ No newline at end of file diff --git a/case-studies/harmony-lemma-formalization/3_free_output_rewriting.bel b/case-studies/harmony-lemma-formalization/3_free_output_rewriting.bel new file mode 100644 index 000000000..a779561d4 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/3_free_output_rewriting.bel @@ -0,0 +1,70 @@ +% Predicate about syntactic equivalence of processes involved in free output transitions: +% ex_fout_rew Q X Y Q' holds iff there exist R, S, x_1,...,x_n such that Q cong (nu x_1)...(nu x_n)((p_out X Y R) p_par S) and +% Q' cong (nu x_1)...(nu x_n)(R p_par S). +% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case +% in which Q cong (nu x)P and Q' cong (nu x)P', where ex_fout_rew P X P' holds inductively. + +LF ex_fout_rew: proc → names → names → proc → type = + | fout_base: Q cong ((p_out X Y R) p_par S) → Q' cong (R p_par S) + → ex_fout_rew Q X Y Q' + | fout_ind: Q cong (p_res P) → Q' cong (p_res P') + → ({w:names} ex_fout_rew (P w) X Y (P' w)) → ex_fout_rew Q X Y Q' +; + + +% We prove the lemma which states that processes involved in free output transitions (fstep Q (f_out X Y) Q') +% can be rewritten (up to congruence) in a canonic way (ex_fout_rew Q X Y Q'). +% Before, we need three additional lemmas which prove the result in particular cases. + +rec fs_out_rew_par1: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_fout_rew Q X Y Q'] + → [g ⊢ ex_fout_rew (Q p_par R) X Y (Q' p_par R)] = +/ total d (fs_out_rew_par1 _ _ _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ fout_base C1 C2] ⇒ [g ⊢ fout_base (c_trans (c_par C1) + (c_sym par_assoc)) (c_trans (c_par C2) (c_sym par_assoc))] + | [g ⊢ fout_ind C1 C2 \w.D1[..,w]] ⇒ let [g,w:names ⊢ D2[..,w]] + = fs_out_rew_par1 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in + [g ⊢ fout_ind (c_trans (c_par C1) sc_ext_par) + (c_trans (c_par C2) sc_ext_par) \w.D2[..,w]] +; + +rec fs_out_rew_par2: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_fout_rew Q X Y Q'] + → [g ⊢ ex_fout_rew (R p_par Q) X Y (R p_par Q')] = +/ total d (fs_out_rew_par2 _ _ _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ fout_base C1 C2] ⇒ [g ⊢ fout_base (c_trans par_comm (c_trans (c_par C1) + (c_sym par_assoc))) (c_trans par_comm (c_trans (c_par C2) (c_sym par_assoc)))] + | [g ⊢ fout_ind C1 C2 \w.D1[..,w]] ⇒ let [g,w:names ⊢ D2[..,w]] + = fs_out_rew_par2 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in + [g ⊢ fout_ind (c_trans par_comm (c_trans (c_par C1) (c_trans sc_ext_par + (c_res \w.par_comm)))) (c_trans par_comm (c_trans (c_par C2) + (c_trans sc_ext_par (c_res \w.par_comm)))) \w.D2[..,w]] +; + +rec fs_out_rew_res: (g:ctx) ([g,z:names ⊢ ex_fout_rew Q[..,z] X[..] Y[..] Q'[..,z]]) + → [g ⊢ ex_fout_rew (p_res \z.Q[..,z]) X Y (p_res \z.Q'[..,z])] = +/ total d (fs_out_rew_res _ _ _ _ _ d) / +fn d ⇒ case d of + | [g,z:names ⊢ fout_base C1[..,z] C2[..,z]] ⇒ [g ⊢ fout_ind (c_res \z.C1[..,z]) + (c_res \z.C2[..,z]) \z.(fout_base c_ref c_ref)] + | [g,z:names ⊢ fout_ind C1[..,z] C2[..,z] \w.D1[..,z,w]] ⇒ let [g,z:names ⊢ D2[..,z]] + = fs_out_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in + [g ⊢ fout_ind (c_res \z.C1[..,z]) (c_res \z.C2[..,z]) \z.D2[..,z]] +; + + +rec fs_out_rew: (g:ctx) [g ⊢ fstep Q (f_out X Y) Q'] + → [g ⊢ ex_fout_rew Q X Y Q'] = +/ total f (fs_out_rew _ _ _ _ _ f) / +fn f ⇒ case f of + | [g ⊢ fs_out] ⇒ [g ⊢ fout_base (c_sym par_unit) (c_sym par_unit)] + | [g ⊢ fs_par1 B1]:[g ⊢ fstep (P p_par R) (f_out X Y) (P' p_par R)] ⇒ + let [g ⊢ D1] = fs_out_rew [g ⊢ B1] in + let [g ⊢ D2] = fs_out_rew_par1 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ fs_par2 B2]:[g ⊢ fstep (R p_par P) (f_out X Y) (R p_par P')] ⇒ + let [g ⊢ D1] = fs_out_rew [g ⊢ B2] in + let [g ⊢ D2] = fs_out_rew_par2 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ fs_res \z.F[..,z]] ⇒ + let [g,z:names ⊢ D1[..,z]] = fs_out_rew [g,z:names ⊢ F[..,z]] in + let [g ⊢ D2] = fs_out_rew_res [g,z:names ⊢ D1[..,z]] in [g ⊢ D2] +; diff --git a/case-studies/harmony-lemma-formalization/4_bound_output_rewriting.bel b/case-studies/harmony-lemma-formalization/4_bound_output_rewriting.bel new file mode 100644 index 000000000..ff9283ba6 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/4_bound_output_rewriting.bel @@ -0,0 +1,85 @@ +% Predicate about syntactic equivalence of processes involved in bound output transitions: +% ex_bout_rew Q X Q' holds iff there exist R, S, z, x_1,...,x_n such that Q cong (nu z)(nu x_1)...(nu x_n)((p_out X z R) p_par S) and +% (Q' z) cong (nu x_1)...(nu x_n)((R z) p_par (S z)). +% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case +% in which Q cong (nu x)P and Q' cong (nu x)P', where ex_bout_rew P X P' holds inductively. + +LF ex_bout_rew: proc → names → (names → proc) → type = + | bout_base: Q cong (p_res \z.((p_out X z (R z)) p_par (S z))) + → ({y:names} (Q' y) cong ((R y) p_par (S y))) → ex_bout_rew Q X Q' + | bout_ind: Q cong (p_res P) → ({y:names} (Q' y) cong (p_res (P' y))) + → ({w:names} ex_bout_rew (P w) X \y.(P' y w)) → ex_bout_rew Q X Q' +; + + +% We prove the lemma which states that processes involved in bound output transitions (bstep Q (b_out X) Q') +% can be rewritten (up to congruence) in a canonic way (ex_bout_rew Q X Q'). +% Before, we need four additional lemmas which prove the result in particular cases. + +rec bs_out_rew_par1: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_bout_rew Q X \y.Q'[..,y]] + → [g ⊢ ex_bout_rew (Q p_par R) X \y.(Q'[..,y] p_par R[..])] = +/ total d (bs_out_rew_par1 _ _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ bout_base C1 \y.C2[..,y]] ⇒ + [g ⊢ bout_base (c_trans (c_par C1) (c_trans sc_ext_par (c_res \z.(c_sym par_assoc)))) + \y.(c_trans (c_par C2[..,y]) (c_sym par_assoc))] + | [g ⊢ bout_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ let [g,w:names ⊢ D2[..,w]] + = bs_out_rew_par1 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in + [g ⊢ bout_ind (c_trans (c_par C1) sc_ext_par) + (\y.(c_trans (c_par C2[..,y]) sc_ext_par)) (\w.D2[..,w])] +; + +rec bs_out_rew_par2: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_bout_rew Q X \y.Q'[..,y]] + → [g ⊢ ex_bout_rew (R p_par Q) X \y.(R[..] p_par Q'[..,y])] = +/ total d (bs_out_rew_par2 _ _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ bout_base C1 \y.C2[..,y]] ⇒ [g ⊢ bout_base (c_trans par_comm + (c_trans (c_par C1) (c_trans sc_ext_par (c_res \z.(c_sym par_assoc))))) + \y.(c_trans par_comm (c_trans (c_par C2[..,y]) (c_sym par_assoc)))] + | [g ⊢ bout_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ let [g,w:names ⊢ D2[..,w]] + = bs_out_rew_par2 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in + [g ⊢ bout_ind (c_trans par_comm (c_trans (c_par C1) (c_trans sc_ext_par + (c_res \w.par_comm)))) (\y.(c_trans par_comm (c_trans (c_par C2[..,y]) + (c_trans sc_ext_par (c_res \w.par_comm))))) (\w.D2[..,w])] +; + +rec bs_out_rew_res: (g:ctx) [g,z:names ⊢ ex_bout_rew Q[..,z] X[..] \y.Q'[..,z,y]] + → [g ⊢ ex_bout_rew (p_res \z.Q[..,z]) X \y.(p_res \z.Q'[..,z,y])] = +/ total d (bs_out_rew_res _ _ _ _ d) / +fn d ⇒ case d of + | [g,z:names ⊢ bout_base C1[..,z] \y.C2[..,z,y]] ⇒ [g ⊢ bout_ind (c_res \z.C1[..,z]) + (\y.(c_res \z.C2[..,z,y])) (\z.(bout_base c_ref \y.c_ref))] + | [g,z:names ⊢ bout_ind C1[..,z] (\y.C2[..,z,y]) (\w.D1[..,z,w])] ⇒ + let [g,z:names ⊢ D2[..,z]] = bs_out_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in + [g ⊢ bout_ind (c_res \z.C1[..,z]) (\y.(c_res \z.C2[..,z,y])) (\z.D2[..,z])] +; + +rec bs_out_rew_open: (g:ctx) [g,z:names ⊢ ex_fout_rew Q[..,z] X[..] z Q'[..,z]] + → [g ⊢ ex_bout_rew (p_res \z.Q[..,z]) X \z.Q'[..,z]] = +/ total d (bs_out_rew_open _ _ _ _ d) / +fn d ⇒ case d of + | [g,z:names ⊢ fout_base C1[..,z] C2[..,z]] ⇒ + [g ⊢ bout_base (c_res \z.C1[..,z]) \z.C2[..,z]] + | [g,z:names ⊢ fout_ind C1[..,z] C2[..,z] \w.D1[..,w,z]] ⇒ + let [g,z:names ⊢ D2[..,z]] = bs_out_rew_open [g,z:names,w:names ⊢ D1[..,z,w]] in + [g ⊢ bout_ind (c_trans (c_res \z.C1[..,z]) sc_ext_res) (\z.C2[..,z]) (\w.D2[..,w])] +; + + +rec bs_out_rew: (g:ctx) [g ⊢ bstep Q (b_out X) \y.Q'[..,y]] + → [g ⊢ ex_bout_rew Q X \y.Q'[..,y]] = +/ total b (bs_out_rew _ _ _ _ b) / +fn b ⇒ case b of + | [g ⊢ bs_par1 B1]:[g ⊢ bstep (P p_par R) (b_out X) \y.(P' p_par R[..])] ⇒ + let [g ⊢ D1] = bs_out_rew [g ⊢ B1] in + let [g ⊢ D2] = bs_out_rew_par1 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ bs_par2 B2]:[g ⊢ bstep (R p_par P) (b_out X) \y.(R[..] p_par P')] ⇒ + let [g ⊢ D1] = bs_out_rew [g ⊢ B2] in + let [g ⊢ D2] = bs_out_rew_par2 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ bs_res \z.B[..,z]] ⇒ + let [g,z:names ⊢ D1[..,z]] = bs_out_rew [g,z:names ⊢ B[..,z]] in + let [g ⊢ D2] = bs_out_rew_res [g,z:names ⊢ D1[..,z]] in [g ⊢ D2] + | [g ⊢ bs_open \z.F[..,z]] ⇒ + let [g,z:names ⊢ D1[..,z]] = fs_out_rew [g,z:names ⊢ F[..,z]] in + let [g ⊢ D2] = bs_out_rew_open [g,z:names ⊢ D1[..,z]] in [g ⊢ D2] +; diff --git a/case-studies/harmony-lemma-formalization/5_theorem1.bel b/case-studies/harmony-lemma-formalization/5_theorem1.bel new file mode 100644 index 000000000..42c534a93 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/5_theorem1.bel @@ -0,0 +1,216 @@ +% In order to prove that a transition of a process P into Q through a tau action (fstep P f_tau Q) implies reduction of P into Q (P red Q), +% we need four additional lemmas which prove the result in particular cases. +% Each of this lemmas is structured in the same way. + + +% First lemma - case of the fs_com1 rule: +% If ex_fout_rew P1 X Y Q1 and ex_inp_rew P2 X Q2, then (P1 p_par P2) red (Q1 p_par (Q2 Y)). + +% In order to prove this lemma, we analyze the structure of both of the types ex_inp_rew and ex_fout_rew that we have as hypotheses. +% When we consider the inductive case of each type, we need to apply structural induction to proceed: +% so we need a lexicographic induction overall. +% To encode this in Beluga, we need to split the proof in two parts: +% A first lemma (fs_com1_impl_red_base), in which we consider the base case of the first type and proceed by induction on the second type; +% a second lemma (fs_com1_impl_red), in which we consider the inductive case of the first type and proceed by induction on that first type. + +rec fs_com1_impl_red_base: (g:ctx) [g ⊢ P2 cong ((p_in X \x.R[..,x]) + p_par S)] → [g,w:names ⊢ Q2[..,w] cong (R[..,w] p_par S[..])] + → [g ⊢ ex_fout_rew P1 X Y Q1] + → [g ⊢ (P1 p_par P2) red (Q1 p_par Q2[..,Y])] = +/ total d1 (fs_com1_impl_red_base _ _ _ _ _ _ _ _ _ _ _ d1) / +fn c3 ⇒ fn c4 ⇒ fn d1 ⇒ case d1 of + | [g ⊢ fout_base C1 C2] ⇒ + let [g ⊢ C3] = c3 in + let [g,w:names ⊢ C4[..,w]] = c4 in + [g ⊢ r_str (c_trans (c_par C1) (c_trans par_comm (c_trans (c_par C3) + par_comm))) (r_str par_assoc (r_par (r_str (c_trans (c_par par_comm) + (c_trans (c_sym par_assoc) par_comm)) (r_par r_com) (c_trans par_comm + (c_trans par_assoc (c_par par_comm))))) (c_sym par_assoc)) (c_trans + (c_par (c_sym C2)) (c_trans par_comm (c_trans (c_par + (c_sym C4[..,_])) par_comm)))] + | [g ⊢ fout_ind C1 C2 \w.D1[..,w]] ⇒ + let [g ⊢ C3] = c3 in + let [g,y:names ⊢ C4[..,y]] = c4 in + let [g,w:names ⊢ R1[..,w]] = fs_com1_impl_red_base + [g,w:names ⊢ C3[..]] [g,w:names,y:names ⊢ C4[..,y]] + [g,w:names ⊢ D1[..,w]] in + [g ⊢ r_str (c_trans (c_par C1) sc_ext_par) (r_res \w.R1[..,w]) + (c_trans (c_sym sc_ext_par) (c_par (c_sym C2)))] +; + +rec fs_com1_impl_red: (g:ctx) [g ⊢ ex_fout_rew P1 X Y Q1] + → [g ⊢ ex_inp_rew P2 X \x.Q2[..,x]] + → [g ⊢ (P1 p_par P2) red (Q1 p_par Q2[..,Y])] = +/ total d2 (fs_com1_impl_red _ _ _ _ _ _ _ _ d2) / +fn d1 ⇒ fn d2 ⇒ case d2 of + | [g ⊢ inp_base C3 \y.C4[..,y]] ⇒ + let [g ⊢ R] = fs_com1_impl_red_base [g ⊢ C3] + [g,y:names ⊢ C4[..,y]] d1 in [g ⊢ R] + | [g ⊢ inp_ind C3 (\y.C4[..,y]) (\w.D2[..,w])] ⇒ + let [g ⊢ D1] = d1 in + let [g,w:names ⊢ R1[..,w]] = fs_com1_impl_red [g,w:names ⊢ D1[..]] + [g,w:names ⊢ D2[..,w]] in + [g ⊢ r_str (c_trans par_comm (c_trans (c_par C3) (c_trans sc_ext_par + (c_res \w.par_comm)))) (r_res \w.R1[..,w]) (c_trans (c_res + \w.par_comm) (c_trans (c_sym sc_ext_par) (c_trans (c_par + (c_sym C4[..,_])) par_comm)))] +; + + +% Second lemma - case of the fs_com2 rule: +% If ex_inp_rew P1 X Q1 and ex_fout_rew P2 X Y Q2, +% then (P1 p_par P2) red ((Q1 Y) p_par Q2). +rec fs_com2_impl_red_base: (g:ctx) [g ⊢ P1 cong ((p_in X \x.R[..,x]) p_par S)] + → [g,w:names ⊢ Q1[..,w] cong (R[..,w] p_par S[..])] + → [g ⊢ ex_fout_rew P2 X Y Q2] → [g ⊢ (P1 p_par P2) red (Q1[..,Y] p_par Q2)] = +/ total d2 (fs_com2_impl_red_base _ _ _ _ _ _ _ _ _ _ _ d2) / +fn c1 ⇒ fn c2 ⇒ fn d2 ⇒ case d2 of + | [g ⊢ fout_base C3 C4] ⇒ + let [g ⊢ C1] = c1 in + let [g,w:names ⊢ C2[..,w]] = c2 in + [g ⊢ r_str (c_trans (c_par C1) (c_trans par_comm (c_trans (c_par C3) par_comm))) + (r_str par_assoc (r_par (r_str (c_trans (c_par par_comm) (c_trans (c_sym par_assoc) par_comm)) + (r_par (r_str par_comm r_com par_comm)) (c_trans par_comm (c_trans par_assoc (c_par par_comm))))) + (c_sym par_assoc)) (c_trans (c_par (c_sym C2[..,_])) + (c_trans par_comm (c_trans (c_par (c_sym C4)) par_comm)))] + | [g ⊢ fout_ind C3 C4 \w.D2[..,w]] ⇒ + let [g ⊢ C1] = c1 in + let [g,y:names ⊢ C2[..,y]] = c2 in + let [g,w:names ⊢ R1[..,w]] = fs_com2_impl_red_base [g,w:names ⊢ C1[..]] + [g,w:names,y:names ⊢ C2[..,y]] [g,w:names ⊢ D2[..,w]] in + [g ⊢ r_str (c_trans par_comm (c_trans (c_par C3) (c_trans sc_ext_par (c_res \w.par_comm)))) + (r_res \w.R1[..,w]) (c_trans (c_res \w.par_comm) (c_trans (c_sym sc_ext_par) + (c_trans (c_par (c_sym C4)) par_comm)))] +; + +rec fs_com2_impl_red: (g:ctx) [g ⊢ ex_inp_rew P1 X \x.Q1[..,x]] + → [g ⊢ ex_fout_rew P2 X Y Q2] → [g ⊢ (P1 p_par P2) red (Q1[..,Y] p_par Q2)] = +/ total d1 (fs_com2_impl_red _ _ _ _ _ _ _ d1 _) / +fn d1 ⇒ fn d2 ⇒ case d1 of + | [g ⊢ inp_base C1 \y.C2[..,y]] ⇒ + let [g ⊢ R] = fs_com2_impl_red_base [g ⊢ C1] [g,y:names ⊢ C2[..,y]] d2 in [g ⊢ R] + | [g ⊢ inp_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ + let [g ⊢ D2] = d2 in + let [g,w:names ⊢ R1[..,w]] = fs_com2_impl_red [g,w:names ⊢ D1[..,w]] [g,w:names ⊢ D2[..]] in + [g ⊢ r_str (c_trans (c_par C1) sc_ext_par) (r_res \w.R1[..,w]) + (c_trans (c_sym sc_ext_par) (c_par (c_sym C2[..,_])))] +; + + +% Third lemma - case of the fs_close1 rule: +% If ex_bout_rew P1 X Q1 and ex_inp_rew P2 X Q2, +% then (P1 p_par P2) red (nu z)((Q1 z) p_par (Q2 z)). + +rec fs_close1_impl_red_base: (g:ctx) [g ⊢ P2 cong ((p_in X \x.R[..,x]) p_par S)] + → [g,w:names ⊢ Q2[..,w] cong (R[..,w] p_par S[..])] → [g ⊢ ex_bout_rew P1 X \x.Q1[..,x]] + → [g ⊢ (P1 p_par P2) red (p_res \x.(Q1[..,x] p_par Q2[..,x]))] = +/ total d1 (fs_close1_impl_red_base _ _ _ _ _ _ _ _ _ _ d1) / +fn c3 ⇒ fn c4 ⇒ fn d1 ⇒ case d1 of + | [g ⊢ bout_base C1 \y.C2[..,y]] ⇒ + let [g ⊢ C3] = c3 in + let [g,w:names ⊢ C4[..,w]] = c4 in + [g ⊢ r_str (c_trans (c_par C1) sc_ext_par) (r_res \z.(r_str (c_trans par_comm + (c_trans (c_par C3[..]) par_comm)) (r_str par_assoc (r_par (r_str (c_trans + (c_par par_comm) (c_trans (c_sym par_assoc) par_comm)) (r_par r_com) (c_trans par_comm + (c_trans par_assoc (c_par par_comm))))) ((c_sym par_assoc))) (c_trans (c_par (c_sym C2[..,_])) + (c_trans par_comm (c_trans (c_par (c_sym C4[..,_])) par_comm))))) (c_ref)] + | [g ⊢ bout_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ + let [g ⊢ C3] = c3 in + let [g,w:names ⊢ C4[..,w]] = c4 in + let [g,w:names ⊢ R1[..,w]] = fs_close1_impl_red_base [g,w:names ⊢ C3[..]] + [g,w:names,y:names ⊢ C4[..,y]] [g,w:names ⊢ D1[..,w]] in + [g ⊢ r_str (c_trans (c_par C1) sc_ext_par) (r_res \w.R1[..,w]) (c_trans sc_ext_res + (c_trans (c_res \z.(c_sym sc_ext_par)) (c_res \z.(c_par (c_sym C2[..,_])))))] +; + +rec fs_close1_impl_red: (g:ctx) [g ⊢ ex_bout_rew P1 X \x.Q1[..,x]] + → [g ⊢ ex_inp_rew P2 X \x.Q2[..,x]] + → [g ⊢ (P1 p_par P2) red (p_res \x.(Q1[..,x] p_par Q2[..,x]))] = +/ total d2 (fs_close1_impl_red _ _ _ _ _ _ _ d2) / +fn d1 ⇒ fn d2 ⇒ case d2 of + | [g ⊢ inp_base C3 \y.C4[..,y]] ⇒ + let [g ⊢ R] = fs_close1_impl_red_base [g ⊢ C3] [g,y:names ⊢ C4[..,y]] d1 in [g ⊢ R] + | [g ⊢ inp_ind C3 (\y.C4[..,y]) (\w.D2[..,w])] ⇒ + let [g ⊢ D1] = d1 in + let [g,w:names ⊢ R1[..,w]] = fs_close1_impl_red [g,w:names ⊢ D1[..]] [g,w:names ⊢ D2[..,w]] in + [g ⊢ r_str (c_trans par_comm (c_trans (c_par C3) (c_trans sc_ext_par (c_res \w.par_comm)))) + (r_res \w.R1[..,w]) (c_trans sc_ext_res (c_trans (c_res \z.(c_res \w.par_comm)) + (c_trans (c_res \z.(c_sym sc_ext_par)) (c_trans (c_res \z.(c_par (c_sym C4[..,_]))) + (c_res \z.par_comm)))))] +; + + +% Fourth lemma - case of the fs_close2 rule: +% If ex_inp_rew P1 X Q1 and ex_bout_rew P2 X Q2, +% then (P1 p_par P2) red (nu z)((Q1 z) p_par (Q2 z)). + +rec fs_close2_impl_red_base: (g:ctx) [g ⊢ P1 cong ((p_in X \x.R[..,x]) p_par S)] + → [g,w:names ⊢ Q1[..,w] cong (R[..,w] p_par S[..])] → [g ⊢ ex_bout_rew P2 X \x.Q2[..,x]] + → [g ⊢ (P1 p_par P2) red (p_res \x.(Q1[..,x] p_par Q2[..,x]))] = +/ total d2 (fs_close2_impl_red_base _ _ _ _ _ _ _ _ _ _ d2) / +fn c1 ⇒ fn c2 ⇒ fn d2 ⇒ case d2 of + | [g ⊢ bout_base C3 \y.C4[..,y]] ⇒ + let [g ⊢ C1] = c1 in + let [g,w:names ⊢ C2[..,w]] = c2 in + [g ⊢ r_str (c_trans par_comm (c_trans (c_par C3) (c_trans sc_ext_par (c_res \z.par_comm)))) + (r_res \z.(r_str (c_par C1[..]) (r_str par_assoc (r_par (r_str (c_trans (c_par par_comm) + (c_trans (c_sym par_assoc) par_comm)) (r_par (r_str par_comm r_com par_comm)) + (c_trans par_comm (c_trans par_assoc (c_par par_comm))))) ((c_sym par_assoc))) + (c_trans (c_par (c_sym C2[..,_])) (c_trans par_comm + (c_trans (c_par (c_sym C4[..,_])) par_comm))))) (c_ref)] + | [g ⊢ bout_ind C3 (\y.C4[..,y]) (\w.D2[..,w])] ⇒ + let [g ⊢ C1] = c1 in + let [g,w:names ⊢ C2[..,w]] = c2 in + let [g,w:names ⊢ R1[..,w]] = fs_close2_impl_red_base [g,w:names ⊢ C1[..]] + [g,w:names,y:names ⊢ C2[..,y]] [g,w:names ⊢ D2[..,w]] in + [g ⊢ r_str (c_trans par_comm (c_trans (c_par C3) (c_trans sc_ext_par (c_res \w.par_comm)))) + (r_res \w.R1[..,w]) (c_trans sc_ext_res (c_trans (c_res \z.(c_res \w.par_comm)) + (c_trans (c_res \z.(c_sym sc_ext_par)) (c_trans (c_res \z.(c_par (c_sym C4[..,_]))) + (c_res \z.par_comm)))))] +; + +rec fs_close2_impl_red: (g:ctx) [g ⊢ ex_inp_rew P1 X \x.Q1[..,x]] + → [g ⊢ ex_bout_rew P2 X \x.Q2[..,x]] + → [g ⊢ (P1 p_par P2) red (p_res \x.(Q1[..,x] p_par Q2[..,x]))] = +/ total d1 (fs_close2_impl_red _ _ _ _ _ _ d1 _) / +fn d1 ⇒ fn d2 ⇒ case d1 of + | [g ⊢ inp_base C1 \y.C2[..,y]] ⇒ + let [g ⊢ R] = fs_close2_impl_red_base [g ⊢ C1] [g,y:names ⊢ C2[..,y]] d2 in [g ⊢ R] + | [g ⊢ inp_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ + let [g ⊢ D2] = d2 in + let [g,w:names ⊢ R1[..,w]] = fs_close2_impl_red [g,w:names ⊢ D1[..,w]] [g,w:names ⊢ D2[..]] in + [g ⊢ r_str (c_trans (c_par C1) sc_ext_par) (r_res \w.R1[..,w]) (c_trans sc_ext_res + (c_trans (c_res \w.(c_sym sc_ext_par)) (c_res \w.(c_par (c_sym C2[..,_])))))] +; + + + +% We now prove the first theorem: a transition of a process P into Q through a tau action (fstep P f_tau Q) implies reduction of P into Q (P red Q). + +rec fstep_impl_red: (g:ctx) [g ⊢ fstep P f_tau Q] → [g ⊢ P red Q] = +/ total f (fstep_impl_red _ _ _ f) / +fn f ⇒ case f of + | [g ⊢ fs_par1 F1] ⇒ let [g ⊢ R] = fstep_impl_red [g ⊢ F1] in + [g ⊢ r_par R] + | [g ⊢ fs_par2 F2] ⇒ let [g ⊢ R] = fstep_impl_red [g ⊢ F2] in + [g ⊢ r_str par_comm (r_par R) par_comm] + | [g ⊢ fs_com1 F1 B1] ⇒ + let [g ⊢ D1] = fs_out_rew [g ⊢ _] [g ⊢ F1] in + let [g ⊢ D2] = bs_in_rew [g ⊢ _] [g ⊢ B1] in + let [g ⊢ R] = fs_com1_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] + | [g ⊢ fs_com2 B1 F1] ⇒ + let [g ⊢ D1] = bs_in_rew [g ⊢ _] [g ⊢ B1] in + let [g ⊢ D2] = fs_out_rew [g ⊢ _] [g ⊢ F1] in + let [g ⊢ R] = fs_com2_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] + | [g ⊢ fs_res \z.F[..,z]] ⇒ + let [g,z:names ⊢ R[..,z]] = fstep_impl_red [g,z:names ⊢ F[..,z]] in + [g ⊢ r_res \z.R[..,z]] + | [g ⊢ fs_close1 B1 B2] ⇒ + let [g ⊢ D1] = bs_out_rew [g ⊢ _][g ⊢ B1] in + let [g ⊢ D2] = bs_in_rew [g ⊢ _] [g ⊢ B2] in + let [g ⊢ R] = fs_close1_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] + | [g ⊢ fs_close2 B1 B2] ⇒ + let [g ⊢ D1] = bs_in_rew [g ⊢ _] [g ⊢ B1] in + let [g ⊢ D2] = bs_out_rew [g ⊢ _] [g ⊢ B2] in + let [g ⊢ R] = fs_close2_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] +; \ No newline at end of file diff --git a/case-studies/harmony-lemma-formalization/6_stepcong_lemma.bel b/case-studies/harmony-lemma-formalization/6_stepcong_lemma.bel new file mode 100644 index 000000000..7d7c97f87 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/6_stepcong_lemma.bel @@ -0,0 +1,657 @@ +% We want to prove that, if P is congruent to Q and P makes a transition through A to P', then there exists a process Q' +% such that Q makes a transition through A into Q' and P' is congruent to Q'. + +% We first need two types encoding the existence of such process Q': one for free transitions and one for bound transitions. +% Free transitions: ex_fstepcong P Q A P' holds iff there exists a process Q' such that fstep Q A Q' and P' cong Q'. +% Bound transitions: ex_bstepcong P Q A P' holds iff there exists a process Q' such that bstep Q A Q' and P' cong Q'. + +LF ex_fstepcong: proc → proc → f_act → proc → type = + | fsc: fstep Q A Q' → P' cong Q' → ex_fstepcong P Q A P' +; + +LF ex_bstepcong: proc → proc → b_act → (names → proc) → type = + | bsc: bstep Q A Q' → ({x:names} (P' x) cong (Q' x)) + → ex_bstepcong P Q A P' +; + + +% Next, we need to prove the following statement: given a transition from P to Q through A in which some variable x doesn't occur free in P +% and doesn't occur bound in A, then x doesn't occur free in Q. +% In Beluga it can be encoded in this way: given a transition from P to Q through A in the context [g, x:names] in which P does not depend on x +% ([g, x:names |- fstep P[..] A Q] in the case of a free transition), then there exists a transition from P to Q' through A' in the context [g] +% ([g |- fstep P A' Q']), with A'=A and Q'=Q in the context [g, x:names]. +% In other words, we need to strengthen the transition so that it still works in a more general context. + + +% We define three types encoding equality of processes, free actions and bound actions: + +LF eqp: proc → proc → type = + | prefl: eqp P P +; + +LF eqf: f_act → f_act → type = + | frefl: eqf A A +; + +LF eqb: b_act → b_act → type = + | brefl: eqb A A +; + +% Now we define two types encoding the existence of such stronger transition. +% We need to define them on the computational level (using the keyword 'ctype') because they are types depending on a contextual object. + +inductive ex_str_fstep: (g:ctx) [g,x:names ⊢ fstep P[..] A Q] → ctype = + | ex_fstep: {F:[g,x:names ⊢ fstep P[..] A Q]} [g ⊢ fstep P A' Q'] + → [g,x:names ⊢ eqf A A'[..]] → [g,x:names ⊢ eqp Q Q'[..]] + → ex_str_fstep [g,x:names ⊢ F] +; + +inductive ex_str_bstep: (g:ctx) [g,x:names ⊢ bstep P[..] A \z.Q[..,x,z]] + → ctype = + | ex_bstep: {B:[g,x:names ⊢ bstep P[..] A \z.Q[..,x,z]]} + [g ⊢ bstep P A' \z.Q'[..,z]] → [g,x:names ⊢ eqb A A'[..]] + → [g,x:names,z:names ⊢ eqp Q[..,x,z] Q'[..,z]] + → ex_str_bstep [g,x:names ⊢ B] +; + + +% Now we can prove the desired result. We state two lemmas (for free/bound transition) and prove them simultaneously. + +rec strengthen_fstep: (g:ctx) {F:[g,x:names ⊢ fstep P[..] A Q]} + → ex_str_fstep [g,x:names ⊢ F] = +/ total f (strengthen_fstep _ _ _ _ f) / +mlam F ⇒ case [_,x:names ⊢ F] of + | [g,x:names ⊢ fs_out] ⇒ ex_fstep [g,x:names ⊢ F] [g ⊢ fs_out] + [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_par1 F1[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F1[..,x]] [g ⊢ F1'] e1 e2 + = strengthen_fstep [g,x:names ⊢ F1[..,x]] in + let [g,x:names ⊢ frefl] = e1 in + let [g,x:names ⊢ prefl] = e2 in + ex_fstep [g,x:names ⊢ fs_par1 F1[..,x]] [g ⊢ fs_par1 F1'] + [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_par2 F2[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F2[..,x]] [g ⊢ F2'] e1 e2 + = strengthen_fstep [g,x:names ⊢ F2[..,x]] in + let [g,x:names ⊢ frefl] = e1 in + let [g,x:names ⊢ prefl] = e2 in + ex_fstep [g,x:names ⊢ fs_par2 F2[..,x]] [g ⊢ fs_par2 F2'] + [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_com1 F1[..,x] B1[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F1[..,x]] [g ⊢ F1'] e1 e2 + = strengthen_fstep [g,x:names ⊢ F1[..,x]] in + let [g,x:names ⊢ frefl] = e1 in + let [g,x:names ⊢ prefl] = e2 in + let ex_bstep [g,x:names ⊢ B1[..,x]] [g ⊢ B1'] e1' e2' + = strengthen_bstep [g,x:names ⊢ B1[..,x]] in + let [g,x:names ⊢ brefl] = e1' in + let [g,x:names,z:names ⊢ prefl] = e2' in + ex_fstep [g,x:names ⊢ fs_com1 F1[..,x] B1[..,x]] + [g ⊢ fs_com1 F1' B1'] [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_com2 B1[..,x] F1[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F1[..,x]] [g ⊢ F1'] e1 e2 + = strengthen_fstep [g,x:names ⊢ F1[..,x]] in + let [g,x:names ⊢ frefl] = e1 in + let [g,x:names ⊢ prefl] = e2 in + let ex_bstep [g,x:names ⊢ B1[..,x]] [g ⊢ B1'] e1' e2' + = strengthen_bstep [g,x:names ⊢ B1[..,x]] in + let [g,x:names ⊢ brefl] = e1' in + let [g,x:names,z:names ⊢ prefl] = e2' in + ex_fstep [g,x:names ⊢ fs_com2 B1[..,x] F1[..,x]] + [g ⊢ fs_com2 B1' F1'] [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_res \y.F1[..,y,x]] ⇒ + let ex_fstep [g,y:names,x:names ⊢ F1[..,y,x]] [g,y:names ⊢ F1'[..,y]] + e1 e2 = strengthen_fstep [g,y:names,x:names ⊢ F1[..,y,x]] in + let [g,y:names,x:names ⊢ frefl] = e1 in + let [g,y:names,x:names ⊢ prefl] = e2 in + ex_fstep [g,x:names ⊢ fs_res \y.F1[..,y,x]] + [g ⊢ fs_res \y.F1'[..,y]] [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_close1 B1[..,x] B2[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B1[..,x]] [g ⊢ B1'] e1 e2 + = strengthen_bstep [g,x:names ⊢ B1[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + let ex_bstep [g,x:names ⊢ B2[..,x]] [g ⊢ B2'] e1' e2' + = strengthen_bstep [g,x:names ⊢ B2[..,x]] in + let [g,x:names ⊢ brefl] = e1' in + let [g,x:names,z:names ⊢ prefl] = e2' in + ex_fstep [g,x:names ⊢ fs_close1 B1[..,x] B2[..,x]] + [g ⊢ fs_close1 B1' B2'] [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + | [g,x:names ⊢ fs_close2 B1[..,x] B2[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B1[..,x]] [g ⊢ B1'] e1 e2 + = strengthen_bstep [g,x:names ⊢ B1[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + let ex_bstep [g,x:names ⊢ B2[..,x]] [g ⊢ B2'] e1' e2' + = strengthen_bstep [g,x:names ⊢ B2[..,x]] in + let [g,x:names ⊢ brefl] = e1' in + let [g,x:names,z:names ⊢ prefl] = e2' in + ex_fstep [g,x:names ⊢ fs_close2 B1[..,x] B2[..,x]] + [g ⊢ fs_close2 B1' B2'] [g,x:names ⊢ frefl] [g,x:names ⊢ prefl] + +and rec strengthen_bstep: (g:ctx) {B:[g,x:names ⊢ bstep P[..] A + \z.Q[..,x,z]]} → ex_str_bstep [g,x:names ⊢ B] = +/ total b (strengthen_bstep _ _ _ _ b) / +mlam B ⇒ case [_,x:names ⊢ B] of + | [g,x:names ⊢ bs_in] ⇒ ex_bstep [g,x:names ⊢ B] [g ⊢ bs_in] + [g,x:names ⊢ brefl] [g,x:names,z:names ⊢ prefl] + | [g,x:names ⊢ bs_par1 B1[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B1[..,x]] [g ⊢ B1'] e1 e2 + = strengthen_bstep [g,x:names ⊢ B1[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + ex_bstep [g,x:names ⊢ bs_par1 B1[..,x]] [g ⊢ bs_par1 B1'] + [g,x:names ⊢ brefl] [g,x:names,z:names ⊢ prefl] + | [g,x:names ⊢ bs_par2 B2[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B2[..,x]] [g ⊢ B2'] e1 e2 + = strengthen_bstep [g,x:names ⊢ B2[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + ex_bstep [g,x:names ⊢ bs_par2 B2[..,x]] [g ⊢ bs_par2 B2'] + [g,x:names ⊢ brefl] [g,x:names,z:names ⊢ prefl] + | [g,x:names ⊢ bs_res \y.B1[..,y,x]] ⇒ + let ex_bstep [g,y:names,x:names ⊢ B1[..,y,x]] [g,y:names ⊢ B1'[..,y]] + e1 e2 = strengthen_bstep [g,y:names,x:names ⊢ B1[..,y,x]] in + let [g,y:names,x:names ⊢ brefl] = e1 in + let [g,y:names,x:names,z:names ⊢ prefl] = e2 in + ex_bstep [g,x:names ⊢ bs_res \y.B1[..,y,x]] + [g ⊢ bs_res \y.B1'[..,y]] [g,x:names ⊢ brefl] + [g,x:names,z:names ⊢ prefl] + | [g,x:names ⊢ bs_open \y.F1[..,y,x]] ⇒ + let ex_fstep [g,y:names,x:names ⊢ F1[..,y,x]] [g,y:names ⊢ F1'[..,y]] + e1 e2 = strengthen_fstep [g,y:names,x:names ⊢ F1[..,y,x]] in + let [g,y:names,x:names ⊢ frefl] = e1 in + let [g,y:names,x:names ⊢ prefl] = e2 in + ex_bstep [g,x:names ⊢ bs_open \y.F1[..,y,x]] + [g ⊢ bs_open \y.F1'[..,y]] [g,x:names ⊢ brefl] + [g,x:names,z:names ⊢ prefl] +; + + +% We can finally prove that, if P is congruent to Q and P makes a transition through A to P', then there exists a process Q' +% such that Q makes a transition through A into Q' and P' is congruent to Q'. + +% In order to prove the desired result, we state two symmetric lemmas: given that P is congruent to Q, +% we either assume that the given free transition involves the left process P (fstep P A Q) or the right process Q (fstep Q A Q'). +% In this way, when performing structural induction on the congruence P cong Q, we immediately obtain the proof +% of the "c_sym" case (the case in which we deduce P cong Q from the congruence Q cong P). + +% We choose to define a single type ex_fstepcong and use it in both lemmas, aiming at a simpler and more economic code and sacrificing symmetry. +% Our choice is equivalent to defining a second type ex_fstepcong' (with ex_fstepcong P Q A P' iff fstep Q A Q' and Q' cong P' for some Q') for perfect symmetry. + +% The same applies to bound transitions: so we have four lemmas which we prove simultaneously. + +rec cong_fstepleft_impl_fstepright: (g:ctx) [g ⊢ P cong Q] + → [g ⊢ fstep P A P'] → [g ⊢ ex_fstepcong P Q A P'] = +/ total c (cong_fstepleft_impl_fstepright _ _ _ _ _ c _)/ +fn c ⇒ fn f ⇒ case c of + | [g ⊢ par_unit] ⇒ let [g ⊢ fs_par1 F1] = f in [g ⊢ fsc F1 par_unit] + | [g ⊢ par_comm] ⇒ + (case f of + | [g ⊢ fs_par1 F1] ⇒ [g ⊢ fsc (fs_par2 F1) par_comm] + | [g ⊢ fs_par2 F2] ⇒ [g ⊢ fsc (fs_par1 F2) par_comm] + | [g ⊢ fs_com1 F1 B1] ⇒ [g ⊢ fsc (fs_com2 B1 F1) par_comm] + | [g ⊢ fs_com2 B1 F1] ⇒ [g ⊢ fsc (fs_com1 F1 B1) par_comm] + | [g ⊢ fs_close1 B1 B2] ⇒ + [g ⊢ fsc (fs_close2 B2 B1) (c_res \x.par_comm)] + | [g ⊢ fs_close2 B1 B2] ⇒ + [g ⊢ fsc (fs_close1 B2 B1) (c_res \x.par_comm)] + ) + | [g ⊢ par_assoc] ⇒ + (case f of + | [g ⊢ fs_par1 F] ⇒ [g ⊢ fsc (fs_par1 (fs_par1 F)) par_assoc] + | [g ⊢ fs_par2 F] ⇒ + (case [g ⊢ F] of + | [g ⊢ fs_par1 F'] ⇒ + [g ⊢ fsc (fs_par1 (fs_par2 F')) par_assoc] + | [g ⊢ fs_par2 F'] ⇒ [g ⊢ fsc (fs_par2 F') par_assoc] + | [g ⊢ fs_com1 F' B] ⇒ + [g ⊢ fsc (fs_com1 (fs_par2 F') B) par_assoc] + | [g ⊢ fs_com2 B F'] ⇒ + [g ⊢ fsc (fs_com2 (bs_par2 B) F') par_assoc] + | [g ⊢ fs_close1 B1 B2] ⇒ + [g ⊢ fsc (fs_close1 (bs_par2 B1) B2) (c_trans + par_comm (c_trans sc_ext_par (c_trans (c_res + \x.par_comm) (c_res \x.par_assoc))))] + | [g ⊢ fs_close2 B1 B2] ⇒ + [g ⊢ fsc (fs_close2 (bs_par2 B1) B2) (c_trans + par_comm (c_trans sc_ext_par (c_trans (c_res + \x.par_comm) (c_res \x.par_assoc))))] + ) + | [g ⊢ fs_com1 F B] ⇒ + (case [g ⊢ B] of + | [g ⊢ bs_par1 B'] ⇒ + [g ⊢ fsc (fs_par1 (fs_com1 F B')) par_assoc] + | [g ⊢ bs_par2 B'] ⇒ + [g ⊢ fsc (fs_com1 (fs_par1 F) B') par_assoc] + ) + | [g ⊢ fs_com2 B F] ⇒ + (case [g ⊢ F] of + | [g ⊢ fs_par1 F'] ⇒ + [g ⊢ fsc (fs_par1 (fs_com2 B F')) par_assoc] + | [g ⊢ fs_par2 F'] ⇒ + [g ⊢ fsc (fs_com2 (bs_par1 B) F') par_assoc] + ) + | [g ⊢ fs_close1 B1 B2] ⇒ + (case [g ⊢ B2] of + | [g ⊢ bs_par1 B2'] ⇒ + [g ⊢ fsc (fs_par1 (fs_close1 B1 B2')) + (c_trans (c_res \x.par_assoc) (c_sym sc_ext_par))] + | [g ⊢ bs_par2 B2'] ⇒ + [g ⊢ fsc (fs_close1 (bs_par1 B1) B2') (c_res \x.par_assoc)] + ) + | [g ⊢ fs_close2 B1 B2] ⇒ + (case [g ⊢ B2] of + | [g ⊢ bs_par1 B2'] ⇒ + [g ⊢ fsc (fs_par1 (fs_close2 B1 B2')) + (c_trans (c_res \x.par_assoc) (c_sym sc_ext_par))] + | [g ⊢ bs_par2 B2'] ⇒ + [g ⊢ fsc (fs_close2 (bs_par1 B1) B2') (c_res \x.par_assoc)] + ) + ) + | [g ⊢ sc_ext_zero] ⇒ + let [g ⊢ fs_res \x.F[..,x]] = f in impossible [g, x:names ⊢ F[..,x]] + | [g ⊢ sc_ext_par] ⇒ + (case f of + | [g ⊢ fs_par1 F1] ⇒ + let [g ⊢ fs_res \x.F1'[..,x]] = [g ⊢ F1] in + [g ⊢ fsc (fs_res \x.(fs_par1 F1'[..,x])) sc_ext_par] + | [g ⊢ fs_par2 F2] ⇒ + [g ⊢ fsc (fs_res \x.(fs_par2 F2[..])) sc_ext_par] + | [g ⊢ fs_com1 F1 B1] ⇒ + let [g ⊢ fs_res \x.F1'[..,x]] = [g ⊢ F1] in + [g ⊢ fsc (fs_res \x.(fs_com1 F1'[..,x] B1[..])) sc_ext_par] + | [g ⊢ fs_com2 B1 F1] ⇒ + let [g ⊢ bs_res \x.B1'[..,x]] = [g ⊢ B1] in + [g ⊢ fsc (fs_res \x.(fs_com2 B1'[..,x] F1[..])) sc_ext_par] + | [g ⊢ fs_close1 B1 B2] ⇒ + (case [g ⊢ B1] of + | [g ⊢ bs_res \x.B1'[..,x]] ⇒ + [g ⊢ fsc (fs_res \x.(fs_close1 B1'[..,x] B2[..])) + (c_trans (c_res \w.sc_ext_par) sc_ext_res)] + | [g ⊢ bs_open \x.F1[..,x]] ⇒ + [g ⊢ fsc (fs_res \x.(fs_com1 F1[..,x] B2[..])) c_ref] + ) + | [g ⊢ fs_close2 B1 B2] ⇒ + let [g ⊢ bs_res \x.B1'[..,x]] = [g ⊢ B1] in + [g ⊢ fsc (fs_res \x.(fs_close2 B1'[..,x] B2[..])) + (c_trans (c_res \w.sc_ext_par) sc_ext_res)] + ) + | [g ⊢ sc_ext_res] ⇒ + let [g ⊢ fs_res \x.F[..,x]] = f in + let [g,x:names ⊢ fs_res \y.F'[..,x,y]] = [g,x:names ⊢ F[..,x]] in + [g ⊢ fsc (fs_res \y.(fs_res \x.F'[..,x,y])) (sc_ext_res)] + | [g ⊢ c_in \x.C1[..,x]] ⇒ impossible f + | [g ⊢ c_out C1] ⇒ let [g ⊢ fs_out] = f in [g ⊢ fsc fs_out C1] + | [g ⊢ c_par C1] ⇒ + (case f of + | [g ⊢ fs_par1 F1] ⇒ + let [g ⊢ fsc F2 C2] = cong_fstepleft_impl_fstepright [g ⊢ C1] + [g ⊢ F1] in [g ⊢ fsc (fs_par1 F2) (c_par C2)] + | [g ⊢ fs_par2 F1] ⇒ [g ⊢ fsc (fs_par2 F1) (c_par C1)] + | [g ⊢ fs_com1 F1 B1] ⇒ + let [g ⊢ fsc F2 C2] = cong_fstepleft_impl_fstepright [g ⊢ C1] + [g ⊢ F1] in [g ⊢ fsc (fs_com1 F2 B1) (c_par C2)] + | [g ⊢ fs_com2 B1 F1] ⇒ + let [g ⊢ bsc B2 \x.C2[..,x]] = cong_bstepleft_impl_bstepright + [g ⊢ C1][g ⊢ B1] in [g ⊢ fsc(fs_com2 B2 F1)(c_par C2[..,_])] + | [g ⊢ fs_close1 B1 B2] ⇒ + let [g ⊢ bsc B1' \x.C2[..,x]] = + cong_bstepleft_impl_bstepright [g ⊢ C1] [g ⊢ B1] in + [g ⊢ fsc (fs_close1 B1' B2) (c_res \x.(c_par C2[..,x]))] + | [g ⊢ fs_close2 B1 B2] ⇒ + let [g ⊢ bsc B1' \x.C2[..,x]] = + cong_bstepleft_impl_bstepright [g ⊢ C1] [g ⊢ B1] in + [g ⊢ fsc (fs_close2 B1' B2) (c_res \x.(c_par C2[..,x]))] + ) + | [g ⊢ c_res \x.C[..,x]] ⇒ + let [g ⊢ fs_res \x.F[..,x]] = f in + let [g,x:names ⊢ fsc F'[..,x] C'[..,x]] = + cong_fstepleft_impl_fstepright [g,x:names ⊢ C[..,x]] + [g,x:names ⊢ F[..,x]] in + [g ⊢ fsc (fs_res \x.F'[..,x]) (c_res \x.C'[..,x])] + | [g ⊢ c_ref] ⇒ let [g ⊢ F] = f in [g ⊢ fsc F c_ref] + | [g ⊢ c_sym C'] ⇒ + let [g ⊢ D] = cong_fstepright_impl_fstepleft [g ⊢ C'] f in [g ⊢ D] + | [g ⊢ c_trans C1 C2] ⇒ + let [g ⊢ fsc F1 C1'] = cong_fstepleft_impl_fstepright [g ⊢ C1] f in + let [g ⊢ fsc F2 C2'] = cong_fstepleft_impl_fstepright [g ⊢ C2] + [g ⊢ F1] in [g ⊢ fsc F2 (c_trans C1' C2')] + +and rec cong_fstepright_impl_fstepleft: (g:ctx) [g ⊢ P cong Q] + → [g ⊢ fstep Q A Q'] → [g ⊢ ex_fstepcong Q P A Q'] = +/ total c (cong_fstepright_impl_fstepleft _ _ _ _ _ c _)/ +fn c ⇒ fn f ⇒ case c of + | [g ⊢ par_unit] ⇒ + let [g ⊢ F] = f in [g ⊢ fsc (fs_par1 F) (c_sym par_unit)] + | [g ⊢ par_comm] ⇒ + (case f of + | [g ⊢ fs_par1 F1] ⇒ [g ⊢ fsc (fs_par2 F1) par_comm] + | [g ⊢ fs_par2 F2] ⇒ [g ⊢ fsc (fs_par1 F2) par_comm] + | [g ⊢ fs_com1 F1 B1] ⇒ [g ⊢ fsc (fs_com2 B1 F1) par_comm] + | [g ⊢ fs_com2 B1 F1] ⇒ [g ⊢ fsc (fs_com1 F1 B1) par_comm] + | [g ⊢ fs_close1 B1 B2] ⇒ + [g ⊢ fsc (fs_close2 B2 B1) (c_res \x.par_comm)] + | [g ⊢ fs_close2 B1 B2] ⇒ + [g ⊢ fsc (fs_close1 B2 B1) (c_res \x.par_comm)] + ) + | [g ⊢ par_assoc] ⇒ + (case f of + | [g ⊢ fs_par1 F] ⇒ + (case [g ⊢ F] of + | [g ⊢ fs_par1 F'] ⇒ [g ⊢ fsc (fs_par1 F') (c_sym par_assoc)] + | [g ⊢ fs_par2 F'] ⇒ + [g ⊢ fsc (fs_par2 (fs_par1 F')) (c_sym par_assoc)] + | [g ⊢ fs_com1 F' B] ⇒ + [g ⊢ fsc (fs_com1 F' (bs_par1 B)) (c_sym par_assoc)] + | [g ⊢ fs_com2 B F'] ⇒ + [g ⊢ fsc (fs_com2 B (fs_par1 F')) (c_sym par_assoc)] + | [g ⊢ fs_close1 B1 B2] ⇒ + [g ⊢ fsc (fs_close1 B1 (bs_par1 B2)) + (c_trans sc_ext_par (c_res \x.(c_sym par_assoc)))] + | [g ⊢ fs_close2 B1 B2] ⇒ + [g ⊢ fsc (fs_close2 B1 (bs_par1 B2)) + (c_trans sc_ext_par (c_res \x.(c_sym par_assoc)))] + ) + | [g ⊢ fs_par2 F] ⇒ + [g ⊢ fsc (fs_par2 (fs_par2 F)) (c_sym par_assoc)] + | [g ⊢ fs_com1 F B] ⇒ + (case [g ⊢ F] of + | [g ⊢ fs_par1 F'] ⇒ + [g ⊢ fsc (fs_com1 F' (bs_par2 B)) (c_sym par_assoc)] + | [g ⊢ fs_par2 F'] ⇒ + [g ⊢ fsc (fs_par2 (fs_com1 F' B)) (c_sym par_assoc)] + ) + | [g ⊢ fs_com2 B F] ⇒ + (case [g ⊢ B] of + | [g ⊢ bs_par1 B'] ⇒ + [g ⊢ fsc (fs_com2 B' (fs_par2 F)) (c_sym par_assoc)] + | [g ⊢ bs_par2 B'] ⇒ + [g ⊢ fsc (fs_par2 (fs_com2 B' F)) (c_sym par_assoc)] + ) + | [g ⊢ fs_close1 B1 B2] ⇒ + (case [g ⊢ B1] of + | [g ⊢ bs_par1 B1'] ⇒ + [g ⊢ fsc (fs_close1 B1' (bs_par2 B2)) + (c_res \x.(c_sym par_assoc))] + | [g ⊢ bs_par2 B1'] ⇒ + [g ⊢ fsc (fs_par2 (fs_close1 B1' B2)) + (c_trans (c_res \x.(c_sym par_assoc)) (c_trans (c_res + \x.par_comm) (c_trans (c_sym sc_ext_par) par_comm)))] + ) + | [g ⊢ fs_close2 B1 B2] ⇒ + (case [g ⊢ B1] of + | [g ⊢ bs_par1 B1'] ⇒ + [g ⊢ fsc (fs_close2 B1' (bs_par2 B2)) + (c_res \x.(c_sym par_assoc))] + | [g ⊢ bs_par2 B1'] ⇒ + [g ⊢ fsc (fs_par2 (fs_close2 B1' B2)) + (c_trans (c_res \x.(c_sym par_assoc)) (c_trans (c_res + \x.par_comm) (c_trans (c_sym sc_ext_par) par_comm)))] + ) + ) + | [g ⊢ sc_ext_zero] ⇒ impossible f + | [g ⊢ sc_ext_par] ⇒ let [g ⊢ fs_res \x.F[..,x]] = f in + (case [g, x:names ⊢ F[..,x]] of + | [g,x:names ⊢ fs_par1 F1[..,x]] ⇒ + [g ⊢ fsc (fs_par1 (fs_res \x.F1[..,x])) (c_sym sc_ext_par)] + | [g,x:names ⊢ fs_par2 F2[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F2[..,x]] [g ⊢ F2'] e1 e2 = + strengthen_fstep [g,x:names ⊢ F2[..,x]] in + let [g,x:names ⊢ frefl] = e1 in + let [g,x:names ⊢ prefl] = e2 in + [g ⊢ fsc (fs_par2 F2') (c_sym sc_ext_par)] + | [g,x:names ⊢ fs_com1 F1[..,x] B1[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B1[..,x]] [g ⊢ B1'] e1 e2 = + strengthen_bstep [g,x:names ⊢ B1[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + let [g,x:names ⊢ F1[..,x]]:[g,x:names ⊢ fstep P (f_out + Z[..] W) P'] = [g,x:names ⊢ F1[..,x]] in + (case [g,x:names ⊢ W] of + | [g,x:names ⊢ #w[..]] ⇒ [g ⊢ fsc (fs_com1 (fs_res + \x.F1[..,x]) B1') (c_sym sc_ext_par)] + | [g,x:names ⊢ x] ⇒ [g ⊢ fsc (fs_close1 (bs_open + \x.F1[..,x]) B1') c_ref] + ) + | [g,x:names ⊢ fs_com2 B1[..,x] F1[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F1[..,x]] [g ⊢ F1'] e1 e2 = + strengthen_fstep [g,x:names ⊢ F1[..,x]] in + let [g,x:names ⊢ frefl] = e1 in + let [g,x:names ⊢ prefl] = e2 in + [g ⊢ fsc (fs_com2 (bs_res \x.B1[..,x]) F1') + (c_sym sc_ext_par)] + | [g,x:names ⊢ fs_close1 B1[..,x] B2[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B2[..,x]] [g ⊢ B2'] e1 e2 = + strengthen_bstep [g,x:names ⊢ B2[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + [g ⊢ fsc (fs_close1 (bs_res \x.B1[..,x]) B2') + (c_trans sc_ext_res (c_res \w.(c_sym sc_ext_par)))] + | [g,x:names ⊢ fs_close2 B1[..,x] B2[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B2[..,x]] [g ⊢ B2'] e1 e2 = + strengthen_bstep [g,x:names ⊢ B2[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names,z:names ⊢ prefl] = e2 in + [g ⊢ fsc (fs_close2 (bs_res \x.B1[..,x]) B2') + (c_trans sc_ext_res (c_res \w.(c_sym sc_ext_par)))] + ) + | [g ⊢ sc_ext_res] ⇒ + let [g ⊢ fs_res \x.F[..,x]] = f in + let [g,x:names ⊢ fs_res \y.F'[..,x,y]] = [g,x:names ⊢ F[..,x]] in + [g ⊢ fsc (fs_res \y.(fs_res \x.F'[..,x,y])) sc_ext_res] + | [g ⊢ c_in \x.C1[..,x]] ⇒ impossible f + | [g ⊢ c_out C1] ⇒ let [g ⊢ fs_out] = f in [g ⊢ fsc fs_out (c_sym C1)] + | [g ⊢ c_par C1] ⇒ + (case f of + | [g ⊢ fs_par1 F1] ⇒ + let [g ⊢ fsc F2 C2] = cong_fstepright_impl_fstepleft [g ⊢ C1] + [g ⊢ F1] in [g ⊢ fsc (fs_par1 F2) (c_par C2)] + | [g ⊢ fs_par2 F1] ⇒ [g ⊢ fsc (fs_par2 F1) (c_par (c_sym C1))] + | [g ⊢ fs_com1 F1 B1] ⇒ + let [g ⊢ fsc F2 C2] = cong_fstepright_impl_fstepleft [g ⊢ C1] + [g ⊢ F1] in [g ⊢ fsc (fs_com1 F2 B1) (c_par C2)] + | [g ⊢ fs_com2 B1 F1] ⇒ + let [g ⊢ bsc B2 \x.C2[..,x]] = cong_bstepright_impl_bstepleft + [g ⊢ C1][g ⊢ B1] in [g ⊢ fsc(fs_com2 B2 F1)(c_par C2[..,_])] + | [g ⊢ fs_close1 B1 B2] ⇒ + let [g ⊢ bsc B1' \x.C2[..,x]] = cong_bstepright_impl_bstepleft + [g ⊢ C1] [g ⊢ B1] in + [g ⊢ fsc (fs_close1 B1' B2) (c_res \x.(c_par C2[..,x]))] + | [g ⊢ fs_close2 B1 B2] ⇒ + let [g ⊢ bsc B1' \x.C2[..,x]] = cong_bstepright_impl_bstepleft + [g ⊢ C1] [g ⊢ B1] in + [g ⊢ fsc (fs_close2 B1' B2) (c_res \x.(c_par C2[..,x]))] + ) + | [g ⊢ c_res \x.C[..,x]] ⇒ + let [g ⊢ fs_res \x.F[..,x]] = f in + let [g,x:names ⊢ fsc F'[..,x] C'[..,x]] = + cong_fstepright_impl_fstepleft [g,x:names ⊢ C[..,x]] + [g,x:names ⊢ F[..,x]] in + [g ⊢ fsc (fs_res \x.F'[..,x]) (c_res \x.C'[..,x])] + | [g ⊢ c_ref] ⇒ let [g ⊢ F] = f in [g ⊢ fsc F c_ref] + | [g ⊢ c_sym C'] ⇒ + let [g ⊢ D] = cong_fstepleft_impl_fstepright [g ⊢ C'] f in [g ⊢ D] + | [g ⊢ c_trans C1 C2] ⇒ + let [g ⊢ fsc F1 C2'] = cong_fstepright_impl_fstepleft [g ⊢ C2] f in + let [g ⊢ fsc F2 C1'] = cong_fstepright_impl_fstepleft [g ⊢ C1] + [g ⊢ F1] in [g ⊢ fsc F2 (c_trans C2' C1')] + +and rec cong_bstepleft_impl_bstepright: (g:ctx) [g ⊢ P cong Q] + → [g ⊢ bstep P A \x.P'[..,x]] → [g ⊢ ex_bstepcong P Q A \x.P'[..,x]] = +/ total c (cong_bstepleft_impl_bstepright _ _ _ _ _ c _)/ +fn c ⇒ fn b ⇒ case c of + | [g ⊢ par_unit] ⇒ + let [g ⊢ bs_par1 B1] = b in [g ⊢ bsc B1 \x.par_unit] + | [g ⊢ par_comm] ⇒ + (case b of + | [g ⊢ bs_par1 B1] ⇒ [g ⊢ bsc (bs_par2 B1) \x.par_comm] + | [g ⊢ bs_par2 B2] ⇒ [g ⊢ bsc (bs_par1 B2) \x.par_comm] + ) + | [g ⊢ par_assoc] ⇒ + (case b of + | [g ⊢ bs_par1 B] ⇒ [g ⊢ bsc (bs_par1 (bs_par1 B)) \x.par_assoc] + | [g ⊢ bs_par2 B] ⇒ + (case [g ⊢ B] of + | [g ⊢ bs_par1 B'] ⇒ + [g ⊢ bsc (bs_par1 (bs_par2 B')) \x.par_assoc] + | [g ⊢ bs_par2 B'] ⇒ [g ⊢ bsc (bs_par2 B') \x.par_assoc] + ) + ) + | [g ⊢ sc_ext_zero] ⇒ + let [g ⊢ bs_res \x.B[..,x]] = b in impossible [g,x:names ⊢ B[..,x]] + | [g ⊢ sc_ext_par] ⇒ + (case b of + | [g ⊢ bs_par1 B1] ⇒ + (case [g ⊢ B1] of + | [g ⊢ bs_res \x.B1'[..,x]] ⇒ + [g ⊢ bsc (bs_res \x.(bs_par1 B1'[..,x])) \x.sc_ext_par] + | [g ⊢ bs_open \x.F1[..,x]] ⇒ + [g ⊢ bsc (bs_open \x.(fs_par1 F1[..,x])) \x.c_ref] + ) + | [g ⊢ bs_par2 B2] ⇒ + [g ⊢ bsc (bs_res \x.(bs_par2 B2[..])) \x.sc_ext_par] + ) + | [g ⊢ sc_ext_res] ⇒ + (case b of + | [g ⊢ bs_res \x.B[..,x]] ⇒ + (case [g,x:names ⊢ B[..,x]] of + | [g,x:names ⊢ bs_res \y.B'[..,x,y]] ⇒ + [g ⊢ bsc (bs_res \y.(bs_res \x.B'[..,x,y])) \x.sc_ext_res] + | [g,x:names ⊢ bs_open \y.F[..,x,y]] ⇒ + [g ⊢ bsc (bs_open \y.(fs_res \x.F[..,x,y])) \x.c_ref] + ) + | [g ⊢ bs_open \x.F[..,x]] ⇒ + let [g,x:names ⊢ fs_res \y.F'[..,x,y]] = [g,x:names ⊢ F[..,x]] + in [g ⊢ bsc (bs_res \y.(bs_open \x.F'[..,x,y])) \x.c_ref] + ) + | [g ⊢ c_in \x.C1[..,x]] ⇒ + let [g ⊢ bs_in] = b in [g ⊢ bsc bs_in \x.C1[..,x]] + | [g ⊢ c_out C1] ⇒ impossible b + | [g ⊢ c_par C1] ⇒ + (case b of + | [g ⊢ bs_par1 B1] ⇒ + let [g ⊢ bsc B2 \x.C2[..,x]] = cong_bstepleft_impl_bstepright + [g ⊢ C1] [g ⊢ B1] in [g ⊢ bsc (bs_par1 B2) \x.(c_par C2[..,x])] + | [g ⊢ bs_par2 B1] ⇒ + [g ⊢ bsc (bs_par2 B1) \x.(c_par C1[..])] + ) + | [g ⊢ c_res \x.C[..,x]] ⇒ + (case b of + | [g ⊢ bs_res \x.B[..,x]] ⇒ + let [g,x:names ⊢ bsc B'[..,x] \y.C'[..,x,y]] = + cong_bstepleft_impl_bstepright [g,x:names ⊢ C[..,x]] + [g,x:names ⊢ B[..,x]] in + [g ⊢ bsc (bs_res \x.B'[..,x]) \y.(c_res \x.C'[..,x,y])] + | [g ⊢ bs_open \x.F[..,x]] ⇒ + let [g,x:names ⊢ fsc F'[..,x] C'[..,x]] = + cong_fstepleft_impl_fstepright [g,x:names ⊢ C[..,x]] + [g,x:names ⊢ F[..,x]] in + [g ⊢ bsc (bs_open \x.F'[..,x]) \x.C'[..,x]] + ) + | [g ⊢ c_ref] ⇒ let [g ⊢ B] = b in [g ⊢ bsc B \x.c_ref] + | [g ⊢ c_sym C'] ⇒ + let [g ⊢ D] = cong_bstepright_impl_bstepleft [g ⊢ C'] b in [g ⊢ D] + | [g ⊢ c_trans C1 C2] ⇒ + let [g ⊢ bsc B1 \x.C1'[..,x]] = + cong_bstepleft_impl_bstepright [g ⊢ C1] b in + let [g ⊢ bsc B2 \x.C2'[..,x]] = + cong_bstepleft_impl_bstepright [g ⊢ C2] [g ⊢ B1] in + [g ⊢ bsc B2 \x.(c_trans C1'[..,x] C2'[..,x])] + + +and rec cong_bstepright_impl_bstepleft: (g:ctx) [g ⊢ P cong Q] + → [g ⊢ bstep Q A \x.Q'[..,x]] → [g ⊢ ex_bstepcong Q P A \x.Q'[..,x]] = +/ total c (cong_bstepright_impl_bstepleft _ _ _ _ _ c _)/ +fn c ⇒ fn b ⇒ case c of + | [g ⊢ par_unit] ⇒ + let [g ⊢ B] = b in [g ⊢ bsc (bs_par1 B) \x.(c_sym par_unit)] + | [g ⊢ par_comm] ⇒ + (case b of + | [g ⊢ bs_par1 B1] ⇒ [g ⊢ bsc (bs_par2 B1) \x.par_comm] + | [g ⊢ bs_par2 B2] ⇒ [g ⊢ bsc (bs_par1 B2) \x.par_comm] + ) + | [g ⊢ par_assoc] ⇒ + (case b of + | [g ⊢ bs_par1 B] ⇒ + (case [g ⊢ B] of + | [g ⊢ bs_par1 B'] ⇒ + [g ⊢ bsc (bs_par1 B') \x.(c_sym par_assoc)] + | [g ⊢ bs_par2 B'] ⇒ + [g ⊢ bsc (bs_par2 (bs_par1 B')) \x.(c_sym par_assoc)] + ) + | [g ⊢ bs_par2 B] ⇒ + [g ⊢ bsc (bs_par2 (bs_par2 B)) \x.(c_sym par_assoc)] + ) + | [g ⊢ sc_ext_zero] ⇒ impossible b + | [g ⊢ sc_ext_par] ⇒ + (case b of + | [g ⊢ bs_res \x.B[..,x]] ⇒ + (case [g, x:names ⊢ B[..,x]] of + | [g,x:names ⊢ bs_par1 B1[..,x]] ⇒ + [g ⊢ bsc (bs_par1 (bs_res \x.B1[..,x])) + \x.(c_sym sc_ext_par)] + | [g,x:names ⊢ bs_par2 B2[..,x]] ⇒ + let ex_bstep [g,x:names ⊢ B2[..,x]] [g ⊢ B2'] e1 e2 = + strengthen_bstep [g,x:names ⊢ B2[..,x]] in + let [g,x:names ⊢ brefl] = e1 in + let [g,x:names, z:names ⊢ prefl] = e2 in + [g ⊢ bsc (bs_par2 B2') \x.(c_sym sc_ext_par)] + ) + | [g ⊢ bs_open \x.F[..,x]] ⇒ + (case [g,x:names ⊢ F[..,x]] of + | [g,x:names ⊢ fs_par1 F1[..,x]] ⇒ + [g ⊢ bsc (bs_par1 (bs_open \x.F1[..,x])) \x.c_ref] + | [g,x:names ⊢ fs_par2 F2[..,x]] ⇒ + let ex_fstep [g,x:names ⊢ F2[..,x]] [g ⊢ F2'] e1 e2 = + strengthen_fstep [g,x:names ⊢ F2[..,x]] in impossible e1 + ) + ) + | [g ⊢ sc_ext_res] ⇒ + (case b of + | [g ⊢ bs_res \x.B[..,x]] ⇒ + (case [g,x:names ⊢ B[..,x]] of + | [g,x:names ⊢ bs_res \y.B'[..,x,y]] ⇒ + [g ⊢ bsc (bs_res \y.(bs_res \x.B'[..,x,y])) \x.sc_ext_res] + | [g,x:names ⊢ bs_open \y.F[..,x,y]] ⇒ + [g ⊢ bsc (bs_open \y.(fs_res \x.F[..,x,y])) \x.c_ref] + ) + | [g ⊢ bs_open \x.F[..,x]] ⇒ + let [g,x:names ⊢ fs_res \y.F'[..,x,y]] = [g,x:names ⊢ F[..,x]] + in [g ⊢ bsc (bs_res \y.(bs_open \x.F'[..,x,y])) \x.c_ref] + ) + | [g ⊢ c_in \x.C1[..,x]] ⇒ + let [g ⊢ bs_in] = b in [g ⊢ bsc bs_in \x.(c_sym C1[..,x])] + | [g ⊢ c_out C1] ⇒ impossible b + | [g ⊢ c_par C1] ⇒ + (case b of + | [g ⊢ bs_par1 B1] ⇒ + let [g ⊢ bsc B2 \x.C2[..,x]] = + cong_bstepright_impl_bstepleft [g ⊢ C1] [g ⊢ B1] in + [g ⊢ bsc (bs_par1 B2) \x.(c_par C2[..,x])] + | [g ⊢ bs_par2 B1] ⇒ + [g ⊢ bsc (bs_par2 B1) \x.(c_par (c_sym C1[..]))] + ) + | [g ⊢ c_res \x.C[..,x]] ⇒ + (case b of + | [g ⊢ bs_res \x.B[..,x]] ⇒ + let [g,x:names ⊢ bsc B'[..,x] \y.C'[..,x,y]] = + cong_bstepright_impl_bstepleft [g,x:names ⊢ C[..,x]] + [g,x:names ⊢ B[..,x]] in + [g ⊢ bsc (bs_res \x.B'[..,x]) \y.(c_res \x.C'[..,x,y])] + | [g ⊢ bs_open \x.F[..,x]] ⇒ + let [g,x:names ⊢ fsc F'[..,x] C'[..,x]] = + cong_fstepright_impl_fstepleft [g,x:names ⊢ C[..,x]] + [g,x:names ⊢ F[..,x]] in + [g ⊢ bsc (bs_open \x.F'[..,x]) \x.C'[..,x]] + ) + | [g ⊢ c_ref] ⇒ let [g ⊢ B] = b in [g ⊢ bsc B \x.c_ref] + | [g ⊢ c_sym C'] ⇒ + let [g ⊢ D] = cong_bstepleft_impl_bstepright [g ⊢ C'] b in [g ⊢ D] + | [g ⊢ c_trans C1 C2] ⇒ + let [g ⊢ bsc B1 \x.C2'[..,x]] = + cong_bstepright_impl_bstepleft [g ⊢ C2] b in + let [g ⊢ bsc B2 \x.C1'[..,x]] = + cong_bstepright_impl_bstepleft [g ⊢ C1] [g ⊢ B1] in + [g ⊢ bsc B2 \x.(c_trans C2'[..,x] C1'[..,x])] +; \ No newline at end of file diff --git a/case-studies/harmony-lemma-formalization/7_reduction_rewriting.bel b/case-studies/harmony-lemma-formalization/7_reduction_rewriting.bel new file mode 100644 index 000000000..a3a93ec04 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/7_reduction_rewriting.bel @@ -0,0 +1,74 @@ +% Predicate about syntactic equivalence of processes involved in reductions: +% ex_red_rew P Q holds iff there exist R1, R2, S, X, Y, x_1,...,x_n such that P cong (nu x_1)...(nu x_n)(((p_out X Y R1) p_par (p_in X R2)) p_par S) and +% Q cong (nu x_1)...(nu x_n)((R1 p_par (R2 Y)) p_par S). +% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case +% in which P cong (nu x)P' and Q cong (nu x)Q', where ex_red_rew P' Q' holds inductively. + +LF ex_red_rew: proc → proc → type = + | red_base: P cong (((p_out X Y R1) p_par (p_in X R2)) p_par S) + → Q cong ((R1 p_par (R2 Y)) p_par S) → ex_red_rew P Q + | red_ind: P cong (p_res P') → Q cong (p_res Q') + → ({w:names} ex_red_rew (P' w) (Q' w)) → ex_red_rew P Q +; + +% We prove the lemma which states that processes involved in reductions (P red Q) +% can be rewritten (up to congruence) in a canonic way (ex_red_rew P Q). +% Before, we need three additional lemmas which prove the result in particular cases. + +rec red_impl_red_rew_par: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_red_rew P Q] + → [g ⊢ ex_red_rew (P p_par R) (Q p_par R)] = +/ total d (red_impl_red_rew_par _ _ _ _ d) / +mlam R ⇒ fn d ⇒ case d of + | [g ⊢ red_base C1 C2] ⇒ + [g ⊢ red_base (c_trans (c_par C1) (c_sym par_assoc)) + (c_trans (c_par C2) (c_sym par_assoc))] + | [g ⊢ red_ind C1 C2 \w.D1[..,w]] ⇒ + let [g,w:names ⊢ D2[..,w]] = red_impl_red_rew_par + [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in + [g ⊢ red_ind (c_trans (c_par C1) sc_ext_par) + (c_trans (c_par C2) sc_ext_par) \w.D2[..,w]] +; + +rec red_impl_red_rew_res: (g:ctx) [g,z:names ⊢ ex_red_rew P[..,z] Q[..,z]] + → [g ⊢ ex_red_rew (p_res \z.P[..,z]) (p_res \z.Q[..,z])] = +/ total d (red_impl_red_rew_res _ _ _ d) / +fn d ⇒ case d of + | [g,z:names ⊢ red_base C1[..,z] C2[..,z]] ⇒ + [g ⊢ red_ind c_ref c_ref \z.(red_base C1[..,z] C2[..,z])] + | [g,z:names ⊢ red_ind C1[..,z] C2[..,z] \w.D1[..,z,w]] ⇒ + let [g,z:names ⊢ D2[..,z]] = red_impl_red_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in + [g ⊢ red_ind (c_res \z.C1[..,z]) (c_res \z.C2[..,z]) \z.D2[..,z]] +; + +rec red_impl_red_rew_str: (g:ctx) [g ⊢ P cong P'] → [g ⊢ ex_red_rew P' Q'] + → [g ⊢ Q' cong Q] → [g ⊢ ex_red_rew P Q] = +/ total d (red_impl_red_rew_str _ _ _ _ _ _ d _) / +fn c1 ⇒ fn d ⇒ fn c2 ⇒ case d of + | [g ⊢ red_base C1' C2'] ⇒ + let [g ⊢ C1] = c1 in + let [g ⊢ C2] = c2 in + [g ⊢ red_base (c_trans C1 C1') (c_trans (c_sym C2) C2')] + | [g ⊢ red_ind C1' C2' \w.D1[..,w]] ⇒ + let [g ⊢ C1] = c1 in + let [g ⊢ C2] = c2 in + [g ⊢ red_ind (c_trans C1 C1') (c_trans (c_sym C2) C2') \w.D1[..,w]] +; + + +rec red_impl_red_rew: (g:ctx) [g ⊢ P red Q] → [g ⊢ ex_red_rew P Q] = +/ total r (red_impl_red_rew _ _ _ r) / +fn r ⇒ case r of + | [g ⊢ r_com] ⇒ [g ⊢ red_base (c_sym par_unit) (c_sym par_unit)] + | [g ⊢ r_par R1]:[g ⊢ (P p_par R) red (Q p_par R)] ⇒ + let [g ⊢ D1] = red_impl_red_rew [g ⊢ R1] in + let [g ⊢ D2] = red_impl_red_rew_par [g ⊢ R] [g ⊢ D1] in [g ⊢ D2] + | [g ⊢ r_res \z.R1[..,z]] ⇒ + let [g,z:names ⊢ D1[..,z]] = red_impl_red_rew + [g,z:names ⊢ R1[..,z]] in + let [g ⊢ D2] = red_impl_red_rew_res [g,z:names ⊢ D1[..,z]] in + [g ⊢ D2] + | [g ⊢ r_str C1 R1 C2] ⇒ + let [g ⊢ D1] = red_impl_red_rew [g ⊢ R1] in + let [g ⊢ D2] = red_impl_red_rew_str [g ⊢ C1] [g ⊢ D1] [g ⊢ C2] in + [g ⊢ D2] +; \ No newline at end of file diff --git a/case-studies/harmony-lemma-formalization/8_theorem2.bel b/case-studies/harmony-lemma-formalization/8_theorem2.bel new file mode 100644 index 000000000..46c84977a --- /dev/null +++ b/case-studies/harmony-lemma-formalization/8_theorem2.bel @@ -0,0 +1,29 @@ +% We now prove that, given two processes P and Q involved in a reduction (P red Q), then there exists a process Q' +% such that P steps into Q' through tau and Q is congruent to Q' (overall, ex_fstepcong P P f_tau Q holds). +% We obtain the result by rewriting the processes P and Q up to congruence in a canonic way (ex_red_rew P Q) +% and stating a lemma which unfolds the type ex_red_rew and reaches the conclusion. + +rec red_rew_impl_fstepcong: (g:ctx) [g ⊢ ex_red_rew P Q] + → [g ⊢ ex_fstepcong P P f_tau Q] = +/ total d (red_rew_impl_fstepcong _ _ _ d) / +fn d ⇒ case d of + | [g ⊢ red_base C1 C2] ⇒ + let [g ⊢ fsc F C3] = cong_fstepright_impl_fstepleft + [g ⊢ C1] [g ⊢ fs_par1 (fs_com1 fs_out bs_in)] in + [g ⊢ fsc F (c_trans C2 C3)] + | [g ⊢ red_ind C1 C2 \w.D1[..,w]] ⇒ + let [g,w:names ⊢ fsc F1[..,w] C3[..,w]] = + red_rew_impl_fstepcong [g,w:names ⊢ D1[..,w]] in + + let [g ⊢ fsc F2 C4] = cong_fstepright_impl_fstepleft + [g ⊢ C1] [g ⊢ fs_res \w.F1[..,w]] in + [g ⊢ fsc F2 (c_trans C2 (c_trans (c_res \w.C3[..,w]) C4))] +; + + +rec red_impl_fstepcong: (g:ctx) [g ⊢ P red Q] + → [g ⊢ ex_fstepcong P P f_tau Q] = +/ total r (red_impl_fstepcong _ _ _ r) / +fn r ⇒ let [g ⊢ D1] = red_impl_red_rew r in + let [g ⊢ D2] = red_rew_impl_fstepcong [g ⊢ D1] in [g ⊢ D2] +; \ No newline at end of file diff --git a/case-studies/harmony-lemma-formalization/README.md b/case-studies/harmony-lemma-formalization/README.md new file mode 100644 index 000000000..a3d37474d --- /dev/null +++ b/case-studies/harmony-lemma-formalization/README.md @@ -0,0 +1,68 @@ +# Overview + +This artifact contains the Beluga mechanization for the paper + + A Beluga Formalization of the Harmony Lemma in the π-Calculus + Gabriele Cecilia and Alberto Momigliano + Proceedings Workshop on LFMTP 2024, Tallinn, Estonia, 8th July 2024, + Electronic Proceedings in Theoretical Computer Science 404, pp. 1-17 + https://doi.org/10.4204/EPTCS.404.1 + +and it contains the code of [this original repository](https://github.com/GabrieleCecilia/concurrent-benchmark-solution/). This work provides a Beluga solution to the 2nd challenge of the Concurrent Calculi Formalisation Benchmark ([CCFB](https://concurrentbenchmark.github.io/)). + +Below are files that are included in this artifact. + + all.cfg - Collects all used Beluga source files + 1_definitions.bel - Contains encoding of syntax and semantics of the pi-calculus + 2_input_rewriting.bel, - Contain proofs of rewriting lemmas for specific transitions + 3_free_output_rewriting.bel, + 4_bound_output_rewriting.bel + 5_theorem1.bel - Proof of the first implication of the Harmony Lemma + 6_stepcong_lemma.bel - Contains proofs of a congruence-as-bisimilarity and a strengthening lemma + 7_reduction_rewriting.bel - Contains proof of a rewriting lemma for reductions + 8_theorem2.bel - Proof of the second implication of the Harmony Lemma + + + +## Paper to Artifact Table + +| Definition/Proofs | Paper | File | Definition Name | +|-----------------------------------------------|---------------|------------------------------|-------------------------------------------| +| Names, processes | Section 3.1 | 1_definitions.bel | names, proc | +| Congruence, reduction | Section 3.2 | 1_definitions.bel | cong, red | +| Actions, transitions | Section 3.3 | 1_definitions.bel | f_act, b_act, f_step, b_step | +| Rewriting lemma for input transitions | Section 3.4.1 | 2_input_rewriting.bel | bs_in_rew | +| Rewriting lemma for free output transitions | Section 3.4.1 | 3_free_output_rewriting.bel | fs_out_rew | +| Rewriting lemma for bound output transitions | Section 3.4.1 | 4_bound_output_rewriting.bel | bs_out_rew | +| Theorem 1 (1st Harmony Lemma implication) | Section 3.4.1 | 5_theorem1.bel | fstep_impl_red | +| Strengthening lemma | Section 3.4.2 | 6_stepcong_lemma.bel | strengthen_fstep, strengthen_bstep | +| Congruence-as-bisimilarity lemma | Section 3.4.2 | 6_stepcong_lemma.bel | cong_fstepleft_impl_fstepright, cong_fstepright_impl_fstepleft, cong_bstepright_impl_bstepleft, cong_fstepleft_impl_fstepright | +| Rewriting lemma for reductions | Section 3.4.2 | 7_reduction_rewriting.bel | red_impl_red_rew | +| Theorem 2 (2nd Harmony Lemma implication) | Section 3.4.2 | 8_theorem2.bel | red_impl_fstepcong | + + +# Execution + +This mechanization is compatible with Beluga version 1.1.1. + +Once Beluga is installed, it can be run on the file `all.cfg`. The +following is the expected output: + + >> beluga all.cfg + ## Type Reconstruction begin: ./1_definitions.bel ## + ## Type Reconstruction done: ./1_definitions.bel ## + ## Type Reconstruction begin: ./2_input_rewriting.bel ## + ## Type Reconstruction done: ./2_input_rewriting.bel ## + ## Type Reconstruction begin: ./3_free_output_rewriting.bel ## + ## Type Reconstruction done: ./3_free_output_rewriting.bel ## + ## Type Reconstruction begin: ./4_bound_output_rewriting.bel ## + ## Type Reconstruction done: ./4_bound_output_rewriting.bel ## + ## Type Reconstruction begin: ./5_theorem1.bel ## + ## Type Reconstruction done: ./5_theorem1.bel ## + ## Type Reconstruction begin: ./6_stepcong_lemma.bel ## + ## Type Reconstruction done: ./6_stepcong_lemma.bel ## + ## Type Reconstruction begin: ./7_reduction_rewriting.bel ## + ## Type Reconstruction done: ./7_reduction_rewriting.bel ## + ## Type Reconstruction begin: ./8_theorem2.bel ## + ## Type Reconstruction done: ./8_theorem2.bel ## + diff --git a/case-studies/harmony-lemma-formalization/all.cfg b/case-studies/harmony-lemma-formalization/all.cfg new file mode 100644 index 000000000..e8350fcc4 --- /dev/null +++ b/case-studies/harmony-lemma-formalization/all.cfg @@ -0,0 +1,8 @@ +1_definitions.bel +2_input_rewriting.bel +3_free_output_rewriting.bel +4_bound_output_rewriting.bel +5_theorem1.bel +6_stepcong_lemma.bel +7_reduction_rewriting.bel +8_theorem2.bel \ No newline at end of file From eab7c5b2c79d3328e86a933ebeefb853f56a642e Mon Sep 17 00:00:00 2001 From: Marc-Antoine Ouimet Date: Mon, 29 Jul 2024 07:44:16 -0400 Subject: [PATCH 2/2] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove extra `[g ⊢ _]` arguments in `fstep_impl_red` --- .../harmony-lemma-formalization/5_theorem1.bel | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/case-studies/harmony-lemma-formalization/5_theorem1.bel b/case-studies/harmony-lemma-formalization/5_theorem1.bel index 42c534a93..977f6e936 100644 --- a/case-studies/harmony-lemma-formalization/5_theorem1.bel +++ b/case-studies/harmony-lemma-formalization/5_theorem1.bel @@ -195,22 +195,22 @@ fn f ⇒ case f of | [g ⊢ fs_par2 F2] ⇒ let [g ⊢ R] = fstep_impl_red [g ⊢ F2] in [g ⊢ r_str par_comm (r_par R) par_comm] | [g ⊢ fs_com1 F1 B1] ⇒ - let [g ⊢ D1] = fs_out_rew [g ⊢ _] [g ⊢ F1] in - let [g ⊢ D2] = bs_in_rew [g ⊢ _] [g ⊢ B1] in + let [g ⊢ D1] = fs_out_rew [g ⊢ F1] in + let [g ⊢ D2] = bs_in_rew [g ⊢ B1] in let [g ⊢ R] = fs_com1_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] | [g ⊢ fs_com2 B1 F1] ⇒ - let [g ⊢ D1] = bs_in_rew [g ⊢ _] [g ⊢ B1] in - let [g ⊢ D2] = fs_out_rew [g ⊢ _] [g ⊢ F1] in + let [g ⊢ D1] = bs_in_rew [g ⊢ B1] in + let [g ⊢ D2] = fs_out_rew [g ⊢ F1] in let [g ⊢ R] = fs_com2_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] | [g ⊢ fs_res \z.F[..,z]] ⇒ let [g,z:names ⊢ R[..,z]] = fstep_impl_red [g,z:names ⊢ F[..,z]] in [g ⊢ r_res \z.R[..,z]] | [g ⊢ fs_close1 B1 B2] ⇒ - let [g ⊢ D1] = bs_out_rew [g ⊢ _][g ⊢ B1] in - let [g ⊢ D2] = bs_in_rew [g ⊢ _] [g ⊢ B2] in + let [g ⊢ D1] = bs_out_rew [g ⊢ B1] in + let [g ⊢ D2] = bs_in_rew [g ⊢ B2] in let [g ⊢ R] = fs_close1_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] | [g ⊢ fs_close2 B1 B2] ⇒ - let [g ⊢ D1] = bs_in_rew [g ⊢ _] [g ⊢ B1] in - let [g ⊢ D2] = bs_out_rew [g ⊢ _] [g ⊢ B2] in + let [g ⊢ D1] = bs_in_rew [g ⊢ B1] in + let [g ⊢ D2] = bs_out_rew [g ⊢ B2] in let [g ⊢ R] = fs_close2_impl_red [g ⊢ D1] [g ⊢ D2] in [g ⊢ R] ; \ No newline at end of file