\import Algebra.Meta
\import Logic.Rewriting.ARS.Relation
\import Data.List (!!, ++, ++_nil, ++-assoc, List, nil, ::)
\import Data.Fin
\import Data.Maybe
\import Data.Shifts
\import Data.SubList
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Paths
\import Paths.Meta
\import Set
\import Logic.Rewriting.TRS.HRS
\import Logic.Rewriting.TRS.Linearity
\import Logic.Rewriting.TRS.MetaContexts
\import Logic.Rewriting.TRS.Substitutions
\import Logic.Rewriting.TRS.Union
\import Logic.Rewriting.TRS.Union.Colors
\import Logic.Rewriting.TRS.Union.TopLevel
\open TheoremContext
\data TopLevelColoredReduction {tc : TheoremContext}
(color : Color)
{mc : MetaContext Sort}
{context : List Sort}
{s : Sort}
(A B : Term env context s mc) \elim A, B
| A, B =>
rewrite-with-rule-colored
(HasColoredRoot color A)
(idx : rule-J {rules color} s)
(substitution : MetaSubstitution env context (rule-linear-mc idx) mc)
(left-coherence : MetaSubstitution.apply (weakening (convert-to-injected-term color (get-rule-pattern idx)) SubList.sublist-nil-free) SubList.identity substitution = A)
(right-coherence : MetaSubstitution.apply (weakening (inject-term envs (rule-right-linear idx)) SubList.sublist-nil-free) SubList.identity substitution = B)
| func f-A arguments-A, func f-B arguments-B =>
rewrite-with-parameter-f-colored
(p : f-A = f-B)
(f-A.1 = color)
(i : Index (domain f-A))
(tlcr : TopLevelColoredReduction color (arguments-A i) (arguments-over-f p arguments-B i))
(eq : \Pi (j : Index (domain f-A)) (j = i -> Empty) -> arguments-A j = arguments-over-f p arguments-B j)
\where {
\lemma extract-root-coloring {tc : TheoremContext} {color : Color} {mc : MetaContext Sort'} {context : List Sort} {s : Sort} {A B : Term env context s mc} (tlcr : TopLevelColoredReduction color A B) : HasColoredRoot color A
\elim A, B, tlcr
| A, B, rewrite-with-rule-colored h _ _ _ _ => h
| func f-A arguments-A, func f-B arguments-B, rewrite-with-parameter-f-colored p p1 i tlcr eq => func-root p1
}
\data OppositeColored {tc : TheoremContext} (maybe : Maybe Color) (negated : Color) : \Prop \elim maybe
| nothing => colored-nothing
| just color => colored-opposite (color /= negated)
\data BorderedParallelReduction
{tc : TheoremContext}
(global-color : Color)
(color : Maybe Color)
{context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
(A B : Term env context s mc) \elim A
| A => equal-trees (A = B)
| func f arguments =>
parallelization-f
(mediator : \Pi (index : Index (domain f)) ->
Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(\Pi (i : env.index-in f) -> \Sigma
(someColor : Maybe Color)
(OppositeColored someColor f.1)
(BorderedParallelReduction global-color someColor (arguments i) (mediator i)))
(SwitchingReduction global-color color (func f mediator) B)
\where {
\func append-tlcr
{tc : TheoremContext}
{global-color : Color}
{color : Maybe Color}
{context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
(A B : Term env context s mc)
(bpr : BorderedParallelReduction global-color color A B)
(C : Term env context s mc)
(B~>*C : Closure (TopLevelColoredReduction global-color) B C)
: \Sigma (someColor : Maybe Color) (BorderedParallelReduction global-color someColor A C) \elim color, A, bpr
| color, A, equal-trees idp => \case Closure.extract B~>*C \with {
| inl eq => rewrite eq (nothing, equal-trees idp)
| inr (inter, rd) => \case \elim B, \elim B~>*C, TopLevelColoredReduction.extract-root-coloring rd \with {
| func _ arguments, B~>*C, func-root _ => (just global-color, parallelization-f arguments (\lam i => (nothing, colored-nothing, equal-trees idp)) (cr-rewrite B~>*C idp))
}
}
| nothing, func f arguments, parallelization-f mediator _x (cr-skip idp) => (just global-color, parallelization-f mediator _x (cr-rewrite B~>*C idp))
| just a, func f arguments, parallelization-f mediator _x (cr-rewrite t p) => (just global-color, parallelization-f mediator _x (cr-rewrite (Closure.compose (rewrite p t) B~>*C) idp))
}
\data SwitchingReduction
{tc : TheoremContext}
{context : List Sort'}
{s : Sort'}
{mc : MetaContext Sort'}
(global-color : Color)
(color : Maybe Color) (A B : Term env context s mc) \elim color
| nothing => cr-skip (A = B)
| just color => cr-rewrite (Closure (TopLevelColoredReduction color) A B) (global-color = color)
\func TrichromaticParallelReduction
{tc : TheoremContext} {mc : MetaContext Sort'} {context : List Sort'} {s : Sort'}
(A B : Term env context s mc) : \Type =>
\Sigma (global-color : Color) (color : Maybe Color) (BorderedParallelReduction global-color color A B)
\func ConfluentialSystem (env : FSignature) (rules : RuleRegistry env) : \Type =>
\Pi {mc : MetaContext Sort} {context : List Sort} {s : Sort}
(A B C : Term env context s mc)
(Closure (RewriteRelation rules) A B)
(Closure (RewriteRelation rules) A C) -> StraightJoin B C (Closure (\lam x y => \Sigma (rd : RewriteRelation rules x y) (FunctionalWitness rd)))
\data FunctionalWitness {env : FSignature} {rules : RuleRegistry env} {context : List Sort} {s : Sort} {mc : MetaContext Sort} {t u : Term env context s mc} (rd : RewriteRelation rules t u) \elim t, u, rd
| A, B, rewrite-with-rule _ _ _ _ => rule-rewriting
| func f-A arguments-A, func f-B arguments-B, rewrite-with-parameter-f _ _ rd _ => param-rewriting (FunctionalWitness rd)
-- | Main function for joining two BorderedParallelReductions. Performs high-level dissection of incoming types.
\func bpr-confluence
{tc : TheoremContext} {gc1 gc2 : Color} (color1 color2 : Maybe Color) {context : List Sort'} {s : Sort'}
{A B C : PureTerm env context s}
(A~>B : BorderedParallelReduction gc1 color1 A B)
(A~>C : BorderedParallelReduction gc2 color2 A C)
(confluence : \Pi (c : Color) -> ConfluentialSystem (envs c) (rules c))
: \Sigma (D : PureTerm env context s)
(color3 : Maybe Color)
(color4 : Maybe Color)
(BorderedParallelReduction gc2 color3 B D)
(BorderedParallelReduction gc1 color4 C D) \elim color1, color2, A, B, C, A~>B, A~>C
| color1, color2, A, B, C, equal-trees p, rd => (C, color2, color1, rewriteI p rd, equal-trees idp)
| color1, color2, A, B, C, rd, equal-trees p => (B, color2, color1, equal-trees idp, rewriteI p rd)
| nothing, nothing, func f arguments, B, C, parallelization-f mediator arguments->med (cr-skip famed=B), parallelization-f mediator' arguments->med' (cr-skip famed'=C)
=>
\let | inner-confluences i => bpr-confluence (arguments->med i).1 (arguments->med' i).1 (arguments->med i).3 (arguments->med' i).3 confluence
| D => func f (\lam i => (inner-confluences i).1)
| (color-1, mediator-1, inrd-1, cwr-1) => collect-reductions-together-raw f mediator (\lam i => (inner-confluences i).1) (\lam i => ((inner-confluences i).2, (inner-confluences i).4))
| (color-2, mediator-2, inrd-2, cwr-2) => collect-reductions-together-raw f mediator' (\lam i => (inner-confluences i).1) (\lam i => ((inner-confluences i).3, (inner-confluences i).5))
\in (func f (\lam i => (inner-confluences i).1),
color-1,
color-2,
rewriteI famed=B (parallelization-f mediator-1 inrd-1 cwr-1),
rewriteI famed'=C (parallelization-f mediator-2 inrd-2 cwr-2))
| nothing, just right-color, func f arguments, B, C, parallelization-f mediator arguments=>med (cr-skip p), parallelization-f mediator' arguments=>med' (cr-rewrite med'~>C gc2=right-color) =>
\let | joined-mediators i => bpr-confluence (arguments=>med i).1 (arguments=>med' i).1 (arguments=>med i).3 (arguments=>med' i).3 confluence
| first-level-reduct => func f (\lam i => (joined-mediators i).1)
| (color-1, mediator-1, inrd-1, cwr-1) => collect-reductions-together-raw f mediator (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).2, (joined-mediators i).4))
| (color-2, mediator-2, inrd-2, cwr-2) => collect-reductions-together-raw f mediator' (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).3, (joined-mediators i).5))
| rd : BorderedParallelReduction gc2 color-1 (func f mediator) (func f (\lam i => (joined-mediators i).1)) => parallelization-f mediator-1 inrd-1 cwr-1
| (rightmost-reduct, flr~>rr, mcl, C=>rr) => unify-top right-color gc1 f mediator' mediator-2 C med'~>C inrd-2
| (X, c1, B=>X, c2, C=>X) => unwrap-cwr (func f mediator) C (func f mediator-2) first-level-reduct rightmost-reduct cwr-2 (rewrite gc2=right-color flr~>rr) rd C=>rr confluence
\in (X,
c1,
c2,
rewriteI p B=>X,
C=>X)
| just left-color, nothing, func f arguments, B, C, parallelization-f mediator arguments=>med (cr-rewrite med~>B gc1=left-color), parallelization-f mediator' arguments=>med' (cr-skip p) =>
\let | joined-mediators i => bpr-confluence (arguments=>med i).1 (arguments=>med' i).1 (arguments=>med i).3 (arguments=>med' i).3 confluence
| first-level-reduct => func f (\lam i => (joined-mediators i).1)
| (color-1, mediator-1, inrd-1, cwr-1) => collect-reductions-together-raw f mediator (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).2, (joined-mediators i).4))
| (color-2, mediator-2, inrd-2, cwr-2) => collect-reductions-together-raw f mediator' (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).3, (joined-mediators i).5))
| (leftmost-reduct, flr~>lr, mcl, B=>lr) => unify-top left-color gc2 f mediator mediator-1 B med~>B inrd-1
| rd : BorderedParallelReduction gc1 color-2 (func f mediator') (func f (\lam i => (joined-mediators i).1)) => parallelization-f mediator-2 inrd-2 cwr-2
| (X, c1, C=>X, c2, B=>X) => unwrap-cwr (func f mediator') B (func f mediator-1) first-level-reduct leftmost-reduct cwr-1 (rewrite gc1=left-color flr~>lr) rd B=>lr confluence
\in (X,
c2,
c1,
B=>X,
rewriteI p C=>X)
| just left-color, just right-color, func f arguments, B, C, parallelization-f mediator arguments=>med (cr-rewrite med~>B gc1=left-color), parallelization-f mediator' arguments=>med' (cr-rewrite med'~>C gc2=right-color)
=> \case Closure.extract med~>B, Closure.extract med'~>C \with {
| inl a, _ => rewriteI a (
\let | joined-mediators i => bpr-confluence (arguments=>med i).1 (arguments=>med' i).1 (arguments=>med i).3 (arguments=>med' i).3 confluence
| first-level-reduct => func f (\lam i => (joined-mediators i).1)
| (color-1, mediator-1, inrd-1, cwr-1) => collect-reductions-together-raw f mediator (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).2, (joined-mediators i).4))
| (color-2, mediator-2, inrd-2, cwr-2) => collect-reductions-together-raw f mediator' (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).3, (joined-mediators i).5))
| rd : BorderedParallelReduction gc2 color-1 (func f mediator) (func f (\lam i => (joined-mediators i).1)) => parallelization-f mediator-1 inrd-1 cwr-1
| (rightmost-reduct, flr~>rr, mcl, C=>rr) => unify-top right-color gc1 f mediator' mediator-2 C med'~>C inrd-2
| (X, c1, B=>X, c2, C=>X) => unwrap-cwr (func f mediator) C (func f mediator-2) first-level-reduct rightmost-reduct cwr-2 (rewrite gc2=right-color flr~>rr) rd C=>rr confluence
\in (X,
c1,
c2,
B=>X,
C=>X))
| _, inl a => rewriteI a (
\let | joined-mediators i => bpr-confluence (arguments=>med i).1 (arguments=>med' i).1 (arguments=>med i).3 (arguments=>med' i).3 confluence
| first-level-reduct => func f (\lam i => (joined-mediators i).1)
| (color-1, mediator-1, inrd-1, cwr-1) => collect-reductions-together-raw f mediator (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).2, (joined-mediators i).4))
| (color-2, mediator-2, inrd-2, cwr-2) => collect-reductions-together-raw f mediator' (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).3, (joined-mediators i).5))
| (leftmost-reduct, flr~>lr, mcl, B=>lr) => unify-top left-color gc2 f mediator mediator-1 B med~>B inrd-1
| rd : BorderedParallelReduction gc1 color-2 (func f mediator') (func f (\lam i => (joined-mediators i).1)) => parallelization-f mediator-2 inrd-2 cwr-2
| (X, c1, C=>X, c2, B=>X) => unwrap-cwr (func f mediator') B (func f mediator-1) first-level-reduct leftmost-reduct cwr-1 (rewrite gc1=left-color flr~>lr) rd B=>lr confluence
\in (X,
c2,
c1,
B=>X,
C=>X))
| inr (_, rd ), inr (_, rd') =>
\let
| hcl-f-left : HasColoredRoot left-color (func f mediator) => TopLevelColoredReduction.extract-root-coloring rd
| hcl-f-right : HasColoredRoot right-color (func f mediator') => TopLevelColoredReduction.extract-root-coloring rd'
| lcolor=rcolor : left-color = right-color => HasColoredRoot.equalize-colors left-color right-color f mediator mediator' hcl-f-left hcl-f-right
| joined-mediators i => bpr-confluence (arguments=>med i).1 (arguments=>med' i).1 (arguments=>med i).3 (arguments=>med' i).3 confluence
| first-level-reduct => func f (\lam i => (joined-mediators i).1)
| (color-1, mediator-1, inrd-1, cwr-1) => collect-reductions-together-raw f mediator (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).2, (joined-mediators i).4))
| (color-2, mediator-2, inrd-2, cwr-2) => collect-reductions-together-raw f mediator' (\lam i => (joined-mediators i).1) (\lam i => ((joined-mediators i).3, (joined-mediators i).5))
| rd : BorderedParallelReduction gc2 color-1 (func f mediator) (func f (\lam i => (joined-mediators i).1)) => parallelization-f mediator-1 inrd-1 cwr-1
| rd' : BorderedParallelReduction gc1 color-2 (func f mediator') (func f (\lam i => (joined-mediators i).1)) => parallelization-f mediator-2 inrd-2 cwr-2
| (leftmost-reduct, flr~>lr, clr-b, B=>lr) => unify-top left-color left-color f mediator mediator-1 B med~>B (rewrite (lcolor=rcolor *> inv gc2=right-color) inrd-1)
| (rightmost-reduct, flr~>rr, clr-c, C=>rr) => unify-top right-color right-color f mediator' mediator-2 C med'~>C (rewrite (inv lcolor=rcolor *> inv gc1=left-color) inrd-2)
| (X, c1, B=>X, c2, C=>X) => unwrap-double-cwr B C (func f mediator-1) (func f mediator-2) first-level-reduct leftmost-reduct rightmost-reduct (rewrite (inv gc2=right-color) cwr-1) (rewrite (inv lcolor=rcolor *> inv gc1=left-color) cwr-2) (rewriteI lcolor=rcolor flr~>lr) flr~>rr (rewriteI lcolor=rcolor B=>lr) C=>rr confluence
\in (X, c1, c2, rewrite gc2=right-color B=>X, rewrite (gc1=left-color *> lcolor=rcolor) C=>X)
}
\where {
\func unwrap-cwr
{tc : TheoremContext} {gc1 gc2 : Color} {color3 color4 : Maybe Color} {context : List Sort'} {s : Sort'}
(T1 T2 A B C : PureTerm env context s) {color-2 : Maybe Color}
(cwr : SwitchingReduction gc1 color-2 A B)
(A~>*C : Closure (TopLevelColoredReduction gc2) A C)
(T1=>B : BorderedParallelReduction gc2 color3 T1 B)
(T2=>C : BorderedParallelReduction gc1 color4 T2 C)
(confluence : \Pi (c : Color) -> ConfluentialSystem (envs c) (rules c))
:
\Sigma (X : PureTerm env context s) (c1 : Maybe Color) (BorderedParallelReduction gc2 c1 T1 X) (c2 : Maybe Color) (BorderedParallelReduction gc1 c2 T2 X)
\elim color-2, cwr
| nothing, cr-skip p => \let (cl-1, t1=>X) => BorderedParallelReduction.append-tlcr T1 B T1=>B C (rewriteI p A~>*C) \in (C, cl-1, t1=>X, color4, T2=>C)
| just color, cr-rewrite A~>*B p =>
\let | (X, B~>*X, C~>*X) => join-multicolor-tlcrs color gc2 A~>*B A~>*C confluence
| (cl-1, t1=>X) => BorderedParallelReduction.append-tlcr T1 B T1=>B X B~>*X
| (cl-2, t2=>X) => BorderedParallelReduction.append-tlcr T2 C T2=>C X (rewrite p C~>*X)
\in (X, cl-1, t1=>X, cl-2, t2=>X)
\func unwrap-double-cwr
{tc : TheoremContext} {gc1 : Color} {color3 color4 : Maybe Color} {context : List Sort'} {s : Sort'}
(T1 T2 A A' E B C : PureTerm env context s) {color-2 color-1 : Maybe Color}
(cwr-1 : SwitchingReduction gc1 color-2 A E)
(cwr-2 : SwitchingReduction gc1 color-1 A' E)
(A~>*B : Closure (TopLevelColoredReduction gc1) A B)
(A'~>*C : Closure (TopLevelColoredReduction gc1) A' C)
(T1=>B : BorderedParallelReduction gc1 color3 T1 B)
(T2=>C : BorderedParallelReduction gc1 color4 T2 C)
(confluence : \Pi (c : Color) -> ConfluentialSystem (envs c) (rules c))
: \Sigma (X : PureTerm env context s) (c1 : Maybe Color) (BorderedParallelReduction gc1 c1 T1 X) (c2 : Maybe Color) (BorderedParallelReduction gc1 c2 T2 X)
\elim color-2, color-1, cwr-1, cwr-2
| nothing, nothing, cr-skip p, cr-skip p1 =>
\let | (X, B~>*X, C~>*X) => join-multicolor-tlcrs gc1 gc1 A~>*B (rewrite {1} (p *> inv p1) A'~>*C) confluence
| (c1, T1=>X) => BorderedParallelReduction.append-tlcr _ _ T1=>B X B~>*X
| (c2, T2=>X) => BorderedParallelReduction.append-tlcr _ _ T2=>C X C~>*X
\in (X, c1, T1=>X, c2, T2=>X)
| nothing, just color, cr-skip p, cr-rewrite A'~>*E p1 =>
\let | (X, B~>*X, C~>*X) => join-multicolor-tlcrs gc1 gc1 (Closure.compose (transport (\lam cl => Closure (TopLevelColoredReduction cl) A' E) (inv p1) A'~>*E) (rewrite {1} (inv p) A~>*B)) A'~>*C confluence
| (c1, T1=>X) => BorderedParallelReduction.append-tlcr _ _ T1=>B X B~>*X
| (c2, T2=>X) => BorderedParallelReduction.append-tlcr _ _ T2=>C X C~>*X
\in (X, c1, T1=>X, c2, T2=>X)
| just color, nothing, cr-rewrite A~>*E p, cr-skip p1 =>
\let | (X, B~>*X, C~>*X) => join-multicolor-tlcrs gc1 gc1 A~>*B (Closure.compose (transport (\lam cl => Closure (TopLevelColoredReduction cl) A E) (inv p) A~>*E) (rewrite {1} (inv p1) A'~>*C)) confluence
| (c1, T1=>X) => BorderedParallelReduction.append-tlcr _ _ T1=>B X B~>*X
| (c2, T2=>X) => BorderedParallelReduction.append-tlcr _ _ T2=>C X C~>*X
\in (X, c1, T1=>X, c2, T2=>X)
| just color, just color1, cr-rewrite A~>*E p, cr-rewrite A'~>*E p1 =>
\let | (M1, B~>*M1, E~>*M1) => join-multicolor-tlcrs gc1 gc1 A~>*B (rewrite p A~>*E) confluence
| (M2, E~>*M2, C~>*M2) => join-multicolor-tlcrs gc1 gc1 (transport (\lam cl => Closure (TopLevelColoredReduction cl) A' E) (inv p1) A'~>*E) A'~>*C confluence
| (X, M1~>*X, M2~>*X) => join-multicolor-tlcrs gc1 gc1 E~>*M1 E~>*M2 confluence
| (c1, T1=>X) => BorderedParallelReduction.append-tlcr _ _ T1=>B X (Closure.compose B~>*M1 M1~>*X)
| (c2, T2=>X) => BorderedParallelReduction.append-tlcr _ _ T2=>C X (Closure.compose C~>*M2 M2~>*X)
\in (X, c1, T1=>X, c2, T2=>X)
\func join-multicolor-tlcrs
{tc : TheoremContext} (color1 color2 : Color) {context : List Sort'} {s : Sort'}
{A B C : PureTerm env context s}
(A~>B : Closure (TopLevelColoredReduction color1) A B)
(A~>C : Closure (TopLevelColoredReduction color2) A C)
(confluence : \Pi (c : Color) -> ConfluentialSystem (envs c) (rules c))
: \Sigma (X : PureTerm env context s) (Closure (TopLevelColoredReduction color2) B X) (Closure (TopLevelColoredReduction color1) C X) =>
\case \elim color2, decideEq color1 color2, \elim A~>C \with {
| _, yes idp, A~>C => join-tlcrs color1 A B C A~>B A~>C (confluence color1)
| color2, no n, A~>C => \case Closure.extract A~>B, Closure.extract A~>C \with {
| inl a, _ => rewriteI a (C, A~>C, c-trivial idp)
| _, inl a => rewriteI a (B, c-trivial idp, A~>B)
| inr (_, rd), inr (_, rd2) =>
\let | a : HasColoredRoot color1 A => TopLevelColoredReduction.extract-root-coloring rd
| b : HasColoredRoot color2 A => TopLevelColoredReduction.extract-root-coloring rd2
\in \case \elim A, \elim a, \elim b \with {
| func f arguments, func-root p, func-root q => absurd (n (inv p *> q))
}
}
}
}
-- | Unifies delayed parallel reduction and top-level single-color reduction.
\func unify-top
{tc : TheoremContext} {context : List Sort'} {s : Sort'} (color color' : Color)
(f : symbol s)
(arguments-A arguments-C : \Pi (index : Index (domain f)) -> PureTerm env (context ++ f env.!!domain index) (f env.!!sort index))
(B : PureTerm env context s)
(A~>B : Closure (TopLevelColoredReduction color) (func f arguments-A) B)
(inner-reductions : \Pi (i : env.index-in f) ->
\Sigma (someColor : Maybe Color)
(OppositeColored someColor f.1)
(BorderedParallelReduction color' someColor (arguments-A i) (arguments-over-f idp arguments-C i)))
: \Sigma (X : PureTerm env context s)
(Closure (TopLevelColoredReduction color) (func f arguments-C) X)
(mcolor : Maybe Color)
(BorderedParallelReduction color' mcolor B X) =>
\let
| (t, rho, t[rho]=A, root-colors) => decompose-term color (func f arguments-A)
| (u, lu[rho]=B, t~>*u) => iterate-decomposition (Linear.convert-to-term {envs color} t) rho B (rewrite unwrap-injection t[rho]=A) A~>B root-colors
| injected-u : Term env context s (LinearMetaContext {envs color} t) => inject-term envs u
| (sigma, C=t[sigma], reds) => alternate-subst {_} color color' (func f arguments-C) t rho root-colors nothing colored-nothing (rewriteI (inv t[rho]=A) (parallelization-f arguments-C inner-reductions (cr-skip idp)))
| uni-right => Closure.lift {_} {_}
{\lam x y => \Sigma (rrd : monochrome-reduction color x y) (FunctionalWitness {envs color} {rules color} rrd)}
{TopLevelColoredReduction color}
(\lam trm => MetaSubstitution.apply (inject-term envs trm) SubList.sublist-nil-free sigma)
(\lam tlcr => lift-relation color sigma tlcr.1 tlcr.2)
(Linear.convert-to-term {envs color} t)
u
t~>*u
| (mcl, uni-left) =>
unify-left color' color injected-u SubList.sublist-nil-free rho sigma reds
\in (MetaSubstitution.apply injected-u SubList.sublist-nil-free sigma,
rewrite C=t[sigma] (rewriteI unwrap-injection uni-right),
mcl,
rewriteI lu[rho]=B uni-left)
-- | Converts a sequence of TopLevelColoredReductions to another sequence of regular RewriteRelations
\func iterate-decomposition
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {inner-mc mc : MetaContext Sort'}
{color : Color}
(t : Term (envs color) context s inner-mc)
(rho : MetaSubstitution env nil inner-mc mc)
{A : Term env context s mc}
(B : Term env context s mc)
(teq : MetaSubstitution.apply (inject-term envs t) SubList.sublist-nil-free rho = A)
(A~>*B : Closure (TopLevelColoredReduction color) A B)
(root-colors : \Pi {s : Sort'} (m : inner-mc.metaname s) -> HasExcludedColoredRoot color (rho m))
: \Sigma
(u : Term (envs color) context s inner-mc)
(MetaSubstitution.apply (inject-term envs u) SubList.sublist-nil-free rho = B)
(Closure (\lam x y => \Sigma (rd : monochrome-reduction color x y) (FunctionalWitness {envs color} {rules color} rd)) t u)
\elim A~>*B
| c-basic A~>B =>
\let | (u, lu[rho]=B, t~>u, fw) => decompose-along-reduction color t B rho root-colors (rewrite teq A~>B)
\in (u, lu[rho]=B, c-basic (t~>u, fw))
| c-connect C A->C C~>*B =>
\let | (c, meq, rd, fw) => decompose-along-reduction color t C rho root-colors (rewrite teq A->C)
| (u, mu, tcl) => iterate-decomposition c rho B meq C~>*B root-colors \in (u, mu, c-connect c (rd, fw) tcl)
| c-trivial idp => (t, teq, c-trivial idp)
-- | Given rho[t] => C, generates sigma, s.t. sigma[t] = C and forall m, rho(m) => sigma(m)
\func alternate-subst
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
(gc rcolor : Color)
(C : Term env context s mc)
(t : LinearTerm (envs gc) context s)
(rho : MetaSubstitution env nil (LinearMetaContext {envs gc} t) mc)
(root-colors : \Pi {s1 : Sort'} -> \Pi (m : metaname {LinearMetaContext {envs gc} t} s1) -> HasExcludedColoredRoot gc (rho m))
(someColor : Maybe Color)
(some-color-diff : OppositeColored someColor gc)
(A=>C : BorderedParallelReduction rcolor someColor (MetaSubstitution.apply (convert-to-injected-term gc {context} {s} t) SubList.sublist-nil-free rho) C)
: \Sigma (sigma : MetaSubstitution env nil (LinearMetaContext {envs gc} t) mc)
(C = MetaSubstitution.apply (convert-to-injected-term gc {context} {s} t) SubList.sublist-nil-free sigma)
(rho~>sigma : \Pi {s : Sort'} (m : metaname {LinearMetaContext {envs gc} t} s) ->
\Sigma (mcolor : Maybe Color) (BorderedParallelReduction rcolor mcolor (rho m) (sigma m)))
\elim t, someColor, A=>C
| l-func f arguments, nothing, parallelization-f mediator inner-reductions (cr-skip p) =>
\let
| inductive-result i => alternate-subst gc rcolor
(mediator i) (arguments i)
(\lam m => rho (i, m))
(\lam {s1} m => root-colors (i, m))
(inner-reductions i).1
(inner-reductions i).2
(rewrite (modular-commutation (\lam j => LinearMetaContext {envs gc} (arguments j)) i SubList.sublist-nil-free (convert-to-injected-term gc (arguments i)) rho)
(rewrite (invariant-through-empty-subst rho SubList.sublist-nil-free (SubList.extend-right-single SubList.sublist-nil-free) (ModularMetaContext.upgrade-metavariables
(\lam j => LinearMetaContext {envs gc} (arguments j)) (convert-to-injected-term gc (arguments i)))) (inner-reductions i).3))
\in (\lam {s1} mvar => (inductive-result mvar.1).1 mvar.2,
inv p *> Term.fext
(\lam index => rewriteI
(modular-commutation (\lam j => LinearMetaContext {envs gc} (arguments j)) index (SubList.extend-right-single SubList.sublist-nil-free) (convert-to-injected-term gc (arguments index)) (\lam {s1} mvar => (inductive-result mvar.1).1 mvar.2))
(rewrite invariant-through-empty-subst (inductive-result index).2)),
\lam {s1} m => (inductive-result m.1).3 m.2)
| l-func f arguments, just color, parallelization-f mediator inner-reductions (cr-rewrite tlcr p) => \case Closure.extract tlcr \with {
| inl a =>
\let | induc index => alternate-subst gc rcolor (mediator index) (arguments index) (\lam m => rho (index, m)) (\lam {s1} m => root-colors (index, m)) (inner-reductions index).1 (inner-reductions index).2 (rewrite modular-commutation (rewrite trivial-sublist-contractible (inner-reductions index).3))
\in (\lam mvar => (induc mvar.1).1 mvar.2,
inv a *> Term.fext
(\lam index => rewriteI
(modular-commutation (\lam j => LinearMetaContext {envs gc} (arguments j)) index (SubList.extend-right-single SubList.sublist-nil-free) (convert-to-injected-term gc (arguments index)) (\lam {s1} mvar => (induc mvar.1).1 mvar.2))
(rewrite invariant-through-empty-subst (induc index).2)),
\lam {s1} m => (induc m.1).3 m.2)
| inr (_, rd) => \case \elim some-color-diff \with {
| colored-opposite gc/=color => absurd (gc/=color (inv (HasColoredRoot.reorganize color (TopLevelColoredReduction.extract-root-coloring rd))))
}
}
| l-func f arguments, someColor, equal-trees p => (rho, inv p, \lam {s1} m => (nothing, equal-trees idp))
| l-full-metavar, someColor, rd =>
(\lam {s1} mvar => transport (Term env context __ mc) (inv mvar) C,
inv (plain-identity-effect C),
\lam {s1} m => (someColor, unify-reduction rho C rd m))
| lt-var index p, someColor, equal-trees p1 => (\lam {s1} mvar => contradiction, inv p1, \lam {s1} m => contradiction)
\where {
\func unify-reduction {tc : TheoremContext} {gc : Color} {someColor : Maybe Color} {context : List Sort'} {s s' : Sort'} {mc : MetaContext Sort'}
(rho : MetaSubstitution env nil (SingularMetaContext s context) mc)
(C : Term env context s mc)
(bpr : BorderedParallelReduction gc someColor (Substitution.apply
(rho idp) (extend-substitution-left SubList.sublist-nil-free (\lam i => var i idp))) C)
(m : s' = s)
: BorderedParallelReduction gc someColor (rho m)
(transport (\lam (srt : Sort') => Term env context srt mc) (inv m) C) \elim m
| idp => rewriteI plain-identity-effect bpr
}
-- | Given forall m, rho(m) => sigma(m), generates s[rho] => s[sigma]
\func unify-left
{tc : TheoremContext} {context context' : List Sort'} {sort : Sort'} {inner-mc : MetaContext Sort'}
(gc anti-color : Color)
(s : Term env context' sort inner-mc)
(sublist : SubList context context')
(rho sigma : MetaSubstitution env context inner-mc EmptyMetaContext)
(rho~>sigma : \Pi {s : Sort'} (m : inner-mc.metaname s) ->
\Sigma (mcolor : Maybe Color) (BorderedParallelReduction gc mcolor (rho m) (sigma m)))
: \Sigma (mcolor : Maybe Color)
(BorderedParallelReduction gc mcolor (MetaSubstitution.apply s sublist rho) (MetaSubstitution.apply s sublist sigma))
\elim s
| var index p => (nothing, equal-trees idp)
| metavar m arguments =>
\let | main-reduction => rho~>sigma m
| rho-subst => extend-substitution-left sublist (\lam i => MetaSubstitution.apply (arguments i) sublist rho)
| sigma-subst => extend-substitution-left sublist (\lam i => MetaSubstitution.apply (arguments i) sublist sigma)
| inductive i => unify-left gc anti-color (arguments i) sublist rho sigma rho~>sigma
| target-reduction => reduction-over-substitution main-reduction.1 (rho m) (sigma m) main-reduction.2 rho-subst sigma-subst (\lam i => extend-substitutuion-left-for-parallel (\lam i => MetaSubstitution.apply (arguments i) sublist rho) (\lam i => MetaSubstitution.apply (arguments i) sublist sigma) inductive sublist i)
\in target-reduction
| func f arguments =>
\let | in-indices i => unify-left gc f.1 (arguments i) (SubList.extend-right-single sublist) rho sigma rho~>sigma
| (someColor, med, inrd, cwr) => collect-reductions-together-raw f
(\lam i => MetaSubstitution.apply (arguments i) (SubList.extend-right-single sublist) rho)
(\lam i => MetaSubstitution.apply (arguments i) (SubList.extend-right-single sublist) sigma)
in-indices
\in (someColor, parallelization-f med inrd cwr)
\where {
\func extend-substitutuion-left-for-parallel
{tc : TheoremContext} {left-context right-context some-context : List Sort'}
{gc : Color}
(subst subst' : Substitution right-context some-context EmptyMetaContext)
(rd' : \Pi (i : Index right-context) ->
\Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (subst i) (subst' i)))
(sublist : SubList left-context some-context)
(index : Index (left-context ++ right-context))
: \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (extend-substitution-left sublist subst index) (extend-substitution-left sublist subst' index)) =>
partial-fin-induction
(\lam ind => \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (extend-substitution-left sublist subst ind) (extend-substitution-left sublist subst' ind)))
(\lam i => rewrite extend-substitution-left.on-begin (nothing, equal-trees (rewrite extend-substitution-left.on-begin idp)))
(\lam i => \let inner => rd' i \in rewrite extend-substitution-left.on-end (rewrite extend-substitution-left.on-end (inner.1, lemma inner.1 (inv (expand-fin-right.correct i)) inner.2)))
index
\where {
\func lemma {tc : TheoremContext} {context : List Sort'}
{gc : Color} {ms : MetaContext Sort'}
(someColor : Maybe Color)
{s s' : Sort'}
(p : s = s')
{A B : Term env context s ms}
(bpr : BorderedParallelReduction gc someColor A B)
: BorderedParallelReduction gc someColor (transport (Term env context __ ms) p A) (transport (Term env context __ ms) p B) \elim p
| idp => bpr
}
}
\func reduction-over-substitution {tc : TheoremContext} {context new-context : List Sort'} {s : Sort'}
{gc : Color}
(color : Maybe Color)
(A B : PureTerm env context s)
(A=>B : BorderedParallelReduction gc color A B)
(subst subst' : Substitution context new-context EmptyMetaContext)
(subst=>subst' : \Pi (i : Index context) -> \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (subst i) (subst' i)))
: \Sigma (mcolor : Maybe Color) (BorderedParallelReduction gc mcolor (Substitution.apply A subst) (Substitution.apply B subst')) \elim color, A, A=>B
| color, A, equal-trees p => rewrite p (distributed-reduction-for-substitution B color _ _ subst=>subst')
| nothing, func f arguments, parallelization-f mediator _x (cr-skip p) =>
\let | medium-reductions i => reduction-over-substitution (_x i).1 (arguments i) (mediator i) (_x i).3 (append-context-right subst) (append-context-right subst') (expand-reduction-right subst subst' subst=>subst')
| (sc, med, inrd, cwr) => collect-reductions-together-raw f (\lam i => Substitution.apply (arguments i) (append-context-right subst)) (\lam i => Substitution.apply (mediator i) (append-context-right subst')) medium-reductions
\in rewriteI p (sc, parallelization-f med inrd cwr)
| just a, func f arguments, parallelization-f mediator _x (cr-rewrite tlcr p) =>
\let | medium-reductions i => reduction-over-substitution (_x i).1 (arguments i) (mediator i) (_x i).3 (append-context-right subst) (append-context-right subst') (expand-reduction-right subst subst' subst=>subst')
| (some-color, med, inrd, cwr) => collect-reductions-together-tlcr (just gc) f (\lam i => Substitution.apply (arguments i) (append-context-right subst)) (\lam i => Substitution.apply (mediator i) (append-context-right subst')) medium-reductions (Substitution.apply B subst') (cr-rewrite (rewrite p (Closure.lift (\lam t => Substitution.apply t subst') (\lam rel => tlcr-over-substitution subst' rel) (func f mediator) B tlcr)) idp)
\in (some-color, parallelization-f med inrd cwr)
\func expand-reduction-right
{tc : TheoremContext} {context new-context additional-context : List Sort'}
{gc : Color}
(subst subst' : Substitution context new-context EmptyMetaContext)
(rd' : \Pi (i : Index context) ->
\Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (subst i) (subst' i)))
(index : Index (context ++ additional-context))
: \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (append-context-right subst index) (append-context-right subst' index)) \elim context, index
| nil, index => (nothing, equal-trees idp)
| :: a context, 0 => \let ind => rd' 0 \in (ind.1, bpr-over-weakening ind.1 (subst 0) (subst' 0) ind.2 (SubList.extend-right-single SubList.identity))
| :: a context, suc index => expand-reduction-right (\lam i => subst (suc i)) (\lam i => subst' (suc i)) (\lam i => rd' (suc i)) index
\func tlcr-over-substitution {tc : TheoremContext} {context new-context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{A B : Term env context s mc}
{color : Color}
(subst : Substitution context new-context mc)
(A~>B : TopLevelColoredReduction color A B)
: TopLevelColoredReduction color (Substitution.apply A subst) (Substitution.apply B subst) \elim A, B, A~>B
| A, B, rewrite-with-rule-colored h idx msubst msubst[l]=A msubst[r]=B =>
rewrite-with-rule-colored
(hcr-over-substitution subst h)
idx
(\lam m => Substitution.apply (msubst m) (append-context-right subst))
(rewrite (inv msubst[l]=A) ((rewrite (trivial-sublist-contractible _ _)) ((rewrite (trivial-sublist-contractible {_} {context})) (rewrite (identity-sublist-contractible {_} {new-context}) (rewrite (identity-sublist-contractible {_} {context}) (rewrite {2} (append-context-right.to-nil subst) (untransport _ ++_nil ++_nil (\lam {s1 : Sort'} (m : metaname {rule-linear-mc idx} s1) => Substitution.apply (msubst m) (append-context-right subst)) _ _ _ _ _ _ (commutation (convert-to-injected-term color (get-rule-pattern idx)) subst msubst))))))))
(rewrite (inv msubst[r]=B) ((rewrite (trivial-sublist-contractible _ _)) ((rewrite (trivial-sublist-contractible {_} {context})) (rewrite (identity-sublist-contractible {_} {new-context}) (rewrite (identity-sublist-contractible {_} {context}) (rewrite {2} (append-context-right.to-nil subst) (untransport _ ++_nil ++_nil (\lam {s1 : Sort'} (m : metaname {rule-linear-mc idx} s1) => Substitution.apply (msubst m) (append-context-right subst)) _ _ _ _ _ _ (commutation (inject-term envs (rule-right-linear idx)) subst msubst))))))))
| func f-A arguments-A, func f-B arguments-B, rewrite-with-parameter-f-colored idp p1 i tlcr eq => rewrite-with-parameter-f-colored idp p1 i (tlcr-over-substitution (append-context-right subst) tlcr) (\lam j _x => rewrite (eq j _x) idp)
\where {
\func untransport {env : FSignature} {context-a context-a' context-b context-b' context-meta context-meta2 : List Sort} {s : Sort} {mc mc' : MetaContext Sort}
(t : Term env nil s mc)
(eq : context-a = context-a')
(eq' : context-b = context-b')
(ms-a : MetaSubstitution env context-meta mc mc')
(sl1 : SubList nil context-a)
(sl2 : SubList context-meta context-a)
(sl3 : SubList nil context-b)
(sl4 : SubList context-meta2 context-b)
(ms-b : MetaSubstitution env context-meta2 mc mc')
(subst : Substitution context-b context-a mc')
(true-eq : MetaSubstitution.apply (weakening t sl1) sl2 ms-a = Substitution.apply (MetaSubstitution.apply (weakening t sl3) sl4 ms-b) subst):
MetaSubstitution.apply (weakening t
(transport (SubList nil) eq sl1))
(transport (SubList context-meta) eq sl2)
ms-a = Substitution.apply (MetaSubstitution.apply (weakening t
(transport (SubList nil) eq' sl3))
(transport (SubList context-meta2) eq' sl4) ms-b)
(transport2 (\lam (ctx : List Sort) (ctx' : List Sort) => Substitution ctx ctx' mc') eq' eq subst) \elim eq, eq'
| idp, idp => true-eq
\lemma commutation {env : FSignature} {s : Sort} {aux-context core-context new-context : List Sort} {old-ms new-ms : MetaContext Sort}
(term : Term env aux-context s old-ms)
(subst : Substitution core-context new-context new-ms)
(metasubst : MetaSubstitution env core-context old-ms new-ms)
:
MetaSubstitution.apply
(weakening term (SubList.extend-left-single SubList.identity))
(SubList.extend-right-single SubList.identity) (\lam {s} m => Substitution.apply (metasubst m) (append-context-right subst))
=
Substitution.apply (MetaSubstitution.apply
(weakening term (SubList.extend-left-single SubList.identity))
(SubList.extend-right-single SubList.identity {aux-context}) metasubst) (append-context-right subst) \elim term
| var index idp => inv (weakening.combine-with-append-left _ (var index idp))
| metavar m arguments => repeat {2} (rewrite subst-comm) (cong (ext (\lam i =>
\let inductive : (\lam j => MetaSubstitution.apply
(weakening (arguments j) (SubList.extend-left-single SubList.identity))
(SubList.extend-right-single SubList.identity) (\lam {s} m => Substitution.apply (metasubst m) (append-context-right subst)))
=
(\lam j => Substitution.apply (MetaSubstitution.apply
(weakening (arguments j) (SubList.extend-left-single SubList.identity))
(SubList.extend-right-single SubList.identity {aux-context}) metasubst) (append-context-right subst)) => ext (\lam j => commutation (arguments j) subst metasubst)
\in rewrite inductive (subst-comm-different subst _ i))))
| func f arguments => Term.fext (\lam index => \let inductive => commutation (arguments index) subst metasubst \in rewrite Transports.lb-ls-to-ls (rewrite Transports.rs-rs-to-rs (rewrite Transports.lb-ls-to-ls (rewrite Transports.rs-rs-to-rs (rewrite append-context-right.composition (inductive-step (arguments index) ++-assoc ++-assoc idp idp _ _ _ _ metasubst subst inductive))))))
\where {
\lemma subst-comm-different
{env : FSignature} {context-a context-b context-c context-d : List Sort} {mc : MetaContext Sort}
(subst : Substitution context-a context-b mc)
(subst2 : Substitution context-c (context-a ++ context-d) mc)
(index : Index (context-a ++ context-c))
: Substitution.apply (append-context-right subst index) (extend-substitution-left (SubList.extend-right-single SubList.identity) (\lam j => Substitution.apply (subst2 j) (append-context-right subst)))
= Substitution.apply (extend-substitution-left (SubList.extend-right-single SubList.identity) subst2 index) (append-context-right subst) =>
partial-fin-induction (\lam i => Substitution.apply (append-context-right subst i) (extend-substitution-left (SubList.extend-right-single SubList.identity) (\lam j => Substitution.apply (subst2 j) (append-context-right subst)))
= Substitution.apply (extend-substitution-left (SubList.extend-right-single SubList.identity) subst2 i) (append-context-right subst))
(\lam i => rewrite append-context-right.on-begin (rewrite extend-substitution-left.on-begin (rewrite weakening.combine-with-extend-right (inductive-step subst i _))))
(\lam i => rewrite append-context-right.on-end (rewrite extend-substitution-left.on-end (rewrite (weakening.combine-with-extend-left (\lam (j : Index context-c) => Substitution.apply (subst2 j) (append-context-right subst)) (var i (expand-fin-right.correct i))) (inductive-step-2 subst subst2 i (expand-fin-right.correct i)))))
index
\where {
\func inductive-step-2 {env : FSignature} {context-a context-b context-c context-d : List Sort} {s : Sort} {mc : MetaContext Sort}
(subst : Substitution context-a context-b mc)
(subst2 : Substitution context-c (context-a ++ context-d) mc)
(index : Index context-c)
(eq : s = context-c !! index) :
Substitution.apply
(var index eq)
(\lam (j : Index context-c) => Substitution.apply (subst2 j) (append-context-right subst)) =
Substitution.apply
(transport (\lam (p0 : Sort) => Term env (context-a ++ context-d) p0 mc) (inv eq) (subst2 index))
(append-context-right subst) \elim eq
| idp => idp
\func inductive-step
{env : FSignature} {context-a context-b context-c : List Sort} {s : Sort} {mc : MetaContext Sort}
(subst : Substitution context-a context-b mc)
(index : Index context-a)
(eq : s = context-a !! index)
: weakening (coe (\lam (i1 : I) => Term env context-b (inv eq @ i1) mc) (subst index) right)
(SubList.extend-right-single SubList.identity {context-c}) =
Substitution.apply
(var (shift-index (SubList.extend-right-single SubList.identity) index)
(Shifts.proof (SubList.extend-right-single SubList.identity) index eq))
(append-context-right subst) \elim eq
| idp => rewrite (weakening.combine-with-append-right subst (var index idp)) idp
}
\lemma inductive-step
{env : FSignature} {s : Sort} {big-context-al big-context-ar new-context term-context core-context rbig-context-al rbig-context-ar : List Sort} {old-ms new-ms : MetaContext Sort}
(term : Term env term-context s old-ms)
(eq : big-context-al = big-context-ar)
(eq' : rbig-context-al = rbig-context-ar)
(eq'' : core-context ++ term-context = rbig-context-ar)
(eq''' : new-context ++ term-context = big-context-ar)
(sl-term-ar : SubList term-context big-context-ar)
(sl-new-ar : SubList new-context big-context-ar)
(sl-term-rar : SubList term-context rbig-context-ar)
(sl-core-rar : SubList core-context rbig-context-ar)
(metasubst : MetaSubstitution env core-context old-ms new-ms)
(subst : Substitution core-context new-context new-ms)
(induction-statement : MetaSubstitution.apply
(weakening term sl-term-ar) sl-new-ar (\lam {s} m => Substitution.apply (metasubst m) (append-context-right subst)) =
Substitution.apply
(MetaSubstitution.apply (weakening term sl-term-rar) sl-core-rar metasubst) (transport2 (\lam ctx1 ctx2 => \Pi (i : Index ctx1) -> Term env ctx2 (ctx1 !! i) new-ms) eq'' eq''' (append-context-right subst)))
: MetaSubstitution.apply
(weakening term (transport (SubList term-context) (inv eq) sl-term-ar))
(transport (SubList new-context) (inv eq) sl-new-ar)
(\lam {s} m => Substitution.apply (metasubst m) (append-context-right subst))
=
Substitution.apply
(MetaSubstitution.apply
(weakening term (transport (SubList term-context) (inv eq') sl-term-rar))
(transport (SubList core-context) (inv eq') sl-core-rar) metasubst)
(transport2 (\lam ctx ctx' => \Pi (index : Index ctx) -> Term env ctx' (ctx !! index) new-ms)
(inv eq')
(inv eq)
(transport2 (\lam ctx1 ctx2 => \Pi (i : Index ctx1) -> Term env ctx2 (ctx1 !! i) new-ms) eq'' eq''' (append-context-right subst)))
\elim eq, eq', eq'', eq'''
| idp, idp, idp, idp => induction-statement
}
\lemma hcr-over-substitution {tc : TheoremContext} {context new-context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{color : Color}
{A : Term env context s mc}
(subst : Substitution context new-context mc)
(hcr : HasColoredRoot color A)
: HasColoredRoot color (Substitution.apply A subst) \elim A, hcr
| func _ arguments, func-root p => func-root p
}
\func bpr-over-weakening
{tc : TheoremContext} {context new-context : List Sort'} {s : Sort'}
{gc : Color}
(someColor : Maybe Color)
(A B : Term env context s EmptyMetaContext)
(bpr : BorderedParallelReduction gc someColor A B)
(sublist : SubList context new-context)
: BorderedParallelReduction gc someColor (weakening A sublist) (weakening B sublist) \elim someColor, A, bpr
| just a, func f arguments, parallelization-f mediator _x (cr-rewrite tlcr idp) =>
\let inductive i => bpr-over-weakening (_x i).1 (arguments i) (mediator i) (_x i).3 (SubList.extend-right-both sublist)
\in parallelization-f
(\lam i => weakening (mediator i) (SubList.extend-right-both sublist))
(\lam i => ((_x i).1, (_x i).2, inductive i))
(cr-rewrite (Closure.lift {Term env context s EmptyMetaContext} {Term env new-context s EmptyMetaContext} {TopLevelColoredReduction a} {TopLevelColoredReduction a} (weakening __ sublist) (\lam {X} {Y} tlcr => tlcr-over-weakening a X Y tlcr sublist) (func f mediator) B tlcr) idp)
| cl , A, equal-trees p1 => equal-trees (pmap (weakening __ sublist) p1)
| nothing, func f arguments, parallelization-f mediator _x (cr-skip idp) =>
\let inductive i => bpr-over-weakening (_x i).1 (arguments i) (mediator i) (_x i).3 (SubList.extend-right-both sublist)
\in parallelization-f (\lam index => weakening (mediator index) (SubList.extend-right-both sublist)) (\lam i => ((_x i).1, (_x i).2, inductive i)) (cr-skip idp)
\func tlcr-over-weakening
{tc : TheoremContext} {context new-context : List Sort'} {s : Sort'}
(color : Color)
(A B : Term env context s EmptyMetaContext)
(tlcr : TopLevelColoredReduction color A B)
(sublist : SubList context new-context)
: TopLevelColoredReduction color (weakening A sublist) (weakening B sublist) =>
\let | weakening-subst => weakening.substitution sublist
| substed-tlcr => tlcr-over-substitution weakening-subst tlcr
\in repeat {2} (rewrite weakening.substitution-eq) substed-tlcr
\func distributed-reduction-for-substitution {tc : TheoremContext} {context new-context : List Sort'} {s : Sort'}
(A : PureTerm env context s)
{gc : Color}
(color : Maybe Color)
(subst subst' : Substitution context new-context EmptyMetaContext)
(subst=>subst' : \Pi (i : Index context) -> \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (subst i) (subst' i)))
: \Sigma (color' : Maybe Color) (BorderedParallelReduction gc color' (Substitution.apply A subst) (Substitution.apply A subst')) \elim A
| var index p => \case \elim s, \elim p \with {
| s, idp => subst=>subst' index
}
| metavar m arguments => contradiction
| func f arguments =>
\let | inner-reductions i => distributed-reduction-for-substitution (arguments i) {gc} color (append-context-right subst) (append-context-right subst') (expand-reduction-right subst subst' subst=>subst')
| (sc, med, inrd, cwr) => collect-reductions-together-raw f
(\lam index => Substitution.apply (arguments index) (append-context-right subst))
(\lam index => Substitution.apply (arguments index) (append-context-right subst'))
inner-reductions \in (sc, parallelization-f med inrd cwr)
\func collect-reductions-together-tlcr
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{gc : Color}
(someColor : Maybe Color)
(f : symbol s)
(arguments-A arguments-B : \Pi (index : Index (domain f)) -> Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(tlcrs : \Pi (index : Index (domain f)) -> \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (arguments-A index) (arguments-B index)))
(C : Term env context s mc)
(B~>*C : SwitchingReduction gc someColor (func f arguments-B) C)
: \Sigma
(someColor : Maybe Color)
(mediator : \Pi (index : Index (domain f)) ->
Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(\Pi (i : env.index-in f) -> \Sigma
(someColor : Maybe Color)
(OppositeColored someColor f.1)
(BorderedParallelReduction gc someColor (arguments-A i) (mediator i)))
(SwitchingReduction gc someColor (func f mediator) C) =>
\let | common-reduction i => unfold-bpr f.1 (arguments-A i) (arguments-B i) (tlcrs i).2
| ind-last =>
modular-induction
(\lam curmed => \Sigma (someColor : Maybe Color) (SwitchingReduction gc someColor (func f curmed) C))
arguments-B
(\lam i => (common-reduction i).1)
(someColor, B~>*C)
(\lam delim prev-result =>
\let arg-rewrite => (common-reduction delim).7
\in propagate-rewriting f C arguments-B (\lam i => (common-reduction i).1) delim prev-result.1 prev-result.2 (common-reduction delim).5 (common-reduction delim).6 arg-rewrite
)
\in (ind-last.1, \lam index => (common-reduction index).1, \lam i => ((common-reduction i).2, (common-reduction i).4, (common-reduction i).3), ind-last.2)
\where {
\func propagate-rewriting
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{gc : Color}
(f : symbol s)
(C : Term env context s mc)
(arguments-B midterms : \Pi (index : Index (domain f)) -> Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(delim : Index (domain f))
(prev-rd-cl : Maybe Color)
(pred-rd-cwr : SwitchingReduction gc prev-rd-cl (func f (\new DArray { | at => modular-function arguments-B midterms delim })) C)
(point-rd-cl : Maybe Color)
(point-coherence : (point-rd-cl = nothing) `Or` (point-rd-cl = just f.1))
(point-rd-cwr : SwitchingReduction gc point-rd-cl (midterms delim) (arguments-B delim)) :
\Sigma (someColor : Maybe Color)
(SwitchingReduction gc someColor (func f (\new DArray { | at => modular-function arguments-B midterms (suc delim) })) C)
\elim prev-rd-cl, pred-rd-cwr, point-rd-cl, point-coherence, point-rd-cwr
| nothing, cr-skip p, nothing, point-coherence, cr-skip p1
=> (nothing, cr-skip (pmap (func f) (ext (inv (modular-function.modular-bridge arguments-B midterms delim (inv p1)))) *> p))
| nothing, cr-skip p, just color, inl (), _
| nothing, cr-skip idp, just color, inr b, cr-rewrite ind1~>ind' idp => (just gc, cr-rewrite (upgrade-iterated-reduction f (just-injective (inv b)) arguments-B midterms delim ind1~>ind') idp)
| just color, cr-rewrite tlcr p, nothing, point-coherence, cr-skip p1
=> (just color, cr-rewrite (rewrite (inv (modular-function.modular-bridge arguments-B midterms delim (inv p1))) tlcr) p)
| just color, cr-rewrite before~>C idpr, just color1, inl (), _
| just color, cr-rewrite before~>C idp, just color1, inr b, cr-rewrite ind1~>ind' idp =>
(just gc, cr-rewrite (Closure.compose (upgrade-iterated-reduction f (just-injective (inv b)) arguments-B midterms delim ind1~>ind') before~>C) idp)
\func upgrade-iterated-reduction
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{gc : Color}
(f : symbol s)
(eq : f.1 = gc)
(arguments-A arguments-B : \Pi (index : Index (domain f)) -> Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(index : Index (domain f))
(rd : Closure (TopLevelColoredReduction gc) (arguments-B index) (arguments-A index))
: Closure (TopLevelColoredReduction gc)
(func f (\new DArray { | at => modular-function arguments-A arguments-B (suc index) }))
(func f (modular-function arguments-A arguments-B index)) =>
\let | modular => modular-function arguments-A arguments-B index
| some' => insert-term f modular index (arguments-B index)
| mapped => Closure.lift {_} {_}
{TopLevelColoredReduction gc {mc} {context ++ f env.!!domain index} {f env.!!sort index}}
{TopLevelColoredReduction gc {mc} {context} {s}}
(insert-term f modular index)
(\lam rel => rewrite-with-parameter-f-colored idp eq index (rewrite pointed-function.at-index (rewrite pointed-function.at-index rel)) (\lam j j-not-index => rewrite (pointed-function.not-at-index modular index _ j j-not-index) (rewrite (pointed-function.not-at-index modular index _ j j-not-index) idp)))
(arguments-B index) (arguments-A index)
rd
\in rewrite (modular-to-pointed-forward arguments-A arguments-B) (rewrite {2} (modular-to-pointed arguments-A arguments-B) mapped)
\func insert-term {env : FSignature} {context : List Sort} {s : Sort} {ms : MetaContext Sort} (f : symbol s)
(arguments : \Pi (index : Index (domain f)) -> Term env (context ++ (f FSignature.!!domain index)) (f FSignature.!!sort index) ms)
(index : Index (domain f))
(point : Term env (context ++ (f FSignature.!!domain index)) (f FSignature.!!sort index) ms)
: Term env context s ms => func f (pointed-function arguments index point)
\func unfold-bpr
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{gc : Color} {someColor : Maybe Color} (required-color : Color)
(A B : Term env context s mc)
(bpr : BorderedParallelReduction gc someColor A B)
: \Sigma (midterm : Term env context s mc)
(new-color : Maybe Color)
(bpr : BorderedParallelReduction gc new-color A midterm)
(OppositeColored new-color required-color)
(nc' : Maybe Color)
((nc' = nothing) `Or` (nc' = just required-color))
(cwr : SwitchingReduction gc nc' midterm B)
\elim someColor, A, bpr
| _, A, equal-trees p => (A, nothing, equal-trees idp, colored-nothing, nothing, inl idp, cr-skip p)
| nothing, func f arguments, parallelization-f mediator _x c => (func f mediator, nothing, parallelization-f mediator _x (cr-skip idp), colored-nothing, nothing, inl idp, c)
| just _, func f arguments, parallelization-f mediator _x (cr-rewrite t idp) => \case decideEq gc required-color \with {
| yes e => (func f mediator, nothing, parallelization-f mediator _x (cr-skip idp), colored-nothing, just gc, inr (pmap just e), cr-rewrite t idp)
| no n => (B, just gc, parallelization-f mediator _x (cr-rewrite t idp), colored-opposite n, nothing, inl idp, cr-skip idp)
}
}
\func collect-reductions-together-raw
{tc : TheoremContext} {context : List Sort'} {s : Sort'} {mc : MetaContext Sort'}
{gc : Color}
(f : symbol s)
(arguments-A arguments-B : \Pi (index : Index (domain f)) -> Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(tlcrs : \Pi (index : Index (domain f)) -> \Sigma (someColor : Maybe Color) (BorderedParallelReduction gc someColor (arguments-A index) (arguments-B index)))
: \Sigma
(someColor : Maybe Color)
(mediator : \Pi (index : Index (domain f)) ->
Term env (context ++ f env.!!domain index) (f env.!!sort index) mc)
(\Pi (i : env.index-in f) -> \Sigma
(someColor : Maybe Color)
(OppositeColored someColor f.1)
(BorderedParallelReduction gc someColor (arguments-A i) (mediator i)))
(SwitchingReduction gc someColor (func f mediator) (func f arguments-B)) =>
collect-reductions-together-tlcr nothing f arguments-A arguments-B tlcrs (func f arguments-B) (cr-skip idp)