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

open import Sets.EquivalenceRelations
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)
open import Setoids.Setoids
open import Groups.Definition
open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Numbers.Naturals.Semiring
open import Groups.Lemmas

module Groups.FreeProduct.Group {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) {a b : _} {A : I → Set a} {S : (i : I) → Setoid {a} {b} (A i)} {_+_ : (i : I) → (A i) → (A i) → A i} (decidableGroups : (i : I) → (x y : A i) → ((Setoid._∼_ (S i) x y)) || ((Setoid._∼_ (S i) x y) → False)) (G : (i : I) → Group (S i) (_+_ i)) where

open import Groups.FreeProduct.Definition decidableIndex decidableGroups G
open import Groups.FreeProduct.Setoid decidableIndex decidableGroups G
open import Groups.FreeProduct.Addition decidableIndex decidableGroups G

private
  plus'WDlemm : {i : I} (x1 x2 : ReducedSequenceBeginningWith i) (y : ReducedSequence) → (=RP' x1 x2) → plus' x1 y =RP plus' x2 y
  plus'WDlemm (ofEmpty i g nonZero) (ofEmpty .i g₁ nonZero₁) y x1=x2 with decidableIndex i i
  plus'WDlemm (ofEmpty i g nonZero) (ofEmpty .i h nonZero2) y x1=x2 | inl refl = prependWD g h nonZero nonZero2 y x1=x2
  plus'WDlemm (prependLetter i g nonZero {j} x1 x) (prependLetter .i h nonZero2 {j2} x2 pr) y x1=x2 with decidableIndex i i
  ... | inl refl with decidableIndex j j2
  plus'WDlemm (prependLetter i g nonZero {j} x1 x) (prependLetter .i h nonZero2 {.j} x2 pr) y x1=x2 | inl refl | inl refl = Equivalence.transitive (Setoid.eq freeProductSetoid) {prepend i g nonZero (plus' x1 y)} {prepend i h nonZero2 (plus' x1 y)} {plus' (prependLetter i h nonZero2 x2 pr) y} (prependWD g h nonZero nonZero2 (plus' x1 y) (_&&_.fst x1=x2)) (prependWD' h nonZero2 (plus' x1 y) (plus' x2 y) (plus'WDlemm x1 x2 y (_&&_.snd x1=x2)))
  ... | inr j!=j2 = exFalso (notEqualIfStartDifferent j!=j2 x1 x2 (_&&_.snd x1=x2))
  plus'WDlemm _ _ _ _ | inr bad = exFalso (bad refl)

  plus'WD : {i j : I} (x1 : ReducedSequenceBeginningWith i) (x2 : ReducedSequenceBeginningWith j) (y : ReducedSequence) → (=RP' x1 x2) → plus' x1 y =RP plus' x2 y
  plus'WD {i} {j} x1 x2 y x1=x2 with decidableIndex i j
  plus'WD {i} {.i} x1 x2 y x1=x2 | inl refl = plus'WDlemm x1 x2 y x1=x2
  plus'WD {i} {j} x1 x2 y x1=x2 | inr x = exFalso (notEqualIfStartDifferent x x1 x2 x1=x2)
  plusWD : (m n o p : ReducedSequence) → (m =RP o) → (n =RP p) → (m +RP n) =RP (o +RP p)
  plusWD empty empty empty empty m=o n=p = record {}
  plusWD empty (nonempty i x) empty (nonempty i₁ x₁) m=o n=p = n=p
  plusWD (nonempty i x) empty (nonempty j y) empty m=o record {} = Equivalence.transitive (Setoid.eq freeProductSetoid) {plus' x empty} {nonempty i x} {plus' y empty} (plusEmptyRight x) (Equivalence.transitive (Setoid.eq freeProductSetoid) {nonempty i x} {nonempty j y} {plus' y empty} m=o (Equivalence.symmetric (Setoid.eq freeProductSetoid) {plus' y empty} {nonempty j y} (plusEmptyRight y)))
  plusWD (nonempty i1 x1) (nonempty i2 x2) (nonempty i3 x3) (nonempty i4 x4) m=o n=p = (Equivalence.transitive (Setoid.eq freeProductSetoid)) {plus' x1 (nonempty i2 x2)} {plus' x3 (nonempty i2 x2)} {plus' x3 (nonempty i4 x4)} (plus'WD x1 x3 (nonempty i2 x2) m=o) (plus'WD' x3 (nonempty i2 x2) (nonempty i4 x4) n=p)

  prependAssocLemma' : {i : I} {g : A i} .(nz : Setoid._∼_ (S i) g (Group.0G (G i)) → False) (b c : ReducedSequence) → (prepend i g nz b +RP c) =RP prepend i g nz (b +RP c)
  prependAssocLemma' {i} {g} nz empty c = Equivalence.reflexive (Setoid.eq freeProductSetoid) {prepend i g _ c}
  prependAssocLemma' {i} nz (nonempty k x) c with decidableIndex i k
  prependAssocLemma' {.k} {g1} nz (nonempty k (ofEmpty .k g nonZero)) c | inl refl with decidableGroups k ((k + g1) g) (Group.0G (G k))
  prependAssocLemma' {.k} {g1} nz (nonempty k (ofEmpty .k g nonZero)) c | inl refl | inl eq1 = Equivalence.symmetric (Setoid.eq freeProductSetoid) {prepend k g1 _ (prepend k g _ c)} {c} (prependFrom' g1 g eq1 c nz nonZero)
  prependAssocLemma' {.k} {g1} nz (nonempty k (ofEmpty .k g nonZero)) c | inl refl | inr neq1 = (prependFrom g1 g neq1 c nz nonZero)
  prependAssocLemma' {.k} {g1} nz (nonempty k (prependLetter .k g nonZero x x₁)) c | inl refl with decidableGroups k ((k + g1) g) (Group.0G (G k))
  prependAssocLemma' {.k} {g1} nz (nonempty k (prependLetter .k g nonZero x x₁)) c | inl refl | inl eq1 = Equivalence.symmetric (Setoid.eq freeProductSetoid) {prepend k g1 _ (prepend k g _ (plus' x c))} {plus' x c} (prependFrom' g1 g eq1 (plus' x c) nz nonZero)
  prependAssocLemma' {.k} {g1} nz (nonempty k (prependLetter .k g nonZero x x₁)) c | inl refl | inr neq1 = prependFrom g1 g neq1 (plus' x c) nz nonZero
  prependAssocLemma' {i} {g} nz (nonempty k x) c | inr i!=k = Equivalence.reflexive (Setoid.eq freeProductSetoid) {prepend i g _ (plus' x c)}

  plusAssocLemma : {i : I} (x : ReducedSequenceBeginningWith i) (b c : ReducedSequence) → (plus' x b +RP c) =RP plus' x (b +RP c)
  plusAssocLemma (ofEmpty i g nonZero) empty c = Equivalence.reflexive (Setoid.eq freeProductSetoid) {prepend i g _ c}
  plusAssocLemma (ofEmpty i g nonZero) (nonempty j b) c with decidableIndex i j
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (ofEmpty .i g₁ nonZero₁)) c | inl refl with decidableIndex i i
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (ofEmpty .i h nonZero₁)) c | inl refl | inl refl with decidableGroups i ((i + g) h) (Group.0G (G i))
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (ofEmpty .i h nonZero₁)) c | inl refl | inl refl | inl t = Equivalence.symmetric (Setoid.eq freeProductSetoid) {prepend i g _ (prepend i h _ c)} {c} (prependFrom' g h t c _ _)
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (ofEmpty .i h nonZero₁)) c | inl refl | inl refl | inr t = prependFrom g h t c _ _
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (ofEmpty .i g₁ nonZero₁)) c | inl refl | inr bad = exFalso (bad refl)
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (prependLetter .i h nonZero₁ b x)) c | inl refl with decidableGroups i ((i + g) h) (Group.0G (G i))
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (prependLetter .i h nonZero₁ b x)) c | inl refl | inl eq1 = Equivalence.symmetric (Setoid.eq freeProductSetoid) {prepend i g _ (prepend i h _ (plus' b c))} {plus' b c} (prependFrom' g h eq1 (plus' b c) _ _)
  plusAssocLemma (ofEmpty i g nonZero) (nonempty .i (prependLetter .i h nonZero₁ b x)) c | inl refl | inr neq1 = prependFrom g h neq1 (plus' b c) nonZero _
  plusAssocLemma (ofEmpty i g nonZero) (nonempty j b) c | inr i!=j = Equivalence.reflexive (Setoid.eq freeProductSetoid) {prepend i g _ (plus' b c)}
  plusAssocLemma (prependLetter i g nonZero {j} w i!=j) b c = Equivalence.transitive (Setoid.eq freeProductSetoid) {prepend i g _ (plus' w b) +RP c} {prepend i g _ (plus' w b +RP c)} {prepend i g _ (plus' w (b +RP c))} (prependAssocLemma' nonZero (plus' w b) c) (prependWD' g nonZero (plus' w b +RP c) (plus' w (b +RP c)) (plusAssocLemma w b c))

  plusAssoc : (a b c : ReducedSequence) → ((a +RP b) +RP c) =RP (a +RP (b +RP c))
  plusAssoc empty b c = Equivalence.reflexive (Setoid.eq freeProductSetoid) {b +RP c}
  plusAssoc (nonempty i x) b c = plusAssocLemma x b c

private
  inv' : {i : I} (x : ReducedSequenceBeginningWith i) → ReducedSequence
  inv' (ofEmpty i g nonZero) = nonempty i (ofEmpty i (Group.inverse (G i) g) (λ pr → nonZero (Equivalence.transitive (Setoid.eq (S i)) (swapInv (G i) pr) (invIdent (G i)))))
  inv' (prependLetter i g nonZero {j} w i!=j) = (inv' w) +RP injection (Group.inverse (G i) g) (λ pr → nonZero (Equivalence.transitive (Setoid.eq (S i)) (swapInv (G i) pr) (invIdent (G i))))

  inv : (x : ReducedSequence) → ReducedSequence
  inv empty = empty
  inv (nonempty i w) = inv' w

private
  abstract
    lemma1 : {i j k : I} (i!=j : (i ≡ j) → False) (g : A i) (h : A j) (w : ReducedSequenceBeginningWith k) (j!=k : (j ≡ k) → False) → .(pr : _) .(pr2 : _) .(pr3 : _) → (prepend i (Group.inverse (G i) g) pr (nonempty i (prependLetter i g pr2 (prependLetter j h pr3 w j!=k) i!=j))) =RP nonempty j (prependLetter j h pr3 w j!=k)
    lemma1 {i} {j} {k} i!=j g h r j!=k pr pr2 pr3 with decidableIndex i i
    ... | inr x = exFalso (x refl)
    lemma1 {i} {j} {k} i!=j g h r j!=k pr pr2 pr3 | inl refl with decidableGroups i ((i + Group.inverse (G i) g) g) (Group.0G (G i))
    ... | inr bad = exFalso (bad (Group.invLeft (G i)))
    lemma1 {i} {j} {k} i!=j g h r j!=k pr pr2 pr3 | inl refl | inl eq1 with decidableIndex j j
    ... | inr bad = exFalso (bad refl)
    ... | inl refl = Equivalence.reflexive (Setoid.eq (S j)) ,, =RP'reflex r

  abstract
    lemma2 : {j k : I} (j!=k : (j ≡ k) → False) (h : A j) (w : ReducedSequenceBeginningWith k) .(pr : _) .(pr2 : _) → (prepend j (Group.inverse (G j) h) pr (nonempty j (prependLetter j h pr2 w j!=k))) =RP (nonempty k w)
    lemma2 {j} {k} j!=k h r pr pr2 with decidableIndex j j
    ... | inr bad = exFalso (bad refl)
    lemma2 {j} {k} j!=k h r pr pr2 | inl refl with decidableGroups j ((j + Group.inverse (G j) h) h) (Group.0G (G j))
    ... | inr bad = exFalso (bad (Group.invLeft (G j)))
    ... | inl x = =RP'reflex r

  abstract
    unpeel : (k : ReducedSequence) {j : I} (g : A j) .(pr : _) .(pr2 : _) → k =RP empty → (prepend j g pr (k +RP (nonempty j (ofEmpty j (Group.inverse (G j) g) pr2)))) =RP empty
    unpeel empty {j} g pr pr2 x with decidableIndex j j
    ... | inr bad = exFalso (bad refl)
    unpeel empty {j} g pr pr2 x | inl refl with decidableGroups j ((j + g) (Group.inverse (G j) g)) (Group.0G (G j))
    ... | inl _ = record {}
    ... | inr bad = exFalso (bad (Group.invRight (G j)))

  abstract
    invRight' : {i : I} (x : ReducedSequenceBeginningWith i) → ((nonempty i x) +RP inv (nonempty i x)) =RP empty
    invRight' {i} (ofEmpty _ g nonZero) with decidableIndex i i
    ... | inr x = exFalso (x refl)
    invRight' {i} (ofEmpty _ g nonZero) | inl refl with decidableGroups i ((i + g) (Group.inverse (G i) g)) (Group.0G (G i))
    ... | inr x = exFalso (x (Group.invRight (G i)))
    ... | inl x = record {}
    invRight' {j} (prependLetter _ g nonZero {k} (ofEmpty .k h nonZero1) j!=k) with decidableIndex k j
    ... | inl x = exFalso (j!=k (equalityCommutative x))
    invRight' {j} (prependLetter _ g nonZero {k} (ofEmpty .k h nonZero1) j!=k) | inr _ with decidableIndex k k
    ... | inr x = exFalso (x refl)
    invRight' {j} (prependLetter _ g nonZero {k} (ofEmpty .k h nonZero1) j!=k) | inr _ | inl refl with decidableGroups k ((k + h) (Group.inverse (G k) h)) (Group.0G (G k))
    ... | inr x = exFalso (x (Group.invRight (G k)))
    invRight' {j} (prependLetter _ g nonZero {k} (ofEmpty .k h nonZero1) j!=k) | inr _ | inl refl | inl _ with decidableIndex j j
    ... | inr x = exFalso (x refl)
    invRight' {j} (prependLetter _ g nonZero {k} (ofEmpty .k h nonZero1) j!=k) | inr _ | inl refl | inl _ | inl refl with decidableGroups j ((j + g) (Group.inverse (G j) g)) (Group.0G (G j))
    ... | inr bad = exFalso (bad (Group.invRight (G j)))
    ... | inl r = record {}
    invRight' {j} (prependLetter _ g nonZero {k} (prependLetter .k h nonZero1 {i} x k!=i) j!=k) rewrite refl {x = 0} = Equivalence.transitive (Setoid.eq freeProductSetoid) {prepend j g _ (prepend k h _ (plus' x ((inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) _)) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) _))))} {prepend j g nonZero (prepend k h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t)))) +RP (nonempty j (ofEmpty j (Group.inverse (G j) g) λ t → nonZero (invZeroImpliesZero (G j) t))))} {empty} (prependWD' g nonZero (prepend k h nonZero1 (plus' x ((inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) _)) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) λ t → nonZero (invZeroImpliesZero (G j) t))))) (prepend k h _ (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t)))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) λ i → nonZero (invZeroImpliesZero (G j) i))) (Equivalence.symmetric (Setoid.eq freeProductSetoid) {(prepend k h _ (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) _))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) _))} {prepend k h _ (plus' x ((inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) _)) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) _)))} t)) (unpeel (prepend k h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) _)))) g nonZero (λ t → nonZero (invZeroImpliesZero (G j) t)) (Equivalence.transitive (Setoid.eq freeProductSetoid) {prepend k h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t))))} {prepend k h nonZero1 ((plus' x (inv' x)) +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t)))} {empty} (prependWD' h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t)))) (plus' x (inv' x) +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t))) (Equivalence.symmetric (Setoid.eq freeProductSetoid) {plus' x (inv' x) +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G k) t))} (plusAssoc (nonempty _ x) (inv' x) (nonempty k (ofEmpty k (Group.inverse (G k) h) (λ t → nonZero1 (invZeroImpliesZero (G k) t))))))) (unpeel (plus' x (inv' x)) h nonZero1 (λ t → nonZero1 (invZeroImpliesZero (G k) t)) (invRight' x))))
      where
        t : (prepend k h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) (λ t → nonZero1 (invZeroImpliesZero (G _) t))))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) (λ t → nonZero (invZeroImpliesZero (G j) t)))) =RP (prepend k h nonZero1 (plus' x ((inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) (λ t → nonZero1 (invZeroImpliesZero (G _) t)))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) (λ t → nonZero (invZeroImpliesZero (G j) t))))))
        t = Equivalence.transitive (Setoid.eq freeProductSetoid) {(prepend k h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) (λ t → nonZero1 (invZeroImpliesZero (G _) t))))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) (λ t → nonZero (invZeroImpliesZero (G j) t))))} {prepend k h _ (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G _) t))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) λ t → nonZero (invZeroImpliesZero (G _) t)))} {(prepend k h nonZero1 (plus' x ((inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) (λ t → nonZero1 (invZeroImpliesZero (G _) t)))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) (λ t → nonZero (invZeroImpliesZero (G j) t))))))} (prependAssocLemma' {k} {h} nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) _))) (nonempty j (ofEmpty j (Group.inverse (G j) g) _))) (prependWD' h nonZero1 (plus' x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G _) t))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) λ t → nonZero (invZeroImpliesZero (G _) t))) (plus' x ((inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G _) t))) +RP nonempty j (ofEmpty j (Group.inverse (G j) g) λ t → nonZero (invZeroImpliesZero (G _) t)))) (plusAssocLemma x (inv' x +RP nonempty k (ofEmpty k (Group.inverse (G k) h) λ t → nonZero1 (invZeroImpliesZero (G _) t))) (nonempty j (ofEmpty j (Group.inverse (G j) g) λ t → nonZero (invZeroImpliesZero (G _) t)))))

  abstract
    invRight : (x : ReducedSequence) → (x +RP (inv x)) =RP empty
    invRight empty = record {}
    invRight (nonempty i w) = invRight' {i} w

  abstract
    invLeft' : {i : I} (x : ReducedSequenceBeginningWith i) → (inv (nonempty i x) +RP (nonempty i x)) =RP empty
    invLeft' {i} (ofEmpty .i g nonZero) with decidableIndex i i
    invLeft' {i} (ofEmpty .i g nonZero) | inl refl with decidableGroups i ((i + Group.inverse (G i) g) g) (Group.0G (G i))
    ... | inl good = record {}
    ... | inr bad = exFalso (bad (Group.invLeft (G i) {g}))
    invLeft' {i} (ofEmpty .i g nonZero) | inr x = exFalso (x refl)
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) with decidableIndex j i
    ... | inl pr = exFalso (i!=j (equalityCommutative pr))
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) | inr pr with decidableIndex i i
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) | inr pr | inl refl with decidableGroups i ((i + Group.inverse (G i) g) g) (Group.0G (G i))
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) | inr pr | inl refl | inl k with decidableIndex j j
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j h nonZero₁) i!=j) | inr pr | inl refl | inl k | inl refl with decidableGroups j ((j + Group.inverse (G j) h) h) (Group.0G (G j))
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j h nonZero₁) i!=j) | inr pr | inl refl | inl k | inl refl | inl good = record {}
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j h nonZero₁) i!=j) | inr pr | inl refl | inl k | inl refl | inr bad = exFalso (bad (Group.invLeft (G j)))
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) | inr pr | inl refl | inl k | inr bad = exFalso (bad refl)
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) | inr pr | inl refl | inr k = exFalso (k (Group.invLeft (G i) {g}))
    invLeft' {i} (prependLetter .i g nonZero {.j} (ofEmpty j g₁ nonZero₁) i!=j) | inr pr | inr bad = exFalso (bad refl)
    invLeft' {i} (prependLetter .i g nonZero {.j} (prependLetter j h nonZero1 {k} w x) i!=j) = Equivalence.transitive (Setoid.eq freeProductSetoid) {(((inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) +RP nonempty i (ofEmpty i (Group.inverse (G i) g) _)) +RP nonempty i (prependLetter i g _ (prependLetter j h _ w x) i!=j))} {_} {empty} (plusAssoc (inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) (nonempty i (ofEmpty i (Group.inverse (G i) g) _)) (nonempty i (prependLetter i g _ (prependLetter j h _ w x) i!=j))) (Equivalence.transitive (Setoid.eq freeProductSetoid) {((inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) +RP (prepend i (Group.inverse (G i) g) _ (nonempty i (prependLetter i g _ (prependLetter j h _ w x) i!=j))))} {(inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) +RP (nonempty j (prependLetter j h nonZero1 w x))} {empty} (plusWD (inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) (prepend i (Group.inverse (G i) g) _ (nonempty i (prependLetter i g _ (prependLetter j h _ w x) i!=j))) (inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) (nonempty j (prependLetter j h _ w x)) (Equivalence.reflexive (Setoid.eq freeProductSetoid) {inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)}) (lemma1 {i} {j} {k} i!=j g h w x (λ p → nonZero (invZeroImpliesZero (G i) p)) nonZero nonZero1)) (Equivalence.transitive (Setoid.eq freeProductSetoid) {(inv' w +RP nonempty j (ofEmpty j (Group.inverse (G j) h) _)) +RP nonempty j (prependLetter j h _ w x)} {inv' w +RP (nonempty j (ofEmpty j (Group.inverse (G j) h) λ p → nonZero1 (invZeroImpliesZero (G j) p)) +RP nonempty j (prependLetter j h nonZero1 w x))} {empty} (plusAssoc (inv' w) (nonempty j (ofEmpty j (Group.inverse (G j) h) _)) (nonempty j (prependLetter j h _ w x))) (Equivalence.transitive (Setoid.eq freeProductSetoid) {inv' w +RP (prepend j (Group.inverse (G j) h) _ (nonempty j (prependLetter j h nonZero1 w x)))} {inv' w +RP (nonempty k w)} {empty} (plusWD (inv' w) (prepend j (Group.inverse (G j) h) _ (nonempty j (prependLetter j h nonZero1 w x))) (inv' w) (nonempty k w) (Equivalence.reflexive (Setoid.eq freeProductSetoid) {inv' w}) (lemma2 {j} {k} x h w (λ p → nonZero1 (invZeroImpliesZero (G j) p)) nonZero1)) (invLeft' {k} w))))

  abstract
    invLeft : (x : ReducedSequence) → ((inv x) +RP x) =RP empty
    invLeft empty = record {}
    invLeft (nonempty i w) = invLeft' {i} w

