WIP: prove the parallel reduction is a series of regular

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

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

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

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}