text:
module sn-calculus-compatconf.same where

open import sn-calculus-compatconf.base

open import sn-calculus
open import sn-calculus-confluence.helper
  using (ready-irr-on-irr-θʳ)
open import utility renaming (_U̬_ to _∪_)
open import context-properties
  using (get-view ; wrap-rho
       ; ->E-view ; ->pot-view ; wrap-rho-pot' ; unwrap-rho
       )

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
  using (Can ; Canₛ ; Canₛₕ ; Canₖ ; Canθ ; Canθₛ ; Canθₛₕ ; module CodeSet)
open import Esterel.Lang.CanFunction.Properties
  using (canθₛ-mergeʳ ; canθₛₕ-mergeʳ)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Context.Properties
  using (unplug ; unplugc ; plug ; plugc ; unplug-eq ; ⟦⟧c-to-⟦⟧e)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; trans ; subst ; subst₂ ; module ≡-Reasoning)
open import Data.Bool
  using (Bool ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _∷_ ; [] ; _++_ ; map)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming ( ++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ )
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function using (_∘_ ; id ; _∋_ ; _$_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ->E-view
open ->pot-view

open EvaluationContext1
open _≐_⟦_⟧e
open Context1
open _≐_⟦_⟧c

open ListSet Data.Nat._≟_

open ≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)

{-
Modified proof from the old E-lift C-any confluence lemma.
Basically this is arbitrary multi-wrap-rho given the correct binding
of p: from a reduction (where E ⟦ ρ θ · qin ⟧ has correct binding)

    E ⟦ ρ θ · qin ⟧ sn⟶₁ E ⟦ ρ θr · ro ⟧

construct the E-wrapped reduction

    ρ θ · E ⟦ qin ⟧ sn⟶₁ ρ θr · E ⟦ ro ⟧
          ( = q )             ( = r )
-}
conf-lift-lemma : ∀ {E qin ro p q θ θr BV FV A Ar} →
  CorrectBinding p BV FV →

  p ≐ E ⟦ ρ⟨ θ , A ⟩· qin ⟧e →
  q ≐ E ⟦ qin ⟧e →

  ρ⟨ θ , A ⟩· qin sn⟶₁ ρ⟨ θr , Ar ⟩· ro →

  ∃ λ r →
    r ≐ E ⟦ ro ⟧e ×
    ρ⟨ θ , A ⟩· q sn⟶₁ ρ⟨ θr , Ar ⟩· r

conf-lift-lemma cb dehole dehole ρθ·pinsn⟶₁ρθq·qin = _ , dehole , ρθ·pinsn⟶₁ρθq·qin

conf-lift-lemma cb@(CBpar cbp' cbq' _ _ _ _) (depar₁ p≐E⟦ρθ·pin⟧) (depar₁ r≐E⟦pin⟧) ρθ·pinsn⟶₁ρθq·qin
  with conf-lift-lemma cbp' p≐E⟦ρθ·pin⟧ r≐E⟦pin⟧ ρθ·pinsn⟶₁ρθq·qin
... | q , q≐E⟦qin⟧ , ρθ·rsn⟶₁ρθq·q
  with get-view ρθ·rsn⟶₁ρθq·q