FreeProductGroup : Group freeProductSetoid _+RP_
Group.+WellDefined FreeProductGroup {m} {n} {x} {y} m=x n=y = plusWD m n x y m=x n=y
Group.0G FreeProductGroup = empty
Group.inverse FreeProductGroup = inv
Group.+Associative FreeProductGroup {a} {b} {c} = Equivalence.symmetric (Setoid.eq freeProductSetoid) {(a +RP b) +RP c} {a +RP (b +RP c)} (plusAssoc a b c)
Group.identRight FreeProductGroup {empty} = Equivalence.reflexive (Setoid.eq freeProductSetoid) {empty}
Group.identRight FreeProductGroup {nonempty i x} rewrite refl {x = 0} = plusEmptyRight x
Group.identLeft FreeProductGroup {empty} = Equivalence.reflexive (Setoid.eq freeProductSetoid) {empty}
Group.identLeft FreeProductGroup {nonempty i x} = Equivalence.reflexive (Setoid.eq freeProductSetoid) {nonempty i x}
Group.invLeft FreeProductGroup {x} = invLeft x
Group.invRight FreeProductGroup {x} = invRight x


text:
------------------------------------------------------------------------------
-- Conversion rules for the greatest common divisor
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module LTC-PCF.Program.GCD.Total.ConversionRules where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Program.GCD.Total.GCD

------------------------------------------------------------------------------

