From 87039feba5cc199fb9b4248f2bd557d6c89755b1 Mon Sep 17 00:00:00 2001 From: Anatolay Date: Fri, 16 Aug 2024 13:14:07 +0300 Subject: [PATCH] WIP: prove the parallel reduction is a series of regular --- Extended/Record.lean | 41 +++++++ Extended/Reduction/Parallel/Properties.lean | 24 ++++ Extended/Reduction/Regular/Confluence.lean | 126 +++++++++++++++++++- Extended/Reduction/Regular/Definition.lean | 30 ++--- 4 files changed, 200 insertions(+), 21 deletions(-) diff --git a/Extended/Record.lean b/Extended/Record.lean index bb8071e3..f39e09e5 100644 --- a/Extended/Record.lean +++ b/Extended/Record.lean @@ -88,4 +88,45 @@ def insert then Record.cons k not_in a tail else Record.cons k not_in a' (insert tail key a) +def consequtive_insert + {keys : List String} + {record : Record α keys} + {key : String} + {a b : α} + : insert (insert record key a) key b + = insert record key b + := match record with + | nil => by rfl + | cons cur_key not_in elem tail => by + simp [insert] + exact dite + (key = cur_key) + (λ eq => by + simp [eq] + exact _ + ) + (λ neq => by + simp [neq] + exact _ + ) + end Record + +namespace Contains + +def contains_after_insert + {keys : List String} + {record : Record α keys} + {key : String} + {a b : α} + (contains : Contains record key a) + : Contains (Record.insert record key b) key b + := match contains with + | head _ _ => by + simp [Record.insert] + exact head _ _ + | tail cur_key _ neq _ contains_tail => by + simp [Record.insert, neq] + exact tail _ _ neq _ (contains_after_insert contains_tail) + +end Contains diff --git a/Extended/Reduction/Parallel/Properties.lean b/Extended/Reduction/Parallel/Properties.lean index 58904208..ad0915f2 100644 --- a/Extended/Reduction/Parallel/Properties.lean +++ b/Extended/Reduction/Parallel/Properties.lean @@ -72,3 +72,27 @@ def single exact FormationPremise.consAttached prefl (single bnds_tail attr pred contains_tail) end FormationPremise + +namespace ApplicationPremise + +def single + {ctx : Ctx} + {t t' : Term} + {attrs : Attrs} + (apps : Record Term attrs) + (attr : Attr) + (preduce : PReduce ctx t t') + (contains : Contains apps attr t) + : ApplicationPremise ctx apps (Record.insert apps attr t') + := match attrs with + | [] => match apps with | Record.nil => ApplicationPremise.nil + | _ :: attrs_tail => match apps with + | Record.cons _ not_in term bnds_tail => match contains with + | Contains.head _ _ => by + simp [Record.insert] + exact ApplicationPremise.cons preduce prefl_app_premise + | Contains.tail _ _ neq _ contains_tail => by + simp [Record.insert, neq] + exact ApplicationPremise.cons prefl (single bnds_tail attr preduce contains_tail) + +end ApplicationPremise diff --git a/Extended/Reduction/Regular/Confluence.lean b/Extended/Reduction/Regular/Confluence.lean index 21b5795b..5d452408 100644 --- a/Extended/Reduction/Regular/Confluence.lean +++ b/Extended/Reduction/Regular/Confluence.lean @@ -8,14 +8,12 @@ set_option autoImplicit false /-! ### Equivalence of `⇛` and `⇝` -/ -/-- Equivalence of `⇛` and `⇝` [KS22, Proposition 3.4 (1)] -/ def reg_to_par : {ctx : Ctx} → {t t' : Term} → Reduce ctx t t' → PReduce ctx t t' - -- := λ { ctx t t' } reduce => match reduce with - := λ { _ _ _ } reduce => match reduce with + := λ reduce => match reduce with -- Dispatch | .r_dot is_attached => .pr_dot prefl is_attached | .r_φ attr_absent φ_present => .pr_φ prefl attr_absent φ_present @@ -32,11 +30,127 @@ def reg_to_par | .r_dc => .pr_dc -- Congruence | .r_cong_appₗ app_bnds t_t' => .pr_cong_app prefl_app_premise (reg_to_par t_t') - | .r_cong_appᵣ app_bnds u_u' => + | .r_cong_appᵣ _ contains u_u' => .pr_cong_app - (ApplicationPremise.cons (reg_to_par u_u') prefl_app_premise) + (ApplicationPremise.single _ _ (reg_to_par u_u') contains) prefl + -- | .r_cong_appᵣ app_bnds contains u_u' => + -- .pr_cong_app + -- (ApplicationPremise.cons (reg_to_par u_u') prefl_app_premise) + -- prefl | .r_cong_dot t_t' => .pr_cong_dot (reg_to_par t_t') - -- TODO | .r_cong_obj contains t_t' => .pr_cong_obj (FormationPremise.single _ _ (reg_to_par t_t') contains) + +inductive R : Ctx → Term → Term → Type where + | refl : {ctx : Ctx} → {t : Term} → R ctx t t + | head + : {ctx : Ctx} + → {t s u : Term} + → Reduce ctx t s + → R ctx s u + → R ctx t u + +def trans_R + {ctx : Ctx} + {t u s : Term} + (r1 : R ctx t u) + (r2 : R ctx u s) + : R ctx t s + := match r1 with + | .refl => r2 + | .head reduce r_tail => + .head reduce (trans_R r_tail r2) + +def congr_dot_R + {attr : Attr} + {ctx : Ctx} + {t t' : Term} + (r : R ctx t t') + : R ctx (dot t attr) (dot t' attr) + := match r with + | .refl => .refl + | .head reduce r' => .head (.r_cong_dot reduce) (congr_dot_R r') + +def congr_appₗ_R + {attrs : Attrs} + {apps : Record Term attrs} + {ctx : Ctx} + {t t' : Term} + (r : R ctx t t') + : R ctx (app t apps) (app t' apps) + := match r with + | .refl => .refl + | .head reduce r' => .head (.r_cong_appₗ _ reduce) (congr_appₗ_R r') + +def congr_appᵣ_R + {attr : Attr} + {attrs : Attrs} + {apps : Record Term attrs} + {ctx : Ctx} + {t u u' : Term} + (r : R ctx u u') + (contains : Contains apps attr u) + : R ctx (app t apps) (app t (Record.insert apps attr u')) + := match r with + | .refl => _ -- TODO .refl + | .head reduce r' => + .head (.r_cong_appᵣ _ contains reduce) (congr_appᵣ_R r' contains.contains_after_insert) + +def par_to_reg + : {ctx : Ctx} + → {t t' : Term} + → PReduce ctx t t' + → R ctx t t' + := λ preduces => match preduces with + | .pr_dot preduce attr_attached => + let reduces := par_to_reg preduce + trans_R (congr_dot_R reduces) (.head (.r_dot attr_attached) .refl) + | .pr_φ preduce attr_absent φ_in => + let reduces := par_to_reg preduce + trans_R (congr_dot_R reduces) (.head (.r_φ attr_absent φ_in) .refl) + | .pr_stop preduce attr_absent φ_absent lam_absent => _ + | .pr_empty preduce => + let reduces := par_to_reg preduce + trans_R (congr_appₗ_R reduces) (.head .r_empty .refl) + | .pr_copy preduce_t preduce_u attr_void => _ + | .pr_over preduce attr_attached => _ + | .pr_miss preduce attr_absent φ_absent lam_absent => _ + | .pr_Φ => .head .r_Φ .refl + | .pr_ξ => .head .r_ξ .refl + | .pr_dd => .head .r_dd .refl + | .pr_dc => .head .r_dc .refl + | .pr_cong_app premise preduce => _ + | .pr_cong_dot preduce => + let reduces := par_to_reg preduce + congr_dot_R reduces + | .pr_cong_obj premise => _ + | .pr_termination_refl => .refl + | .pr_ξ_refl => .refl + | .pr_Φ_refl => .refl + + +-- def par_to_reg +-- : {t t' : Term} +-- → PReducesTo t t' +-- → ReducesToMany t t' +-- := λ preduces => match preduces with +-- | .pr_dot preduce attr_attached => _ +-- | .pr_φ preduce attr_absent φ_in => _ +-- | .pr_stop preduce attr_absent φ_absent lam_absent => _ +-- | .pr_empty preduce => _ +-- | .pr_copy preduce_t preduce_u attr_void => _ +-- | .pr_over preduce attr_attached => _ +-- | .pr_miss preduce attr_absent φ_absent lam_absent => _ +-- | .pr_Φ => .head .r_Φ .refl +-- | .pr_ξ => .head .r_ξ .refl +-- | .pr_dd => .head .r_dd .refl +-- | .pr_dc => .head .r_dc .refl +-- | .pr_cong_app premise preduce => _ +-- | .pr_cong_dot preduce => +-- let reduce := par_to_reg preduce +-- _ +-- | .pr_cong_obj premise => _ +-- | .pr_termination_refl => .refl +-- | .pr_ξ_refl => .refl +-- | .pr_Φ_refl => .refl diff --git a/Extended/Reduction/Regular/Definition.lean b/Extended/Reduction/Regular/Definition.lean index 2684d1ad..aab07a01 100644 --- a/Extended/Reduction/Regular/Definition.lean +++ b/Extended/Reduction/Regular/Definition.lean @@ -120,27 +120,27 @@ inductive Reduce : Ctx → Term → Term → Type where -- This would simplify the rules. On the other hand, from the point of view of "intermediate -- representation for optimizations", it would make sence to allow congruence for any term of -- the application. - -- | r_cong_appᵣ -- congruence of arbitrary app term - -- : { ctx : Ctx } - -- → {t u u' : Term} - -- → {attr : Attr} - -- → {app_attrs : Attrs} - -- → (app_bnds : Record Term app_attrs) - -- → Contains app_bnds attr u - -- → Reduce ctx u u' - -- → Reduce ctx (app t app_bnds) (app t (Record.insert app_bnds attr u')) - | r_cong_appᵣ -- congruence of the first app term + | r_cong_appᵣ -- congruence of arbitrary app term : { ctx : Ctx } → {t u u' : Term} → {attr : Attr} → {app_attrs : Attrs} - → {not_in : attr ∉ app_attrs} → (app_bnds : Record Term app_attrs) + → Contains app_bnds attr u → Reduce ctx u u' - → Reduce - ctx - (app t (Record.cons attr not_in u app_bnds)) - (app t (Record.cons attr not_in u' app_bnds)) + → Reduce ctx (app t app_bnds) (app t (Record.insert app_bnds attr u')) + -- | r_cong_appᵣ -- congruence of the first app term + -- : { ctx : Ctx } + -- → {t u u' : Term} + -- → {attr : Attr} + -- → {app_attrs : Attrs} + -- → {not_in : attr ∉ app_attrs} + -- → (app_bnds : Record Term app_attrs) + -- → Reduce ctx u u' + -- → Reduce + -- ctx + -- (app t (Record.cons attr not_in u app_bnds)) + -- (app t (Record.cons attr not_in u' app_bnds)) | r_cong_dot : { ctx : Ctx } → {t t' : Term}