... | inj₁ (E' , pin' , qin' , r≐E'⟦pin'⟧ , q≐E'⟦qin'⟧ , e-view) =
  _ , depar₁ q≐E⟦qin⟧ ,′
  proj₁ (wrap-rho ρθ·rsn⟶₁ρθq·q r≐E'⟦pin'⟧ q≐E'⟦qin'⟧ e-view _
          (depar₁ r≐E'⟦pin'⟧) (depar₁ q≐E'⟦qin'⟧))
... | inj₂ (refl , refl , pot) with wrap-rho-pot' (depar₁ p≐E⟦ρθ·pin⟧) cb ρθ·rsn⟶₁ρθq·q pot
... | _ , depar₁ dehole , ρθ·p'∥tsn⟶₁ρθq·p'∥t , pot' = -- need pattern matching for LHS of sn⟶₁
  _ , depar₁ q≐E⟦qin⟧ ,′
    ρθ·p'∥tsn⟶₁ρθq·p'∥t

conf-lift-lemma cb@(CBpar cbp' cbq' _ _ _ _) (depar₂ p≐E⟦ρθ·pin⟧) (depar₂ r≐E⟦pin⟧) ρθ·pinsn⟶₁ρθq·qin
  with conf-lift-lemma cbq' p≐E⟦ρθ·pin⟧ r≐E⟦pin⟧ ρθ·pinsn⟶₁ρθq·qin
... | q , q≐E⟦qin⟧ , ρθ·rsn⟶₁ρθq·q
  with get-view ρθ·rsn⟶₁ρθq·q
... | inj₁ (E' , pin' , qin' , r≐E'⟦pin'⟧ , q≐E'⟦qin'⟧ , e-view) =
  _ , depar₂ q≐E⟦qin⟧ ,′
  proj₁ (wrap-rho ρθ·rsn⟶₁ρθq·q r≐E'⟦pin'⟧ q≐E'⟦qin'⟧ e-view _
          (depar₂ r≐E'⟦pin'⟧) (depar₂ q≐E'⟦qin'⟧))
... | inj₂ (refl , refl , pot) with wrap-rho-pot' (depar₂ p≐E⟦ρθ·pin⟧) cb ρθ·rsn⟶₁ρθq·q pot
... | _ , depar₂ dehole , ρθ·t∥q'sn⟶₁ρθq·t∥q' , pot' =
  _ , depar₂ q≐E⟦qin⟧ ,′
    ρθ·t∥q'sn⟶₁ρθq·t∥q'

conf-lift-lemma cb@(CBseq cbp' cbq' _) (deseq p≐E⟦ρθ·pin⟧) (deseq r≐E⟦pin⟧) ρθ·pinsn⟶₁ρθq·qin
  with conf-lift-lemma cbp' p≐E⟦ρθ·pin⟧ r≐E⟦pin⟧ ρθ·pinsn⟶₁ρθq·qin
... | q , q≐E⟦qin⟧ , ρθ·rsn⟶₁ρθq·q
  with get-view ρθ·rsn⟶₁ρθq·q
... | inj₁ (E' , pin' , qin' , r≐E'⟦pin'⟧ , q≐E'⟦qin'⟧ , e-view) =
  _ , deseq q≐E⟦qin⟧ ,′
  proj₁ (wrap-rho ρθ·rsn⟶₁ρθq·q r≐E'⟦pin'⟧ q≐E'⟦qin'⟧ e-view _
          (deseq r≐E'⟦pin'⟧) (deseq q≐E'⟦qin'⟧))
... | inj₂ (refl , refl , pot) with wrap-rho-pot' (deseq p≐E⟦ρθ·pin⟧) cb ρθ·rsn⟶₁ρθq·q pot
... | _ , deseq dehole , ρθ·t>>q'sn⟶₁ρθq·t>>q' , pot' =
  _ , deseq q≐E⟦qin⟧ ,′
    ρθ·t>>q'sn⟶₁ρθq·t>>q'

conf-lift-lemma cb@(CBloopˢ cbp' cbq' _ _) (deloopˢ p≐E⟦ρθ·pin⟧) (deloopˢ r≐E⟦pin⟧) ρθ·pinsn⟶₁ρθq·qin
  with conf-lift-lemma cbp' p≐E⟦ρθ·pin⟧ r≐E⟦pin⟧ ρθ·pinsn⟶₁ρθq·qin
... | q , q≐E⟦qin⟧ , ρθ·rsn⟶₁ρθq·q
  with get-view ρθ·rsn⟶₁ρθq·q
... | inj₁ (E' , pin' , qin' , r≐E'⟦pin'⟧ , q≐E'⟦qin'⟧ , e-view) =
  _ , deloopˢ q≐E⟦qin⟧ ,′
  proj₁ (wrap-rho ρθ·rsn⟶₁ρθq·q r≐E'⟦pin'⟧ q≐E'⟦qin'⟧ e-view _
          (deloopˢ r≐E'⟦pin'⟧) (deloopˢ q≐E'⟦qin'⟧))
... | inj₂ (refl , refl , pot) with wrap-rho-pot' (deloopˢ p≐E⟦ρθ·pin⟧) cb ρθ·rsn⟶₁ρθq·q pot
... | _ , deloopˢ dehole , ρθ·t>>q'sn⟶₁ρθq·t>>q' , pot' =
  _ , deloopˢ q≐E⟦qin⟧ ,′
    ρθ·t>>q'sn⟶₁ρθq·t>>q'

conf-lift-lemma cb@(CBsusp cb' _) (desuspend p≐E⟦ρθ·pin⟧) (desuspend r≐E⟦pin⟧) ρθ·pinsn⟶₁ρθq·qin
  with conf-lift-lemma cb' p≐E⟦ρθ·pin⟧ r≐E⟦pin⟧ ρθ·pinsn⟶₁ρθq·qin
... | q , q≐E⟦qin⟧ , ρθ·rsn⟶₁ρθq·q
  with get-view ρθ·rsn⟶₁ρθq·q
... | inj₁ (E' , pin' , qin' , r≐E'⟦pin'⟧ , q≐E'⟦qin'⟧ , e-view) =
  _ , desuspend q≐E⟦qin⟧ ,′
  proj₁ (wrap-rho ρθ·rsn⟶₁ρθq·q r≐E'⟦pin'⟧ q≐E'⟦qin'⟧ e-view _
          (desuspend r≐E'⟦pin'⟧) (desuspend q≐E'⟦qin'⟧))
... | inj₂ (refl , refl , pot) with wrap-rho-pot' (desuspend p≐E⟦ρθ·pin⟧) cb ρθ·rsn⟶₁ρθq·q pot
... | _ , desuspend dehole , ρθ·susptsn⟶₁ρθq·suspt , pot' =
  _ , desuspend q≐E⟦qin⟧ ,′
    ρθ·susptsn⟶₁ρθq·suspt

conf-lift-lemma cb@(CBtrap cb') (detrap p≐E⟦ρθ·pin⟧) (detrap r≐E⟦pin⟧) ρθ·pinsn⟶₁ρθq·qin
  with conf-lift-lemma cb' p≐E⟦ρθ·pin⟧ r≐E⟦pin⟧ ρθ·pinsn⟶₁ρθq·qin
... | q , q≐E⟦qin⟧ , ρθ·rsn⟶₁ρθq·q
  with get-view ρθ·rsn⟶₁ρθq·q
... | inj₁ (E' , pin' , qin' , r≐E'⟦pin'⟧ , q≐E'⟦qin'⟧ , e-view) =
  _ , detrap q≐E⟦qin⟧ ,′
  proj₁ (wrap-rho ρθ·rsn⟶₁ρθq·q r≐E'⟦pin'⟧ q≐E'⟦qin'⟧ e-view _
          (detrap r≐E'⟦pin'⟧) (detrap q≐E'⟦qin'⟧))
... | inj₂ (refl , refl , pot) with wrap-rho-pot' (detrap p≐E⟦ρθ·pin⟧) cb ρθ·rsn⟶₁ρθq·q pot
... | _ , detrap dehole , ρθ·traptsn⟶₁ρθq·trapt , pot' =
  _ , detrap q≐E⟦qin⟧ ,′
    ρθ·traptsn⟶₁ρθq·trapt

{-
Base case where (E, C) = ([], []).

  The most complicated case where LHS is  ρθ.ρθ'.qin sn⟶₁ ρ(θ←θ').qin   (qin = ρθ'.rin)
  and RHS is  (ρθ.) ρθ'.rin sn⟶₁ (ρθ.) ρθr.ro,  i.e. arbitrary ->E-view and ->pot-view.

     p
  ρθ. E⟦ρθ'.qin⟧   -- sn⟶₁ ->    ρ(θ←θ'). E⟦qin⟧
 (ρθ) E⟦ρθ'.qin⟧   -- sn⟶₁ ->   (ρθ)      E⟦ρθr.ro⟧
-}
1-steplρ-E-view-ecsame : ∀{E p qin q qo rin r ro θ θ←θ' BV FV A A⊓A'} →
  {ρθ·psn⟶₁ρθ←θ'·q  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θ←θ' , A⊓A' ⟩· q} →
  CorrectBinding p BV FV →

  (p≐E⟦qin⟧  :  p ≐ E ⟦ qin ⟧e) →
  (q≐E⟦qo⟧   :  q ≐ E ⟦ qo ⟧e) →
  ->E-view  ρθ·psn⟶₁ρθ←θ'·q  p≐E⟦qin⟧  q≐E⟦qo⟧ →

  (p≐E⟦rin⟧  :  p ≐ (map ceval E) ⟦ rin ⟧c) →
  (r≐E⟦ro⟧   :  r ≐ (map ceval E) ⟦ ro ⟧c) →
  -- rinsn⟶₁ro can only be  (ρ⟨ θ' , A' ⟩· qin) sn⟶₁ (ρ⟨ θr , Ar ⟩· ro)
  (rinsn⟶₁ro  :  rin sn⟶₁ ro) →

  Σ ((Env × Ctrl × Term) × EvaluationContext × Term × Term) λ { ((θo , Ao , po) , E' , roin , poin) →
    ρ⟨ θ←θ' , A⊓A' ⟩· q sn⟶₁ ρ⟨ θo , Ao ⟩· po ×
    Σ[ ρθ·rsn⟶₁ρθo·po  ∈  ρ⟨ θ , A ⟩·    r sn⟶₁ ρ⟨ θo , Ao ⟩· po ]
    Σ[ r≐E'⟦roin⟧     ∈  r ≐ E' ⟦ roin ⟧e ]
    Σ[ po≐E'⟦poin⟧    ∈  po ≐ E' ⟦ poin ⟧e ]
      ->E-view  ρθ·rsn⟶₁ρθo·po  r≐E'⟦roin⟧  po≐E'⟦poin⟧
    }

1-steplρ-E-view-ecsame cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ e-view p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro
  with unplug-eq p≐E⟦ρθ'·qin⟧ (⟦⟧c-to-⟦⟧e p≐C⟦rin⟧)
1-steplρ-E-view-ecsame cb _ _ vis-present           _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vis-absent            _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vemit                 _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vraise-shared         _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vset-shared-value-old _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vset-shared-value-new _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vraise-var            _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vset-var              _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vif-false             _ _ () | refl
1-steplρ-E-view-ecsame cb _ _ vif-true              _ _ () | refl

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb
  p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge
  p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl
  with ρ-stays-ρ-sn⟶₁ rinsn⟶₁ro
... | θr , roin , Ar , refl
  with conf-lift-lemma cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ rinsn⟶₁ro
... | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r' -- q ≐ E ⟦ qin ⟧
  with get-view ρθ'·qsn⟶₁ρθr·r'

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦present⟧ , r'≐E⟦roin'⟧ ,
          vis-present {.θ'} {S} {E = .E'} {S∈Domθ'} {θ'S≡present} {q≐E'⟦present⟧}) =
  _ ,
      (ris-present {S = S}
        (Env.sig-←-monoʳ S θr θ S∈Domθ')
        (trans
          (SigMap.get-U-right-irr-m {_} S (Env.sig θ) (Env.sig θr)
            (Env.sig-←-monoʳ S θr θ S∈Domθ') S∈Domθ')
          θ'S≡present)
        q≐E'⟦present⟧) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , q≐E⟦qo'⟧ , r'≐E⟦roin'⟧ ,
          vis-absent {.θ'} {S} {E = .E'} {S∈Domθ'} {θ'S≡absent} {q≐E'⟦absent⟧}) =
  _ ,
      (ris-absent {S = S}
        (Env.sig-←-monoʳ S θr θ S∈Domθ')
        (trans
          (SigMap.get-U-right-irr-m {_} S (Env.sig θ) (Env.sig θr)
            (Env.sig-←-monoʳ S θr θ S∈Domθ') S∈Domθ')
          θ'S≡absent)
        q≐E'⟦absent⟧) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦if⟧ , r'≐E⟦roin'⟧ ,
          vif-false {x = x} {.E'} {x∈Domθ'} {θ'x≡zero} {q≐E'⟦if⟧}) =
  _ ,
      (rif-false {x = x}
        (Env.seq-←-monoʳ x θr θ x∈Domθ')
        (trans
          (VarMap.get-U-right-irr-m {_} x (Env.var θ) (Env.var θr)
            (Env.seq-←-monoʳ x θr θ x∈Domθ') x∈Domθ')
          θ'x≡zero)
        q≐E'⟦if⟧) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦if⟧ , r'≐E⟦roin'⟧ ,
          vif-true {x = x} {.E'} {_} {x∈Domθ'} {θ'x≡suc} {q≐E'⟦if⟧}) =
  _ ,
      (rif-true {x = x}
        (Env.seq-←-monoʳ x θr θ x∈Domθ')
        (trans
          (Env.var-vals-←-right-irr' x θ θr x∈Domθ' (Env.seq-←-monoʳ x θr θ x∈Domθ'))
          θ'x≡suc)
        q≐E'⟦if⟧) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦shared⟧ , r'≐E⟦roin'⟧ ,
          vraise-shared {s = s} {E = .E'} {e'} {q≐E'⟦shared⟧})
  with ready-irr-on-irr-θʳ θ e'
... | e'' , δe'≡δe'' rewrite δe'≡δe'' =
  _ ,
      rraise-shared e'' q≐E'⟦shared⟧ ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦var⟧ , r'≐E⟦roin'⟧ ,
            vraise-var {E = .E'} {e'} {q≐E'⟦var⟧})
  with ready-irr-on-irr-θʳ θ e'
... | e'' , δe'≡δe'' rewrite δe'≡δe'' =
  _ ,
      rraise-var e'' q≐E'⟦var⟧ ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} {A₁ = A} {.GO} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦emit⟧ , r'≐E⟦roin'⟧ ,
            vemit {S = S} {.E'} {S∈Domθ'} {θ'S≢absent} {q≐E'⟦emit⟧}) =
  _ ,
       (subst₂ (λ θ* go → ρ⟨ (θ ← θ') , go ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , go ⟩· E' ⟦ nothin ⟧e)
        (begin
            Env.set-sig {S} (θ ← θ') S∈Domθ←θ' Signal.present
          ≡⟨ Env.sig-set=← (θ ← θ') S Signal.present S∈Domθ←θ' ⟩
            (θ ← θ') ← [S↦present]
          ≡⟨ sym (Env.←-assoc θ θ' [S↦present]) ⟩
            θ ← (θ' ← [S↦present])
          ≡⟨ cong (θ ←_) (sym (Env.sig-set=← θ' S Signal.present S∈Domθ')) ⟩
            θ ← (Env.set-sig {S} θ' S∈Domθ' Signal.present)
         ∎)
         (sym $ A-max-GO-≡-right A)
        (remit {θ ← θ'} {S = S} S∈Domθ←θ'
          (θ'S≢absent ∘ trans (sym ⟨θ←θ'⟩S≡θ'S))
          q≐E'⟦emit⟧))   ,′
       (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))
  where
    [S↦present] = Θ SigMap.[ S ↦ Signal.present ] ShrMap.empty VarMap.empty
    S∈Domθ←θ'   = Env.sig-←-monoʳ S θ' θ S∈Domθ'
    ⟨θ←θ'⟩S≡θ'S = Env.sig-stats-←-right-irr' S θ θ' S∈Domθ' S∈Domθ←θ'

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} {A₁ = A} {.GO} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦s⇐e⟧ , r'≐E⟦roin'⟧ ,
          vset-shared-value-old {s = s} {E = .E'} {e'} {s∈Domθ'} {θ's≡old} {q≐E'⟦s⇐e⟧})
  with ready-irr-on-irr-θʳ θ e'
... | e'' , δe'≡δe'' rewrite δe'≡δe'' =
  _ ,
       (subst₂ (λ θ* go → ρ⟨ (θ ← θ') , go ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , go ⟩· E' ⟦ nothin ⟧e)
        (begin
            Env.set-shr {s} (θ ← θ') s∈Domθ←θ' SharedVar.new (δ e'')
          ≡⟨ Env.shr-set=← (θ ← θ') s SharedVar.new (δ e'') s∈Domθ←θ' ⟩
            (θ ← θ') ← [s↦new,δe'']
          ≡⟨ sym (Env.←-assoc θ θ' [s↦new,δe'']) ⟩
            θ ← (θ' ← [s↦new,δe''])
          ≡⟨ cong (θ ←_) (sym (Env.shr-set=← θ' s SharedVar.new (δ e'') s∈Domθ')) ⟩
            θ ← (Env.set-shr {s} θ' s∈Domθ' SharedVar.new (δ e''))
         ∎)
         (sym $ A-max-GO-≡-right A)
        (rset-shared-value-old {θ ← θ'} e'' s∈Domθ←θ'
          (trans (Env.shr-stats-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ') θ's≡old)
          q≐E'⟦s⇐e⟧))   ,′
       (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))
 where
    [s↦new,δe''] = [s,δe-new]-env s (δ e'')
    s∈Domθ←θ'   = Env.shr-←-monoʳ s θ' θ s∈Domθ'

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E}  {A₁ = A} {.GO} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , .q≐E'⟦s⇐e⟧ , r'≐E⟦roin'⟧ ,
          vset-shared-value-new {s = s} {E = .E'} {e'} {s∈Domθ'} {θ's≡old} {q≐E'⟦s⇐e⟧})
  with ready-irr-on-irr-θʳ θ e'
... | e'' , δe'≡δe'' rewrite δe'≡δe'' =
  _ ,
       (subst₂ (λ θ* go → ρ⟨ (θ ← θ') , go ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , go ⟩· E' ⟦ nothin ⟧e)
        (begin
            Env.set-shr {s} (θ ← θ') s∈Domθ←θ' SharedVar.new (⟨θ←θ'⟩s + δ e'')
          ≡⟨ cong(Env.set-shr{s}(θ ← θ')s∈Domθ←θ' SharedVar.new ∘ (_+ δ e''))⟨θ←θ'⟩s≡θ's ⟩
            Env.set-shr {s} (θ ← θ') s∈Domθ←θ' SharedVar.new (θ's + δ e'')
          ≡⟨ Env.shr-set=← (θ ← θ') s SharedVar.new (θ's + δ e'') s∈Domθ←θ' ⟩
            (θ ← θ') ← [s↦new,θ's+δe'']
          ≡⟨ sym (Env.←-assoc θ θ' [s↦new,θ's+δe'']) ⟩
            θ ← (θ' ← [s↦new,θ's+δe''])
          ≡⟨ cong (θ ←_) (sym (Env.shr-set=← θ' s SharedVar.new (θ's + δ e'') s∈Domθ')) ⟩
            θ ← (Env.set-shr {s} θ' s∈Domθ' SharedVar.new (θ's + δ e''))
         ∎)
         (sym $ A-max-GO-≡-right A)
        (rset-shared-value-new {θ ← θ'} e'' s∈Domθ←θ'
          (trans (Env.shr-stats-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ') θ's≡old)
          q≐E'⟦s⇐e⟧))  ,′
       (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))
 where
    s∈Domθ←θ'   = Env.shr-←-monoʳ s θ' θ s∈Domθ'
    θ's = Env.shr-vals {s} θ' s∈Domθ'
    ⟨θ←θ'⟩s = Env.shr-vals {s} (θ ← θ') s∈Domθ←θ'
    ⟨θ←θ'⟩s≡θ's = Env.shr-vals-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ'
    [s↦new,θ's+δe''] = [s,δe-new]-env s (θ's + δ e'')

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} {A₁ = A} {A'} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , q≐E⟦qo'⟧ , r'≐E⟦roin'⟧ ,
          vset-var {x = x} {E = .E'} {x∈Domθ'} {e'} {q≐E'⟦x≔e⟧})
  with ready-irr-on-irr-θʳ θ e'
... | e'' , δe'≡δe'' rewrite δe'≡δe'' =
  _ ,
      (subst (λ θ* → ρ⟨ (θ ← θ') , A-max A A' ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , A-max A A' ⟩· E' ⟦ nothin ⟧e)
        (begin
            Env.set-var {x} (θ ← θ') x∈Domθ←θ' (δ e'')
          ≡⟨ Env.seq-set=← (θ ← θ') x (δ e'') x∈Domθ←θ' ⟩
            (θ ← θ') ← [x↦δe'']
          ≡⟨ sym (Env.←-assoc θ θ' [x↦δe'']) ⟩
            θ ← (θ' ← [x↦δe''])
          ≡⟨ cong (θ ←_) (sym (Env.seq-set=← θ' x (δ e'') x∈Domθ')) ⟩
            θ ← (Env.set-var {x} θ' x∈Domθ' (δ e''))
         ∎)
        (rset-var {θ ← θ'} x∈Domθ←θ' e'' q≐E'⟦x≔e⟧)) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))
 where
    [x↦δe'']  = [x,δe]-env x (δ e'')
    x∈Domθ←θ' = Env.seq-←-monoʳ x θ' θ x∈Domθ'

1-steplρ-E-view-ecsame {E} {A = A} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} {A₂ = A'} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | (.(θ' ← θr) , roin , .(A-max A' Ar) , refl)
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₁ (E' , qo' , roin' , q≐E⟦qo'⟧ , r'≐E⟦roin'⟧ ,
          vmerge {.θ'} {θr} {_} {.roin'} {.E'} {_} {Ar} {q≐E'⟦ρθr·roin'⟧}) =
  ((_ , (A-max A (A-max A' Ar)) , _) , _) ,
       (subst₂ (λ θ* A* → ρ⟨ (θ ← θ') , A-max A A' ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , A* ⟩· E' ⟦ roin' ⟧e)
         (sym (Env.←-assoc θ θ' θr))
         (sym (A-max-assoc A A' Ar))
         (rmerge {θ ← θ'} {θr} {A₁ = A-max A A'} {Ar} q≐E'⟦ρθr·roin'⟧))   ,′
       (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₂ (refl , refl , vabsence S S∈Domθ' θ'S≡unknown S∉canθ-θ'-q-[]) =
  _ ,
      (subst (λ θ* → ρ⟨ (θ ← θ') , _ ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , _ ⟩· E ⟦ qin ⟧e)
        (begin
            Env.set-sig {S} (θ ← θ') S∈Domθ←θ' Signal.absent
          ≡⟨ Env.sig-set=← (θ ← θ') S Signal.absent S∈Domθ←θ' ⟩
            (θ ← θ') ← [S↦absent]
          ≡⟨ sym (Env.←-assoc θ θ' [S↦absent]) ⟩
            θ ← (θ' ← [S↦absent])
          ≡⟨ cong (θ ←_) (sym (Env.sig-set=← θ' S Signal.absent S∈Domθ')) ⟩
            θ ← (Env.set-sig {S} θ' S∈Domθ' Signal.absent)
         ∎)
        (rabsence {θ ← θ'} {S = S} S∈Domθ←θ'
          (trans (Env.sig-stats-←-right-irr' S θ θ' S∈Domθ' S∈Domθ←θ') θ'S≡unknown)
          (λ S∈canθ-θ←θ''-q-[] →
            S∉canθ-θ'-q-[]
              (canθₛ-mergeʳ (Env.sig θ) θ' (E ⟦ qin ⟧e) Env.[]env (λ _ ())
                 S S∈canθ-θ←θ''-q-[])))) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))
  where
    [S↦absent] = Θ SigMap.[ S ↦ Signal.absent ] ShrMap.empty VarMap.empty
    S∈Domθ←θ'   = Env.sig-←-monoʳ S θ' θ S∈Domθ'

1-steplρ-E-view-ecsame {E} {ρθ·psn⟶₁ρθ←θ'·q = rmerge {θ} {θ'} {_} {qin} {.E} .p≐E⟦ρθ'·qin⟧}
  cb p≐E⟦ρθ'·qin⟧ q≐E⟦qin⟧ vmerge p≐C⟦rin⟧ r≐C⟦ro⟧ rinsn⟶₁ro | refl | θr , roin , Ar , refl
  | r' , r'≐E⟦roin⟧ , ρθ'·qsn⟶₁ρθr·r'
  | inj₂ (refl , refl , vreadyness s s∈Domθ' θ's≡old⊎θ's≡new s∉canθ-θ'-q-[]) =
  _ ,
      (subst (λ θ* → ρ⟨ (θ ← θ') , _ ⟩· E ⟦ qin ⟧e sn⟶₁ ρ⟨ θ* , _ ⟩· E ⟦ qin ⟧e)
        (begin
            Env.set-shr {s} (θ ← θ') s∈Domθ←θ' SharedVar.ready ⟨θ←θ'⟩s
          ≡⟨ cong (Env.set-shr {s} (θ ← θ') s∈Domθ←θ' SharedVar.ready) ⟨θ←θ'⟩s≡θ's ⟩
            Env.set-shr {s} (θ ← θ') s∈Domθ←θ' SharedVar.ready θ's
          ≡⟨ Env.shr-set=← (θ ← θ') s SharedVar.ready θ's s∈Domθ←θ' ⟩
            (θ ← θ') ← [s↦ready,θ's]
          ≡⟨ sym (Env.←-assoc θ θ' [s↦ready,θ's]) ⟩
            θ ← (θ' ← [s↦ready,θ's])
          ≡⟨ cong (θ ←_) (sym (Env.shr-set=← θ' s SharedVar.ready θ's s∈Domθ')) ⟩
            θ ← (Env.set-shr {s} θ' s∈Domθ' SharedVar.ready θ's)
         ∎)
        (rreadyness {θ ← θ'} {s = s} s∈Domθ←θ'
          (Data.Sum.map
            (trans (Env.shr-stats-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ'))
            (trans (Env.shr-stats-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ'))
            θ's≡old⊎θ's≡new)
          (λ s∈canθ-θ←θ''-q-[] →
            s∉canθ-θ'-q-[]
              (canθₛₕ-mergeʳ (Env.sig θ) θ' (E ⟦ qin ⟧e) Env.[]env (λ _ ())
                 s s∈canθ-θ←θ''-q-[])))) ,′
      (subst (λ po* → Σ[ r ∈ ρ⟨ _ , _ ⟩· _ sn⟶₁ ρ⟨ _ , _ ⟩· po* ]
                      Σ[ a ∈ _ ≐ _ ⟦ _ ⟧e ]
                      Σ[ b ∈ po* ≐ _ ⟦ _ ⟧e ]
                        ->E-view r a b)
        (unplug r'≐E⟦roin⟧)
        (rmerge (⟦⟧c-to-⟦⟧e r≐C⟦ro⟧) ,
         _ , plug refl , vmerge))
  where
    s∈Domθ←θ'   = Env.shr-←-monoʳ s θ' θ s∈Domθ'
    θ's = Env.shr-vals {s} θ' s∈Domθ'
    ⟨θ←θ'⟩s = Env.shr-vals {s} (θ ← θ') s∈Domθ←θ'
    ⟨θ←θ'⟩s≡θ's = Env.shr-vals-←-right-irr' s θ θ' s∈Domθ' s∈Domθ←θ'
    [s↦ready,θ's] =
      Θ ShrMap.empty ShrMap.[ s ↦ (SharedVar.ready , θ's) ] VarMap.empty


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a strict order to incorporate a new supremum
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Supremum

open import Relation.Binary

module Relation.Binary.Construct.Add.Supremum.Strict
  {a r} {A : Set a} (_<_ : Rel A r) where

open import Level using (_⊔_)
open import Data.Product
open import Function
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
import Relation.Binary.PropositionalEquality as P
open import Relation.Nullary.Construct.Add.Supremum
import Relation.Binary.Construct.Add.Supremum.Equality as Equality
import Relation.Binary.Construct.Add.Supremum.NonStrict as NonStrict

------------------------------------------------------------------------
-- Definition

infix 4 _<⁺_

data _<⁺_ : Rel (A ⁺) (a ⊔ r) where
  [_]    : {k l : A} → k < l → [ k ] <⁺ [ l ]
  [_]<⊤⁺ : (k : A)           → [ k ] <⁺ ⊤⁺

------------------------------------------------------------------------
-- Relational properties

[<]-injective : ∀ {k l} → [ k ] <⁺ [ l ] → k < l
[<]-injective [ p ] = p

<⁺-asym : Asymmetric _<_ → Asymmetric _<⁺_
<⁺-asym <-asym [ p ]    [ q ] = <-asym p q
<⁺-asym <-asym [ k ]<⊤⁺ ()

<⁺-trans : Transitive _<_ → Transitive _<⁺_
<⁺-trans <-trans [ p ] [ q ]    = [ <-trans p q ]
<⁺-trans <-trans [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺

<⁺-dec : Decidable _<_ → Decidable _<⁺_
<⁺-dec _<?_ [ k ] [ l ] = Dec.map′ [_] [<]-injective (k <? l)
<⁺-dec _<?_ [ k ] ⊤⁺    = yes [ k ]<⊤⁺
<⁺-dec _<?_ ⊤⁺    [ l ] = no (λ ())
<⁺-dec _<?_ ⊤⁺    ⊤⁺    = no (λ ())

<⁺-irrelevant : Irrelevant _<_ → Irrelevant _<⁺_
<⁺-irrelevant <-irr [ p ]    [ q ]    = P.cong _ (<-irr p q)
<⁺-irrelevant <-irr [ k ]<⊤⁺ [ k ]<⊤⁺ = P.refl

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  <⁺-cmp : Trichotomous _≈_ _<_ → Trichotomous _≈⁺_ _<⁺_
  <⁺-cmp <-cmp ⊤⁺    ⊤⁺    = tri≈ (λ ()) ⊤⁺≈⊤⁺ (λ ())
  <⁺-cmp <-cmp ⊤⁺    [ l ] = tri> (λ ()) (λ ()) [ l ]<⊤⁺
  <⁺-cmp <-cmp [ k ] ⊤⁺    = tri< [ k ]<⊤⁺ (λ ()) (λ ())
  <⁺-cmp <-cmp [ k ] [ l ] with <-cmp k l
  ... | tri< a ¬b ¬c = tri< [ a ] (¬b ∘ [≈]-injective) (¬c ∘ [<]-injective)
  ... | tri≈ ¬a b ¬c = tri≈ (¬a ∘ [<]-injective) [ b ] (¬c ∘ [<]-injective)
  ... | tri> ¬a ¬b c = tri> (¬a ∘ [<]-injective) (¬b ∘ [≈]-injective) [ c ]

  <⁺-irrefl : Irreflexive _≈_ _<_ → Irreflexive _≈⁺_ _<⁺_
  <⁺-irrefl <-irrefl [ p ] [ q ] = <-irrefl p q
  <⁺-irrefl <-irrefl ⊤⁺≈⊤⁺ ()

  <⁺-respˡ-≈⁺ : _<_ Respectsˡ _≈_ → _<⁺_ Respectsˡ _≈⁺_
  <⁺-respˡ-≈⁺ <-respˡ-≈ [ p ] [ q ]      = [ <-respˡ-≈ p q ]
  <⁺-respˡ-≈⁺ <-respˡ-≈ [ p ] ([ l ]<⊤⁺) = [ _ ]<⊤⁺
  <⁺-respˡ-≈⁺ <-respˡ-≈ ⊤⁺≈⊤⁺ q          = q

  <⁺-respʳ-≈⁺ : _<_ Respectsʳ _≈_ → _<⁺_ Respectsʳ _≈⁺_
  <⁺-respʳ-≈⁺ <-respʳ-≈ [ p ] [ q ] = [ <-respʳ-≈ p q ]
  <⁺-respʳ-≈⁺ <-respʳ-≈ ⊤⁺≈⊤⁺ q     = q

  <⁺-resp-≈⁺ : _<_ Respects₂ _≈_ → _<⁺_ Respects₂ _≈⁺_
  <⁺-resp-≈⁺ = map <⁺-respʳ-≈⁺ <⁺-respˡ-≈⁺

module _ {r} {_≤_ : Rel A r} where

  open NonStrict _≤_

  <⁺-transʳ : Trans _≤_ _<_ _<_ → Trans _≤⁺_ _<⁺_ _<⁺_
  <⁺-transʳ <-transʳ [ p ] [ q ]    = [ <-transʳ p q ]
  <⁺-transʳ <-transʳ [ p ] [ k ]<⊤⁺ = [ _ ]<⊤⁺

  <⁺-transˡ : Trans _<_ _≤_ _<_ → Trans _<⁺_ _≤⁺_ _<⁺_
  <⁺-transˡ <-transˡ [ p ]    [ q ]       = [ <-transˡ p q ]
  <⁺-transˡ <-transˡ [ p ]    ([ _ ] ≤⊤⁺) = [ _ ]<⊤⁺
  <⁺-transˡ <-transˡ [ k ]<⊤⁺ (⊤⁺ ≤⊤⁺)    = [ k ]<⊤⁺

------------------------------------------------------------------------
-- Structures

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  <⁺-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ →
                            IsStrictPartialOrder _≈⁺_ _<⁺_
  <⁺-isStrictPartialOrder strict = record
    { isEquivalence = ≈⁺-isEquivalence isEquivalence
    ; irrefl        = <⁺-irrefl irrefl
    ; trans         = <⁺-trans trans
    ; <-resp-≈      = <⁺-resp-≈⁺ <-resp-≈
    } where open IsStrictPartialOrder strict

  <⁺-isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ →
                               IsDecStrictPartialOrder _≈⁺_ _<⁺_
  <⁺-isDecStrictPartialOrder dectot = record
    { isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
    ; _≟_                  = ≈⁺-dec _≟_
    ; _<?_                 = <⁺-dec _<?_
    } where open IsDecStrictPartialOrder dectot

  <⁺-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ →
                          IsStrictTotalOrder _≈⁺_ _<⁺_
  <⁺-isStrictTotalOrder strictot = record
    { isEquivalence = ≈⁺-isEquivalence isEquivalence
    ; trans         = <⁺-trans trans
    ; compare       = <⁺-cmp compare
    } where open IsStrictTotalOrder strictot

ext: agda


text:
-- The SIP applied to groups
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.GroupPath where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

private
  variable
    ℓ ℓ' ℓ'' : Level

open Iso
open GroupStr
open IsGroupHom

𝒮ᴰ-Group : DUARel (𝒮-Univ ℓ) GroupStr ℓ
𝒮ᴰ-Group =
  𝒮ᴰ-Record (𝒮-Univ _) IsGroupEquiv
    (fields:
      data[ _·_ ∣ autoDUARel _ _ ∣ pres· ]
      data[ 1g ∣ autoDUARel _ _ ∣ pres1 ]
      data[ inv ∣ autoDUARel _ _ ∣ presinv ]
      prop[ isGroup ∣ (λ _ _ → isPropIsGroup _ _ _) ])
  where
  open GroupStr
  open IsGroupHom

GroupPath : (M N : Group ℓ) → GroupEquiv M N ≃ (M ≡ N)
GroupPath = ∫ 𝒮ᴰ-Group .UARel.ua

-- The module below defines a group induced from an equivalence
-- between a group G and a type A which preserves the full raw group
-- structure from G to A. This version is useful when proving that
-- some type equivalent to a group is a group while also specifying
-- the binary operation, unit and inverse.
module _ (G : Group ℓ) {A : Type ℓ}
  (m : A → A → A)
  (u : A)
  (inverse : A → A)
  (e : ⟨ G ⟩ ≃ A)
  (p· : ∀ x y → e .fst (G .snd ._·_ x y) ≡ m (e .fst x) (e .fst y))
  (pu : e .fst (G .snd .1g) ≡ u)
  (pinv : ∀ x → e .fst (G .snd .inv x) ≡ inverse (e .fst x))
  where

  private
    module G = GroupStr (G .snd)

    BaseΣ : Type (ℓ-suc ℓ)
    BaseΣ = Σ[ B ∈ Type ℓ ] (B → B → B) × B × (B → B)

    FamilyΣ : BaseΣ → Type ℓ
    FamilyΣ (B , m , u , i) = IsGroup u m i

    inducedΣ : FamilyΣ (A , m , u , inverse)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel BaseΣ) (e , p· , pu , pinv))
        G.isGroup

  InducedGroup : Group ℓ
  InducedGroup .fst = A
  InducedGroup .snd ._·_ = m
  InducedGroup .snd .1g = u
  InducedGroup .snd .inv = inverse
  InducedGroup .snd .isGroup = inducedΣ

  InducedGroupEquiv : GroupEquiv G InducedGroup
  fst InducedGroupEquiv = e
  snd InducedGroupEquiv = makeIsGroupHom p·

  InducedGroupPath : G ≡ InducedGroup
  InducedGroupPath = GroupPath _ _ .fst InducedGroupEquiv

-- The module below defines a group induced from an equivalence which
-- preserves the binary operation (i.e. a group isomorphism). This
-- version is useful when proving that some type equivalent to a group
-- G is a group when one doesn't care about what the unit and inverse
-- are. When using this version the unit and inverse will both be
-- defined by transporting over the unit and inverse from G to A.
module _ (G : Group ℓ) {A : Type ℓ}
  (m : A → A → A)
  (e : ⟨ G ⟩ ≃ A)
  (p· : ∀ x y → e .fst (G .snd ._·_ x y) ≡ m (e .fst x) (e .fst y))
  where

  private
    module G = GroupStr (G .snd)

    FamilyΣ : Σ[ B ∈ Type ℓ ] (B → B → B) → Type ℓ
    FamilyΣ (B , n) = Σ[ e ∈ B ] Σ[ i ∈ (B → B) ] IsGroup e n i

    inducedΣ : FamilyΣ (A , m)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel (Σ[ B ∈ Type ℓ ] (B → B → B))) (e , p·))
        (G.1g , G.inv , G.isGroup)

  InducedGroupFromPres· : Group ℓ
  InducedGroupFromPres· .fst = A
  InducedGroupFromPres· .snd ._·_ = m
  InducedGroupFromPres· .snd .1g = inducedΣ .fst
  InducedGroupFromPres· .snd .inv = inducedΣ .snd .fst
  InducedGroupFromPres· .snd .isGroup = inducedΣ .snd .snd

  InducedGroupEquivFromPres· : GroupEquiv G InducedGroupFromPres·
  fst InducedGroupEquivFromPres· = e
  snd InducedGroupEquivFromPres· = makeIsGroupHom p·

  InducedGroupPathFromPres· : G ≡ InducedGroupFromPres·
  InducedGroupPathFromPres· = GroupPath _ _ .fst InducedGroupEquivFromPres·

uaGroup : {G H : Group ℓ} → GroupEquiv G H → G ≡ H
uaGroup {G = G} {H = H} = equivFun (GroupPath G H)

-- Group-ua functoriality
Group≡ : (G H : Group ℓ) → (
  Σ[ p ∈ ⟨ G ⟩ ≡ ⟨ H ⟩ ]
  Σ[ q ∈ PathP (λ i → p i) (1g (snd G)) (1g (snd H)) ]
  Σ[ r ∈ PathP (λ i → p i → p i → p i) (_·_ (snd G)) (_·_ (snd H)) ]
  Σ[ s ∈ PathP (λ i → p i → p i) (inv (snd G)) (inv (snd H)) ]
  PathP (λ i → IsGroup (q i) (r i) (s i)) (isGroup (snd G)) (isGroup (snd H)))
  ≃ (G ≡ H)
Group≡ G H = isoToEquiv theIso
  where
  theIso : Iso _ _
  fun theIso (p , q , r , s , t) i = p i , groupstr (q i) (r i) (s i) (t i)
  inv theIso x = cong ⟨_⟩ x , cong (1g ∘ snd) x , cong (_·_ ∘ snd) x , cong (inv ∘ snd) x , cong (isGroup ∘ snd) x
  rightInv theIso _ = refl
  leftInv theIso _ = refl

caracGroup≡ : {G H : Group ℓ} (p q : G ≡ H) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
caracGroup≡ {G = G} {H = H} p q P =
  sym (transportTransport⁻ (ua (Group≡ G H)) p)
                                   ∙∙ cong (transport (ua (Group≡ G H))) helper
                                   ∙∙ transportTransport⁻ (ua (Group≡ G H)) q
    where
    helper : transport (sym (ua (Group≡ G H))) p ≡ transport (sym (ua (Group≡ G H))) q
    helper = Σ≡Prop
               (λ _ → isPropΣ
                         (isOfHLevelPathP' 1 (is-set (snd H)) _ _)
                         λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd H)) _ _)
                         λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd H)) _ _)
                         λ _ → isOfHLevelPathP 1 (isPropIsGroup _ _ _) _ _)
               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))

uaGroupId : (G : Group ℓ) → uaGroup (idGroupEquiv {G = G}) ≡ refl
uaGroupId G = caracGroup≡ _ _ uaIdEquiv

uaCompGroupEquiv : {F G H : Group ℓ} (f : GroupEquiv F G) (g : GroupEquiv G H)
                 → uaGroup (compGroupEquiv f g) ≡ uaGroup f ∙ uaGroup g
uaCompGroupEquiv f g = caracGroup≡ _ _ (
  cong ⟨_⟩ (uaGroup (compGroupEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  cong ⟨_⟩ (uaGroup f) ∙ cong ⟨_⟩ (uaGroup g)
    ≡⟨ sym (cong-∙ ⟨_⟩ (uaGroup f) (uaGroup g)) ⟩
  cong ⟨_⟩ (uaGroup f ∙ uaGroup g) ∎)

-- J-rule for GroupEquivs
GroupEquivJ : {G : Group ℓ} (P : (H : Group ℓ) → GroupEquiv G H → Type ℓ')
            → P G idGroupEquiv
            → ∀ {H} e → P H e
GroupEquivJ {G = G} P p {H} e =
  transport (λ i → P (GroupPath G H .fst e i)
    (transp (λ j → GroupEquiv G (GroupPath G H .fst e (i ∨ ~ j))) i e))
      (subst (P G) (sym lem) p)
  where
  lem : transport (λ j → GroupEquiv G (GroupPath G H .fst e (~ j))) e
       ≡ idGroupEquiv
  lem = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
       (Σ≡Prop (λ _ → isPropIsEquiv _)
         (funExt λ x → (λ i → fst (fst (fst e .snd .equiv-proof
                          (transportRefl (fst (fst e) (transportRefl x i)) i))))
                         ∙ retEq (fst e) x))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.List.Properties where

open import Agda.Builtin.List
open import Cubical.Core.Everything
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Relation.Nullary

open import Cubical.Data.List.Base

module _ {ℓ} {A : Type ℓ} where

  ++-unit-r : (xs : List A) → xs ++ [] ≡ xs
  ++-unit-r [] = refl
  ++-unit-r (x ∷ xs) = cong (_∷_ x) (++-unit-r xs)

  ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
  ++-assoc [] ys zs = refl
  ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

  rev-snoc : (xs : List A) (y : A) → rev (xs ++ [ y ]) ≡ y ∷ rev xs
  rev-snoc [] y = refl
  rev-snoc (x ∷ xs) y = cong (_++ [ x ]) (rev-snoc xs y)

  rev-++ : (xs ys : List A) → rev (xs ++ ys) ≡ rev ys ++ rev xs
  rev-++ [] ys = sym (++-unit-r (rev ys))
  rev-++ (x ∷ xs) ys =
    cong (λ zs → zs ++ [ x ]) (rev-++ xs ys)
    ∙ ++-assoc (rev ys) (rev xs) [ x ]

  rev-rev : (xs : List A) → rev (rev xs) ≡ xs
  rev-rev [] = refl
  rev-rev (x ∷ xs) = rev-snoc (rev xs) x ∙ cong (_∷_ x) (rev-rev xs)

  rev-rev-snoc : (xs : List A) (y : A) →
    Square (rev-rev (xs ++ [ y ])) (cong (_++ [ y ]) (rev-rev xs)) (cong rev (rev-snoc xs y)) refl
  rev-rev-snoc [] y = sym (lUnit refl)
  rev-rev-snoc (x ∷ xs) y i j =
    hcomp
      (λ k → λ
        { (i = i1) → compPath-filler (rev-snoc (rev xs) x) (cong (x ∷_) (rev-rev xs)) k j ++ [ y ]
        ; (j = i0) → rev (rev-snoc xs y i ++ [ x ])
        ; (j = i1) → x ∷ rev-rev-snoc xs y i k
        })
      (rev-snoc (rev-snoc xs y i) x j)

  data SnocView : List A → Type ℓ where
    nil : SnocView []
    snoc : (x : A) → (xs : List A) → (sx : SnocView xs) → SnocView (xs ∷ʳ x)

  snocView : (xs : List A) → SnocView xs
  snocView xs = helper nil xs
    where
    helper : {l : List A} -> SnocView l -> (r : List A) -> SnocView (l ++ r)
    helper {l} sl [] = subst SnocView (sym (++-unit-r l)) sl
    helper {l} sl (x ∷ r) = subst SnocView (++-assoc l (x ∷ []) r) (helper (snoc x l sl) r)

-- Path space of list type
module ListPath {ℓ} {A : Type ℓ} where

  Cover : List A → List A → Type ℓ
  Cover [] [] = Lift Unit
  Cover [] (_ ∷ _) = Lift ⊥
  Cover (_ ∷ _) [] = Lift ⊥
  Cover (x ∷ xs) (y ∷ ys) = (x ≡ y) × Cover xs ys

  reflCode : ∀ xs → Cover xs xs
  reflCode [] = lift tt
  reflCode (_ ∷ xs) = refl , reflCode xs

  encode : ∀ xs ys → (p : xs ≡ ys) → Cover xs ys
  encode xs _ = J (λ ys _ → Cover xs ys) (reflCode xs)

  encodeRefl : ∀ xs → encode xs xs refl ≡ reflCode xs
  encodeRefl xs = JRefl (λ ys _ → Cover xs ys) (reflCode xs)

  decode : ∀ xs ys → Cover xs ys → xs ≡ ys
  decode [] [] _ = refl
  decode [] (_ ∷ _) (lift ())
  decode (x ∷ xs) [] (lift ())
  decode (x ∷ xs) (y ∷ ys) (p , c) = cong₂ _∷_ p (decode xs ys c)

  decodeRefl : ∀ xs → decode xs xs (reflCode xs) ≡ refl
  decodeRefl [] = refl
  decodeRefl (x ∷ xs) = cong (cong₂ _∷_ refl) (decodeRefl xs)

  decodeEncode : ∀ xs ys → (p : xs ≡ ys) → decode xs ys (encode xs ys p) ≡ p
  decodeEncode xs _ =
    J (λ ys p → decode xs ys (encode xs ys p) ≡ p)
      (cong (decode xs xs) (encodeRefl xs) ∙ decodeRefl xs)

  isOfHLevelCover : (n : HLevel) (p : isOfHLevel (suc (suc n)) A)
    (xs ys : List A) → isOfHLevel (suc n) (Cover xs ys)
  isOfHLevelCover n p [] [] =
    isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isPropUnit)
  isOfHLevelCover n p [] (y ∷ ys) =
    isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
  isOfHLevelCover n p (x ∷ xs) [] =
    isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
  isOfHLevelCover n p (x ∷ xs) (y ∷ ys) =
    isOfHLevelΣ (suc n) (p x y) (\ _ → isOfHLevelCover n p xs ys)

isOfHLevelList : ∀ {ℓ} (n : HLevel) {A : Type ℓ}
  → isOfHLevel (suc (suc n)) A → isOfHLevel (suc (suc n)) (List A)
isOfHLevelList n ofLevel xs ys =
  isOfHLevelRetract (suc n)
    (ListPath.encode xs ys)
    (ListPath.decode xs ys)
    (ListPath.decodeEncode xs ys)
    (ListPath.isOfHLevelCover n ofLevel xs ys)

private
  variable
    ℓ : Level
    A : Type ℓ

  caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B
  caseList n _ []      = n
  caseList _ c (_ ∷ _) = c

  safe-head : A → List A → A
  safe-head x []      = x
  safe-head _ (x ∷ _) = x

  safe-tail : List A → List A
  safe-tail []       = []
  safe-tail (_ ∷ xs) = xs

cons-inj₁ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y
cons-inj₁ {x = x} p = cong (safe-head x) p

cons-inj₂ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
cons-inj₂ = cong safe-tail

¬cons≡nil : ∀ {x : A} {xs} → ¬ (x ∷ xs ≡ [])
¬cons≡nil {A = A} p = lower (subst (caseList (Lift ⊥) (List A)) p [])

¬nil≡cons : ∀ {x : A} {xs} → ¬ ([] ≡ x ∷ xs)
¬nil≡cons {A = A} p = lower (subst (caseList (List A) (Lift ⊥)) p [])

¬snoc≡nil : ∀ {x : A} {xs} → ¬ (xs ∷ʳ x ≡ [])
¬snoc≡nil {xs = []} contra = ¬cons≡nil contra
¬snoc≡nil {xs = x ∷ xs} contra = ¬cons≡nil contra

¬nil≡snoc : ∀ {x : A} {xs} → ¬ ([] ≡ xs ∷ʳ x)
¬nil≡snoc contra = ¬snoc≡nil (sym contra)

cons≡rev-snoc : (x : A) → (xs : List A) → x ∷ rev xs ≡ rev (xs ∷ʳ x)
cons≡rev-snoc _ [] = refl
cons≡rev-snoc x (y ∷ ys) = λ i → cons≡rev-snoc x ys i ++ y ∷ []

isContr[]≡[] : isContr (Path (List A) [] [])
isContr[]≡[] = refl , ListPath.decodeEncode [] []

isPropXs≡[] : {xs : List A} → isProp (xs ≡ [])
isPropXs≡[] {xs = []} = isOfHLevelSuc 0 isContr[]≡[]
isPropXs≡[] {xs = x ∷ xs} = λ p _ → ⊥.rec (¬cons≡nil p)

discreteList : Discrete A → Discrete (List A)
discreteList eqA []       []       = yes refl
discreteList eqA []       (y ∷ ys) = no ¬nil≡cons
discreteList eqA (x ∷ xs) []       = no ¬cons≡nil
discreteList eqA (x ∷ xs) (y ∷ ys) with eqA x y | discreteList eqA xs ys
... | yes p | yes q = yes (λ i → p i ∷ q i)
... | yes _ | no ¬q = no (λ p → ¬q (cons-inj₂ p))
... | no ¬p | _     = no (λ q → ¬p (cons-inj₁ q))

foldrCons : (xs : List A) → foldr _∷_ [] xs ≡ xs
foldrCons [] = refl
foldrCons (x ∷ xs) = cong (x ∷_) (foldrCons xs)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox ; ⟨ABox⟩ ; _,_ )
open import Web.Semantic.DL.ABox.Interp using
  ( Interp ; _,_ ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; _,_ ; _**_ ; ≲⌊_⌋ ; ≲-resp-ind ; _≋_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; ⊨a-resp-≲ ; ⟨ABox⟩-resp-⊨ ; *-resp-⟨ABox⟩
  ; on-bnode ; bnodes ; _⊨b_ ; _,_ )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; _⇒_w/_ ; _,_ ; BN ; impl ; impl✓ )
open import Web.Semantic.DL.Category.Object using
  ( Object ; _,_ ; IN ; iface )
open import Web.Semantic.DL.Integrity using
  ( Unique ; Mediated ; Mediator ; Initial ; _⊕_⊨_ ; _>>_ ; _,_
  ; med-≲ ; med-≋ ; med-uniq ; init-≲ ; init-⊨ ; init-med
  ; extension ; ext-⊨ ; ext-init ; ext✓ )
open import Web.Semantic.DL.KB using ( KB ; _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox ; _,_ )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans ) renaming
  ( Interp to Interp′ )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ )
open import Web.Semantic.DL.TBox.Interp.Morphism using
  ( ≲-image ; ≲-refl ; ≲-trans ; ≲-resp-≈ ) renaming
  ( _≲_ to _≲′_ )
open import Web.Semantic.Util using
  ( _⊕_⊕_ ; inode ; bnode ; enode ; left ; right ; hmerge ; _∘_ )

module Web.Semantic.DL.Category.Composition {Σ : Signature} where

infixr 5 _⟫_ _∙_

_⟫_ : ∀ {V W X Y Z} → ABox Σ (X ⊕ V ⊕ Y) → ABox Σ (Y ⊕ W ⊕ Z) →
  ABox Σ (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z)
F ⟫ G = (⟨ABox⟩ left F , ⟨ABox⟩ right G)

pipe : ∀ {V W X Y Z} →
  (J : Interp Σ (X ⊕ V ⊕ Y)) → (K : Interp Σ (Y ⊕ W ⊕ Z)) →
    (enode * J ≲ inode * K) → (Interp Σ (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z))
pipe (J , j) (K , k) (J≲K , j≲k) = (K , hmerge (≲-image J≲K ∘ j) k)

pipe-≳ : ∀ {V W X Y Z} → (I : Interp Σ X) →
  (J : Interp Σ (X ⊕ V ⊕ Y)) → (K : Interp Σ (Y ⊕ W ⊕ Z)) →
    (I≲J : I ≲ inode * J) → (J≲K : enode * J ≲ inode * K) →
      (I ≲ inode * (pipe J K J≲K))
pipe-≳ (I , i) (J , j) (K , k) (I≲J , i≲j) (J≲K , j≲k) =
  (≲-trans I≲J J≲K , λ x → ≲-resp-≈ J≲K (i≲j x))

pipe-left : ∀ {V W X Y Z} → (J : Interp Σ (X ⊕ V ⊕ Y)) →
  (K : Interp Σ (Y ⊕ W ⊕ Z)) → (J≲K : enode * J ≲ inode * K) →
    (J ≲ left * (pipe J K J≲K))
pipe-left (J , j) (K , k) (J≲K , j≲k) = (J≲K , lemma) where

  lemma : ∀ x →
    K ⊨ ≲-image J≲K (j x) ≈ hmerge (≲-image J≲K ∘ j) k (left x)
  lemma (inode x) = ≈-refl K
  lemma (bnode v) = ≈-refl K
  lemma (enode y) = j≲k y

pipe-right : ∀ {V W X Y Z} → (J : Interp Σ (X ⊕ V ⊕ Y)) →
  (K : Interp Σ (Y ⊕ W ⊕ Z)) → (J≲K : enode * J ≲ inode * K) →
    (K ≲ right * (pipe J K J≲K))
pipe-right (J , j) (K , k) (J≲K , j≲k) = (≲-refl K , lemma) where

  lemma : ∀ x →
    K ⊨ k x ≈ hmerge (≲-image J≲K ∘ j) k (right x)
  lemma (inode y) = ≈-refl K
  lemma (bnode w) = ≈-refl K
  lemma (enode z) = ≈-refl K

pipe-exp :  ∀ {V W X Y Z} → (J : Interp Σ (X ⊕ V ⊕ Y)) →
  (K : Interp Σ (Y ⊕ W ⊕ Z)) → (J≲K : enode * J ≲ inode * K) →
    ∀ KB → (enode * K ⊨ KB) → (enode * pipe J K J≲K ⊨ KB)
pipe-exp (J , j) (K , k) (J≲K , j≲k) KB K⊨KB = K⊨KB

⊨a-intro-⟫ : ∀ {V W X Y Z} → (I : Interp Σ (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z)) →
  (F : ABox Σ (X ⊕ V ⊕ Y)) → (G : ABox Σ (Y ⊕ W ⊕ Z)) →
    (left * I ⊨a F) → (right * I ⊨a G) → (I ⊨a F ⟫ G)
⊨a-intro-⟫ (I , i) F G I⊨F I⊨G =
  ( ⟨ABox⟩-resp-⊨ left (λ x → ≈-refl I) F I⊨F
  , ⟨ABox⟩-resp-⊨ right (λ x → ≈-refl I) G I⊨G )

⊨b-intro-⟫ : ∀ {V₁ W₁ V₂ W₂ X Y Z} → (I : Interp Σ (X ⊕ (V₁ ⊕ Y ⊕ W₁) ⊕ Z)) →
  (F : ABox Σ (X ⊕ V₂ ⊕ Y)) → (G : ABox Σ (Y ⊕ W₂ ⊕ Z)) →
    (left * I ⊨b F) → (right * I ⊨b G) → (I ⊨b F ⟫ G)
⊨b-intro-⟫ {V₂ = V₂} {W₂ = W₂} {Y = Y} (I , i) F G (f , I⊨F) (g , I⊨G) =
  (h , I⊨F⟫G) where

  h : (V₂ ⊕ Y ⊕ W₂) → Δ I
  h (inode v) = f v
  h (bnode y) = i (bnode (bnode y))
  h (enode w) = g w

  lemmaˡ : ∀ x →
    I ⊨ on-bnode f (i ∘ left) x ≈ on-bnode h i (left x)
  lemmaˡ (inode x) = ≈-refl I
  lemmaˡ (bnode v) = ≈-refl I
  lemmaˡ (enode y) = ≈-refl I

  lemmaʳ : ∀ x →
    I ⊨ on-bnode g (i ∘ right) x ≈ on-bnode h i (right x)
  lemmaʳ (inode x) = ≈-refl I
  lemmaʳ (bnode v) = ≈-refl I
  lemmaʳ (enode y) = ≈-refl I

  I⊨F⟫G : bnodes (I , i) h ⊨a F ⟫ G
  I⊨F⟫G = ⊨a-intro-⟫ (bnodes (I , i) h) F G
    (⊨a-resp-≲ (≲-refl I , lemmaˡ) F I⊨F)
    (⊨a-resp-≲ (≲-refl I , lemmaʳ) G I⊨G)

pipe-uniq : ∀ {V W X Y Z} I J K (M : Interp Σ (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z))
  (I≲J : I ≲ inode * J) (I≲M : I ≲ inode * M) →
    (J≲K : enode * J ≲ inode * K) (J≲M : J ≲ left * M) →
      (I≲M ≋ I≲J >> J≲M) →
        (Unique I J (left * M) I≲J I≲M) →
          (Unique (enode * J) K (right * M) J≲K (enode ** J≲M)) →
            (Unique I (pipe J K J≲K) M (pipe-≳ I J K I≲J J≲K) I≲M)
pipe-uniq {V} {W} {X} {Y} {Z} (I , i) (J , j) (K , k) (M , m)
  (I≲J , i≲j) (I≲M , i≲m) (J≲K , j≲k) (J≲M , j≲m) I≲M≋I≲J≲M J≲M-uniq K≲M-uniq
    (L≲₁M , l≲₁m) (L≲₂M , l≲₂m) I≲M≋I≲L≲₁M I≲M≋I≲L≲₂M =
      K≲M-uniq
        (L≲₁M , lemmaʳ L≲₁M l≲₁m I≲M≋I≲L≲₁M)
        (L≲₂M , lemmaʳ L≲₂M l≲₂m I≲M≋I≲L≲₂M)
        (J≲M-uniq (J≲M , j≲m)
          (≲-trans J≲K L≲₁M , lemmaˡ L≲₁M l≲₁m I≲M≋I≲L≲₁M)
          I≲M≋I≲J≲M
          I≲M≋I≲L≲₁M )
        (J≲M-uniq (J≲M , j≲m)
          ( ≲-trans J≲K L≲₂M , lemmaˡ L≲₂M l≲₂m I≲M≋I≲L≲₂M)
          I≲M≋I≲J≲M
          I≲M≋I≲L≲₂M ) where

  L : Interp′ Σ
  L = K

  l : (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z) → Δ L
  l = hmerge (≲-image J≲K ∘ j) k

  I≲L : I ≲′ L
  I≲L = ≲-trans I≲J J≲K

  lemmaˡ : ∀ L≲M → (∀ x → M ⊨ ≲-image L≲M (l x) ≈ m x) →
    (∀ x → M ⊨ ≲-image I≲M x ≈ ≲-image L≲M (≲-image I≲L x)) →
      ∀ x → M ⊨ ≲-image L≲M (≲-image J≲K (j x)) ≈ m (left x)
  lemmaˡ L≲M l≲m I≲M≋I≲L≲M (inode x) = l≲m (inode x)
  lemmaˡ L≲M l≲m I≲M≋I≲L≲M (bnode v) = l≲m (bnode (inode v))
  lemmaˡ L≲M l≲m I≲M≋I≲L≲M (enode y) =
    ≈-trans M (≲-resp-≈ L≲M (j≲k y)) (l≲m (bnode (bnode y)))

  lemmaʳ : ∀ L≲M → (∀ x → M ⊨ ≲-image L≲M (l x) ≈ m x) →
    (∀ x → M ⊨ ≲-image I≲M x ≈ ≲-image L≲M (≲-image I≲L x)) →
      ∀ x → M ⊨ ≲-image L≲M (k x) ≈ m (right x)
  lemmaʳ L≲M l≲m I≲M≋I≲L≲M (inode y) = l≲m (bnode (bnode y))
  lemmaʳ L≲M l≲m I≲M≋I≲L≲M (bnode w) = l≲m (bnode (enode w))
  lemmaʳ L≲M l≲m I≲M≋I≲L≲M (enode z) = l≲m (enode z)

pipe-mediated : ∀ {V W X Y Z} I J K (M : Interp Σ (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z))
  (I≲J : I ≲ inode * J) (I≲M : I ≲ inode * M) →
    (J≲K : enode * J ≲ inode * K) →
      (m : Mediated I J (left * M) I≲J I≲M) →
        (Mediated (enode * J) K (right * M) J≲K (enode ** (med-≲ m))) →
          (Mediated I (pipe J K J≲K) M (pipe-≳ I J K I≲J J≲K) I≲M)
pipe-mediated {V} {W} {X} {Y} {Z} (I , i) (J , j) (K , k) (M , m)
  (I≲J , i≲j) (I≲M , i≲m) (J≲K , j≲k)
    ((J≲M , j≲m) , I≲M≋I≲J≲M , J≲M-uniq)
      ((K≲M , k≲m) , J≲M≋J≲K≲M , K≲M-uniq) =
        ( (L≲M , l≲m) , I≲M≋I≲L≲M , L≲M-uniq) where

  L : Interp′ Σ
  L = K

  l : (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z) → Δ L
  l = hmerge (≲-image J≲K ∘ j) k

  I≲L : I ≲′ L
  I≲L = ≲-trans I≲J J≲K

  i≲l : ∀ x → L ⊨ ≲-image I≲L (i x) ≈ l (inode x)
  i≲l x = ≲-resp-≈ J≲K (i≲j x)

  L≲M : L ≲′ M
  L≲M = K≲M

  l≲m : ∀ x → M ⊨ ≲-image K≲M (l x) ≈ m x
  l≲m (inode x) =
    ≈-trans M (≈-sym M (J≲M≋J≲K≲M (j (inode x)))) (j≲m (inode x))
  l≲m (bnode (inode v)) =
    ≈-trans M (≈-sym M (J≲M≋J≲K≲M (j (bnode v)))) (j≲m (bnode v))
  l≲m (bnode (bnode y)) = k≲m (inode y)
  l≲m (bnode (enode w)) = k≲m (bnode w)
  l≲m (enode z) = k≲m (enode z)

  I≲M≋I≲L≲M : ∀ x → M ⊨ ≲-image I≲M x ≈ ≲-image L≲M (≲-image I≲L x)
  I≲M≋I≲L≲M x = ≈-trans M (I≲M≋I≲J≲M x) (J≲M≋J≲K≲M (≲-image I≲J x))

  L≲M-uniq : Unique (I , i) (L , l) (M , m) (I≲L , i≲l) (I≲M , i≲m)
  L≲M-uniq = pipe-uniq (I , i) (J , j) (K , k) (M , m)
    (I≲J , i≲j) (I≲M , i≲m) (J≲K , j≲k) (J≲M , j≲m)
      I≲M≋I≲J≲M J≲M-uniq K≲M-uniq

pipe-mediator : ∀ S {V W X Y Z I}
  {J : Interp Σ (X ⊕ V ⊕ Y)} {K : Interp Σ (Y ⊕ W ⊕ Z)} {I≲J J≲K} F G →
    (Mediator I J I≲J (S , F)) → (Mediator (enode * J) K J≲K (S , G)) →
      (Mediator I (pipe J K J≲K) (pipe-≳ I J K I≲J J≲K) (S , F ⟫ G))
pipe-mediator S {V} {W} {X} {Y} {Z}
  {I , i} {J , j} {K , k} {I≲J , i≲j} {J≲K , j≲k}
    F G J-med K-med (M , m) (I≲M , i≲m) (M⊨S , M⊨F , M⊨G) =
      pipe-mediated (I , i) (J , j) (K , k) (M , m)
        (I≲J , i≲j) (I≲M , i≲m) (J≲K , j≲k)
          I≲J≲M-med J≲K≲M-med where

  mˡ : (X ⊕ V ⊕ Y) → Δ M
  mˡ x = m (left x)

  mʳ : (Y ⊕ W ⊕ Z) → Δ M
  mʳ x = m (right x)

  I≲J≲M-med : Mediated (I , i) (J , j) (M , mˡ) (I≲J , i≲j) (I≲M , i≲m)
  I≲J≲M-med = J-med (M , mˡ) (I≲M , i≲m)
    (M⊨S , *-resp-⟨ABox⟩ left (M , m) F M⊨F)

  J≲M : J ≲′ M
  J≲M = ≲⌊ med-≲ I≲J≲M-med ⌋

  j≲m : ∀ x → M ⊨ ≲-image J≲M (j x) ≈ mˡ x
  j≲m = ≲-resp-ind (med-≲ I≲J≲M-med)

  j′ : Y → Δ J
  j′ y = j (enode y)

  j≲m′ : ∀ x → M ⊨ ≲-image J≲M (j′ x) ≈ m (bnode (bnode x))
  j≲m′ x = j≲m (enode x)

  J≲K≲M-med : Mediated (J , j′) (K , k) (M , mʳ) (J≲K , j≲k) (J≲M , j≲m′)
  J≲K≲M-med = K-med (M , mʳ) (J≲M , j≲m′)
    (M⊨S , *-resp-⟨ABox⟩ right (M , m) G M⊨G)

pipe-init : ∀ {S V W X Y Z I}
  {J : Interp Σ (X ⊕ V ⊕ Y)} {K : Interp Σ (Y ⊕ W ⊕ Z)} {F G} →
    (J-init : J ∈ Initial I (S , F)) →
      (K-init : K ∈ Initial (enode * J) (S , G)) →
        (pipe J K (init-≲ K-init) ∈ Initial I (S , F ⟫ G))
pipe-init {S} {V} {W} {X} {Y} {Z} {I , i} {J , j} {K , k} {F} {G}
  ((I≲J , i≲j) , (J⊨S , J⊨F) , J-med) ((J≲K , j≲k) , (K⊨S , K⊨G) , K-med) =
    ( (I≲L , i≲l) , (L⊨S , L⊨F⟫G) , L-med) where

  L : Interp′ Σ
  L = K

  l : (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z) → Δ L
  l = hmerge (≲-image J≲K ∘ j) k

  I≲L : I ≲′ L
  I≲L = ≲-trans I≲J J≲K

  i≲l : ∀ x → L ⊨ ≲-image I≲L (i x) ≈ l (inode x)
  i≲l x = ≲-resp-≈ J≲K (i≲j x)

  L⊨S : L ⊨t S
  L⊨S = K⊨S

  L⊨F⟫G : (L , l) ⊨a F ⟫ G
  L⊨F⟫G = ⊨a-intro-⟫ (L , l) F G
    (⊨a-resp-≲ (pipe-left (J , j) (K , k) (J≲K , j≲k)) F J⊨F)
    (⊨a-resp-≲ (pipe-right (J , j) (K , k) (J≲K , j≲k)) G K⊨G)

  L-med : Mediator (I , i) (L , l) (I≲L , i≲l) (S , F ⟫ G)
  L-med = pipe-mediator S F G J-med K-med

compose-⊨ : ∀ {S T V W X Y Z} A B C
  (F : ABox Σ (X ⊕ V ⊕ Y)) (G : ABox Σ (Y ⊕ W ⊕ Z)) →
    (∀ I → (I ⊨ (S , T) , A) → (I ⊕ S , F ⊨ T , B)) →
      (∀ J → (J ⊨ (S , T) , B) → (J ⊕ S , G ⊨ T , C)) →
        (∀ I → (I ⊨ (S , T) , A) → (I ⊕ S , F ⟫ G ⊨ T , C))
compose-⊨ {S} {T} {V} {W} {X} {Y} {Z} A B C F G F✓ G✓ I I⊨STA =
  ( pipe J K J≲K
  , pipe-init J-init K-init
  , pipe-exp J K J≲K (T , C) K⊨TC ) where

  I⊕SF⊨TB : I ⊕ S , F ⊨ T , B
  I⊕SF⊨TB = F✓ I I⊨STA

  J : Interp Σ (X ⊕ V ⊕ Y)
  J = extension I⊕SF⊨TB

  J-init : J ∈ Initial I (S , F)
  J-init = ext-init I⊕SF⊨TB

  J⊕SG⊨TC : enode * J ⊕ S , G ⊨ T , C
  J⊕SG⊨TC = G✓ (enode * J) (ext✓ I⊕SF⊨TB)

  K : Interp Σ (Y ⊕ W ⊕ Z)
  K = extension J⊕SG⊨TC

  K⊨TC : enode * K ⊨ (T , C)
  K⊨TC = ext-⊨ J⊕SG⊨TC

  K-init : K ∈ Initial (enode * J) (S , G)
  K-init = ext-init J⊕SG⊨TC

  J≲K : enode * J ≲ inode * K
  J≲K = init-≲ K-init

_∙′_ : ∀ {S T} {A B C : Object S T} → (F : A ⇒ B) → (G : B ⇒ C) →
  (A ⇒ C w/ (BN F ⊕ IN B ⊕ BN G))
_∙′_ {S} {T} {X , X∈Fin , A} {Y , Y∈Fin , B} {Z , Z∈Fin , C} (V , F , F✓) (W , G , G✓) =
  (F ⟫ G , compose-⊨ A B C F G F✓ G✓)

_∙_ : ∀ {S T} {A B C : Object S T} → (A ⇒ B) → (B ⇒ C) → (A ⇒ C)
F ∙ G = ( _ , F ∙′ G )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module Utility.Bool where

open import Agda.Builtin.Bool using (Bool; true; false)

not : Bool → Bool
not false = true
not true = false

_or_ : Bool → Bool → Bool
true or _ = true
_ or true = true
_ or _ = false

_and_ : Bool → Bool → Bool
true and true = true
_ and _ = false

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-# OPTIONS --no-pattern-matching #-}

id : {A : Set} (x : A) → A
id x = x

const : {A B : Set} (x : A) (y : B) → A
const x y = x

happ : {A B C : Set} (f : A → B → C) (g : A → B) (x : A) → C
happ f g x = f x (g x)

K = const
S = happ

I : {A : Set} (x : A) → A
I = S K K

-- Mmh, pretty boring...

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2013-11-07
-- Instance candidates are now considered module judgemental equality.
module Issue899 where

postulate
  A B : Set
  f : {{ x : A }} → B
  instance a : A

instance
  a' : A
  a' = a

test : B
test = f

{- The previous code fails with the following message:

  Resolve implicit argument _x_257 : A. Candidates: [a : A, a : A]

There are indeed two values in scope of type A (a and a'), but given
that they are definitionally equal, Agda should not complain about it
but just pick any one of them.  -}


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Test3 where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic

abstract
  !_ : ∀{ℓ} {X : Type ℓ} → X → X
  ! x = x

  !-≡ : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
  !-≡ = refl -- makes use of the definition of `!_` within this block

  !!_ : ∀{ℓ} {X : Type ℓ} → X → ! X
  !!_ {X = X} x = transport (sym (!-≡ {X = X})) x

  !!⁻¹_ : ∀{ℓ} {X : Type ℓ} → ! X → X
  !!⁻¹_ {X = X} x = transport (!-≡ {X = X}) x

  infix 1 !_
  infix 1 !!_
  infix 1 !!⁻¹_

-- !-≡' : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
-- !-≡' = refl -- cannot make use of the definition of `!_` anymore

hPropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
hPropRel A B ℓ' = A → B → hProp ℓ'

module TestB {ℓ ℓ'} (X : Type ℓ)
             (0ˣ : X) (_+_ _·_ : X → X → X) (_<_ : hPropRel X X ℓ')
             (let infixl 5 _+_; _+_ = _+_) where

  _≤_ : hPropRel X X ℓ'
  x ≤ y = ¬(y < x)

  postulate
    sqrt : (x : X) → {{ ! [ 0ˣ ≤ x ] }} → X
    0≤x² : ∀ x → [ 0ˣ ≤ (x · x) ]

  instance -- module-scope instances
    _ = λ {x} → !! 0≤x² x

  test4 : (x y z : X) → [ 0ˣ ≤ x ] → [ 0ˣ ≤ y ] → X
  test4 x y z 0≤x 0≤y =
    let instance -- let-scope instances
          _ = !! 0≤x
          _ = !! 0≤y
          _ = !! 0≤x² x -- preferred over the instance from module-scope
    in ( (sqrt x)       -- works
       + (sqrt y)       -- also works
       + (sqrt (z · z)) -- uses instance from module scope
       + (sqrt (x · x)) -- uses instance from let-scope (?) -- NOTE: see https://github.com/agda/agda/issues/4688
       )

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module Oscar where

import Everything
import Test

-- journals
import $RequiredForInstanceResolution
import AbstractStrictlyPositive
import AgdaErrorDisplayForm197
import AgdaFeatureInstanceResolutionViaConstraint
import AgdaFeatureNeedHiddenVariableTypeConstructorWrapper
import AgdaFeatureNoInstanceFromHidden
import AgdaFeaturePitfallInstanceResolution
import AgdaFeatureTerminationViaExplicitness
import AgdaIssue2557
import AgdaModuleEqualsSyntaxProblem
import AgdaSubstitute98Bug
import ExplicitInstanceSearchRequired
import MutualLevel
import NoEtaExpandedInstanceFromSuperclass
import NonuniqueUnification
import ReflexivityInFlexibility
import TroubleUnifyingExtensionalReflection
import UnificationIncompleteness
import UnificationRant


text:
module Coirc where
open import Coinduction
open import IO
open import Data.String
open import Data.Maybe

data SP (A B : Set) : Set where
  get : (A → SP A B) → SP A B
  put : B → ∞ (SP A B) → SP A B

data Event : Set where
  notice mode numeric ping : Event
  privmsg : (source text : String) → Event

data Action : Set where
  print : (text : String) → Action
  nick : (name : String) → Action
  user : (name real : String) → Action
  pong : (name : String) → Action
  join part : (channel : String) → Action
  privmsg : (target text : String) → Action
  quit : (text : String) → Action

Bot = SP Event Action

max_stars_repo_name: larrytheliquid/coirc

max_issues_repo_name: larrytheliquid/coirc

max_forks_repo_name: larrytheliquid/coirc


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import Functions.Definition
open import Groups.Definition
open import Rings.Homomorphisms.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Sets.EquivalenceRelations
open import Groups.Lemmas
open import Rings.Ideals.Definition

module Rings.Cosets {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) {pred : A → Set c} (ideal : Ideal R pred) where

open Ring R
open import Rings.Lemmas R
open import Groups.Subgroups.Normal.Lemmas

open import Groups.Cosets additiveGroup (Ideal.isSubgroup ideal)

open Setoid S
open Equivalence eq
open Ideal ideal
open Group additiveGroup

cosetRing : Ring cosetSetoid _+_ _*_
Ring.additiveGroup cosetRing = cosetGroup (abelianGroupSubgroupIsNormal (Ideal.isSubgroup ideal) abelianUnderlyingGroup)
Ring.*WellDefined cosetRing {r} {s} {t} {u} r=t s=u = need
  where
    r=t' : pred ((inverse t + r) * u)
    r=t' = accumulatesTimes r=t
    s=u' : pred ((inverse u + s) * r)
    s=u' = accumulatesTimes s=u
    need : pred (inverse (t * u) + (r * s))
    need = isSubset (transitive (+WellDefined (*DistributesOver+') *DistributesOver+') (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined ringMinusExtracts' (transitive (+WellDefined reflexive (transitive ringMinusExtracts' (inverseWellDefined additiveGroup *Commutative))) invRight)) identRight)) *Commutative))) (closedUnderPlus r=t' s=u')
Ring.1R cosetRing = 1R
Ring.groupIsAbelian cosetRing = isSubset (transitive (symmetric invLeft) (+WellDefined (inverseWellDefined additiveGroup groupIsAbelian) reflexive)) containsIdentity
Ring.*Associative cosetRing = isSubset (transitive (symmetric invLeft) (+WellDefined (inverseWellDefined additiveGroup *Associative) reflexive)) containsIdentity
Ring.*Commutative cosetRing {a} {b} = isSubset (transitive (symmetric invLeft) (+WellDefined (inverseWellDefined additiveGroup *Commutative) reflexive)) containsIdentity
Ring.*DistributesOver+ cosetRing = isSubset (symmetric (transitive (+WellDefined (inverseWellDefined additiveGroup (symmetric *DistributesOver+)) reflexive) invLeft)) containsIdentity
Ring.identIsIdent cosetRing = isSubset (symmetric (transitive (Group.+WellDefined additiveGroup reflexive identIsIdent) invLeft)) containsIdentity

cosetRingHom : RingHom R cosetRing id
RingHom.preserves1 cosetRingHom = isSubset (symmetric invLeft) (Ideal.containsIdentity ideal)
RingHom.ringHom cosetRingHom = isSubset (symmetric invLeft) (Ideal.containsIdentity ideal)
RingHom.groupHom cosetRingHom = cosetGroupHom (abelianGroupSubgroupIsNormal (Ideal.isSubgroup ideal) abelianUnderlyingGroup)


text:
module BasicIPC.Metatheory.Hilbert-TarskiGluedClosedImplicit where

open import BasicIPC.Syntax.Hilbert public
open import BasicIPC.Semantics.TarskiGluedClosedImplicit public

open ImplicitSyntax (∅ ⊢_) public

-- Completeness with respect to a particular model, for closed terms only.

module _ {{_ : Model}} where
  reify : ∀ {A} → ⊩ A → ∅ ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B} → ⊩ A → ⊩ B ▻ A
  ⟪K⟫ a = app ck (reify a) ⅋ K a

  ⟪S⟫′ : ∀ {A B C} → ⊩ A ▻ B ▻ C → ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ s₁ = app cs (reify s₁) ⅋ λ s₂ →
              app (app cs (reify s₁)) (reify s₂) ⅋ ⟪S⟫ s₁ s₂

  _⟪,⟫′_ : ∀ {A B} → ⊩ A → ⊩ B ▻ A ∧ B
  _⟪,⟫′_ a = app cpair (reify a) ⅋ _,_ a

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)   γ = lookup i γ
eval (app t u) γ = eval t γ ⟪$⟫ eval u γ
eval ci        γ = ci ⅋ I
eval ck        γ = ck ⅋ ⟪K⟫
eval cs        γ = cs ⅋ ⟪S⟫′
eval cpair     γ = cpair ⅋ _⟪,⟫′_
eval cfst      γ = cfst ⅋ π₁
eval csnd      γ = csnd ⅋ π₂
eval unit      γ = ∙

-- Correctness of evaluation with respect to conversion.

eval✓ : ∀ {{_ : Model}} {A Γ} {t t′ : Γ ⊢ A} → t ⋙ t′ → eval t ≡ eval t′
eval✓ refl⋙                   = refl
eval✓ (trans⋙ p q)            = trans (eval✓ p) (eval✓ q)
eval✓ (sym⋙ p)                = sym (eval✓ p)
eval✓ (congapp⋙ p q)          = cong² _⟦$⟧_ (eval✓ p) (eval✓ q)
eval✓ (congi⋙ p)              = cong I (eval✓ p)
eval✓ (congk⋙ p q)            = cong² K (eval✓ p) (eval✓ q)
eval✓ (congs⋙ p q r)          = cong³ ⟦S⟧ (eval✓ p) (eval✓ q) (eval✓ r)
eval✓ (congpair⋙ {A} {B} p q) = cong² (_⟦,⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congfst⋙ {A} {B} p)    = cong (⟦π₁⟧ {A} {B}) (eval✓ p)
eval✓ (congsnd⋙ {A} {B} p)    = cong (⟦π₂⟧ {A} {B}) (eval✓ p)
eval✓ beta▻ₖ⋙                 = refl
eval✓ beta▻ₛ⋙                 = refl
eval✓ beta∧₁⋙                 = refl
eval✓ beta∧₂⋙                 = refl
eval✓ eta∧⋙                   = refl
eval✓ eta⊤⋙                  = refl

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_ = λ P → ∅ ⊢ α P
      }

-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ∅ ⊨ A → ∅ ⊢ A
quot₀ t = reify (t ∙)

-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ∅ ⊢ A → ∅ ⊢ A
norm₀ = quot₀ ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- Code related to the paper draft "Structurally Recursive Descent
-- Parsing"
--
-- Nils Anders Danielsson and Ulf Norell
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing where

-- The code presented here is not identical to that in the paper; it
-- has evolved.

-- Parser type indices.

import StructurallyRecursiveDescentParsing.Index

-- Parsers containing non-terminals, and grammars using such parsers.

import StructurallyRecursiveDescentParsing.Grammar

-- A library of derived parser combinators.

import StructurallyRecursiveDescentParsing.Lib

-- Some small examples.

import StructurallyRecursiveDescentParsing.Examples

-- An example: parsing PBM image files.

import StructurallyRecursiveDescentParsing.PBM

-- A depth-first backend.

import StructurallyRecursiveDescentParsing.DepthFirst

-- The backend does not work directly on the parsers in
-- StructurallyRecursiveDescentParsing.Grammar. The following
-- simplified parsers are used instead. The function
-- StructurallyRecursiveDescentParsing.Grammar.⟦_⟧ turns parsers
-- containing non-terminals into simplified parsers.

import StructurallyRecursiveDescentParsing.Simplified
import StructurallyRecursiveDescentParsing.Simplified.Semantics

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module IrrelevantRecordField where
import Common.Irrelevance

record R (A : Set) : Set where
  constructor inn
  field
     .out : A

proj : {A : Set} -> R A -> A
proj (inn a) = a
-- needs to fail, since a is irrelevant under inn

max_stars_repo_name: asr/agda-kanso


text:
{-# OPTIONS --without-K --rewriting #-}

module Base where

  open import lib.Basics

  open import lib.Funext
  open import lib.NType2
  open import lib.types.Truncation
  open import lib.types.Bool

  quodlibet : {i : ULevel} {A : Type i} → ⊥ → A
  quodlibet = ⊥-elim

  -- infix notation for piping a term argument into a dependent function
  _|>_ : ∀ {i j} {A : Type i} {B : A → Type j}
        (a : A) (f : (a : A) → B a) → B a
  a |> f = f a

  -- infix notation for applying a path between two functions to an argument to give a path from f x to g x
  _at_ : ∀ {i j} {A : Type i} {P : A → Type j} {f g : Π A P} (p : f == g) → f ∼ g
  p at x = app= p x

  End : ∀ {i} (X : Type i) → Type i
  End X = X → X

  -- composition of a dependent function with a fiberwise dependent function
  infixl 80 _>>_
  _>>_ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → (B a → Type k)}
          → (f : Π A B) → (g : {a : A} → Π (B a) (C a)) → Π A (λ a → C a (f a))
  f >> g = λ x → g (f x)

  -- Crisp function types (the domain must be crisp)
  _::→_ : {@♭ i : ULevel} {j : ULevel} (@♭ A : Type i) (B : Type j) → Type (lmax i j)
  A ::→ B = (@♭ _ : A) → B

  crispen : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} {B : A → Type j}
            → ((a : A) → B a)
            → ((@♭ a : A) → B a)
  crispen f a = f a

  const : {i j : ULevel} {A : Type i} {B : Type j}
          (b : B) → A → B
  const b _ = b

  crisp-const : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i} {B : Type j}
                (b : B) → A ::→ B
  crisp-const b _ = b

  -- Crisp function extensionality (postulated for now, because I'm lazy)
  postulate
    -- domain is a crisp term of a crisp type
    ♭λ= : {@♭ i : ULevel} {j : ULevel} {@♭ A : Type i}
          {B : A → Type j} {f g : (@♭ a : A) → B a}
          (h : (@♭ a : A) → f a == g a)
          → f == g
  -- Fully crisp function extensionalty: domain and codomain are crisp types
  ♭♭λ= : {@♭ i j : ULevel} {@♭ A : Type i}
          {@♭ B : A → Type j} {@♭ f g : (@♭ a : A) → B a}
          (@♭ h : (@♭ a : A) → f a == g a)
          → f == g
  ♭♭λ= h = ♭λ= h

  -- The "identity path" is called refl
  -- refl : ∀ {i} { A : Type i} {a : A} → a == a
  pattern refl = idp

  _is-an-equiv = is-equiv

  _is-an-equivalence-because_is-inverse-by_and_ : ∀ {i} {j} {A : Type i} {B : Type j}
                                                  → (f : A → B)
                                                    (g : B → A) (f-g : (b : B) → f (g b) == b)
                                                    (g-f : (a : A) → g (f a) == a) → is-equiv f
  f is-an-equivalence-because g is-inverse-by f-g and g-f = is-eq f g f-g g-f

  _is-split-inj : {i j : ULevel} {A : Type i} {B : Type j} (s : A → B) → Type (lmax i j)
  _is-split-inj {A = A} {B = B} s = Σ (B → A) (λ r → (a : A) → r (s a) == a)

  -- Implicit and Explicit function types are equivalent

  imp-equiv-exp : {i j : ULevel} {A : Type i} {B : A → Type j}
                  → ({a : A} → B a) ≃ ((a : A) → B a)
  imp-equiv-exp = (λ f x → f {x}) ,
                    record
                    { g = λ z {x} → z x
                    ; f-g = λ b → idp
                    ; g-f = λ a → idp
                    ; adj = λ a → idp
                    }

  exp-equiv-imp : {i j : ULevel} {A : Type i} {B : A → Type j}
                  → ((a : A) → B a) ≃ ({a : A} → B a)
  exp-equiv-imp = imp-equiv-exp ⁻¹

  _⊔→_ : {i j k l : ULevel} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
          (f : A → C) (g : B → D)
          → A ⊔ B → C ⊔ D
  (f ⊔→ g) (inl a)  = inl (f a)
  (f ⊔→ g) (inr b)  = inr (g b)

  _⊔e_ : {i j k l : ULevel} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
          (f : A ≃ C) (g : B ≃ D)
          → A ⊔ B ≃ C ⊔ D
  f ⊔e g =
    equiv
      ((–> f) ⊔→ (–> g))
      ((<– f) ⊔→ (<– g))
      (λ {(inl c) → ap inl ((<–-inv-r f) c) ; (inr d) → ap inr ((<–-inv-r g) d) })
      (λ {(inl a) → ap inl ((<–-inv-l f) a) ; (inr b) → ap inr ((<–-inv-l g) b) })

  -- A non-instance version of this function because I find that instance so annoying
  ≃-preserves-level : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A ≃ B)
                      → has-level n A → has-level n B
  ≃-preserves-level e p = equiv-preserves-level e {{p}}

  -- An equivalence version of the above
  ≃-preserves-level-eq : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A ≃ B)
                          → has-level n A ≃ has-level n B
  ≃-preserves-level-eq e =
    equiv
      (≃-preserves-level e)
      (≃-preserves-level (e ⁻¹))
      (λ b → prop-path has-level-is-prop _ _)
      (λ a → prop-path has-level-is-prop _ _)

  -- An equivalence between has-level-aux and has-level
  has-level-def-eq : {i : ULevel} {A : Type i} {n : ℕ₋₂}
                      → (has-level n A) ≃ (has-level-aux n A)
  has-level-def-eq {A = A} {n = n} = equiv has-level-apply has-level-in (λ b → refl) (λ a → refl)

  -- Compositional reasoning (like equational reasoning, but for composing)
  infixr 15 _→∎
  infixr 10 _–⟨_⟩→_

  _–⟨_⟩→_ : ∀ {i j k} (A : Type i) {B : A → Type j} {C : (a : A) → B a → Type k}
            → (f : (a : A) → B a) → (g : {a : A} → (b : B a) → C a b)
            → ((a : A) → C a (f a))
  _ –⟨ f ⟩→ g = f >> g

  _→∎ : ∀ {i} (A : Type i) → A → A
  _→∎ = idf

  {-
  -- SKETCHING
  lemma : ∀ {i j} (A : Type i) (B : Type j) (a₀ : A)
          (p : (f : A → B) (a : A) → (f a₀) == (f a))
          → (const {A = A} {B = B}) is-an-equiv
  lemma A B a₀ p = is-eq const (λ f → f a₀) fro-to to-fro
    where
      to-fro : ∀ a → ((const a) a₀) == a
      to-fro a = refl

      fro-to : ∀ (f : A → B) → (const (f a₀)) == f
      fro-to f =
        λ= $
          λ a → p f a

  module _ {i j} (R : Type i) (r₀ : R) (B : Type j) (S : Type j)  where
    postulate
      σ : B → S
      contr : (γ : R → S) (r : R) → (γ r₀) == (γ r)

    _is-discrete : ∀ {k} (X : Type k) → Type _
    X is-discrete = (const {A = R} {B = X}) is-an-equiv

    S-is-discrete : S is-discrete
    S-is-discrete = lemma R S r₀ contr

  -}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
record R : Set where
  a : R
  a = r -- r should not ever be in scope

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2021-07-14, issue #5470, reported by HarrisonGrodin
--
-- Importing a rewrite rule that was declared private
-- at the point of definition caused an internal error.

{-# OPTIONS --rewriting #-}

-- {-# OPTIONS -v impossible:10 #-}
-- {-# OPTIONS -v rewriting:100 #-}

module Issue5470 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

open import Issue5470.Import

postulate
  _≤_ : (n m : Nat) → Set
  ≤-refl : ∀{n} → n ≤ n

infix 4 _IsRelatedTo_

data _IsRelatedTo_ (x : Nat) : (y : Nat) → Set where
  equals : x IsRelatedTo x

begin : ∀ {x y} → x IsRelatedTo y → x ≤ y
begin equals = ≤-refl

example : ∀ n → n ≤ bar n
example n = begin equals

-- WAS: internal error
-- Unbound name: Issue5470Import.lemma[0,10]@ModuleNameHash 8608063155492000951

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Connectedness for pointed types
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Pointed-type.Connected
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import Group equality-with-J as G using (_≃ᴳ_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
import Nat equality-with-J as Nat
open import Pointed-type equality-with-J
open import Pointed-type.Homotopy-group eq

private
  variable
    p : Level
    P : Pointed-type p

-- Connectedness.
--
-- This definition of what it means for a pointed type to be connected
-- is based on a characterisation given in the HoTT Book.

Connected : Pointed-type p → Type p
Connected (A , x) = (y : A) → ∥ x ≡ y ∥

-- The connected component of a pointed type.
--
-- I got this definition from Christian Sattler.

Connected-component : Pointed-type p → Pointed-type p
Connected-component (A , x) =
  (∃ λ y → ∥ x ≡ y ∥) , (x , ∣ refl _ ∣)

-- There is a based embedding from the connected component of P to P.
--
-- This definition was suggested to me by Christian Sattler.

Connected-component↣ᴮ : Connected-component P ↝[ embedding ]ᴮ P
Connected-component↣ᴮ =
    record { to           = proj₁
           ; is-embedding = λ x y →
               _≃_.is-equivalence $
               Eq.with-other-function
                 (x ≡ y              ↔⟨ inverse $ ignore-propositional-component T.truncation-is-proposition ⟩□
                  proj₁ x ≡ proj₁ y  □)
                 (cong proj₁)
                 proj₁-Σ-≡,≡←≡
           }
  , refl _

-- The connected component is connected.
--
-- This definition was suggested to me by Christian Sattler.

Connected-Connected-component :
  {P : Pointed-type p} →
  Connected (Connected-component P)
Connected-Connected-component y =
  flip T.∥∥-map (proj₂ y) λ eq →
    Σ-≡,≡→≡ eq (T.truncation-is-proposition _ _)

-- If P has a certain positive h-level, then the same applies to the
-- connected component of P.

H-level-Connected-component :
  ∀ {P : Pointed-type p} n →
  H-level (1 + n) (proj₁ P) →
  H-level (1 + n) (proj₁ (Connected-component P))
H-level-Connected-component {P = A , x} n =
  H-level (1 + n) A                    ↝⟨ (λ h →
                                             Σ-closure (1 + n) h λ _ →
                                             mono (Nat.suc≤suc (Nat.zero≤ n))
                                             T.truncation-is-proposition) ⟩
  H-level (1 + n) (∃ λ y → ∥ x ≡ y ∥)  □

-- If the loop space of P has a certain h-level, then the same applies
-- to the loop space of the connected component of P.

H-level-Ω-Connected-component :
  ∀ {P : Pointed-type p} n →
  H-level n (proj₁ (Ω P)) →
  H-level n (proj₁ (Ω (Connected-component P)))
H-level-Ω-Connected-component {P = _ , x} n =
  H-level n (x ≡ x)              ↝⟨ H-level-cong _ _ (ignore-propositional-component T.truncation-is-proposition) ⟩□
  H-level n ((x , _) ≡ (x , _))  □

-- The fundamental group of the connected component of P is equivalent
-- to the fundamental group of P.
--
-- This definition was suggested to me by Christian Sattler.

Fundamental-group′-Connected-component≃ᴳ :
  {s₁ : Is-set (proj₁ (Ω (Connected-component P)))}
  {s₂ : Is-set (proj₁ (Ω P))} →
  Fundamental-group′ (Connected-component P) s₁ ≃ᴳ
  Fundamental-group′ P s₂
Fundamental-group′-Connected-component≃ᴳ {P = _ , x} = λ where
  .G.Homomorphic.related →
    Eq.with-other-function
      ((x , _) ≡ (x , _)  ↔⟨ inverse $ ignore-propositional-component T.truncation-is-proposition ⟩□
       x ≡ x              □)
      (cong proj₁)
      proj₁-Σ-≡,≡←≡
  .G.Homomorphic.homomorphic p q →
    cong proj₁ (trans p q)               ≡⟨ cong-trans _ _ _ ⟩∎
    trans (cong proj₁ p) (cong proj₁ q)  ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Example:
--   postulate ℓ : Lvl.Level
--   postulate A B C D : Type{ℓ}
--   postulate a : A
--   postulate ab : A → B
--   postulate bc : B → C
--   postulate cd : C → D
--
--   ad : A → D
--   ad =
--     A ⇒-[ ab ]
--     B ⇒-[ bc ]
--     C ⇒-[ cd ]
--     D ⇒-end
--
--   d : D
--   d =
--     a ⇒
--     A ⇒-[ ab ]
--     B ⇒-[ bc ]
--     C ⇒-[ cd ]
--     D ⇒-end
module Syntax.Implication where

open import Functional using (const ; id ; _∘_ ; _∘₂_ ; _∘₃_ ; swap)
open import Logic.Propositional
import      Lvl
import      Syntax.Implication.Dependent as Dependent
open import Type

private variable ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Lvl.Level

open Dependent using (_⇒-end ; _⇒_) public

_⇒-start_ : ∀{X : Type{ℓ₁}}{Y : Type{ℓ₂}} → X → (X → Y) → Y
_⇒-start_ x xy = xy x
infixr 0.98 _⇒-start_
{-# INLINE _⇒-start_ #-}

_⇒-[_]_ : ∀(X : Type{ℓ₁}){Y : Type{ℓ₂}}{Z : Type{ℓ₃}} → (X → Y) → (Y → Z) → (X → Z)
_⇒-[_]_ _ = swap(_∘_)
infixr 0.98 _⇒-[_]_
{-# INLINE _⇒-[_]_ #-}

_⇒-[]_ : ∀(X : Type{ℓ₁}){Y : Type{ℓ₂}} → (X → Y) → (X → Y)
_⇒-[]_ _ = id
infixr 0.98 _⇒-[]_
{-# INLINE _⇒-[]_ #-}

•_•_⇒₂-[_]_ : ∀{X₁ : Type{ℓ₁}}{X₂ : Type{ℓ₂}}{Y : Type{ℓ₃}}{Z : Type{ℓ₄}} → X₁ → X₂ → (X₁ → X₂ → Y) → (Y → Z) → Z
•_•_⇒₂-[_]_ x₁ x₂ g f = (f ∘₂ g) x₁ x₂
infixr 0.97 •_•_⇒₂-[_]_
{-# INLINE •_•_⇒₂-[_]_ #-}

•_•_•_⇒₃-[_]_ : ∀{X₁ : Type{ℓ₁}}{X₂ : Type{ℓ₂}}{X₃ : Type{ℓ₃}}{Y : Type{ℓ₄}}{Z : Type{ℓ₅}} → X₁ → X₂ → X₃ → (X₁ → X₂ → X₃ → Y) → (Y → Z) → Z
•_•_•_⇒₃-[_]_ x₁ x₂ x₃ g f = (f ∘₃ g) x₁ x₂ x₃
infixr 0.97 •_•_•_⇒₃-[_]_
{-# INLINE •_•_•_⇒₃-[_]_ #-}

_⇔-end : ∀(X : Type{ℓ₁}) → (X ↔ X)
_⇔-end _ = [↔]-intro id id
infixr 0.99 _⇔-end
{-# INLINE _⇔-end #-}

_⇔_ = Functional.apply
infixl 0.97 _⇔_
{-# INLINE _⇔_ #-}

_⇔-[_]_ : ∀(X : Type{ℓ₁}){Y : Type{ℓ₂}}{Z : Type{ℓ₃}} → (X ↔ Y) → (Y ↔ Z) → (X ↔ Z)
_⇔-[_]_ _ ([↔]-intro pₗ pᵣ) ([↔]-intro qₗ qᵣ) = [↔]-intro (pₗ ∘ qₗ) (qᵣ ∘ pᵣ)
infixr 0.98 _⇔-[_]_
{-# INLINE _⇔-[_]_ #-}

_⇔-[_]-sym_ : ∀(X : Type{ℓ₁}){Y : Type{ℓ₂}}{Z : Type{ℓ₃}} → (Y ↔ X) → (Y ↔ Z) → (X ↔ Z)
_⇔-[_]-sym_ X ([↔]-intro pₗ pᵣ) q = X ⇔-[ ([↔]-intro pᵣ pₗ) ] q
infixr 0.98 _⇔-[_]-sym_
{-# INLINE _⇔-[_]-sym_ #-}

_⇔-[]_ : ∀(X : Type{ℓ₁}){Y : Type{ℓ₂}} → (X ↔ Y) → (X ↔ Y)
_⇔-[]_ _ = id
infixr 0.98 _⇔-[]_
{-# INLINE _⇔-[]_ #-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-

This file contains:

- Definitions equivalences

- Glue types

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Core.Glue where

open import Cubical.Core.Primitives

open import Agda.Builtin.Cubical.Glue public
  using ( isEquiv       -- ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ ⊔ ℓ')

        ; equiv-proof   -- ∀ (y : B) → isContr (fiber f y)

        ; _≃_           -- ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ ⊔ ℓ')

        ; equivFun      -- ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → A → B

        ; equivProof    -- ∀ {ℓ ℓ'} (T : Type ℓ) (A : Type ℓ') (w : T ≃ A) (a : A) φ →
                        -- Partial φ (fiber (equivFun w) a) → fiber (equivFun w) a

        ; primGlue      -- ∀ {ℓ ℓ'} (A : Type ℓ) {φ : I} (T : Partial φ (Type ℓ'))
                        -- → (e : PartialP φ (λ o → T o ≃ A)) → Type ℓ'

        ; prim^unglue   -- ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I} {T : Partial φ (Type ℓ')}
                        -- → {e : PartialP φ (λ o → T o ≃ A)} → primGlue A T e → A

        -- The ∀ operation on I. This is commented out as it is not currently used for anything
        -- ; primFaceForall -- (I → I) → I
        )
  renaming ( prim^glue   to glue         -- ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I} {T : Partial φ (Type ℓ')}
                                         -- → {e : PartialP φ (λ o → T o ≃ A)}
                                         -- → PartialP φ T → A → primGlue A T e

           ; pathToEquiv to lineToEquiv  -- ∀ {ℓ : I → Level} (P : (i : I) → Type (ℓ i)) → P i0 ≃ P i1
           )

private
  variable
    ℓ ℓ' : Level

-- Uncurry Glue to make it more pleasant to use
Glue : (A : Type ℓ) {φ : I}
       → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
       → Type ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

-- Make the φ argument of prim^unglue explicit
unglue : {A : Type ℓ} (φ : I) {T : Partial φ (Type ℓ')}
         {e : PartialP φ (λ o → T o ≃ A)} → primGlue A T e → A
unglue φ = prim^unglue {φ = φ}

-- People unfamiliar with [Glue], [glue] and [uglue] can find the types below more
-- informative as they demonstrate the computational behavior.
--
-- Full inference rules can be found in Section 6 of CCHM:
-- https://arxiv.org/pdf/1611.02108.pdf
-- Cubical Type Theory: a constructive interpretation of the univalence axiom
-- Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
private

  module GluePrims (A : Type ℓ) {φ : I} (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A)) where
    T : Partial φ (Type ℓ')
    T φ1 = Te φ1 .fst
    e : PartialP φ (λ φ → T φ ≃ A)
    e φ1 = Te φ1 .snd

    -- Glue can be seen as a subtype of Type that, at φ, is definitionally equal to the left type
    -- of the given equivalences.
    Glue-S : Type ℓ' [ φ ↦ T ]
    Glue-S = inS (Glue A Te)

    -- Which means partial elements of T are partial elements of Glue
    coeT→G :
      ∀ (t : PartialP φ T)
      → Partial φ (Glue A Te)
    coeT→G t (φ = i1) = t 1=1

    -- ... and elements of Glue can be seen as partial elements of T
    coeG→T :
      ∀ (g : Glue A Te)
      → PartialP φ T
    coeG→T g (φ = i1) = g

    -- What about elements that are applied to the equivalences?
    trans-e :
      ∀ (t : PartialP φ T)
      → Partial φ A
    trans-e t ϕ1 = equivFun (e ϕ1) (t ϕ1)

    -- glue gives a partial element of Glue given an element of A. Note that it "undoes"
    -- the application of the equivalences!
    glue-S :
      ∀ (t : PartialP φ T)
      → A [ φ ↦ trans-e t ]
      → Glue A Te [ φ ↦ coeT→G t ]
    glue-S t s = inS (glue t (outS s))

    -- typechecking glue enforces this, e.g. you can not simply write
    -- glue-bad : (t : PartialP φ T) → A → Glue A Te
    -- glue-bad t s = glue t s

    -- unglue does the inverse:
    unglue-S :
      ∀ (b : Glue A Te)
      → A [ φ ↦ trans-e (coeG→T b) ]
    unglue-S b = inS (unglue φ b)

  module GlueTransp (A : I → Type ℓ) (Te : (i : I) → Partial (i ∨ ~ i) (Σ[ T ∈ Type ℓ' ] T ≃ A i)) where
    A0 A1 : Type ℓ
    A0 = A i0
    A1 = A i1
    T : (i : I) → Partial (i ∨ ~ i) (Type ℓ')
    T i φ = Te i φ .fst
    e : (i : I) → PartialP (i ∨ ~ i) (λ φ → T i φ ≃ A i)
    e i φ = Te i φ .snd
    T0 T1 : Type ℓ'
    T0 = T i0 1=1
    T1 = T i1 1=1
    e0 : T0 ≃ A0
    e0 = e i0 1=1
    e1 : T1 ≃ A1
    e1 = e i1 1=1

    open import Cubical.Foundations.Prelude using (transport)
    transportA : A0 → A1
    transportA = transport (λ i → A i)

    -- copied over from Foundations/Equiv for readability, can't directly import due to cyclic dependency
    invEq : ∀ {X : Type ℓ'} {ℓ''} {Y : Type ℓ''} (w : X ≃ Y) → Y → X
    invEq w y = w .snd .equiv-proof y .fst .fst

    -- transport in Glue reduces to transport in A + the application of the equivalences in forward and backward
    -- direction.
    transp-S : (t0 : T0) → T1 [ i1 ↦ (λ _ → invEq e1 (transportA (equivFun e0 t0))) ]
    transp-S t0 = inS (transport (λ i → Glue (A i) (Te i)) t0)


text:
module Tactic.Nat.Subtract.Reflect where

open import Prelude
import Agda.Builtin.Nat as Builtin
open import Builtin.Reflection
open import Control.Monad.State
open import Control.Monad.Transformer
open import Tactic.Reflection
open import Tactic.Reflection.Quote

open import Tactic.Nat.Reflect
open import Tactic.Nat.Subtract.Exp

⟨suc⟩s : SubExp →  SubExp
⟨suc⟩s (lit n) = lit (suc n)
⟨suc⟩s (lit n ⟨+⟩ e) = lit (suc n) ⟨+⟩ e
⟨suc⟩s e = lit 1 ⟨+⟩ e

freshS : Term → R SubExp
freshS t =
  get >>= uncurry′ λ i Γ →
  var i <$ put (suc i , (t , i) ∷ Γ)

pattern _`-_ x y = def (quote Builtin._-_) (vArg x ∷ vArg y ∷ [])

private
  forceInstance : Name → Term → R ⊤
  forceInstance i v = lift $ unify v (def₀ i)
  forceNumber   = forceInstance (quote NumberNat)
  forceSemiring = forceInstance (quote SemiringNat)
  forceSubtractive = forceInstance (quote SubtractiveNat)

termToSubExpR : Term → R SubExp
termToSubExpR (a `+ b) = _⟨+⟩_ <$> termToSubExpR a <*> termToSubExpR b
termToSubExpR (a `* b) = _⟨*⟩_ <$> termToSubExpR a <*> termToSubExpR b
termToSubExpR (a `- b) = _⟨-⟩_ <$> termToSubExpR a <*> termToSubExpR b
-- Handle unsolved instances
termToSubExpR (def (quote Semiring._+_) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ vArg a ∷ vArg b ∷ [])) = do
  forceSemiring i
  ⦇ termToSubExpR a ⟨+⟩ termToSubExpR b ⦈
termToSubExpR (def (quote Semiring._*_) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ vArg a ∷ vArg b ∷ [])) = do
  lift $ unify i (def₀ (quote SemiringNat))
  ⦇ termToSubExpR a ⟨*⟩ termToSubExpR b ⦈
termToSubExpR (def (quote Subtractive._-_) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ vArg a ∷ vArg b ∷ [])) = do
  forceSubtractive i
  ⦇ termToSubExpR a ⟨-⟩ termToSubExpR b ⦈
termToSubExpR (def (quote Semiring.zro) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ [])) = do
  forceSemiring i
  pure (lit 0)
termToSubExpR (def (quote Semiring.one) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ [])) = do
  forceSemiring i
  pure (lit 1)
termToSubExpR (def (quote Number.fromNat) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ vArg a ∷ _ ∷ [])) = do
  forceNumber i
  termToSubExpR a
termToSubExpR `0       = pure (lit 0)
termToSubExpR (`suc a) = ⟨suc⟩s <$> termToSubExpR a
termToSubExpR (meta x _) = lift (blockOnMeta x)
termToSubExpR (lit (nat n)) = pure (lit n)
termToSubExpR unknown  = fail
termToSubExpR t = do
  lift $ ensureNoMetas t
  just i ← gets (flip lookup t ∘ snd)
    where nothing → freshS t
  pure (var i)

termToSubEqR : Term → R (SubExp × SubExp)
termToSubEqR (lhs `≡ rhs) = _,_ <$> termToSubExpR lhs <*> termToSubExpR rhs
termToSubEqR (def (quote _≡_) (_ ∷ hArg (meta x _) ∷ _)) = lift (blockOnMeta x)
termToSubEqR _ = fail

termToSubEq : Term → TC (Maybe ((SubExp × SubExp) × List Term))
termToSubEq t = runR (termToSubEqR t)

pattern _`<_ a b = def (quote LessNat) (vArg a ∷ vArg b ∷ [])

termToSubEqnR : Term → R Eqn
termToSubEqnR (def (quote Ord._<_) (_ ∷ _ ∷ vArg i@(meta _ _) ∷ vArg lhs ∷ vArg rhs ∷ [])) = do
  forceInstance (quote OrdNat) i
  ⦇ termToSubExpR lhs :< termToSubExpR rhs ⦈
termToSubEqnR (lhs `< rhs) = _:<_ <$> termToSubExpR lhs <*> termToSubExpR rhs
termToSubEqnR (lhs `≡ rhs) = _:≡_ <$> termToSubExpR lhs <*> termToSubExpR rhs
termToSubEqnR (def (quote _≡_) (_ ∷ hArg (meta x _) ∷ _)) = lift (blockOnMeta x)
termToSubEqnR t = lift (ensureNoMetas t) *> fail

termToSubEqn : Term → TC (Maybe (Eqn × List Term))
termToSubEqn t = runR (termToSubEqnR t)

private
  lower : Nat → Term → R Term
  lower 0 = pure
  lower i = liftMaybe ∘ strengthen i

termToSubHypsR′ : Nat → Term → R (List Eqn)
termToSubHypsR′ i (pi (vArg hyp) (abs _ a)) =
  _∷_ <$> (termToSubEqnR =<< lower i hyp) <*> termToSubHypsR′ (suc i) a
termToSubHypsR′ _ (meta x _) = lift (blockOnMeta x)
termToSubHypsR′ i a = [_] <$> (termToSubEqnR =<< lower i a)

termToSubHypsR : Term → R (List Eqn)
termToSubHypsR = termToSubHypsR′ 0

termToSubHyps : Term → TC (Maybe (List Eqn × List Term))
termToSubHyps t = runR (termToSubHypsR t)

instance
  QuotableSubExp : Quotable SubExp
  ` {{QuotableSubExp}} (var x) = con (quote SubExp.var) (vArg (` x) ∷ [])
  ` {{QuotableSubExp}} (lit n) = con (quote SubExp.lit) (vArg (` n) ∷ [])
  ` {{QuotableSubExp}} (e ⟨+⟩ e₁) = con (quote SubExp._⟨+⟩_) (map defaultArg $ ` e ∷ ` e₁ ∷ [])
  ` {{QuotableSubExp}} (e ⟨-⟩ e₁) = con (quote SubExp._⟨-⟩_) (map defaultArg $ ` e ∷ ` e₁ ∷ [])
  ` {{QuotableSubExp}} (e ⟨*⟩ e₁) = con (quote SubExp._⟨*⟩_) (map defaultArg $ ` e ∷ ` e₁ ∷ [])

  QuotableEqn : Quotable Eqn
  ` {{QuotableEqn}} (a :≡ b) = con (quote _:≡_) (vArg (` a) ∷ vArg (` b) ∷ [])
  ` {{QuotableEqn}} (a :< b) = con (quote _:<_) (vArg (` a) ∷ vArg (` b) ∷ [])

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

record R₁ (F : Set → Set) : Set₁ where
  constructor mkR₁
  field
    f₁ : ∀ {A} → A → F A

open R₁ {{...}}

record R₂ (F : Set → Set) : Set₁ where
  constructor mkR₂
  field
    instance
      r₁ : R₁ F

record R₃ (_ : Set) : Set where
  constructor mkR₃

postulate
  instance
    r₃ : R₂ R₃

  A : Set
  a : A

record R₄ : Set where
  constructor c
  field
    f₂ : A

postulate
  F : (r₄ : R₄) → c a ≡ r₄ → Set

G : Set → Set
G _ = F _ (refl {x = f₁ a})

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Relation.Binary.Core

module PLRTree.DropLast.Heap {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_)  where

open import PLRTree {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.Heap _≤_

lemma-dropLast-≤* : {x : A}{t : PLRTree} → x ≤* t → x ≤* dropLast t
lemma-dropLast-≤* {x} (lf≤* .x) = lf≤* x
lemma-dropLast-≤* (nd≤* {perfect} {x} {y} {l} {r} x≤y x≤*l x≤*r)
    with r
... | leaf = x≤*r
... | node _ _ _ _ = nd≤* x≤y x≤*l (lemma-dropLast-≤* x≤*r)
lemma-dropLast-≤* (nd≤* {left} {x} {y} {l} {r} x≤y x≤*l x≤*r)
    with l | x≤*l | dropLast l | lemma-dropLast-≤* x≤*l
... | leaf | _ | _ | _ = lf≤* x
... | node perfect _ _ _ | _ | node perfect y' l' r' | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node perfect _ _ _ | _ | leaf | (lf≤* .x) = nd≤* x≤y (lf≤* x) x≤*r
... | node perfect _ _ _ | _ | node left _ _ _ | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node perfect _ _ _ | _ | node right _ _ _ | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node left _ _ _ | _ | node perfect y' l' r' | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node left _ _ _ | _ | leaf | (lf≤* .x) = nd≤* x≤y (lf≤* x) x≤*r
... | node left _ _ _ | _ | node left _ _ _ | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node left _ _ _ | _ | node right _ _ _ | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node right _ _ _ | _ | node perfect y' l' r' | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node right _ _ _ | _ | leaf | (lf≤* .x) = nd≤* x≤y (lf≤* x) x≤*r
... | node right _ _ _ | _ | node left _ _ _ | x≤*dll = nd≤* x≤y x≤*dll x≤*r
... | node right _ _ _ | _ | node right _ _ _ | x≤*dll = nd≤* x≤y x≤*dll x≤*r
lemma-dropLast-≤* (nd≤* {right} {x} {y} {l} {r} x≤y x≤*l x≤*r)
    with r
... | leaf = nd≤* x≤y x≤*r x≤*r
... | node perfect y' l' r' = nd≤* x≤y (lemma-dropLast-≤* x≤*l) x≤*r
... | node left _ _ _ = nd≤* x≤y x≤*l  (lemma-dropLast-≤* x≤*r)
... | node right _ _ _ = nd≤* x≤y x≤*l  (lemma-dropLast-≤* x≤*r)

lemma-dropLast-heap : {t : PLRTree} → Heap t → Heap (dropLast t)
lemma-dropLast-heap leaf = leaf
lemma-dropLast-heap (node {perfect} {x} {l} {r} x≤*l x≤*r hl hr)
    with r
... | leaf = hr
... | node _ _ _ _ = node x≤*l (lemma-dropLast-≤* x≤*r) hl (lemma-dropLast-heap hr)
lemma-dropLast-heap (node {left} {x} {l} {r} x≤*l x≤*r hl hr)
    with l | x≤*l | hl | dropLast l | lemma-dropLast-≤* x≤*l | lemma-dropLast-heap hl
... | leaf | _ | _ | _ | _ | _ = leaf
... | node perfect _ _ _ |  _ | _ | node perfect y' l' r' | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node perfect _ _ _ |  _ | _ | leaf | (lf≤* .x) | leaf = node (lf≤* x) x≤*r leaf hr
... | node perfect _ _ _ |  _ | _ | node left _ _ _ | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node perfect _ _ _ |  _ | _ | node right _ _ _ | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node left _ _ _ | _ | _ | node perfect y' l' r' | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node left _ _ _  |  _ | _ | leaf | (lf≤* .x) | leaf = node (lf≤* x) x≤*r leaf hr
... | node left _ _ _  |  _ | _ | node left _ _ _ | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node left _ _ _  |  _ | _ | node right _ _ _ | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node right _ _ _ |  _ | _ | node perfect y' l' r' | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node right _ _ _ |  _ | _ | leaf | (lf≤* .x) | leaf = node (lf≤* x) x≤*r leaf hr
... | node right _ _ _ |  _ | _ | node left _ _ _ | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
... | node right _ _ _ |  _ | _ | node right _ _ _ | x≤*dll | hdll = node x≤*dll x≤*r hdll hr
lemma-dropLast-heap (node {right} {x} {l} {r} x≤*l x≤*r hl hr)
    with r
... | leaf = node x≤*r x≤*r hr hr
... | node perfect y' l' r' = node (lemma-dropLast-≤* x≤*l) x≤*r (lemma-dropLast-heap hl) hr
... | node left _ _ _ = node x≤*l (lemma-dropLast-≤* x≤*r) hl (lemma-dropLast-heap hr)
... | node right _ _ _ = node x≤*l (lemma-dropLast-≤* x≤*r) hl (lemma-dropLast-heap hr)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
data D : Set where
  @0 c : D

postulate
  P : D → Set
  p : (x : D) → P x

bad : P c
bad = p _

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Datalog where
open import Data.Nat as ℕ
open import Data.List
open import Data.Integer as ℤ
open import Relation.Binary.PropositionalEquality
open import Data.List.Any

module Term where
  data tt : Set where
    τ-int : tt

  open Membership (setoid tt)

  ctx = List tt

  data Lit : tt → Set where
    int : ℤ → Lit τ-int

  data Expr {τ : tt} {{ Γ : ctx }} {{ Δ : ctx }} : Set where
    lit   : (Lit τ) → Expr {τ}
    e-var : (τ ∈ Γ) → Expr {τ}
    a-var : (τ ∈ Δ) → Expr {τ}

module Program where

  at = List Term.tt

  open Membership (setoid at)

  ctx = List at

  data PartialAtom {Γ : Term.ctx} {Δ : Term.ctx} {Ρ : ctx} (ρ : at) : Set where
    predicate : (ρ ∈ Ρ) → PartialAtom ρ
    apply : ∀ {τ : Term.tt} → PartialAtom {Γ} {Δ} {Ρ} (τ ∷ ρ) → Term.Expr {τ} ⦃ Γ ⦄ ⦃ Δ ⦄ → PartialAtom {Γ} {Δ} {Ρ} ρ

  data Atom {Γ : Term.ctx} {Δ : Term.ctx} ⦃ Ρ : ctx ⦄ : Set where
    close : PartialAtom {Γ} {Δ} {Ρ} [] → Atom

  data Rule {Ρ : ctx} : Set where
    -- Here, we should also be checking that the rhs uses Γ to make it a relevant ctx
    -- when used in the universal position
    -- I don't think I need that property for proofs yet, so it can wait
    rule : {Γ : Term.ctx} → Atom {Γ} {[]} → List (Atom {[]} {Γ}) → Rule

  Program : {Ρ : ctx} → Set
  Program {Ρ} = List (Rule {Ρ})

  data Derivable {Ρ} : Program {Ρ} → Atom {[]} {[]} → Set where

{-
  Proof sketch:
  0.) match as an assumed-correct-primitive
  1.) Proof of upper bound : prog, ∀ r ∈ prog. ∀ db. ∀ s ∈ match db r.body. subst s r.head ∈ upper
  2.) semantics : p : Program → db → ∀ a ∈ db. Derivable Ρ prog a → upper → (∀ r ∈ p. ∀ vdb. ∀ s ∈ match vdb r.body. let h = subst s r.head in (h ∈ upper) || (h ∈ db))
      a.) Go through prog, trying to generate the proof of termination
      b.) If on any rule you fail, take the failing fact:
          i.) Move the fact from upper to db
          ii.) Add derivability proof for the fact you just derived (look up the matched facts derivation and build up)
          iii.) Fix up the completeness term by demonstrating that if all that happened moved from upper to db, the property is just as true
  3.) Proof of correctness is:
      db, ∀ a ∈ db. Derivable {Ρ} prog a, ∀ r ∈ prog. ∀ s ∈ match db r.body. subst s r.head ∈ db
      e.g. database, proof that database is sound, proof that database is complete
-}

max_stars_repo_name: maurer/holmes

max_issues_repo_name: maurer/holmes

max_forks_repo_name: maurer/holmes