private
  -- Before to prove some properties for the gcd it is convenient to
  -- descompose the behavior of the function step by step.

  -- Initially, we define the possible states (gcd-s₁, gcd-s₂,
  -- ...). Then we write down the proof for the execution step from
  -- the state p to the state q, e.g.
  --
  -- proof₂₋₃ : ∀ m n → gcd-s₂ m n → gcd-s₃ m n.

  -- The functions gcd-00, gcd-S0, gcd-0S, gcd-Sm>Sn and gcd-Sm≯Sn
  -- show the use of the states gcd-s₁, gcd-s₂, ..., and the proofs
  -- associated with the execution steps.

  ----------------------------------------------------------------------------
  -- The steps

  -- Initially, the conversion rule fix-eq is applied.
  gcd-s₁ : D → D → D
  gcd-s₁ m n = gcdh (fix gcdh) · m · n

  -- First argument application.
  gcd-s₂ : D → D
  gcd-s₂ m = lam (λ n →
               if (iszero₁ n)
                 then m
                 else (if (iszero₁ m)
                         then n
                         else (if (gt m n)
                                 then fix gcdh · (m ∸ n) · n
                                 else fix gcdh · m · (n ∸ m))))

  -- Second argument application.
  gcd-s₃ : D → D → D
  gcd-s₃ m n = if (iszero₁ n)
                 then m
                 else (if (iszero₁ m)
                         then n
                         else (if (gt m n)
                                 then fix gcdh · (m ∸ n) · n
                                 else fix gcdh · m · (n ∸ m)))

  -- First if_then_else_ iszero₁ n = b.
  gcd-s₄ : D → D → D → D
  gcd-s₄ m n b = if b
                   then m
                   else (if (iszero₁ m)
                           then n
                           else (if (gt m n)
                                   then fix gcdh · (m ∸ n) · n
                                   else fix gcdh · m · (n ∸ m)))

  -- First if_then_else_ when if true ...
  gcd-s₅ : D → D
  gcd-s₅ m = m

  -- First if_then_else_ when if false ...
  gcd-s₆ : D → D → D
  gcd-s₆ m n = if (iszero₁ m)
                 then n
                 else (if (gt m n)
                         then fix gcdh · (m ∸ n) · n
                         else fix gcdh · m · (n ∸ m))

  -- Second if_then_else_ iszero₁ m = b.
  gcd-s₇ : D → D → D → D
  gcd-s₇ m n b = if b
                   then n
                   else (if (gt m n)
                           then fix gcdh · (m ∸ n) · n
                           else fix gcdh · m · (n ∸ m))

  -- Second if_then_else_ when if false ...
  gcd-s₈ : D → D → D
  gcd-s₈ m n = if (gt m n)
                  then fix gcdh · (m ∸ n) · n
                  else fix gcdh · m · (n ∸ m)

  -- Third if_then_else_ gt m n = b.
  gcd-s₉ : D → D → D → D
  gcd-s₉ m n b = if b then fix gcdh · (m ∸ n) · n else fix gcdh · m · (n ∸ m)

  ----------------------------------------------------------------------------
  -- Congruence properties

  gcd-s₉Cong₃ : ∀ {m n b b'} → b ≡ b' → gcd-s₉ m n b ≡ gcd-s₉ m n b'
  gcd-s₉Cong₃ refl = refl

  ----------------------------------------------------------------------------
  -- The execution steps

  {-

  To prove the execution steps, e.g.

  proof₃₋₄ : ∀ m n → gcd-s₃ m n → gcd_s₄ m n,

  we usually need to prove that

                         C [m] ≡ C [n] (1)

  given that
                             m ≡ n,    (2)

  where (2) is a conversion rule usually.
  We prove (1) using

  subst : ∀ {x y} (D : A → Set) → x ≡ y → P x → P y

  where
   • P is given by λ m → C [m ] ≡ C [n],
   • x ≡ y is given n ≡ m (actually, we use sym (m ≡ n)) and
   • P x is given by C [n] ≡ C [n] (i.e. refl).
  -}

  proof₀₋₁ : ∀ m n → fix gcdh · m · n ≡ gcd-s₁ m n
  proof₀₋₁ m n = subst (λ x → x · m · n ≡ gcdh (fix gcdh) · m · n)
                       (sym (fix-eq gcdh))
                       refl

  proof₁₋₂ : ∀ m n → gcd-s₁ m n ≡ gcd-s₂ m · n
  proof₁₋₂ m n = subst (λ x → x · n ≡ gcd-s₂ m · n)
                       (sym (beta gcd-s₂ m))
                       refl

  proof₂₋₃ : ∀ m n → gcd-s₂ m · n ≡ gcd-s₃ m n
  proof₂₋₃ m n = beta (gcd-s₃ m) n

  -- 25 April 2014. Failed with Andreas' --without-K.
  proof₃₋₄ : ∀ m n b → iszero₁ n ≡ b → gcd-s₃ m n ≡ gcd-s₄ m n b
  proof₃₋₄ m n .(iszero₁ n) refl = refl

  proof₄₊ : ∀ m n → gcd-s₄ m n true ≡ gcd-s₅ m
  proof₄₊ m _ = if-true (gcd-s₅ m)

  proof₄₋₆ : ∀ m n → gcd-s₄ m n false ≡ gcd-s₆ m n
  proof₄₋₆ m n = if-false (gcd-s₆ m n)

  proof₆₋₇ : ∀ m n b → iszero₁ m ≡ b → gcd-s₆ m n ≡ gcd-s₇ m n b
  proof₆₋₇ m n .(iszero₁ m) refl = refl

  proof₇₊ : ∀ m n → gcd-s₇ m n true ≡ n
  proof₇₊ _ n = if-true n

  proof₇₋₈ : ∀ m n → gcd-s₇ m n false ≡ gcd-s₈ m n
  proof₇₋₈ m n = if-false (gcd-s₈ m n)

  proof₈₋₉ : ∀ m n b → gt m n ≡ b → gcd-s₈ m n ≡ gcd-s₉ m n b
  proof₈₋₉ m n b = gcd-s₉Cong₃

  proof₉₊ : ∀ m n → gcd-s₉ m n true ≡ fix gcdh · (m ∸ n) · n
  proof₉₊ m n = if-true (fix gcdh · (m ∸ n) · n)

  proof₉₋ : ∀ m n → gcd-s₉ m n false ≡ fix gcdh · m · (n ∸ m)
  proof₉₋ m n = if-false (fix gcdh · m · (n ∸ m))

------------------------------------------------------------------------------
-- The five equations for gcd

-- First equation.
gcd-00 : gcd zero zero ≡ zero
gcd-00 =
  gcd zero zero         ≡⟨ proof₀₋₁ zero zero ⟩
  gcd-s₁ zero zero      ≡⟨ proof₁₋₂ zero zero ⟩
  gcd-s₂ zero · zero    ≡⟨ proof₂₋₃ zero zero ⟩
  gcd-s₃ zero zero      ≡⟨ proof₃₋₄ zero zero true iszero-0 ⟩
  gcd-s₄ zero zero true ≡⟨ proof₄₊ zero zero ⟩
  zero                  ∎

-- Second equation.
gcd-S0 : ∀ n → gcd (succ₁ n) zero ≡ succ₁ n
gcd-S0 n =
  gcd (succ₁ n) zero         ≡⟨ proof₀₋₁ (succ₁ n) zero ⟩
  gcd-s₁ (succ₁ n) zero      ≡⟨ proof₁₋₂ (succ₁ n) zero ⟩
  gcd-s₂ (succ₁ n) · zero    ≡⟨ proof₂₋₃ (succ₁ n) zero ⟩
  gcd-s₃ (succ₁ n) zero      ≡⟨ proof₃₋₄ (succ₁ n) zero true iszero-0 ⟩
  gcd-s₄ (succ₁ n) zero true ≡⟨ proof₄₊ (succ₁ n) zero ⟩
  succ₁ n                    ∎

-- Third equation.
gcd-0S : ∀ n → gcd zero (succ₁ n) ≡ succ₁ n
gcd-0S n =
  gcd zero (succ₁ n)          ≡⟨ proof₀₋₁ zero (succ₁ n) ⟩
  gcd-s₁ zero (succ₁ n)       ≡⟨ proof₁₋₂ zero (succ₁ n) ⟩
  gcd-s₂ zero · (succ₁ n)     ≡⟨ proof₂₋₃ zero (succ₁ n) ⟩
  gcd-s₃ zero (succ₁ n)       ≡⟨ proof₃₋₄ zero (succ₁ n) false (iszero-S n) ⟩
  gcd-s₄ zero (succ₁ n) false ≡⟨ proof₄₋₆ zero (succ₁ n) ⟩
  gcd-s₆ zero (succ₁ n)       ≡⟨ proof₆₋₇ zero (succ₁ n) true iszero-0 ⟩
  gcd-s₇ zero (succ₁ n) true  ≡⟨ proof₇₊  zero (succ₁ n) ⟩
  succ₁ n                     ∎

-- Fourth equation.
gcd-S>S : ∀ m n → succ₁ m > succ₁ n →
          gcd (succ₁ m) (succ₁ n) ≡ gcd (succ₁ m ∸ succ₁ n) (succ₁ n)

gcd-S>S m n Sm>Sn =
  gcd (succ₁ m) (succ₁ n)
    ≡⟨ proof₀₋₁ (succ₁ m) (succ₁ n) ⟩
  gcd-s₁ (succ₁ m) (succ₁ n)
    ≡⟨ proof₁₋₂ (succ₁ m) (succ₁ n) ⟩
  gcd-s₂ (succ₁ m) · (succ₁ n)
    ≡⟨ proof₂₋₃ (succ₁ m) (succ₁ n) ⟩
  gcd-s₃ (succ₁ m) (succ₁ n)
    ≡⟨ proof₃₋₄ (succ₁ m) (succ₁ n) false (iszero-S n) ⟩
  gcd-s₄ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₄₋₆ (succ₁ m) (succ₁ n) ⟩
  gcd-s₆ (succ₁ m) (succ₁ n)
    ≡⟨ proof₆₋₇ (succ₁ m) (succ₁ n) false (iszero-S m) ⟩
  gcd-s₇ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₇₋₈ (succ₁ m) (succ₁ n) ⟩
  gcd-s₈ (succ₁ m) (succ₁ n)
    ≡⟨ proof₈₋₉ (succ₁ m) (succ₁ n) true Sm>Sn ⟩
  gcd-s₉ (succ₁ m) (succ₁ n) true
    ≡⟨ proof₉₊  (succ₁ m) (succ₁ n) ⟩
  fix gcdh · (succ₁ m ∸ succ₁ n) · succ₁ n ∎

-- Fifth equation.
gcd-S≯S : ∀ m n → succ₁ m ≯ succ₁ n →
          gcd (succ₁ m) (succ₁ n) ≡ gcd (succ₁ m) (succ₁ n ∸ succ₁ m)
gcd-S≯S m n Sm≯Sn =
  gcd (succ₁ m) (succ₁ n)
    ≡⟨ proof₀₋₁ (succ₁ m) (succ₁ n) ⟩
  gcd-s₁ (succ₁ m) (succ₁ n)
    ≡⟨ proof₁₋₂ (succ₁ m) (succ₁ n) ⟩
  gcd-s₂ (succ₁ m) · (succ₁ n)
    ≡⟨ proof₂₋₃ (succ₁ m) (succ₁ n) ⟩
  gcd-s₃ (succ₁ m) (succ₁ n)
    ≡⟨ proof₃₋₄ (succ₁ m) (succ₁ n) false (iszero-S n) ⟩
  gcd-s₄ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₄₋₆ (succ₁ m) (succ₁ n) ⟩
  gcd-s₆ (succ₁ m) (succ₁ n)
    ≡⟨ proof₆₋₇ (succ₁ m) (succ₁ n) false (iszero-S m) ⟩
  gcd-s₇ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₇₋₈ (succ₁ m) (succ₁ n) ⟩
  gcd-s₈ (succ₁ m) (succ₁ n)
    ≡⟨ proof₈₋₉ (succ₁ m) (succ₁ n) false Sm≯Sn ⟩
  gcd-s₉ (succ₁ m) (succ₁ n) false
    ≡⟨ proof₉₋ (succ₁ m) (succ₁ n) ⟩
  fix gcdh · succ₁ m · (succ₁ n ∸ succ₁ m) ∎

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module sortedLists where

open import lib

{- we use internal verification to define a datatype of sorted lists
   of natural numbers, where typing ensures that the lists are truly
   sorted in non-decreasing order.

   A list of type (sortedList n) is sorted and guaranteed to have
   all its data greater than or equal to n; so n is a lower bound
   on the data in the list.  Keeping this lower bound explicit in
   the type enables us to require a proof of a constant-time check,
   namely d ≤ n, when insert d into a list with lower-bound n.  For
   cons nodes, we allow the lower-bound to be less than the head of
   the list.  This is needed for merge below.

   There are three constructors:

   -- nil, as usual (empty list)
   -- cons, as usual (build a new list from head and tail)
   -- weaken, decrease the lower bound (this was missing in my first
      attempt, which led to nasty problems in the case of merge below)

 -}

data sortedList : ℕ → Set where
  nil : ∀ (n : ℕ) → sortedList n  -- empty lists can have any lower bound you like
  cons : ∀ (d : ℕ) → -- the head of the list
           {n : ℕ} → -- the lower-bound for the tail
           sortedList n → -- the tail of the list, with lower bound n on its data
           d ≤ n ≡ tt → {- proof that d is less than or equal to that lower bound, and
                           hence less than or equal to all data in the tail -}
           sortedList d -- d is the lower bound for the new list created by the cons
  weaken : ∀ (n : ℕ) {n' : ℕ} → sortedList n' → n ≤ n' ≡ tt → sortedList n

-- fill in the holes below, just to help you get a feel for how the sortedList datatype works
-- [5 points]
simple : sortedList 1
simple = weaken 1 (cons 2 (nil 3) refl)refl

{- glb stands for greatest lower bound.  min d n is the greatest
   lower bound of d and n, in the sense that if any other d' is a lower bound
   of both d and n, then it is also a lower bound of min d n.  (Ideas from
   basic lattice theory.)

   To prove this, you will run into a mess if you case split on d', d, or n.
   Instead, you should consider cases for whether or not d < n.  You can use
   "with" for this, as discussed in Section 4.3.3 (page 86) of the book.
   -}
-- [10 points]
glb : ∀ d' d n → d' ≤ d ≡ tt → d' ≤ n ≡ tt → d' ≤ min d n ≡ tt
glb d' d n x y with keep (d < n)
... | tt , p rewrite p = x
... | ff , p rewrite p = y
{- insert d xs should insert d into xs as the right position to keep the list
   sorted.

   So you will case split on xs (the sortedList), and in the cons case,
   consider whether the data you are inserting is ≤ the data at the head of the
   list.

   I found I needed to use the "with keep" idiom; see Section 4.3.3 (page 90).

   Another hint: I also needed a few theorems from nat-thms.agda in the IAL:

     <≤, min-mono2, <ff

  Note that you can pattern match on implicit arguments, for example for a cons, like this:

  (cons d' {n} xs x)

  The {n} is used to match on that implicit lower-bound for the sortedList xs.

  [15 points]
-}

insert : ∀ (d : ℕ) → {n : ℕ} → sortedList n → sortedList (min d n)
insert d (nil n) with keep ( d < n )
... | tt , p rewrite p = cons d (nil n) (<≤ {d} p)
... | ff , p rewrite p = weaken n (cons d (nil d) (≤-refl d)) (<ff {d} p)

insert d (cons d1 {n} xs x) with keep ( d < d1 )
... | tt , p rewrite p = cons d ( cons d1 {n} xs x ) ( <≤ {d} {d1} p )
... | ff , p rewrite p  = cons d1 (nil d) (<ff {d} {d1} p )

insert d (weaken d1 {n} xs x) with keep ( d < d1 )
... | tt , p rewrite p =  cons d ( weaken d1 xs x ) ( <≤ {d} p )
... | ff , p rewrite p = weaken d1 (insert d xs) (glb d1 d n (<ff {d} p) x)
{- Write code to merge two sorted lists.

   I found I needed these lemmas from the IAL:

   min-<1, min-<2, <ff, <≤

   Additionally, I found I could save myself some cases by considering these cases for two input lists:

     nil and ys

     xs and nil

     weaken and ys

     xs and weaken

     cons and cons

   This is just five cases, instead of the nine that would be required if you considered the three
   cases for the first list simultaneously with the three for the second (3 * 3 gives 9 cases).
   You will see light gray highlighting on the patterns in the cases if you do this, but that
   is ok (it is just Agda warning you that you are not breaking out all the cases explicitly).

   [20 points]
-}
merge : ∀ {n : ℕ} → sortedList n → {m : ℕ} → sortedList m → sortedList (min n m)
merge (nil d) (nil d1) with keep ( d < d1 )
... | tt , p rewrite p = weaken d (nil d1) (<≤ {d} p)
... | ff , p rewrite p = weaken d1 (nil d) (<ff {d} p)
merge (nil d) (cons d1 d1s pd1) with keep ( d < d1 )
... | tt , p rewrite p = weaken d (cons d1 d1s pd1 ) ( <≤ {d} p)
... | ff , p rewrite p = cons d1 d1s pd1
merge ( nil d ) ( weaken d1 d1s pd1 ) with keep ( d < d1 )
... | tt , p rewrite p = weaken d ( weaken d1 d1s pd1 ) ( <≤ {d} p )
... | ff , p rewrite p = weaken d1 d1s pd1
merge ( cons d ds pd ) ( nil d1 ) with keep ( d < d1 )
... | tt , p rewrite p = cons d ds pd
... | ff , p rewrite p = weaken d1 ( cons d ds pd ) ( <ff {d} p )
merge ( cons d {dn} ds pd ) ( cons d1 {d1n} d1s pd1 ) with keep ( d < d1 )
... | tt , p rewrite p = cons d ( merge ds ( cons d1 d1s pd1 ) ) ( glb d dn d1 pd ( <≤ {d} p ) )
... | ff , p rewrite p = cons d1 ( merge d1s ( cons d ds pd) ) ( glb d1 d1n d pd1 ( <ff {d} p ) )
merge ( cons d {dn} ds pd ) ( weaken d1 {d1n} d1s pd1 ) with keep ( d < d1 )
... | tt , p rewrite p = cons d ( merge ds ( weaken d1 d1s pd1 ) ) ( glb d dn d1 pd ( <≤ {d} p ) )
... | ff , p rewrite p = weaken d1 ( merge d1s ( cons d ds pd ) ) ( glb d1 d1n d pd1 ( <ff {d} p ) )
merge ( weaken d ds pd ) ( nil d1 ) with keep ( d < d1 )
... | tt , p rewrite p = weaken d ds pd
... | ff , p rewrite p = weaken d1 ( weaken d ds pd ) ( <ff {d} p )
merge ( weaken d {dn} ds pd ) ( cons d1 {d1n} d1s pd1 ) with keep ( d < d1 )
... | tt , p rewrite p = weaken d ( merge ds ( cons d1 d1s pd1 ) ) ( glb d dn d1 pd ( <≤ {d} p ) )
... | ff , p rewrite p = cons d1 ( merge d1s ( weaken d ds pd ) ) ( glb d1 d1n d pd1 ( <ff {d} p ) )
merge ( weaken d {dn} ds pd ) ( weaken d1 {d1n} d1s pd1 ) with keep ( d < d1 )
... | tt , p rewrite p = weaken d ( merge ds ( weaken d1 d1s pd1 ) ) ( glb d dn d1 pd ( <≤ {d} p ) )
... | ff , p rewrite p = weaken d1 ( merge d1s ( weaken d ds pd ) ) ( glb d1 d1n d pd1 ( <ff {d} p ) )


text:
-- Andreas, 2016-06-01, issue 1997 reported by Andres

{-# OPTIONS --rewriting #-}

infix  4 _≡_
infixl 6 _+_

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

{-# BUILTIN REWRITE _≡_ #-}

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + m = m
suc n + m = suc (n + m)

plus0 : (x : ℕ) → x + zero ≡ x
plus0 zero    = refl
plus0 (suc x) = cong suc (plus0 x)

{-# REWRITE plus0 #-}
{-# REWRITE plus0 #-}

-- Should complain about duplicate rewrite rule

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 Mergesort.Impl2.Correctness.Order {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Data.List
open import Function using (_∘_)
open import List.Sorted _≤_
open import Mergesort.Impl2 _≤_ tot≤
open import OList _≤_
open import OList.Properties _≤_

theorem-mergesort-sorted : (xs : List A) → Sorted (forget (mergesort xs))
theorem-mergesort-sorted = lemma-olist-sorted  ∘ mergesort

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import Categories.Category
open import Categories.Functor

module Categories.Diagram.Limit.Properties
       {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′}  where

open import Function.Equality using (Π)
open import Relation.Binary using (Setoid)

open import Categories.Category.Instance.Setoids
open import Categories.Diagram.Cone.Properties
open import Categories.Functor.Hom
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; module ≃)
open import Categories.Morphism.Reasoning C
open import Categories.Morphism C

import Categories.Category.Construction.Cones as Con
import Categories.Diagram.Limit as Lim

open Π
open Hom C

private
  module J = Category J
  module C = Category C

  open C
  variable
    X Y Z : Obj
    f g h : X ⇒ Y

open HomReasoning

-- Hom functor preserves limits in C
module _ (W : Obj) {F : Functor J C} (lim : Lim.Limit F) where
  private
    module F  = Functor F
    module LF = Lim F
    module CF = Con F
    module lim = LF.Limit lim
    open lim
    HomF : Functor J (Setoids ℓ e)
    HomF = Hom[ W ,-] ∘F F

    module LHomF = Lim HomF
    module CHomF = Con HomF

  hom-resp-limit : LHomF.Limit
  hom-resp-limit = record
    { terminal = record
      { ⊤        = ⊤
      ; !        = !
      ; !-unique = !-unique
      }
    }
    where ⊤ : CHomF.Cone
          ⊤ = record
            { N    = hom-setoid {W} {apex}
            ; apex = record
              { ψ       = λ X → record
                { _⟨$⟩_ = λ f → proj X ∘ f
                ; cong  = ∘-resp-≈ʳ
                }
              ; commute = λ {X Y} f {h i} eq → begin
                F.F₁ f ∘ (proj X ∘ h) ∘ C.id ≈⟨ center⁻¹ (limit-commute f) identityʳ ⟩
                proj Y ∘ h                   ≈⟨ refl⟩∘⟨ eq ⟩
                proj Y ∘ i                   ∎
              }
            }

          KW : (K : CHomF.Cone) → Setoid.Carrier (CHomF.Cone.N K) → CF.Cone
          KW K x = record
            { N    = W
            ; apex = record
              { ψ       = λ X → K.ψ X ⟨$⟩ x
              ; commute = λ f → sym (∘-resp-≈ʳ identityʳ) ○ K.commute f (Setoid.refl K.N)
              }
            }
            where module K = CHomF.Cone K

          ! : ∀ {K : CHomF.Cone} → CHomF.Cones [ K , ⊤ ]
          ! {K} = record
            { arr     = record
              { _⟨$⟩_ = λ x → rep (KW K x)
              ; cong  = λ {x y} eq → LF.ψ-≈⇒rep-≈ W (CF.Cone.apex (KW K x)) (CF.Cone.apex (KW K y)) lim
                                                  (λ A → cong (K.ψ A) eq)
              }
            ; commute = λ {X} {x y} eq → begin
              proj X ∘ rep (KW K x) ≈⟨ lim.commute ⟩
              K.ψ X ⟨$⟩ x           ≈⟨ cong (K.ψ X) eq ⟩
              K.ψ X ⟨$⟩ y           ∎
            }
            where module K = CHomF.Cone K

          !-unique : ∀ {K : CHomF.Cone} (f : CHomF.Cones [ K , ⊤ ]) → CHomF.Cones [ ! ≈ f ]
          !-unique {K} f {x} {y} x≈y = begin
            rep (KW K x) ≈⟨ terminal.!-unique f′ ⟩
            f.arr ⟨$⟩ x  ≈⟨ cong f.arr x≈y ⟩
            f.arr ⟨$⟩ y  ∎
            where module K = CHomF.Cone K
                  module f = CHomF.Cone⇒ f

                  f′ : CF.Cones [ KW K x , limit ]
                  f′ = record
                    { arr     = f.arr ⟨$⟩ x
                    ; commute = f.commute (Setoid.refl K.N)
                    }

-- natural isomorphisms respects limits
module _ {F G : Functor J C} (F≃G : F ≃ G) where
  private
    module F  = Functor F
    module G  = Functor G
    module LF = Lim F
    module LG = Lim G
    open NaturalIsomorphism F≃G

  ≃-resp-lim : LF.Limit → LG.Limit
  ≃-resp-lim L = record
    { terminal = record
      { ⊤        = record
        { apex = record
          { ψ       = λ j → ⇒.η j ∘ proj j
          ; commute = λ {X Y} f → begin
            G.F₁ f ∘ ⇒.η X ∘ proj X   ≈⟨ pullˡ (⇒.sym-commute f) ⟩
            (⇒.η Y ∘ F.F₁ f) ∘ proj X ≈⟨ pullʳ (limit-commute f) ⟩
            ⇒.η Y ∘ proj Y            ∎
          }
        }
      ; !        = λ {A} → record
        { arr     = rep (nat-map-Cone F⇐G A)
        ; commute = λ {j} → assoc ○ ⟺ (switch-tofromˡ (record { iso = iso j }) (⟺ commute))
        }
      ; !-unique = λ {K} f →
        let module f = Con.Cone⇒ G f
        in terminal.!-unique record
          { arr     = f.arr
          ; commute = λ {j} → switch-fromtoˡ (record { iso = iso j }) (sym-assoc ○ f.commute)
          }
      }
    }
    where open LF.Limit L

  ≃⇒Cone⇒ : ∀ (Lf : LF.Limit) (Lg : LG.Limit) → Con.Cones G [ LG.Limit.limit (≃-resp-lim Lf) , LG.Limit.limit Lg ]
  ≃⇒Cone⇒ Lf Lg = rep-cone (LG.Limit.limit (≃-resp-lim Lf))
    where open LG.Limit Lg

≃⇒lim≅ : ∀ {F G : Functor J C} (F≃G : F ≃ G) (Lf : Lim.Limit F) (Lg : Lim.Limit G) → Lim.Limit.apex Lf ≅ Lim.Limit.apex Lg
≃⇒lim≅ {F = F} {G} F≃G Lf Lg = record
  { from = arr (≃⇒Cone⇒ F≃G Lf Lg)
  ; to   = arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)
  ; iso  = record
    { isoˡ = Lf.terminal.⊤-id record
      { commute = λ {j} → begin
        Lf.proj j ∘ arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf) ∘ arr (≃⇒Cone⇒ F≃G Lf Lg) ≈⟨ pullˡ (⇒-commute (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)) ⟩
        (⇐.η j ∘ Lg.proj j) ∘ arr (≃⇒Cone⇒ F≃G Lf Lg)                         ≈⟨ pullʳ (⇒-commute (≃⇒Cone⇒ F≃G Lf Lg)) ⟩
        ⇐.η j ∘ ⇒.η j ∘ Lf.proj j                                             ≈⟨ cancelˡ (iso.isoˡ j) ⟩
        Lf.proj j                                                             ∎
      }
    ; isoʳ = Lg.terminal.⊤-id record
      { commute = λ {j} → begin
        Lg.proj j ∘ arr (≃⇒Cone⇒ F≃G Lf Lg) ∘ arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf) ≈⟨ pullˡ (⇒-commute (≃⇒Cone⇒ F≃G Lf Lg)) ⟩
        (⇒.η j ∘ Lf.proj j) ∘ arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)                 ≈⟨ pullʳ (⇒-commute (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)) ⟩
        ⇒.η j ∘ ⇐.η j ∘ Lg.proj j                                             ≈⟨ cancelˡ (iso.isoʳ j) ⟩
        Lg.proj j                                                             ∎
      }
    }
  }
  where open Con.Cone⇒ renaming (commute to ⇒-commute)
        module Lf = Lim.Limit Lf
        module Lg = Lim.Limit Lg
        open NaturalIsomorphism F≃G

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Infinite merge operation for coinductive lists
------------------------------------------------------------------------

{-# OPTIONS --without-K --guardedness #-}

module Codata.Musical.Colist.Infinite-merge where

open import Codata.Musical.Notation
open import Codata.Musical.Colist as Colist hiding (_⋎_)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod
open import Data.Sum
open import Data.Sum.Properties
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Induction.Nat using (<′-wellFounded)
import Induction.WellFounded as WF
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Some code that is used to work around Agda's syntactic guardedness
-- checker.

private

  infixr 5 _∷_ _⋎_

  data ColistP {a} (A : Set a) : Set a where
    []  : ColistP A
    _∷_ : A → ∞ (ColistP A) → ColistP A
    _⋎_ : ColistP A → ColistP A → ColistP A

  data ColistW {a} (A : Set a) : Set a where
    []  : ColistW A
    _∷_ : A → ColistP A → ColistW A

  program : ∀ {a} {A : Set a} → Colist A → ColistP A
  program []       = []
  program (x ∷ xs) = x ∷ ♯ program (♭ xs)

  mutual

    _⋎W_ : ∀ {a} {A : Set a} → ColistW A → ColistP A → ColistW A
    []       ⋎W ys = whnf ys
    (x ∷ xs) ⋎W ys = x ∷ (ys ⋎ xs)

    whnf : ∀ {a} {A : Set a} → ColistP A → ColistW A
    whnf []        = []
    whnf (x ∷ xs)  = x ∷ ♭ xs
    whnf (xs ⋎ ys) = whnf xs ⋎W ys

  mutual

    ⟦_⟧P : ∀ {a} {A : Set a} → ColistP A → Colist A
    ⟦ xs ⟧P = ⟦ whnf xs ⟧W

    ⟦_⟧W : ∀ {a} {A : Set a} → ColistW A → Colist A
    ⟦ [] ⟧W     = []
    ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P

  mutual

    ⋎-homP : ∀ {a} {A : Set a} (xs : ColistP A) {ys} →
             ⟦ xs ⋎ ys ⟧P ≈ ⟦ xs ⟧P Colist.⋎ ⟦ ys ⟧P
    ⋎-homP xs = ⋎-homW (whnf xs) _

    ⋎-homW : ∀ {a} {A : Set a} (xs : ColistW A) ys →
             ⟦ xs ⋎W ys ⟧W ≈ ⟦ xs ⟧W Colist.⋎ ⟦ ys ⟧P
    ⋎-homW (x ∷ xs) ys = x ∷ ♯ ⋎-homP ys
    ⋎-homW []       ys = begin ⟦ ys ⟧P ∎
      where open ≈-Reasoning

  ⟦program⟧P : ∀ {a} {A : Set a} (xs : Colist A) →
               ⟦ program xs ⟧P ≈ xs
  ⟦program⟧P []       = []
  ⟦program⟧P (x ∷ xs) = x ∷ ♯ ⟦program⟧P (♭ xs)

  Any-⋎P : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
           Any P ⟦ program xs ⋎ ys ⟧P ↔ (Any P xs ⊎ Any P ⟦ ys ⟧P)
  Any-⋎P {P = P} xs {ys} =
    Any P ⟦ program xs ⋎ ys ⟧P                ↔⟨ Any-cong Inv.id (⋎-homP (program xs)) ⟩
    Any P (⟦ program xs ⟧P Colist.⋎ ⟦ ys ⟧P)  ↔⟨ Any-⋎ _ ⟩
    (Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P)   ↔⟨ Any-cong Inv.id (⟦program⟧P _) ⊎-cong (_ ∎) ⟩
    (Any P xs ⊎ Any P ⟦ ys ⟧P)                ∎
    where open Related.EquationalReasoning

  index-Any-⋎P :
    ∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
    (p : Any P ⟦ program xs ⋎ ys ⟧P) →
    index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎P xs) ⟨$⟩ p)
  index-Any-⋎P xs p
    with       Any-resp      id  (⋎-homW (whnf (program xs)) _) p
       | index-Any-resp {f = id} (⋎-homW (whnf (program xs)) _) p
  index-Any-⋎P xs p | q | q≡p
    with Inverse.to (Any-⋎ ⟦ program xs ⟧P) ⟨$⟩ q
       |       index-Any-⋎ ⟦ program xs ⟧P      q
  index-Any-⋎P xs p | q | q≡p | inj₂ r | r≤q rewrite q≡p = r≤q
  index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q
    with       Any-resp      id  (⟦program⟧P xs) r
       | index-Any-resp {f = id} (⟦program⟧P xs) r
  index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q | s | s≡r
    rewrite s≡r | q≡p = r≤q

------------------------------------------------------------------------
-- Infinite variant of _⋎_.

private

  merge′ : ∀ {a} {A : Set a} → Colist (A × Colist A) → ColistP A
  merge′ []               = []
  merge′ ((x , xs) ∷ xss) = x ∷ ♯ (program xs ⋎ merge′ (♭ xss))

merge : ∀ {a} {A : Set a} → Colist (A × Colist A) → Colist A
merge xss = ⟦ merge′ xss ⟧P

------------------------------------------------------------------------
-- Any lemma for merge.

module _ {a p} {A : Set a} {P : A → Set p} where

  Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss
  Any-merge xss = inverse (proj₁ ∘ to xss) from (proj₂ ∘ to xss) to∘from
    where
    open P.≡-Reasoning

    -- The from function.

    Q = λ { (x , xs) → P x ⊎ Any P xs }

    from : ∀ {xss} → Any Q xss → Any P (merge xss)
    from (here (inj₁ p))        = here p
    from (here (inj₂ p))        = there (Inverse.from (Any-⋎P _)  ⟨$⟩ inj₁ p)
    from (there {x = _ , xs} p) = there (Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ (from p))

    -- The from function is injective.

    from-injective : ∀ {xss} (p₁ p₂ : Any Q xss) →
                     from p₁ ≡ from p₂ → p₁ ≡ p₂
    from-injective (here (inj₁ p))  (here (inj₁ .p)) P.refl = P.refl
    from-injective (here (inj₁ _))  (here (inj₂ _))  ()
    from-injective (here (inj₂ _))  (here (inj₁ _))  ()
    from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq     =
      P.cong (here ∘ inj₂) $
      inj₁-injective $
      Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₁ p₂} $
      there-injective eq
    from-injective (here (inj₁ _))  (there _)  ()
    from-injective (here (inj₂ p₁)) (there p₂) eq
      with Inverse.injective (Inv.sym (Any-⋎P _))
                             {x = inj₁ p₁} {y = inj₂ (from p₂)}
                             (there-injective eq)
    ... | ()
    from-injective (there _)  (here (inj₁ _))  ()
    from-injective (there p₁) (here (inj₂ p₂)) eq
      with Inverse.injective (Inv.sym (Any-⋎P _))
                             {x = inj₂ (from p₁)} {y = inj₁ p₂}
                             (there-injective eq)
    ... | ()
    from-injective (there {x = _ , xs} p₁) (there p₂) eq =
      P.cong there $
      from-injective p₁ p₂ $
      inj₂-injective $
      Inverse.injective (Inv.sym (Any-⋎P xs))
                        {x = inj₂ (from p₁)} {y = inj₂ (from p₂)} $
      there-injective eq

    -- The to function (defined as a right inverse of from).

    Input = ∃ λ xss → Any P (merge xss)

    Pred : Input → Set _
    Pred (xss , p) = ∃ λ (q : Any Q xss) → from q ≡ p

    to : ∀ xss p → Pred (xss , p)
    to = λ xss p →
      WF.All.wfRec (WF.InverseImage.wellFounded size <′-wellFounded) _
                   Pred step (xss , p)
      where
      size : Input → ℕ
      size (_ , p) = index p

      step : ∀ p → WF.WfRec (_<′_ on size) Pred p → Pred p
      step ([]             , ())      rec
      step ((x , xs) ∷ xss , here  p) rec = here (inj₁ p) , P.refl
      step ((x , xs) ∷ xss , there p) rec
        with Inverse.to (Any-⋎P xs) ⟨$⟩ p
           | Inverse.left-inverse-of (Any-⋎P xs) p
           | index-Any-⋎P xs p
      ... | inj₁ q | P.refl | _   = here (inj₂ q) , P.refl
      ... | inj₂ q | P.refl | q≤p =
        Prod.map there
                 (P.cong (there ∘ _⟨$⟩_ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
                 (rec (♭ xss , q) (s≤′s q≤p))

    to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))

-- Every member of xss is a member of merge xss, and vice versa (with
-- equal multiplicities).

∈-merge : ∀ {a} {A : Set a} {y : A} xss →
          y ∈ merge xss ↔ ∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs)
∈-merge {y = y} xss =
  y ∈ merge xss                                           ↔⟨ Any-merge _ ⟩
  Any (λ { (x , xs) → y ≡ x ⊎ y ∈ xs }) xss               ↔⟨ Any-∈ ⟩
  (∃ λ { (x , xs) → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs) })  ↔⟨ Σ-assoc ⟩
  (∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs))         ∎
  where open Related.EquationalReasoning


text:
------------------------------------------------------------------------
-- Order morphisms
------------------------------------------------------------------------

module Relation.Binary.OrderMorphism where

open import Relation.Binary
open Poset
import Data.Function as F

record _⇒-Poset_ (po₁ po₂ : Poset) : Set where
  field
    fun      : carrier po₁ → carrier po₂
    monotone : _≤_ po₁ =[ fun ]⇒ _≤_ po₂

_⇒-DTO_ : (dto₁ dto₂ : DecTotalOrder) → Set
dto₁ ⇒-DTO dto₂ = poset dto₁ ⇒-Poset poset dto₂
  where open DecTotalOrder

open _⇒-Poset_

id : ∀ {po} → po ⇒-Poset po
id = record
  { fun      = F.id
  ; monotone = F.id
  }

_∘_ : ∀ {po₁ po₂ po₃} →
      po₂ ⇒-Poset po₃ → po₁ ⇒-Poset po₂ → po₁ ⇒-Poset po₃
f ∘ g = record
  { fun      = F._∘_ (fun f)      (fun g)
  ; monotone = F._∘_ (monotone f) (monotone g)
  }

const : ∀ {po₁ po₂} → carrier po₂ → po₁ ⇒-Poset po₂
const {po₂ = po₂} x = record
  { fun      = F.const x
  ; monotone = F.const (refl po₂)
  }

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- An example: A non-terminating program that runs in bounded stack
-- space
------------------------------------------------------------------------

module Lambda.Interpreter.Stack-sizes.Example where

open import Equality.Propositional as E using (refl)
open import Prelude
open import Prelude.Size

open import Colist E.equality-with-J as C
open import Conat E.equality-with-J as Conat hiding (pred)
open import Function-universe E.equality-with-J hiding (id; _∘_)
open import Monad E.equality-with-J
open import Nat E.equality-with-J
open import Vec.Data E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity as D using (later; force)

open import Upper-bounds

import Lambda.Delay-crash-trace as DCT
import Lambda.Interpreter
import Lambda.Interpreter.Stack-sizes

open DCT.Delay-crash-trace

-- This module uses a name type with a single inhabitant, allowing
-- (and requiring) the definition and use of one named definition.

open import Lambda.Syntax ⊤

open Closure Tm

-- A definition that calls itself repeatedly using a tail call.

def : ⊤ → Tm 1
def tt = call tt (con true)

-- The two interpreters are instantiated with this definition.

open Lambda.Interpreter def
module I = Lambda.Interpreter.Stack-sizes def

-- A top-level term to get things going.

go : Tm 0
go = call tt (con true)

-- The semantics of go is the non-terminating computation never.

go-loops : ∀ {i} → D.[ i ] ⟦ go ⟧ [] ∼ never
go-loops = later λ { .force → go-loops }

-- Colists used to analyse the stack space usage of go.

loop-sizes : ∀ {i} → Colist ℕ i
loop-sizes = 1 ∷′ 2 ∷ λ { .force → loop-sizes }

go-sizes : Colist ℕ ∞
go-sizes = 0 ∷′ 1 ∷′ loop-sizes

-- When go is interpreted (starting with an empty stack) the stack
-- sizes that are encountered match the sizes in go-sizes.

stack-sizes-go∼go-sizes : ∀ {i} → C.[ i ] I.stack-sizes go ∼ go-sizes
stack-sizes-go∼go-sizes =
  I.numbers (I.⟦ go ⟧ [] false) 0                                     C.∼⟨ ∷∼∷′ ⟩
  0 ∷′ I.numbers (I.[ id , pred ] lam (def tt) [] ∙ con true) 1       C.∼⟨ (refl ∷ λ { .force → ∷∼∷′ }) ⟩
  0 ∷′ 1 ∷′ I.numbers (I.⟦ def tt ⟧ ρ true >>= tell pred ∘ return) 1  C.∼⟨ (refl ∷ λ { .force → refl ∷ λ { .force → numbers-loop∼loop-sizes _ }}) ⟩
  0 ∷′ 1 ∷′ loop-sizes                                                C.∼⟨⟩
  go-sizes                                                            C.∎
  where
  ρ = con true ∷ []

  numbers-loop∼loop-sizes :
    ∀ {i} k → C.[ i ] I.numbers (I.⟦ def tt ⟧ ρ true >>= k) 1 ∼ loop-sizes
  numbers-loop∼loop-sizes k =
    I.numbers (I.⟦ def tt ⟧ ρ true >>= k) 1                                 C.∼⟨ ∷∼∷′ ⟩
    1 ∷′ I.numbers (I.[ pred , id ] lam (def tt) [] ∙ con true >>= k) 2     C.∼⟨ (refl ∷ λ { .force → ∷∼∷′ }) ⟩
    1 ∷′ 2 ∷′ I.numbers (I.⟦ def tt ⟧ ρ true >>= tell id ∘ return >>= k) 1  C.∼⟨ (refl ∷ λ { .force → refl ∷ λ { .force → I.numbers-cong (
                                                                                DCT.symmetric (DCT.associativity (I.⟦ def tt ⟧ ρ true) _ _)) }}) ⟩
    1 ∷′ 2 ∷′ I.numbers (I.⟦ def tt ⟧ ρ true >>= tell id ∘ k) 1             C.∼⟨ (refl ∷ λ { .force → refl ∷ λ { .force →
                                                                                numbers-loop∼loop-sizes _ }}) ⟩
    1 ∷′ 2 ∷′ loop-sizes                                                    C.∼⟨ (refl ∷ λ { .force → C.symmetric-∼ ∷∼∷′ }) ⟩
    loop-sizes                                                              C.∎

-- The least upper bound of go-sizes is 2.

lub-go-sizes-2 : LUB go-sizes ⌜ 2 ⌝
lub-go-sizes-2 =
  lub-∷ʳ zero (lub-∷ʳ 1≤2 lub-loop-sizes-2)
  where
  1≤2 = suc λ { .force → zero }

  2∷[] = λ { .force → 2 ∷′ [] }

  cycle-1-2∷[]∼loop-sizes :
    ∀ {i} → C.[ i ] cycle 1 2∷[] ∼ loop-sizes
  cycle-1-2∷[]∼loop-sizes =
    refl ∷ λ { .force → refl ∷ λ { .force → cycle-1-2∷[]∼loop-sizes }}

  lub-loop-sizes-2 : LUB loop-sizes ⌜ 2 ⌝
  lub-loop-sizes-2 =          $⟨ lub-∷ʳ 1≤2 (lub-∷ˡ zero lub-[]) ⟩
    LUB (1 ∷ 2∷[]) ⌜ 2 ⌝      ↝⟨ lub-cycle ⟩
    LUB (cycle 1 2∷[]) ⌜ 2 ⌝  ↝⟨ LUB-∼ cycle-1-2∷[]∼loop-sizes (Conat.reflexive-∼ _) ⟩□
    LUB loop-sizes ⌜ 2 ⌝      □

-- The maximum stack size encountered when running go (starting with
-- an empty stack) is 2.

go-bounded-stack : LUB (I.stack-sizes go) ⌜ 2 ⌝
go-bounded-stack =
  LUB-∼ (C.symmetric-∼ stack-sizes-go∼go-sizes)
        (Conat.reflexive-∼ _)
        lub-go-sizes-2

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module Conway where

open import Data.Bool renaming (_≟_ to _B≟_)
open import Data.Nat renaming (_+_ to _ℕ+_ ; _*_ to _ℕ*_ ; _≟_ to _ℕ≟_)
open import Data.Integer
  renaming (_+_ to _ℤ+_ ; _*_ to _ℤ*_ ; -_ to ℤ-_ ; _≟_ to _ℤ≟_)
open import Data.Rational renaming (_≟_ to _ℚ≟_)
open import Relation.Nullary.Core
open import Relation.Nullary.Decidable

open import Rat -- operations on rationals

------------------------------------------------------------------------------
-- Universe of games

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U
  NEG   : U → U
  RECIP : U → U

-- Conversion from the rationals to the universe of games

n2U : ℕ → U
n2U 0       = ZERO
n2U (suc n) = PLUS ONE (n2U n)

z2U : ℤ → U
z2U -[1+ n ] = NEG (n2U (ℕ.suc n))
z2U (+ n)    = n2U n

q2U : ℚ → U
q2U p = TIMES (z2U (ℚ.numerator p)) (RECIP (n2U (ℕ.suc (ℚ.denominator-1 p))))

-- Conversion from the universe of games to the rationals

-- use meadows?

mutual

  u2q : U → ℚ
  u2q ZERO        = 0ℚ
  u2q ONE         = 1ℚ
  u2q (PLUS g h)  = (u2q g) + (u2q h)
  u2q (TIMES g h) = (u2q g) * (u2q h)
  u2q (NEG g)     = - (u2q g)
  u2q (RECIP g)   = 1/_ (u2q g) {{!!}}
-- need to know that | numerator (u2q g) | is not 0

  u2q≢0 : (u : U) → {u≢0 : False (u2q u ℚ≟ 0ℚ)} → ℚ
  u2q≢0 u {u≢0} with (u2q u ℚ≟ 0ℚ)
  u2q≢0 u {()} | yes _
  u2q≢0 u {_}  | no _ = u2q u

------------------------------------------------------------------------------
-- Small tests

private

  test₁ = q2U (- (+ 1 ÷ 3))
  {--
    TIMES
      (NEG (PLUS ONE ZERO))
      (RECIP (PLUS ONE (PLUS ONE (PLUS ONE ZERO))))
  --}

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module puzzle where

---- 仮定
-- 猫か犬を飼っている人は山羊を飼ってない
-- 猫を飼ってない人は、犬かウサギを飼っている
-- 猫も山羊も飼っていない人は、ウサギを飼っている
--
---- 問題
-- 山羊を飼っている人は、犬を飼っていない
-- 山羊を飼っている人は、ウサギを飼っている
-- ウサギを飼っていない人は、猫を飼っている

module pet-research where
  open import logic
  open import Relation.Nullary
  open import Data.Empty

  postulate
     lem : (a : Set) → a ∨ ( ¬ a )

  record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where
     field
        fact1 : ( Cat ∨ Dog ) → ¬ Goat
        fact2 : ¬ Cat →  ( Dog ∨ Rabbit )
        fact3 : ¬ ( Cat ∨ Goat ) →  Rabbit

  module tmp ( Cat Dog Goat Rabbit : Set ) (p :  PetResearch  Cat Dog Goat Rabbit ) where

    open PetResearch

    problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit
    problem0 with lem Cat | lem Goat
    ... | case1 c | g = case1 c
    ... | c | case1 g = case2 ( case2 ( case1 g ) )
    ... | case2 ¬c | case2 ¬g  = case2 ( case2 ( case2 ( fact3 p lemma1 ))) where
        lemma1 : ¬ ( Cat ∨ Goat )
        lemma1 (case1 c) = ¬c c
        lemma1 (case2 g) = ¬g g

    problem1 : Goat → ¬ Dog
    problem1 g d = fact1 p (case2 d) g

    problem2 : Goat → Rabbit
    problem2 g with lem Cat | lem Dog
    problem2 g | case1 c | d = ⊥-elim ( fact1 p (case1 c ) g )
    problem2 g | case2 ¬c | case1 d = ⊥-elim ( fact1 p (case2 d ) g )
    problem2 g | case2 ¬c | case2 ¬d with lem Rabbit
    ... | case1  r = r
    ... | case2 ¬r = fact3 p lemma2 where
        lemma2 : ¬ ( Cat ∨ Goat )
        lemma2 (case1 c) = ¬c c
        lemma2 (case2 g) with fact2 p ¬c
        lemma2 (case2 g) | case1 d = ¬d d
        lemma2 (case2 g) | case2 r = ¬r r

    problem3 : (¬ Rabbit ) → Cat
    problem3 ¬r with lem Cat | lem Goat
    problem3 ¬r | case1 c | g = c
    problem3 ¬r | case2 ¬c | g = ⊥-elim ( ¬r ( fact3 p lemma3 )) where
        lemma3 :  ¬ ( Cat ∨ Goat )
        lemma3 (case1 c) = ¬c c
        lemma3 (case2 g) with fact2 p ¬c
        lemma3 (case2 g) | case1 d = fact1 p (case2 d ) g
        lemma3 (case2 g) | case2 r = ¬r r

module pet-research1 ( Cat Dog Goat Rabbit : Set ) where

  open import Data.Bool
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality

  _=>_ :  Bool → Bool → Bool
  _ => true = true
  false => _ = true
  true => false = false

  ¬_ : Bool → Bool
  ¬ p = not p

  problem0 :  ( Cat Dog Goat Rabbit : Bool ) →
    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
    => (Cat ∨ Dog ∨ Goat ∨ Rabbit) ≡ true
  problem0 true d g r = refl
  problem0 false true g r = refl
  problem0 false false true r = refl
  problem0 false false false true = refl
  problem0 false false false false = refl

  problem1 :  ( Cat Dog Goat Rabbit : Bool ) →
    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
    => ( Goat => ( ¬ Dog )) ≡ true
  problem1 c false false r = refl
  problem1 c true false r = refl
  problem1 c false true r = refl
  problem1 false true true r = refl
  problem1 true true true r = refl

  problem2 :  ( Cat Dog Goat Rabbit : Bool ) →
    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
    => ( Goat => Rabbit ) ≡ true
  problem2 c d false false = refl
  problem2 c d false true = refl
  problem2 c d true true = refl
  problem2 true d true false = refl
  problem2 false false true false = refl
  problem2 false true true false = refl

  problem3 :  ( Cat Dog Goat Rabbit : Bool ) →
    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
    => ( (¬ Rabbit ) => Cat ) ≡ true
  problem3 false d g true = refl
  problem3 true d g true = refl
  problem3 true d g false = refl
  problem3 false false false false = refl
  problem3 false false true false = refl
  problem3 false true false false = refl
  problem3 false true true false = refl

-- module pet-research2 ( Cat Dog Goat Rabbit : Set ) where
--
--   open import Data.Bool hiding ( _∨_ )
--   open import Relation.Binary
--   open import Relation.Binary.PropositionalEquality
--
--   ¬_ : Bool → Bool
--   ¬ p = p xor true
--
--   infixr 5 _∨_
--   _∨_ :  Bool → Bool → Bool
--   a ∨ b = ¬ ( (¬ a) ∧ (¬ b ) )
--
--   _=>_ :  Bool → Bool → Bool
--   a => b = (¬ a ) ∨ b
--
--   open import Data.Bool.Solver using (module xor-∧-Solver)
--   open xor-∧-Solver
--
--   problem0' :  ( Cat : Bool ) → (Cat xor Cat ) ≡ false
--   problem0' = solve 1 (λ c → (c :+ c ) := con false ) refl
--
--   problem1' :  ( Cat : Bool ) → (Cat ∧ (Cat xor true ))  ≡ false
--   problem1' = solve 1 (λ c → ((c :* (c :+ con true )) ) := con false ) {!!}
--
--   open import Data.Nat
--   :¬_ : {n : ℕ} → Polynomial n → Polynomial n
--   :¬ p = p :+ con true
--
--   _:∨_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
--   a :∨ b = :¬ ( ( :¬ a ) :* ( :¬ b ))
--
--   _:=>_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
--   a :=> b = ( :¬ a ) :∨ b
--
--   _:∧_ = _:*_
--
--   infixr 6 _:∧_
--   infixr 5 _:∨_
--
--   problem0 :  ( Cat Dog Goat Rabbit : Bool ) →
--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
--     => (Cat ∨ Dog ∨ Goat ∨ Rabbit) ≡ true
--   problem0 = solve 4 ( λ Cat Dog Goat Rabbit → (
--     ( ((Cat :∨ Dog ) :=> (:¬ Goat)) :∧ ( ((:¬ Cat ) :=>  ( Dog :∨ Rabbit )) :∧ (( :¬ ( Cat :∨ Goat ) ) :=>  Rabbit)  ))
--     :=> ( Cat :∨ (Dog :∨ ( Goat :∨ Rabbit))) ) := con true ) {!!}
--
--   problem1 :  ( Cat Dog Goat Rabbit : Bool ) →
--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
--     => ( Goat => ( ¬ Dog )) ≡ true
--   problem1 c false false r = {!!}
--   problem1 c true false r = {!!}
--   problem1 c false true r = {!!}
--   problem1 false true true r = refl
--   problem1 true true true r = refl
--
--   problem2 :  ( Cat Dog Goat Rabbit : Bool ) →
--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
--     => ( Goat => Rabbit ) ≡ true
--   problem2 c d false false = {!!}
--   problem2 c d false true = {!!}
--   problem2 c d true true = {!!}
--   problem2 true d true false = refl
--   problem2 false false true false = refl
--   problem2 false true true false = refl
--
--   problem3 :  ( Cat Dog Goat Rabbit : Bool ) →
--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
--     => ( (¬ Rabbit ) => Cat ) ≡ true
--   problem3 false d g true = {!!}
--   problem3 true d g true = {!!}
--   problem3 true d g false = {!!}
--   problem3 false false false false = refl
--   problem3 false false true false = refl
--   problem3 false true false false = refl
--   problem3 false true true false = refl

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


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

module Data.Binary where

open import Data.Binary.Definitions               using (𝔹) public
open import Data.Binary.Operations.Semantics      using (⟦_⇑⟧; ⟦_⇓⟧) public
open import Data.Binary.Operations.Addition       using (_+_) public
open import Data.Binary.Operations.Multiplication using (_*_) public
open import Data.Binary.Operations.Unary          using (inc; dec) public

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
{-# OPTIONS --without-K #-}
module hott.level.closure.extra where

open import level
open import decidable
open import sum
open import level using (lsuc; ↑; lift)
open import equality.core
open import equality.calculus
open import function.core using (_∘_; const)
open import function.extensionality
open import function.isomorphism
open import sets.bool
open import sets.unit
open import sets.nat.core
-- open import sets.nat.ordering.leq.core
open import hott.level.core
open import hott.level.sets
open import hott.level.closure.core
open import hott.equivalence.core
  using (weak-equiv; _≈_)
open import hott.univalence
open import sets.empty

abstract
  -- Π preserves h-levels
  Π-level : ∀ {i j n} {X : Set i}{Y : X → Set j}
           → ((x : X) → h n (Y x))
           → h n ((x : X) → Y x)
  Π-level {n = 0} c = Π-contr c
  Π-level {n = suc n} {X = X}{Y} hn = λ f g →
    subst (h n) strong-funext (Π-level (λ x → hn x (f x) (g x)))

  -- Σ preserves h-levels
  Σ-level : ∀ {i j n} {X : Set i}{Y : X → Set j}
           → h n X → ((x : X) → h n (Y x))
           → h n (Σ X Y)
  Σ-level {n = 0}{X = X}{Y} (x₀ , cx) hy =
    (x₀ , proj₁ (hy x₀)) , λ { (x , y) → c x y }
    where
      c : (x : X)(y : Y x) → (x₀ , proj₁ (hy x₀)) ≡ (x , y)
      c x y = ap (λ x → (x , proj₁ (hy x))) (cx x)
            · ap (_,_ x) (proj₂ (hy x) y)
  Σ-level {n = suc n} hx hy = λ a b → iso-level Σ-split-iso
    (Σ-level (hx _ _) (λ p → hy (proj₁ b) _ _))

  -- × preserves h-levels
  ×-level : ∀ {i j n}{X : Set i}{Y : Set j}
           → h n X → h n Y → h n (X × Y)
  ×-level hx hy = Σ-level hx (λ _ → hy)

  -- ⊎ preserves h-levels
--  ⊎-level : ∀ {i j n}{X : Set i}{Y : Set j}
--           → 2 ≤ n → h n X → h n Y → h n (X ⊎ Y)
--  ⊎-level {i}{j}{n} {X}{Y} p hx hy = iso-level lem
--    (Σ-level (h! {p = decide p} bool-set) P-level)
--    where
--      P : Bool → Set (i ⊔ j)
--      P true = ↑ j X
--      P false = ↑ i Y
--
--      P-level : (b : Bool) → h n (P b)
--      P-level true = iso-level (lift-iso j X) hx
--      P-level false = iso-level (lift-iso i Y) hy
--
--      lem : Σ Bool P ≅ (X ⊎ Y)
--      lem = iso f g H K
--        where
--          f : (Σ Bool P) → (X ⊎ Y)
--          f (true , lift x) = inj₁ x
--          f (false , lift y) = inj₂ y
--
--          g : (X ⊎ Y) → (Σ Bool P)
--          g (inj₁ x) = (true , lift x)
--          g (inj₂ y) = (false , lift y)
--
--          H : (x : Σ Bool P) → g (f x) ≡ x
--          H (true , lift x) = refl
--          H (false , lift y) = refl
--
--          K : (x : X ⊎ Y) → f (g x) ≡ x
--          K (inj₁ x) = refl
--          K (inj₂ y) = refl

  Π-level-impl : ∀ {i j n} {X : Set i}{Y : X → Set j}
                → ((x : X) → h n (Y x))
                → h n ({x : X} → Y x)
  Π-level-impl {X = X}{Y} hY = iso-level impl-iso (Π-level hY)

  -- being contractible is a proposition
  contr-h1 : ∀ {i}(X : Set i) → h 1 (contr X)
  contr-h1 X = prop⇒h1 λ { (x₀ , c₀) (x₁ , c₁) →
      unapΣ (c₀ x₁ , contr⇒prop (lem (x₀ , c₀) x₁) _ _) }
    where
      lem : ∀ {i}{A : Set i} → contr A → (x : A) → contr ((x' : A) → x ≡ x')
      lem c x = Π-level (λ x' → h↑ c x x')

  -- being of h-level n is a proposition
  hn-h1 : ∀ {i} n (X : Set i) → h 1 (h n X)
  hn-h1 0 X = contr-h1 X
  hn-h1 (suc n) X = Π-level λ x → Π-level λ y → hn-h1 n (x ≡ y)

  -- being a weak equivalence is a proposition
  weak-equiv-h1 : ∀ {i j}{X : Set i}{Y : Set j}
                → (f : X → Y)
                → h 1 (weak-equiv f)
  weak-equiv-h1 f = Π-level λ y
                  → contr-h1 _

  ⊎-h1 : ∀ {i j}{A : Set i}{B : Set j}
       → h 1 A → h 1 B → ¬ (A × B)
       → h 1 (A ⊎ B)
  ⊎-h1 {A = A}{B = B} hA hB u = prop⇒h1 ⊎-prop
    where
      ⊎-prop : prop (A ⊎ B)
      ⊎-prop (inj₁ a) (inj₁ a') = ap inj₁ (h1⇒prop hA a a')
      ⊎-prop (inj₁ a) (inj₂ b') = ⊥-elim (u (a , b'))
      ⊎-prop (inj₂ b) (inj₁ a') = ⊥-elim (u (a' , b))
      ⊎-prop (inj₂ b) (inj₂ b') = ap inj₂ (h1⇒prop hB b b')

  inj-level : ∀ {i j n}{A : Set i}{B : Set j}
             → (f : A → B)
             → h (suc n) A → h n (injective f)
  inj-level f hA
    = Π-level-impl λ x
    → Π-level-impl λ x'
    → Π-level λ p
    → hA x x'

  ↣-level : ∀ {i j n}{A : Set i}{B : Set j}
           → h (suc n) A → h n B → h n (A ↣ B)
  ↣-level hA hB
    = Σ-level (Π-level λ _ → hB) λ f
    → inj-level f hA

  ¬-h1 : ∀ {i}{X : Set i} → h 1 (¬ X)
  ¬-h1 = Π-level λ _ → ⊥-prop

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Cats.Category.Zero where

open import Data.Empty using (⊥ ; ⊥-elim)
open import Level

open import Cats.Category

Zero : ∀ lo la l≈ → Category lo la l≈
Zero lo la l≈ = record
    { Obj = Lift lo ⊥
    ; _⇒_ = λ()
    ; _≈_ = λ {}
    ; id = λ{}
    ; _∘_ = λ{}
    ; equiv = λ{}
    ; ∘-resp = λ{}
    ; id-r = λ{}
    ; id-l = λ{}
    ; assoc = λ{}
    }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-

Some theory about Bi-Invertible Equivalences

- BiInvEquiv to Iso
- BiInvEquiv to Equiv
- BiInvEquiv to HAEquiv
- Iso to BiInvEquiv

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.BiInvEquiv where

open import Cubical.Core.Glue

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HAEquiv

record BiInvEquiv {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  constructor biInvEquiv
  field
    fun : A → B
    invr : B → A
    invr-rightInv : section fun invr
    invl : B → A
    invl-leftInv : retract fun invl

  invr≡invl : ∀ b → invr b ≡ invl b
  invr≡invl b =            invr b   ≡⟨ sym (invl-leftInv (invr b)) ⟩
                invl (fun (invr b)) ≡⟨ cong invl (invr-rightInv b) ⟩
                invl b              ∎

  invr-leftInv : retract fun invr
  invr-leftInv a = invr≡invl (fun a) □ (invl-leftInv a)

  invr≡invl-leftInv : ∀ a → PathP (λ j → invr≡invl (fun a) j ≡ a) (invr-leftInv a) (invl-leftInv a)
  invr≡invl-leftInv a j i = compPath'-filler (invr≡invl (fun a)) (invl-leftInv a) (~ j) i

  invl-rightInv : section fun invl
  invl-rightInv a = sym (cong fun (invr≡invl a)) □ (invr-rightInv a)

  invr≡invl-rightInv : ∀ a → PathP (λ j → fun (invr≡invl a j) ≡ a) (invr-rightInv a) (invl-rightInv a)
  invr≡invl-rightInv a j i = compPath'-filler (sym (cong fun (invr≡invl a))) (invr-rightInv a) j i

module _ {ℓ} {A B : Type ℓ} (e : BiInvEquiv A B) where
  open BiInvEquiv e

  biInvEquiv→Iso-right : Iso A B
  Iso.fun biInvEquiv→Iso-right      = fun
  Iso.inv biInvEquiv→Iso-right      = invr
  Iso.rightInv biInvEquiv→Iso-right = invr-rightInv
  Iso.leftInv biInvEquiv→Iso-right  = invr-leftInv

  biInvEquiv→Iso-left : Iso A B
  Iso.fun biInvEquiv→Iso-left      = fun
  Iso.inv biInvEquiv→Iso-left      = invl
  Iso.rightInv biInvEquiv→Iso-left = invl-rightInv
  Iso.leftInv biInvEquiv→Iso-left  = invl-leftInv

  biInvEquiv→Equiv-right biInvEquiv→Equiv-left : A ≃ B
  biInvEquiv→Equiv-right = fun , isoToIsEquiv biInvEquiv→Iso-right
  biInvEquiv→Equiv-left  = fun , isoToIsEquiv biInvEquiv→Iso-left

  -- since Iso.rightInv ends up getting modified during iso→HAEquiv, in some sense biInvEquiv→Iso-left
  --  is the most natural choice for forming a HAEquiv from a BiInvEquiv
  biInvEquiv→HAEquiv : HAEquiv A B
  biInvEquiv→HAEquiv = iso→HAEquiv biInvEquiv→Iso-left

module _ {ℓ} {A B : Type ℓ} (i : Iso A B) where
  open Iso i

  iso→BiInvEquiv : BiInvEquiv A B
  BiInvEquiv.fun iso→BiInvEquiv           = fun
  BiInvEquiv.invr iso→BiInvEquiv          = inv
  BiInvEquiv.invr-rightInv iso→BiInvEquiv = rightInv
  BiInvEquiv.invl iso→BiInvEquiv          = inv
  BiInvEquiv.invl-leftInv iso→BiInvEquiv  = leftInv

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where every consecutative pair of elements is related.
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Linked {a} {A : Set a} where

open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.Product as Prod using (_,_; _×_; uncurry; <_,_>)
open import Function using (id; _∘_)
open import Level using (Level; _⊔_)
open import Relation.Binary as B using (Rel; _⇒_)
open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Nullary.Product using (_×-dec_)

private
  variable
    p q r ℓ : Level

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

-- Linked R xs means that every consecutative pair of elements
-- in xs is a member of relation R.

infixr 5 _∷_

data Linked (R : Rel A ℓ) : List A → Set (a ⊔ ℓ) where
  []  : Linked R []
  [-] : ∀ {x} → Linked R (x ∷ [])
  _∷_ : ∀ {x y xs} → R x y → Linked R (y ∷ xs) → Linked R (x ∷ y ∷ xs)

------------------------------------------------------------------------
-- Operations

module _ {R : Rel A p} {x y xs} where

  head : Linked R (x ∷ y ∷ xs) → R x y
  head (Rxy ∷ Rxs) = Rxy

  tail : Linked R (x ∷ y ∷ xs) → Linked R (y ∷ xs)
  tail (Rxy ∷ Rxs) = Rxs

module _ {R : Rel A p} {S : Rel A q} where

  map : R ⇒ S → Linked R ⊆ Linked S
  map R⇒S []           = []
  map R⇒S [-]          = [-]
  map R⇒S (x~xs ∷ pxs) = R⇒S x~xs ∷ map R⇒S pxs

module _ {P : Rel A p} {Q : Rel A q} {R : Rel A r} where

  zipWith : P ∩ᵇ Q ⇒ R → Linked P ∩ᵘ Linked Q ⊆ Linked R
  zipWith f ([] , [])             = []
  zipWith f ([-] , [-])           = [-]
  zipWith f (px ∷ pxs , qx ∷ qxs) = f (px , qx) ∷ zipWith f (pxs , qxs)

  unzipWith : R ⇒ P ∩ᵇ Q → Linked R ⊆ Linked P ∩ᵘ Linked Q
  unzipWith f []         = [] , []
  unzipWith f [-]        = [-] , [-]
  unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (f rx) (unzipWith f rxs)

module _ {P : Rel A p} {Q : Rel A q} where

  zip : Linked P ∩ᵘ Linked Q ⊆ Linked (P ∩ᵇ Q)
  zip = zipWith id

  unzip : Linked (P ∩ᵇ Q) ⊆ Linked P ∩ᵘ Linked Q
  unzip = unzipWith id

------------------------------------------------------------------------
-- Properties of predicates preserved by Linked

module _ {R : Rel A ℓ} where

  linked? : B.Decidable R → U.Decidable (Linked R)
  linked? R? []           = yes []
  linked? R? (x ∷ [])     = yes [-]
  linked? R? (x ∷ y ∷ xs) =
    map′ (uncurry _∷_) < head , tail > (R? x y ×-dec linked? R? (y ∷ xs))

  irrelevant : B.Irrelevant R → U.Irrelevant (Linked R)
  irrelevant irr []           []           = refl
  irrelevant irr [-]          [-]          = refl
  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
    cong₂ _∷_ (irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)

  satisfiable : U.Satisfiable (Linked R)
  satisfiable = [] , []


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

-- This file contains an implementation of the stack-based compiler for Hutton's
-- razor, as from:
--
--   P. Bahr and G. Hutton, “Calculating correct compilers,” Journal of
--   Functional Programming, vol. 25, no. e14, Sep. 2015,
--   doi: 10.1017/S0956796815000180.
--
-- The compiler is total and the evaluator is stack-safe, and furthermore we have
-- proven a full isomorphism between the code representation and the AST.

module Data.Dyck.Prog where

open import Prelude
open import Data.Nat using (_+_)

private variable n : ℕ

--------------------------------------------------------------------------------
-- We have 2 forms that we want to convert between: an AST and a flat code.
--------------------------------------------------------------------------------

data Expr : Type where
  [_] : ℕ → Expr
  _⊕_ : Expr → Expr → Expr

--------------------------------------------------------------------------------
-- We do the conversion with cayley forms of the dyck monoids
--------------------------------------------------------------------------------

⟨_⟩_↝_ : (ℕ → Type) → ℕ → ℕ → Type
⟨ C ⟩ n ↝ m = ∀ {i} → C (n + i) → C (m + i)

--------------------------------------------------------------------------------
-- An encoding of an AST
--------------------------------------------------------------------------------

data Code : ℕ → Type where
  HALT : Code 1
  PUSH : ℕ → ⟨ Code ⟩ 1 ↝ 0
  ADD  :     ⟨ Code ⟩ 1 ↝ 2

--------------------------------------------------------------------------------
-- We will need a stack (a snoc-list)
--------------------------------------------------------------------------------

Stack : Type → ℕ → Type
Stack A zero    = ⊤
Stack A (suc n) = Stack A n × A

infixl 5 _∷_
pattern _∷_ xs x = xs , x

foldl : (P : ℕ → Type) → (A → ⟨ P ⟩ 1 ↝ 0) → Stack A n → P n → P zero
foldl {n = zero}  P f tt       = id
foldl {n = suc n} P f (xs ∷ x) = foldl P f xs ∘ f x

private variable st : Stack Expr n

--------------------------------------------------------------------------------
-- Conversion to and from code
--------------------------------------------------------------------------------

--            Code n → ⟨ Stack Expr ⟩ n ↝ 1
code→expr⊙ : Code n → Stack Expr n → Expr
code→expr⊙ HALT        (tt ∷ e)       = e
code→expr⊙ (PUSH v is) st             = code→expr⊙ is (st ∷ [ v ])
code→expr⊙ (ADD is)    (st ∷ xs ∷ ys) = code→expr⊙ is (st ∷ xs ⊕ ys)

code→expr : Code 0 → Expr
code→expr ds = code→expr⊙ ds tt

expr→code⊙ : Expr → ⟨ Code ⟩ 1 ↝ 0
expr→code⊙ [ x ]     = PUSH x
expr→code⊙ (xs ⊕ ys) = expr→code⊙ xs ∘ expr→code⊙ ys ∘ ADD

expr→code : Expr → Code 0
expr→code xs = expr→code⊙ xs HALT

--------------------------------------------------------------------------------
-- Proof of isomorphism
--------------------------------------------------------------------------------

expr→code→expr⊙ : {is : Code (1 + n)} (e : Expr) →
  code→expr⊙ (expr→code⊙ e is) st ≡ code→expr⊙ is (st ∷ e)
expr→code→expr⊙ [ x ]     = refl
expr→code→expr⊙ (xs ⊕ ys) = expr→code→expr⊙ xs ; expr→code→expr⊙ ys

code→expr→code⊙ : (is : Code n) →
 expr→code (code→expr⊙ is st) ≡ foldl Code expr→code⊙ st is
code→expr→code⊙  HALT       = refl
code→expr→code⊙ (PUSH i is) = code→expr→code⊙ is
code→expr→code⊙ (ADD    is) = code→expr→code⊙ is

prog-iso : Code 0 ⇔ Expr
prog-iso .fun = code→expr
prog-iso .inv = expr→code
prog-iso .rightInv = expr→code→expr⊙
prog-iso .leftInv  = code→expr→code⊙

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Agda.Builtin.Equality

postulate
  foo : (A : Set) → A ≡ A

helper : {W : Set} (A : Set) → W → W ≡ A → (A → Set) → Set
helper A w refl f = f w

bar : (A : Set) → A → Set
bar A a = let A≡A = foo A in helper A a (foo A) {!!} -- A≡A : A ≡ A

baz : (A : Set) → A → Set
baz A a = let A≡A = foo A in helper A a (foo A) λ a' → {!!} -- A≡A : a ≡ a

f : (A : Set) → A → Set → Set
f A x = let y = x in λ B → {!!} -- y : x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module cedille-syntax where
open import lib
open import ctxt
open import syntax-util
open import general-util
open import is-free
open import cedille-types

-- App, AppTp
infixl 10 _`_ _-_ _·_
-- Pattern and constructor
pattern _`_ t t' = App t NotErased t'
pattern _-_ t t' = App t Erased t'
pattern _·_ t T = AppTp t T

-- Beta
infix 9 β<_> β[_] β<_>[_] `β<_> `β[_] `β<_>[_]
pattern β = Beta _ NoTerm NoTerm
pattern β<_> t = Beta _ (SomeTerm t _) NoTerm
pattern β[_] t = Beta _ NoTerm (SomeTerm t _)
pattern β<_>[_] t t' = Beta _ (SomeTerm t _) (SomeTerm t' _)
`β = Beta pi-gen NoTerm NoTerm
`β<_> = λ t → Beta pi-gen (SomeTerm t pi-gen) NoTerm
`β[_] = λ t → Beta pi-gen NoTerm (SomeTerm t pi-gen)
`β<_>[_] = λ t t' → Beta pi-gen (SomeTerm t pi-gen) (SomeTerm t' pi-gen)

-- Chi
infixr 8 χ-_ χ_-_ `χ-_ `χ_-_
pattern χ-_ t = Chi _ NoType t
pattern χ_-_ T t = Chi _ (SomeType T) t
`χ-_ = Chi pi-gen NoType
`χ_-_ = λ T t → Chi pi-gen (SomeType T) t

-- Delta
infixr 8 δ-_ δ_-_ `δ-_ `δ_-_
pattern δ-_ t = Delta _ NoType t
pattern δ_-_ T t = Delta _ (SomeType T) t
`δ-_ = Delta pi-gen NoType
`δ_-_ = λ T t → Delta pi-gen (SomeType T) t

-- Epsilon
infixr 8 ε_ εl_ εr_ ε-_ εl-_ εr-_ `ε_ `εl_ `εr_ `ε-_ `εl-_ `εr-_
pattern ε_ t = Epsilon _ Both ff t
pattern εl_ t = Epsilon _ Left ff t
pattern εr_ t = Epsilon _ Right ff t
pattern ε-_ t = Epsilon _ Both tt t
pattern εl-_ t = Epsilon _ Left tt t
pattern εr-_ t = Epsilon _ Right tt t
`ε_ = Epsilon pi-gen Both ff
`εl_ = Epsilon pi-gen Left ff
`εr_ = Epsilon pi-gen Right ff
`ε-_ = Epsilon pi-gen Both tt
`εl-_ = Epsilon pi-gen Left tt
`εr-_ = Epsilon pi-gen Right tt

-- Hole
pattern ● = Hole _
`● = Hole pi-gen

-- IotaPair
pattern [_`,_] t₁ t₂ = IotaPair _ t₁ t₂ NoGuide _
pattern [_`,_*_₊_] t₁ t₂ x T = IotaPair _ t₁ t₂ (Guide _ x T) _ -- "₊" = "\_+"
`[_`,_] = λ t₁ t₂ → IotaPair pi-gen t₁ t₂ NoGuide pi-gen
`[_`,_*_₊_] = λ t₁ t₂ x T → IotaPair pi-gen t₁ t₂ (Guide pi-gen x T) pi-gen

-- IotaProj
infixl 5 _₊1 _₊2 _₊#_ _`₊1 _`₊2 _`₊#_
pattern _₊1 t = IotaProj t "1" _
pattern _₊2 t = IotaProj t "2" _
pattern _₊#_ t n = IotaProj t n _
_`₊1 = λ t → IotaProj t "1" pi-gen
_`₊2 = λ t → IotaProj t "2" pi-gen
_`₊#_ = λ t n → IotaProj t n pi-gen

-- Lam
infixr 4 λ`_₊_ λ`_:ₜ_₊_ λ`_:ₖ_₊_ Λ_₊_ Λ_:ₜ_₊_ Λ_:ₖ_₊_ `λ_₊_ `λ_:ₜ_₊_ `λ_:ₖ_₊_ `Λ_₊_ `Λ_:ₜ_₊_ `Λ_:ₖ_₊_
pattern λ`_₊_ x t = Lam _ NotErased _ x NoClass t
pattern λ`_:ₜ_₊_ x T t = Lam _ NotErased _ x (SomeClass (Tkt T)) t
pattern λ`_:ₖ_₊_ x k t = Lam _ NotErased _ x (SomeClass (Tkk k)) t
pattern Λ_₊_ x t = Lam _ Erased _ x NoClass t
pattern Λ_:ₜ_₊_ x T t = Lam _ Erased _ x (SomeClass (Tkt T)) t
pattern Λ_:ₖ_₊_ x k t = Lam _ Erased _ x (SomeClass (Tkk k)) t
`λ_₊_ = λ x t → Lam pi-gen NotErased pi-gen x NoClass t
`λ_:ₜ_₊_ = λ x T t → Lam pi-gen NotErased pi-gen x (SomeClass (Tkt T)) t
`λ_:ₖ_₊_ = λ x k t → Lam pi-gen NotErased pi-gen x (SomeClass (Tkk k)) t
`Λ_₊_ = λ x t → Lam pi-gen Erased pi-gen x NoClass t
`Λ_:ₜ_₊_ = λ x T t → Lam pi-gen Erased pi-gen x (SomeClass (Tkt T)) t
`Λ_:ₖ_₊_ = λ x k t → Lam pi-gen Erased pi-gen x (SomeClass (Tkk k)) t

-- Let
infixr 8 [_`=_]-_ [_:ₜ_`=_]-_ [_:ₖ_`=_]-_ -[_`=_]-_ -[_:ₜ_`=_]-_ -[_:ₖ_`=_]-_ `[_`=_]-_ `[_:ₜ_`=_]-_ `[_:ₖ_`=_]-_ `-[_`=_]-_ `-[_:ₜ_`=_]-_ `-[_:ₖ_`=_]-_
pattern [_`=_]-_ x t t' = Let _ NotErased (DefTerm _ x NoType t _) t'
pattern [_:ₜ_`=_]-_ x T t t' = Let _ NotErased (DefTerm _ x (SomeType T) t _) t'
pattern [_:ₖ_`=_]-_ x k T t' = Let _ NotErased (DefType _ x k T _) t'
pattern -[_`=_]-_ x t t' = Let _ Erased (DefTerm _ x NoType t _) t'
pattern -[_:ₜ_`=_]-_ x T t t' = Let _ Erased (DefTerm _ x (SomeType T) t _) t'
pattern -[_:ₖ_`=_]-_ x k T t' = Let _ Erased (DefType _ x k T _) t'
`[_`=_]-_ = λ x t t' → Let pi-gen NotErased (DefTerm pi-gen x NoType t) t'
`[_:ₜ_`=_]-_ = λ x T t t' → Let pi-gen NotErased (DefTerm pi-gen x (SomeType T) t) t'
`[_:ₖ_`=_]-_ = λ x k T t' → Let pi-gen NotErased (DefType pi-gen x k T) t'
`-[_`=_]-_ = λ x t t' → Let pi-gen Erased (DefTerm pi-gen x NoType t) t'
`-[_:ₜ_`=_]-_ = λ x T t t' → Let pi-gen Erased (DefTerm pi-gen x (SomeType T) t) t'
`-[_:ₖ_`=_]-_ = λ x k T t' → Let pi-gen Erased (DefType pi-gen x k T) t'

-- Open
infixr 8 open`_-_ `open_-_ close`_-_ `close_-_
pattern open`_-_ x t = Open _ OpacTrans _ x t
pattern close`_-_ x t = Open _ OpacOpaque _ x t
`open_-_ = Open pi-gen OpacTrans pi-gen
`close_-_ = Open pi-gen OpacOpaque pi-gen

--Parens
infix 4 ⦅_⦆ `⦅_⦆
pattern ⦅_⦆ t = Parens _ t _
`⦅_⦆ = λ t → Parens pi-gen t pi-gen

-- Phi
infix 8 φ_-_[_] `φ_-_[_]
pattern φ_-_[_] eq t₁ t₂ = Phi _ eq t₁ t₂ _
`φ_-_[_] = λ eq t₁ t₂ → Phi pi-gen eq t₁ t₂ pi-gen

-- Rho
infixr 8 ρ_-_ ρ<_>_-_ ρ_*_₊_-_ ρ<_>_*_₊_-_ ρ+_-_ ρ+<_>_-_ ρ+_*_₊_-_ ρ+<_>_*_₊_-_ `ρ_-_ `ρ<_>_-_ `ρ_*_₊_-_ `ρ<_>_*_₊_-_ `ρ+_-_ `ρ+<_>_-_ `ρ+_*_₊_-_ `ρ+<_>_*_₊_-_
pattern ρ_-_ t t' = Rho _ ff NoNums t NoGuide t'
pattern ρ<_>_-_ ns t t' = Rho _ ff (SomeNums ns) t NoGuide t'
pattern ρ_*_₊_-_ t x T t' = Rho _ ff NoNums t (Guide _ x T) t'
pattern ρ<_>_*_₊_-_ ns t x T t' = Rho _ ff (SomeNums ns) t (Guide _ x T) t'
pattern ρ+_-_ t t' = Rho _ tt NoNums t NoGuide t'
pattern ρ+<_>_-_ ns t t' = Rho _ tt (SomeNums ns) t NoGuide t'
pattern ρ+_*_₊_-_ t x T t' = Rho _ tt NoNums t (Guide _ x T) t'
pattern ρ+<_>_*_₊_-_ ns t x T t' = Rho _ tt (SomeNums ns) t (Guide _ x T) t'
`ρ_-_ = λ t t' → Rho pi-gen ff NoNums t NoGuide t'
`ρ<_>_-_ = λ ns t t' → Rho pi-gen ff (SomeNums ns) t NoGuide t'
`ρ_*_₊_-_ = λ t x T t' → Rho pi-gen ff NoNums t (Guide pi-gen x T) t'
`ρ<_>_*_₊_-_ = λ ns t x T t' → Rho pi-gen ff (SomeNums ns) t (Guide pi-gen x T) t'
`ρ+_-_ = λ t t' → Rho pi-gen tt NoNums t NoGuide t'
`ρ+<_>_-_ = λ ns t t' → Rho pi-gen tt (SomeNums ns) t NoGuide t'
`ρ+_*_₊_-_ = λ t x T t' → Rho pi-gen tt NoNums t (Guide pi-gen x T) t'
`ρ+<_>_*_₊_-_ = λ ns t x T t' → Rho pi-gen tt (SomeNums ns) t (Guide pi-gen x T) t'

-- Sigma
infixr 9 ς_ `ς_
pattern ς_ t = Sigma _ t
`ς_ = Sigma pi-gen

-- Theta
infix 9 θ_`_ θ+_`_ θ<_>_`_ `θ_`_ `θ+_`_ `θ<_>_`_
pattern θ_`_ t ts = Theta _ Abstract t ts
pattern θ+_`_ t ts = Theta _ AbstractEq t ts
pattern θ<_>_`_ vs t ts = Theta _ (AbstractVars vs) t ts
`θ_`_ = λ t ts → Theta pi-gen Abstract t ts
`θ+_`_ = λ t ts → Theta pi-gen AbstractEq t ts
`θ<_>_`_ = λ vs t ts → Theta pi-gen (AbstractVars vs) t ts

-- Mu
infix 9 μ_₊_[_] μ_₊_*_[_] `μ_₊_[_] `μ_₊_*_[_]
pattern μ_₊_[_] x t ms = Mu _ _ x t NoType _ ms _
pattern μ_₊_*_[_] x t T ms = Mu _ _ x t (SomeType T) _ ms _
`μ_₊_[_] = λ x t ms → Mu pi-gen pi-gen x t NoType pi-gen ms pi-gen
`μ_₊_*_[_] = λ x t T ms → Mu pi-gen pi-gen x t (SomeType T) pi-gen ms pi-gen

-- Mu'
infix 9 μ'_[_] μ'_*_[_] μ'<_>_[_] μ'<_>_*_[_] `μ'_[_] `μ'_*_[_] `μ'_[_] `μ'_*_[_]
pattern μ'_[_] t ms = Mu' _ NoTerm t NoType _ ms _
pattern μ'_*_[_] t T ms = Mu' _ NoTerm t (SomeType T) _ ms _
pattern μ'<_>_[_] t t' ms = Mu' _ (SomeTerm t) t' NoType _ ms _
pattern μ'<_>_*_[_] t t' T ms = Mu' _ (SomeTerm t) t' (SomeType T) _ ms _
`μ'_[_] = λ t ms → Mu' pi-gen NoTerm t NoType pi-gen ms pi-gen
`μ'_*_[_] = λ t T ms → Mu' pi-gen NoTerm t (SomeType T) pi-gen ms pi-gen
`μ'<_>_[_] = λ t t' ms → Mu' pi-gen (SomeTerm t pi-gen) t' NoType pi-gen ms pi-gen
`μ'<_>_*_[_] = λ t t' T ms → Mu' pi-gen (SomeTerm t pi-gen) t' (SomeType T) pi-gen ms pi-gen

-- Var
infixr 11 vₓ_ `vₓ_
pattern vₓ_ x = Var _ x
`vₓ_ = Var pi-gen

-- Abs
infixr 5 ∀`_:ₜ_₊_ ∀`_:ₖ_₊_ Π_:ₜ_₊_ Π_:ₖ_₊_ `∀_:ₜ_₊_ `∀_:ₖ_₊_ `Π_:ₜ_₊_ `Π_:ₖ_₊_
pattern ∀`_:ₜ_₊_ x T T' = Abs _ All _ x (Tkt T) T'
pattern ∀`_:ₖ_₊_ x k T = Abs _ All _ x (Tkk k) T
pattern Π_:ₜ_₊_ x T T' = Abs _ Pi _ x (Tkt T) T'
pattern Π_:ₖ_₊_ x k T = Abs _ Pi _ x (Tkk k) T
`∀_:ₜ_₊_ = λ x T T' → Abs pi-gen All pi-gen x (Tkt T) T'
`∀_:ₖ_₊_ = λ x k T → Abs pi-gen All pi-gen x (Tkk k) T
`Π_:ₜ_₊_ = λ x T T' → Abs pi-gen Pi pi-gen x (Tkt T) T'
`Π_:ₖ_₊_ = λ x k T → Abs pi-gen Pi pi-gen x (Tkk k) T

-- Iota
infix 4 ι_:ₜ_₊_ `ι_:ₜ_₊_
pattern ι_:ₜ_₊_ x T T' = Iota _ _ x T T'
`ι_:ₜ_₊_ = Iota pi-gen pi-gen

-- Lft
infix 4 ↑_₊_:ₗ_ `↑_₊_:ₗ_
pattern ↑_₊_:ₗ_ X t lT = Lft _ _ X t lT
`↑_₊_:ₗ_ = Lft pi-gen pi-gen

-- NoSpans
infix 4 [^_^] `[^_^]
pattern [^_^] T = NoSpans T _
`[^_^] = λ T → NoSpans T pi-gen

-- TpLet
infixr 5 [_`=_]ₜ-_ [_:ₜ_`=_]ₜ-_ [_:ₖ_`=_]ₜ-_ `[_`=_]ₜ-_ `[_:ₜ_`=_]ₜ-_ `[_:ₖ_`=_]ₜ-_
pattern [_`=_]ₜ-_ x t t' = TpLet _ (DefTerm _ x NoType t _) t'
pattern [_:ₜ_`=_]ₜ-_ x T t t' = TpLet _ (DefTerm _ x (SomeType T) t _) t'
pattern [_:ₖ_`=_]ₜ-_ x k T t' = TpLet _ (DefType _ x k T _) t'
`[_`=_]ₜ-_ = λ x t t' → TpLet pi-gen (DefTerm pi-gen x NoType t) t'
`[_:ₜ_`=_]ₜ-_ = λ x T t t' → TpLet pi-gen (DefTerm pi-gen x (SomeType T) t) t'
`[_:ₖ_`=_]ₜ-_ = λ x k T t' → TpLet pi-gen (DefType pi-gen x k T) t'

-- TpApp, TpAppt
infixl 10 _·ₜ_ _`ₜ_
-- Pattern and constructor
pattern _·ₜ_ T T' = TpApp T T'
pattern _`ₜ_ T t = TpAppt T t

-- TpArrow
infixr 5 _➔_ _➾_  -- "➔" = "\r" (↕ 5, ↔ 1), "➾" = "\r" (↕ 7, ↔ 8)
pattern _➔_ T T' = TpArrow T NotErased T'
pattern _➾_ T T' = TpArrow T Erased T'

-- TpEq
infix 4 [_≃_] `[_≃_]
pattern [_≃_] t₁ t₂ = TpEq _ t₁ t₂ _
`[_≃_] = λ t₁ t₂ → TpEq pi-gen t₁ t₂ pi-gen

-- TpHole
pattern ●ₜ = TpHole _
`●ₜ = TpHole pi-gen

-- TpLambda
infixr 4 λₜ_:ₜ_₊_ λₜ_:ₖ_₊_ `λₜ_:ₜ_₊_ `λₜ_:ₖ_₊_
pattern λₜ_:ₜ_₊_ x T T' = TpLambda _ _ x (Tkt T) T'
pattern λₜ_:ₖ_₊_ x k T = TpLambda _ _ x (Tkk k) T
`λₜ_:ₜ_₊_ = λ x T T' → TpLambda pi-gen pi-gen x (Tkt T) T'
`λₜ_:ₖ_₊_ = λ x k T → TpLambda pi-gen pi-gen x (Tkk k) T

-- TpParens
infix 4 ⦅_⦆ₜ `⦅_⦆ₜ
pattern ⦅_⦆ₜ T = TpParens _ T _
`⦅_⦆ₜ = λ T → TpParens pi-gen T pi-gen

-- TpVar
infix 11 Vₓ_ `Vₓ_
pattern Vₓ_ x = TpVar _ x
`Vₓ_ = TpVar pi-gen

-- KndArrow : kind → kind → kind

-- KndParens : posinfo → kind → posinfo → kind
infix 4 ⦅_⦆ₖ `⦅_⦆ₖ
pattern ⦅_⦆ₖ k = KndParens _ k _
`⦅_⦆ₖ = λ k → KndParens pi-gen k pi-gen

-- KndPi : posinfo → posinfo → bvar → tk → kind → kind

-- KndTpArrow : type → kind → kind

-- KndVar
infix 11 κ_`_ `κ_`_
pattern κ_`_ x as = KndVar _ x as
`κ_`_ = KndVar pi-gen

-- Star
pattern ★ = Star _
`★ = Star pi-gen

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
{-# OPTIONS --without-K #-}
module mini-quine where
open import common

infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_
infixl 3 _‘’ₐ_
infixl 3 _w‘‘’’ₐ_
infixr 2 _‘∘’_

mutual
  data Context : Set where
    ε : Context
    _▻_ : (Γ : Context) → Type Γ → Context

  data Type : Context → Set where
    W : ∀ {Γ A} → Type Γ → Type (Γ ▻ A)
    W1 : ∀ {Γ A B} → Type (Γ ▻ B) → Type (Γ ▻ A ▻ (W {Γ = Γ} {A = A} B))
    _‘’_ : ∀ {Γ A} → Type (Γ ▻ A) → Term {Γ} A → Type Γ
    ‘Typeε’ : ∀ {Γ} → Type Γ
    ‘□’ : ∀ {Γ} → Type (Γ ▻ ‘Typeε’)
    _‘→’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
    Quine : Type (ε ▻ ‘Typeε’) → Type ε
    ‘⊤’ : ∀ {Γ} → Type Γ
    ‘⊥’ : ∀ {Γ} → Type Γ

  data Term : {Γ : Context} → Type Γ → Set where
    ⌜_⌝ : ∀ {Γ} → Type ε → Term {Γ} ‘Typeε’
    ⌜_⌝t : ∀ {Γ T} → Term {ε} T → Term {Γ} (‘□’ ‘’ ⌜ T ⌝)
    ‘⌜‘VAR₀’⌝t’ : ∀ {T} → Term {ε ▻ ‘□’ ‘’ ⌜ T ⌝} (W (‘□’ ‘’ ⌜ ‘□’ ‘’ ⌜ T ⌝ ⌝))
    ‘λ∙’ : ∀ {Γ A B} → Term {Γ ▻ A} (W B) → Term {Γ} (A ‘→’ B)
    ‘VAR₀’ : ∀ {Γ T} → Term {Γ ▻ T} (W T)
    _‘’ₐ_ : ∀ {Γ A B} → Term {Γ} (A ‘→’ B) → Term {Γ} A → Term {Γ} B
    quine→ : ∀ {φ} → Term {ε} (Quine φ        ‘→’ φ ‘’ ⌜ Quine φ ⌝)
    quine← : ∀ {φ} → Term {ε} (φ ‘’ ⌜ Quine φ ⌝ ‘→’ Quine φ)
    ‘tt’ : ∀ {Γ} → Term {Γ} ‘⊤’
    →SW1SV→W : ∀ {Γ T X A B} {x : Term X}
      → Term {Γ} (T ‘→’ (W1 A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x)
      → Term {Γ} (T ‘→’ A ‘’ x ‘→’ B)
    ←SW1SV→W : ∀ {Γ T X A B} {x : Term X}
      → Term {Γ} ((W1 A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x ‘→’ T)
      → Term {Γ} ((A ‘’ x ‘→’ B) ‘→’ T)
    w : ∀ {Γ A T} → Term {Γ} A → Term {Γ ▻ T} (W A)
    w→ : ∀ {Γ A B X} → Term {Γ} (A ‘→’ B) → Term {Γ ▻ X} (W A ‘→’ W B)
    _‘∘’_ : ∀ {Γ A B C} → Term {Γ} (B ‘→’ C) → Term {Γ} (A ‘→’ B) → Term {Γ} (A ‘→’ C)
    _w‘‘’’ₐ_ : ∀ {A B T} → Term {ε ▻ T} (W (‘□’ ‘’ ⌜ A ‘→’ B ⌝)) → Term {ε ▻ T} (W (‘□’ ‘’ ⌜ A ⌝)) → Term {ε ▻ T} (W (‘□’ ‘’ ⌜ B ⌝))

□ : Type ε → Set _
□ = Term {ε}

max-level : Level
max-level = lzero

mutual
  Context⇓ : (Γ : Context) → Set (lsuc max-level)
  Context⇓ ε = ⊤
  Context⇓ (Γ ▻ T) = Σ (Context⇓ Γ) (Type⇓ {Γ} T)

  Type⇓ : {Γ : Context} → Type Γ → Context⇓ Γ → Set max-level
  Type⇓ (W T) Γ⇓ = Type⇓ T (Σ.proj₁ Γ⇓)
  Type⇓ (W1 T) Γ⇓ = Type⇓ T ((Σ.proj₁ (Σ.proj₁ Γ⇓)) , (Σ.proj₂ Γ⇓))
  Type⇓ (T ‘’ x) Γ⇓ = Type⇓ T (Γ⇓ , Term⇓ x Γ⇓)
  Type⇓ ‘Typeε’ Γ⇓ = Lifted (Type ε)
  Type⇓ ‘□’ Γ⇓ = Lifted (Term {ε} (lower (Σ.proj₂ Γ⇓)))
  Type⇓ (A ‘→’ B) Γ⇓ = Type⇓ A Γ⇓ → Type⇓ B Γ⇓
  Type⇓ ‘⊤’ Γ⇓ = ⊤
  Type⇓ ‘⊥’ Γ⇓ = ⊥
  Type⇓ (Quine φ) Γ⇓ = Type⇓ φ (Γ⇓ , (lift (Quine φ)))

  Term⇓ : ∀ {Γ : Context} {T : Type Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Type⇓ T Γ⇓
  Term⇓ ⌜ x ⌝ Γ⇓ = lift x
  Term⇓ ⌜ x ⌝t Γ⇓ = lift x
  Term⇓ ‘⌜‘VAR₀’⌝t’ Γ⇓ = lift ⌜ (lower (Σ.proj₂ Γ⇓)) ⌝t
  Term⇓ (f ‘’ₐ x) Γ⇓ = Term⇓ f Γ⇓ (Term⇓ x Γ⇓)
  Term⇓ ‘tt’ Γ⇓ = tt
  Term⇓ (quine→ {φ}) Γ⇓ x = x
  Term⇓ (quine← {φ}) Γ⇓ x = x
  Term⇓ (‘λ∙’ f) Γ⇓ x = Term⇓ f (Γ⇓ , x)
  Term⇓ ‘VAR₀’ Γ⇓ = Σ.proj₂ Γ⇓
  Term⇓ (←SW1SV→W f) = Term⇓ f
  Term⇓ (→SW1SV→W f) = Term⇓ f
  Term⇓ (w x) Γ⇓ = Term⇓ x (Σ.proj₁ Γ⇓)
  Term⇓ (w→ f) Γ⇓ = Term⇓ f (Σ.proj₁ Γ⇓)
  Term⇓ (g ‘∘’ f) Γ⇓ x = Term⇓ g Γ⇓ (Term⇓ f Γ⇓ x)
  Term⇓ (f w‘‘’’ₐ x) Γ⇓ = lift (lower (Term⇓ f Γ⇓) ‘’ₐ lower (Term⇓ x Γ⇓))

module inner (‘X’ : Type ε) (‘f’ : Term {ε} (‘□’ ‘’ ⌜ ‘X’ ⌝ ‘→’ ‘X’)) where
  ‘H’ : Type ε
  ‘H’ = Quine (W1 ‘□’ ‘’ ‘VAR₀’ ‘→’ W ‘X’)

  ‘toH’ : □ ((‘□’ ‘’ ⌜ ‘H’ ⌝ ‘→’ ‘X’) ‘→’ ‘H’)
  ‘toH’ = ←SW1SV→W quine←

  ‘fromH’ : □ (‘H’ ‘→’ (‘□’ ‘’ ⌜ ‘H’ ⌝ ‘→’ ‘X’))
  ‘fromH’ = →SW1SV→W quine→

  ‘□‘H’→□‘X’’ : □ (‘□’ ‘’ ⌜ ‘H’ ⌝ ‘→’ ‘□’ ‘’ ⌜ ‘X’ ⌝)
  ‘□‘H’→□‘X’’ = ‘λ∙’ (w ⌜ ‘fromH’ ⌝t w‘‘’’ₐ ‘VAR₀’ w‘‘’’ₐ ‘⌜‘VAR₀’⌝t’)

  ‘h’ : Term ‘H’
  ‘h’ = ‘toH’ ‘’ₐ (‘f’ ‘∘’ ‘□‘H’→□‘X’’)

  Lӧb : □ ‘X’
  Lӧb = ‘fromH’ ‘’ₐ ‘h’ ‘’ₐ ⌜ ‘h’ ⌝t

Lӧb : ∀ {X} → Term {ε} (‘□’ ‘’ ⌜ X ⌝ ‘→’ X) → Term {ε} X
Lӧb {X} f = inner.Lӧb X f

⌞_⌟ : Type ε → Set _
⌞ T ⌟ = Type⇓ T tt

‘¬’_ : ∀ {Γ} → Type Γ → Type Γ
‘¬’ T = T ‘→’ ‘⊥’

lӧb : ∀ {‘X’} → □ (‘□’ ‘’ ⌜ ‘X’ ⌝ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
lӧb f = Term⇓ (Lӧb f) tt

incompleteness : ¬ □ (‘¬’ (‘□’ ‘’ ⌜ ‘⊥’ ⌝))
incompleteness = lӧb

soundness : ¬ □ ‘⊥’
soundness x = Term⇓ x tt

non-emptyness : Σ (Type ε) (λ T → □ T)
non-emptyness = ‘⊤’ , ‘tt’

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob