text:
-- if curious: https://agda.readthedocs.io/en/v2.6.0.1/language/without-k.html
{-# OPTIONS --without-K --allow-unsolved-metas #-}

{-
  CS 598 TLR
  Artifact 1: Proof Objects
  Student Copy

  READ ME FIRST: You will absolutely not be graded on your ability to finish
  these proofs. It's OK to be confused and find this hard. It's also
  OK to come into this class as an Agda wizard and breeze through this,
  perhaps even using a bunch of features of Agda that aren't mentioned
  in this file at all (if you do that, though, please help your partner
  understand what you are doing, and please discuss what you did at the end).
  The point is to pay attention to what is hard and where you wish you
  had better automation, and to learn about proof objects.

  At the end of this class (or, if you're not attending in person,
  sometime before 1230 PM the day of class) you'll post on the forum
  about what you found challenging, what you enjoyed, and─most importantly
  for this class─what kind of automation you wish you had.
  If you or someone you're working with is an Agda wizard already,
  and you know about automation or syntax that already exists that makes the
  job easy, definitely take note of that and mention it as well.

  If you have a lot of trouble with a proof, it's OK to ask me for help
  (or post in the forum if you're not here in person). It's also OK to
  ask people in other groups.

  But please, please don't stress about finishing these proofs.
  The theorems will still be here after class if you feel tempted by them.
  I'm also happy to distribute my own answer key, or to let you share
  proofs with other students later─the point is to think about the proof
  objects you construct throughout, and the experience you have constructing
  them. It's about the journey, not the destination.
-}
module proof-objects where

{-
  Some built-in datatypes we'll use in this exercise:
-}
open import Agda.Builtin.Nat -- natural numbers
open import Agda.Builtin.List -- polymorphic lists
open import Agda.Builtin.Char -- characters
open import Agda.Builtin.Equality -- equality

{-
  You can see these definitions by clicking them and then pressing the Alt
  key along with the period. Or you can use the middle button of your mouse,
  if you have one.

  For example, if we click on Agda.Builtin.List and press the Alt key
  along with the period, it will open up the file that defines the
  list datatype. A polymorphic list in Agda is defined a lot like the
  list datatype in Coq that we saw in the slides for the first class.
  It is an inductive datatype with two cases:

    data List (A : Set) : Set where
      []  : List A
      _∷_ : A → List A → List A

  In other words, as in Coq, a list is either empty ([]) or the result
  of consing (∷) an element of type A in front of some other list of
  elements of type A.

  For example, let's define some empty lists of numbers and characters.
  In Agda, a definition has its type on the first line, and then the
  term with that type on the next line:
-}

-- The empty list of natural numbers
empty-nat : List Nat -- the type
empty-nat = [] -- the term

-- The empty list of characters
empty-char : List Char -- the type
empty-char = [] -- the term

{-
  Cool. Now let's define some non-empty lists.

  NOTE: The Agda community has an unfortunate obsession with Unicode.
  The syntax for the cons constructor in Coq is two colons, written ::.
  Confusingly, the Agda cons constructor is actually denoted with a
  single special unicode character, written ∷. You can write this
  special character by typing \:: (with two colons), and it will
  magically turn into ∷.

  OK, with that in mind:
-}

-- A list [1; 2; 3; 4]
1-2-3-4 : List Nat -- type
1-2-3-4 = 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] -- term

-- A list [x; y; z]
x-y-z : List Char -- type
x-y-z = 'x' ∷ 'y' ∷ 'z' ∷ [] -- term

{-
  As in Coq, we can write functions about lists, like our length function,
  which we define by pattern matching. The syntax for pattern matching in
  Agda is defining each case on a different line:
-}

-- list length
length : ∀ {A : Set} → List A → Nat -- type
length [] = 0 -- term in the empty case
length (h ∷ tl) = suc (length tl) -- term in the cons case

{-
  That is, the length of the empty list ([]) is zero (0), and the
  length any other list (h ∷ tl) is one plus (suc, for "successor")
  the length of the tail of the list (length tl).

  NOTE: Thanks to the Agda community's unicode obsession, you can write
  the above ∀ by typing \forall, and you can write the above → by typing
  \r or \->. But it's OK to spell them out as forall and ->.

  EXERCISE 1: Write a function that reverses a list.
  You may use the function app I've written for you below,
  which appends two lists.

  NOTE: The {! !} syntax I've written inside of the sketch of rev is a
  hole─you will want to replace this with your implementation of rev for
  each case. These holes change color when you compile files, and numbers
  appear next to them; I explain this a bit more later on.

  NOTE: You can compile this file by running C-c C-l, to just
  invoke the type checker. To produce an executable file,
  you can run C-c C-x C-c and specify the GHC backend, but this isn't necessary
  to just check the proofs you'll write in this file. The first time
  you compile this file, you'll see a bunch of numbered constrants;
  these correspond to the holes I've left in the file for you to fill.
-}

-- list append
app : ∀ {A : Set} → List A → List A → List A -- type
app [] l = l -- term in the empty case
app (h ∷ tl) l = h ∷ app tl l -- term in the cons case

-- list rev
rev : ∀ {A : Set} → List A → List A -- type
rev [] = {! !} -- your term in the empty case goes here
rev (h ∷ tl) = {! !} -- your term in the cons case goes here

{-
  Let's test your rev function.
  We're going to check that, on the lists we've defined at the top
  of this file, the result of calling rev gives us the reverse lists.

  To do that, we need a way to state what it means for two things to be
  equal. Equality in Agda is written ≡, which is typed as \== using the same
  magic as before, because of the community's unicode obsession:

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

  Equality is an inductive datatype, just like lists. But one thing that's
  cool about the equality type is that it's something called a dependent type.
  A dependent type is a lot like a polymorphic type, but instead of taking
  a type argument (like the A in List A), it takes a _term_ argument
  (like the x in x ≡ x). Dependent types can refer to values!
  So we can define the type of all terms that prove our lists
  behave the way we want them to. And then we can write terms that
  have those types─our proofs.

  There is exactly one constructor for the equality type in Agda:
  refl, for reflexivity. Two things are equal by reflexivity when they
  compute to the same result. So if your rev function is correct,
  these test cases should compile:
-}

-- empty-nat doesn't change
rev-empty-nat-empty-nat : rev empty-nat ≡ empty-nat
rev-empty-nat-empty-nat = refl

-- empty-char doesn't change
rev-empty-char-empty-char : rev empty-char ≡ empty-char
rev-empty-char-empty-char = refl

-- [1; 2; 3; 4] becomes [4; 3; 2; 1]
rev-1-2-3-4-4-3-2-1 : rev 1-2-3-4 ≡ 4 ∷ 3 ∷ 2 ∷ 1 ∷ []
rev-1-2-3-4-4-3-2-1 = refl

-- [x; y; z] becomes [z; y; x]
rev-x-y-z-z-y-x : rev x-y-z ≡ 'z' ∷ 'y' ∷ 'x' ∷ []
rev-x-y-z-z-y-x = refl

{-
  These test cases are actually proofs! Even though they all hold
  by computation (reflexivity), they are terms, just like the lists
  we refer to inside of them. Their types are the theorems that they prove.

  That's the beauty of Curry-Howard; our terms here are proof objects
  that prove the theorems stated by the types they inhabit.
  These programs are proofs!

  So now it's your turn to test my length function and, in the process,
  write some proofs yourself.

  EXERCISE 2: Prove that 1-2-3-4 and x-y-z have the right lengths.
  As before, you'll want to replace each hole {! !} with your own code.
  This time, I want you to define both the types and the terms.
-}

-- 1-2-3-4 has the right length
length-1-2-3-4-OK : {! !}
length-1-2-3-4-OK = {! !}

-- x-y-z has the right length
length-x-y-z-OK : {! !}
length-x-y-z-OK = {! !}

{-
  Those proofs are very small proofs that hold by computation.
  There are also some cooler proofs we can prove by computation,
  like that appending the empty list to the left of any list
  gives us back that list:
-}

-- left identity of nil for append
app-nil-l : ∀ {A : Set} → (l : List A) → app [] l ≡ l -- type or theorem
app-nil-l l = refl -- term or proof

{-
  But sometimes we need to get fancier! For example, if we simply swap
  the [] and l in the type definition above above, to define app-nil-r,
  this will no longer hold by reflexivity, since app is defined by
  matching over the first list, not the second. Because of this,
  when you put the empty list as the first argument, Agda can reduce it;
  when you put it as the second argument instead, Agda cannot reduce it.

  If we try to prove app-nil-r by reflexivity, we'll get a scary looking
  type error, like this:

    app l [] != l of type List A
    when checking that the expression refl has type app l [] ≡ l

  But here's the thing─the equality is still true!
  It's just not true by computation. We have to prove it differently.
  Agda needs our help figuring this out.

  So let's help Agda. We're going to need to write some fancier proofs
  about equality. But how do we do that if there's just one constructor
  for equality─refl? Well, there are two things we can do with inductive
  datatypes: we can construct them, and we can pattern match over their cases
  (the latter is also called destructing them or, for reasons you'll see later,
  in specific contexts, inducting over them).

  Since equality is defined as an inductive type, we can pattern match
  over it just like we do over lists. When we do, there will be just one
  case─refl. But that actually turns out to give us a lot of power to
  prove some cool things about equality. So let's do that.

  Our first lemma is congruence, which comes from the standard library,
  and states that function application preserves equality:
-}

-- congruence
cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y -- the lemma
cong f refl = refl -- the proof

{-
  In other words, this matches over the input argument of type x ≡ y.
  Since equality has just one case, pattern matching breaks this into
  just one case, which is when that equality is refl.
  When that equality is refl, then we have x ≡ x.
  Thus, we are trying to show f x ≡ f x, which also holds by refl,
  since these terms are the same.

  One thing to note here is that it can be super hard to track this information
  in your head. In Agda, you can create holes in your functions
  by typing {! !}, much like I've done for you throughout. So you could write:

    cong f refl = {! !}

  If you compile that with C-c C-l, it'll change colors and there
  will be a 0 next to it, indicating that it's the 0th goal. In the AgdaInfo
  buffer, you'll see the goal that you need to satisfy for that hole:

    ?0 : f x ≡ f x

  This goal is the type you're trying to inhabit. From there,
  you can figure out that refl has that type, without having to track
  so much information in your head about what Agda is doing.

  With this, we should be able to prove app-nil-r:
-}

-- right identity of nil for append
app-nil-r : ∀ {A : Set} → (l : List A) → app l [] ≡ l
app-nil-r [] = refl
app-nil-r (h ∷ tl) = cong (λ l′ → h ∷ l′) (app-nil-r tl)

{-
  EXERCISE 3: Prove the lemma sym, which states that equality is symmetric.
  I have inserted a hole into this lemma, denoted {! !}, which may
  already look green if you've compiled this file. You can use the
  workflow described above to figure out the type you're trying to inhabit.
-}

-- symmetry of equality
sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = {! !}

{-
  EXERCISE 4: Prove that l ≡ app l [], using symmetry. I have inserted
  a hole into this lemma where you will need to figure out a term.
-}

-- symmetric right identity of nil for append
app-nil-r-sym : ∀ {A : Set} → (l : List A) → l ≡ app l []
app-nil-r-sym l = sym {! !}

{-
  EXERCISE 5: Prove the lemma trans, which states that equality
  is transitive. I have inserted a hole into this lemma as well.
-}

-- transitivity of equality
trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = {! !}

{-
  Equalities like this that we have to prove by pattern matching over
  the equality type are what we called propositional equalities
  in QED at Large. This is in contrast with definitional equalities,
  which hold by computation.

  For example, app [] l and l are definitionally equal, since Agda
  reduces both of them to the same term. But app l [] and l are not
  definitionally equal, as we saw earlier, since app is defined by
  pattern matching over the first term rather than the second.
  They are only propositionally─provably, that is─equal.

  In Agda, Coq, and Lean, two things that are definitionally equal are
  necessarily propositionally equal, but the reverse is not necessarily true.
  This is why we can't prove app-nil-r by reflexivity.

  This is important to pay attention to─in many of these languages, it is
  really standard for your proofs to mirror the structure of
  the programs they are about. There is a deep type theoretical
  reason that this is true.

  ASIDE: Definitional equality is─for many proof assistants we care about in
  this class─a decidable judgment that follows from a few reduction rules,
  like unfolding some constants (δ-expansion), applying functions to
  arguments (Β-reduction, which is sometimes called ι-reduction for
  inductive datatypes), renaming (α-conversion), and more.

  These may sound familiar if you're familiar with the λ-calculus,
  a simple functional programming language that is often used as an example
  in programming languages courses. The proof assistants Agda, Coq, and Lean
  all build on extensions of the λ-calculus with not just simple types,
  but also polymorphism (like how list takes a type argument A), dependent
  types (like how ≡ takes a term argument x), and inductive types (like
  how both the list and ≡ datatypes are defined by defining all ways to
  construct them).

  But if you haven't heard of these, that's OK. I super recommend reading this
  chapter of Certified Programming with Dependent Types by Adam Chlipala:
  http://adam.chlipala.net/cpdt/html/Equality.html. If you'd like more
  information, that will really help─though it's in Coq. I hope to
  show you some automation that steps through equalities like this next week.

  BACK TO BUSINESS: It can be kind of annoying to keep pattern matching
  over equality, which is why the lemmas above─also defined in the standard
  library─can be really useful.

  An especially useful lemma about equality is substitution,
  which is also found inside of the standard library:
-}

-- substitution
subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

{-
  This states that for any property P, if x ≡ y, and we have a proof
  that P x holds, we can substitute y for x inside of that to show
  that P y holds. This is really powerful, but a little hard to use,
  because you have to figure out what P is. For example, here is a proof
  of app-nil-r using subst instead of cong:
-}

-- right identity of nil for append, proven by substitution instead
app-nil-r′ : ∀ {A : Set} → (l : List A) → app l [] ≡ l
app-nil-r′ [] = refl
app-nil-r′ (h ∷ tl) = subst (λ l′ → h ∷ l′ ≡ h ∷ tl) (sym (app-nil-r′ tl)) refl

{-
  Your turn to try. You can use cong or subst here─whatever you find
  more convenient.

  EXERCISE 6: Finish the proof of length-succ-r.
-}
length-succ-r :
  ∀ {A} → (l : List A) → (a : A) → length (app l (a ∷ [])) ≡ suc (length l)
length-succ-r [] a = refl  -- base case
length-succ-r {A} (h ∷ tl) a = -- inductive case
  {! !}

{-
  EXERCISE 7: Show that the reverse function that you wrote preserves
  the length of the input list. You may use length-succ-r, and any of the
  equality lemmas we've defined so far like trans, subst, sym, and
  cong. (You probably won't need all of them.)
-}
rev-pres-length : ∀ {A} → (l : List A) → length (rev l) ≡ length l
rev-pres-length [] = {! !}
rev-pres-length (h ∷ tl) = {! !}

{-
  That's it for now! You can keep playing with other proofs if you have
  extra time. If you have a lot of extra time, I recommend looking at the
  Agda source code on Github to get a sense for how it's implemented:
  https://github.com/agda/agda. In any case, when we have 25 minutes
  left of class, please do this:

    1. Turn to your group and discuss the question below.
    2. Post your answer─just one answer for your group, clearly indicating
       all members of the group. (If you are not here, and are working alone,
       you can post your answer alone.)
    3. With 10 minutes left, finish posting your answer, so we can discuss
       a bit as a class.

  You'll be graded based on whether you post an answer, not based on
  what it is, so don't worry too much about saying something silly.

  DISCUSSION QUESTION: What was it like constructing these proofs directly,
  as terms in a programming language? What did you find challenging about
  this experience, if anything? What did you find helpful, if anything? Did
  you get stuck at any point, and if so, where and why? Where do you wish
  you'd had more automation to help you out?
-}


text:
------------------------------------------------------------------------
-- The semantics given in OneSemantics and TwoSemantics are equivalent
------------------------------------------------------------------------

module Lambda.Substitution.Equivalence where

open import Codata.Musical.Notation

open import Lambda.Syntax
open WHNF
open import Lambda.Substitution.OneSemantics
open import Lambda.Substitution.TwoSemantics

⇒⟶⇓ : ∀ {n t} {v : Value n} → t ⇒ val v → t ⇓ v
⇒⟶⇓ val                 = val
⇒⟶⇓ (app t₁⇓ t₂⇓ t₁t₂⇒) = app (⇒⟶⇓ t₁⇓) (⇒⟶⇓ t₂⇓) (⇒⟶⇓ t₁t₂⇒)

⇒⊥⟶⇑ : ∀ {n} {t : Tm n} → t ⇒ ⊥ → t ⇑
⇒⊥⟶⇑ (·ˡ t₁⇑)            = ·ˡ (♯ (⇒⊥⟶⇑ (♭ t₁⇑)))
⇒⊥⟶⇑ (·ʳ t₁⇓ t₂⇑)        = ·ʳ (⇒⟶⇓ t₁⇓) (♯ (⇒⊥⟶⇑ (♭ t₂⇑)))
⇒⊥⟶⇑ (app t₁⇓ t₂⇓ t₁t₂⇒) = app (⇒⟶⇓ t₁⇓) (⇒⟶⇓ t₂⇓) (♯ (⇒⊥⟶⇑ (♭ t₁t₂⇒)))

⇓⟶⇒ : ∀ {n t} {v : Value n} → t ⇓ v → t ⇒ val v
⇓⟶⇒ val                 = val
⇓⟶⇒ (app t₁⇓ t₂⇓ t₁t₂⇓) = app (⇓⟶⇒ t₁⇓) (⇓⟶⇒ t₂⇓) (⇓⟶⇒ t₁t₂⇓)

⇑⟶⇒⊥ : ∀ {n} {t : Tm n} → t ⇑ → t ⇒ ⊥
⇑⟶⇒⊥ (·ˡ t₁⇑)            = ·ˡ (♯ (⇑⟶⇒⊥ (♭ t₁⇑)))
⇑⟶⇒⊥ (·ʳ t₁⇓ t₂⇑)        = ·ʳ (⇓⟶⇒ t₁⇓) (♯ (⇑⟶⇒⊥ (♭ t₂⇑)))
⇑⟶⇒⊥ (app t₁⇓ t₂⇓ t₁t₂⇓) = app (⇓⟶⇒ t₁⇓) (⇓⟶⇒ t₂⇓) (♯ (⇑⟶⇒⊥ (♭ t₁t₂⇓)))

ext: agda

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Coinduction using ( ∞ ; ♯_ ; ♭ )
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₂ )
open import Data.Nat using ( ℕ ; zero ; suc )
open import Data.Empty using ( ⊥ )
open import FRP.LTL.ISet.Core using ( ISet ; M⟦_⟧ ; ⟦_⟧ ; ⌈_⌉ ; _,_ ; splitM⟦_⟧ ) renaming ( [_] to ⟪_⟫ )
open import FRP.LTL.ISet.Globally using ( □ ; [_] )
open import FRP.LTL.ISet.Stateless using ( _⇒_ ; _$_  )
open import FRP.LTL.RSet.Core using ( RSet )
open import FRP.LTL.Time.Bound using
  ( Time∞ ; fin ; +∞ ; _≺_ ; _≼_ ; _⋠_ ; ≺-Indn ; _,_
  ; ≺-impl-≼ ; ≼-refl ; _≼-trans_ ; ≡-impl-≽ ; ≺-impl-≢ ; ≺-impl-⋡ ; t≺+∞ ; ∞≼-impl-≡∞ ; ≺-indn )
open import FRP.LTL.Time.Interval using ( [_⟩ ; Int ; ↑ )
open import FRP.LTL.Util using ( ⊥-elim )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Unary using ( _∈_ )

module FRP.LTL.ISet.Causal where

infixr 2 _⊵_
infixr 3 _⋙_ _≫_ _⊨_≫_

-- A ⊵ B is the causal function space from A to B

data _∙_⊸_∙_ (A : ISet) (s : Time∞) (B : ISet) (u : Time∞) : Set where
  inp : .(s ≼ u) → .(u ≺ +∞) →
    (∀ {t} .(s≺t : s ≺ t) → M⟦ A ⟧ [ s≺t ⟩ → ∞ (A ∙ t ⊸ B ∙ u)) →
      (A ∙ s ⊸ B ∙ u)
  out : ∀ {v} .(u≺v : u ≺ v) →
    M⟦ B ⟧ [ u≺v ⟩ → ∞ (A ∙ s ⊸ B ∙ v) →
      (A ∙ s ⊸ B ∙ u)
  done : .(u ≡ +∞) →
    (A ∙ s ⊸ B ∙ u)

_⊵_ : ISet → ISet → ISet
A ⊵ B = ⌈ (λ t → A ∙ fin t ⊸ B ∙ fin t) ⌉

-- Categorical structure

ar : ∀ {A B} t → M⟦ A ⇒ B ⟧ (↑ t) → (A ∙ fin t ⊸ B ∙ fin t)
ar {A} {B} t f = inp ≼-refl t≺+∞ P where

  P : ∀ {u} .(t≺u : fin t ≺ u) → M⟦ A ⟧ [ t≺u ⟩ → ∞ (A ∙ u ⊸ B ∙ fin t)
  P {+∞}    t≺u σ = ♯ out t≺u (f $ σ) (♯ done refl)
  P {fin u} t≺u σ with splitM⟦ A ⇒ B ⟧ [ t≺u ⟩ (↑ u) refl f
  P {fin u} t≺u σ | (f₁ , f₂) = ♯ out t≺u (f₁ $ σ) (♯ ar u f₂)

arr : ∀ {A B} → ⟦ □ (A ⇒ B) ⇒ (A ⊵ B) ⟧
arr ⟪ ⟪ f ⟫ ⟫ = ⟪ (λ t t∈i → ar t (f t t∈i) ) ⟫

-- We could define id in terms of arr, but we define it explictly for efficiency.

id : ∀ {A} t → (A ∙ t ⊸ A ∙ t)
id +∞      = done refl
id (fin t) = inp ≼-refl t≺+∞ (λ {u} t≺u σ → ♯ out t≺u σ (♯ id u))

identity : ∀ {A} → ⟦ A ⊵ A ⟧
identity = ⟪ (λ t t∈i → id (fin t)) ⟫

-- The following typechecks but does not pass the termination checker,
-- due to the possibility of infinite left-to-right chatter:

-- _≫_ : ∀ {A B C s t u} → (A ∙ s ⊸ B ∙ t) → (B ∙ t ⊸ C ∙ u) → (A ∙ s ⊸ C ∙ u)
-- P             ≫ out u≺w τ Q   = out u≺w τ (♯ (P ≫ ♭ Q))
-- P             ≫ done u≡∞      = done u≡∞
-- inp s≼t t≺∞ P ≫ inp t≼u u≺∞ Q = inp (s≼t ≼-trans t≼u) u≺∞ (λ s≺v σ → ♯ (♭ (P s≺v σ) ≫ inp t≼u u≺∞ Q))
-- done t≡∞      ≫ inp t≼u u≺∞ Q = ⊥-elim (≺-impl-≢ u≺∞ (∞≼-impl-≡∞ (≡-impl-≽ t≡∞ ≼-trans t≼u)))
-- out t≺v σ P   ≫ inp t≼u u≺∞ Q = out t≺v σ P ≫ inp t≼u u≺∞ Q

-- We have to be explicit about the induction scheme in the case of left-to-right
-- communication, which is because, for any t and u ≺ ∞, there is a bound
-- on the length of any ≺-chain between t and u.

mutual

  _⊨_≫_ : ∀ {A B C s t u} → (≺-Indn t u) → (A ∙ s ⊸ B ∙ t) → (B ∙ t ⊸ C ∙ u) → (A ∙ s ⊸ C ∙ u)
  n     , t+n≻u   ⊨ P             ≫ out u≺w τ Q   = out u≺w τ (♯ (P ≫ ♭ Q))
  n     , t+n≻u   ⊨ P             ≫ done u≡∞      = done u≡∞
  n     , t+n≻u   ⊨ inp s≼t t≺∞ P ≫ inp t≼u u≺∞ Q = inp (s≼t ≼-trans t≼u) u≺∞ (λ s≺v σ → ♯ (♭ (P s≺v σ) ≫ inp t≼u u≺∞ Q))
  n     , t+n≻u   ⊨ done t≡∞      ≫ inp t≼u u≺∞ Q = ⊥-elim (≺-impl-≢ u≺∞ (∞≼-impl-≡∞ (≡-impl-≽ t≡∞ ≼-trans t≼u)))
  zero  , u≺t     ⊨ out t≺v σ P   ≫ inp t≼u u≺∞ Q = ⊥-elim (≺-impl-⋡ u≺t t≼u)
  suc n , t+1+n≻u ⊨ out t≺v σ P   ≫ inp t≼u u≺∞ Q = n , t+1+n≻u t≺v ⊨ ♭ P ≫ ♭ (Q t≺v σ)

  _≫_ : ∀ {A B C s t u} → (A ∙ s ⊸ B ∙ t) → (B ∙ t ⊸ C ∙ u) → (A ∙ s ⊸ C ∙ u)
  P             ≫ out u≺w τ Q   = out u≺w τ (♯ (P ≫ ♭ Q))
  P             ≫ done u≡∞      = done u≡∞
  inp s≼t t≺∞ P ≫ inp t≼u u≺∞ Q = inp (s≼t ≼-trans t≼u) u≺∞ (λ s≺v σ → ♯ (♭ (P s≺v σ) ≫ inp t≼u u≺∞ Q))
  done t≡∞      ≫ inp t≼u u≺∞ Q = ⊥-elim (≺-impl-≢ u≺∞ (∞≼-impl-≡∞ (≡-impl-≽ t≡∞ ≼-trans t≼u)))
  out t≺v σ P   ≫ inp t≼u u≺∞ Q = ≺-indn u≺∞ ⊨ out t≺v σ P ≫ inp t≼u u≺∞ Q

_⋙_ : ∀ {A B C} → ⟦ (A ⊵ B) ⇒ (B ⊵ C) ⇒ (A ⊵ C) ⟧
(⟪ ⟪ f ⟫ ⟫ ⋙ ⟪ ⟪ g ⟫ ⟫) = ⟪ (λ t t∈i → f t t∈i ≫ g t t∈i) ⟫

-- Apply a process to some of its output

_/_/_ : ∀ {A B s t u} → (A ∙ s ⊸ B ∙ u) → .(s≺t : s ≺ t) → M⟦ A ⟧ [ s≺t ⟩ → (A ∙ t ⊸ B ∙ u)
inp s≼u u≺∞ P / s≺t / σ = ♭ (P s≺t σ)
out u≺v τ P   / s≺t / σ = out u≺v τ (♯ (♭ P / s≺t / σ))
done u≡∞      / s≺t / σ = done u≡∞

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Helper reflection functions
------------------------------------------------------------------------

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

module Tactic.RingSolver.Core.ReflectionHelp where

open import Agda.Builtin.Reflection

open import Data.List as List using (List; []; _∷_)
open import Data.Nat.Base as ℕ using (ℕ; suc; zero)
open import Data.Nat.GeneralisedArithmetic using (fold)
open import Data.Fin.Base as Fin using (Fin)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Data.String using (String)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Product
open import Function
open import Level using (Level)
open import Reflection.Term
open import Reflection.Argument

open import Tactic.RingSolver.Core.NatSet as NatSet
private
  variable
    a : Level
    A : Set a

-- TO-DO - once `Reflection` is --safe after v1.3 a lot of this can be simplified

hlams : ∀ {n} → Vec String n → Term → Term
hlams vs xs = Vec.foldr (const Term) (λ v vs → lam hidden (abs v vs)) xs vs

vlams : ∀ {n} → Vec String n → Term → Term
vlams vs xs = Vec.foldr (const Term) (λ v vs → lam visible (abs v vs)) xs vs

getVisible : Arg Term → Maybe Term
getVisible (arg (arg-info visible relevant) x) = just x
getVisible _                                   = nothing

getArgs : ∀ n → Term → Maybe (Vec Term n)
getArgs n (def _ xs) = Maybe.map Vec.reverse (List.foldl f c (List.mapMaybe getVisible xs) n)
  where
  f : (∀ n → Maybe (Vec Term n)) → Term → ∀ n → Maybe (Vec Term n)
  f xs x zero    = just []
  f xs x (suc n) = Maybe.map (x ∷_) (xs n)

  c : ∀ n → Maybe (Vec Term n)
  c zero     = just []
  c (suc _ ) = nothing
getArgs _ _ = nothing

underPi : Term → ∃[ n ] (Vec String n × Term)
underPi = go (λ xs y → _ , xs , y)
  where
  go : (∀ {n} → Vec String n → Term → A) → Term → A
  go k (pi a (abs s x)) = go (k ∘ (s ∷_)) x
  go k t                = k [] t

curriedTerm : NatSet → Term
curriedTerm = List.foldr go (quote Vec.[] ⟨ con ⟩ 2 ⋯⟅∷⟆ []) ∘ NatSet.toList
  where
  go : ℕ → Term → Term
  go x xs = quote Vec._∷_ ⟨ con ⟩ 3 ⋯⟅∷⟆ var x [] ⟨∷⟩ xs ⟨∷⟩ []


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

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

module Data.Maybe.Relation.Unary.All.Properties where

open import Data.Maybe.Base
open import Data.Maybe.Relation.Unary.All as All
  using (All; nothing; just)
open import Data.Product using (_×_; _,_)
open import Function
open import Relation.Unary

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for maybe operations
------------------------------------------------------------------------
-- map

module _ {a b p} {A : Set a} {B : Set b} {P : Pred B p} {f : A → B} where

  map⁺ : ∀ {mx} → All (P ∘ f) mx → All P (map f mx)
  map⁺ (just p) = just p
  map⁺ nothing  = nothing

  map⁻ : ∀ {mx} → All P (map f mx) → All (P ∘ f) mx
  map⁻ {just x}  (just px) = just px
  map⁻ {nothing} nothing   = nothing

-- A variant of All.map.

module _ {a b p q} {A : Set a} {B : Set b} {f : A → B}
         {P : Pred A p} {Q : Pred B q} where

  gmap : P ⊆ Q ∘ f → All P ⊆ All Q ∘ map f
  gmap g = map⁺ ∘ All.map g

------------------------------------------------------------------------
-- _<∣>_

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

  <∣>⁺ : ∀ {mx my} → All P mx → All P my → All P (mx <∣> my)
  <∣>⁺ (just px) pmy = just px
  <∣>⁺ nothing   pmy = pmy

  <∣>⁻ : ∀ mx {my} → All P (mx <∣> my) → All P mx
  <∣>⁻ (just x) pmxy = pmxy
  <∣>⁻ nothing  pmxy = nothing


text:
open import Prelude
open import RW.Language.RTerm
open import RW.Language.RTermUtils
open import RW.Language.RTermIdx
open import RW.Data.RTrie

open import RW.Strategy using (Trs; Symmetry; UData; u-data)

module RW.Language.RTermTrie where

  open import RW.Utils.Monads
  open Monad {{...}}

  add-action : Name → ℕ × RTrie → ℕ × RTrie
  add-action act bt
    = let
      ty = lift-ivar $ typeResult $ Ag2RType $ type act
    in insertTerm act ty bt

  replicateM : {A : Set} → List (Maybe A) → Maybe (List A)
  replicateM [] = just []
  replicateM (nothing ∷ _)  = nothing
  replicateM (just x  ∷ xs) with replicateM xs
  ...| just xs' = just (x ∷ xs')
  ...| nothing  = nothing

  postulate
    not-found       : Name × UData
    ul-is-nothing   : Name × UData

  search-action : RTermName → RBinApp ⊥ → RTrie → List (Name × UData)
  search-action hd (_ , g₁ , g₂) trie
    = let g□ = g₁ ∩↑ g₂
          u₁ = g□ -↓ g₁
          u₂ = g□ -↓ g₂
          ul = replicateM (u₁ ∷ u₂ ∷ [])
    in maybe (mkSearch g□) (ul-is-nothing ∷ []) ul
    where
      convert : RTerm (Maybe ⊥) → List (ℕ × RTerm ⊥) × Name → Name × UData
      convert g□ (ns , act) = act , u-data (⊥2UnitCast g□) ns []

      convert-sym : RTerm (Maybe ⊥) → List (ℕ × RTerm ⊥) × Name → Name × UData
      convert-sym g□ (ns , act) = act , u-data (⊥2UnitCast g□) ns (Symmetry ∷ [])

      mkLkup : List (RTerm ⊥) → Maybe (List (List (ℕ × RTerm ⊥) × Name))
      mkLkup ul with lookupTerm (rapp hd ul) trie
      ...| [] = nothing
      ...| l  = just l

      mkSearch : RTerm (Maybe ⊥) → List (RTerm ⊥) → List (Name × UData)
      mkSearch g□ ul with mkLkup ul
      ...| just l = map (convert g□) l
      ...| nothing with mkLkup (reverse ul)
      ...| nothing = not-found ∷ []
      ...| just l  = map (convert-sym g□) l

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
module _ where

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Equality
open import Agda.Builtin.String

macro
  m : Name → Term → TC _
  m f hole = do
     ty ← getType f
     ty ← normalise ty
     quoteTC ty >>= unify hole

open import Agda.Builtin.Nat

import Agda.Builtin.Nat as Nat₁ renaming (Nat to Hombre)
import Agda.Builtin.Nat as Nat₂ renaming (Nat to ℕumber)
import Agda.Builtin.Nat as Nat₃ renaming (Nat to n)
import Agda.Builtin.Nat as Nat₄ renaming (Nat to N)

infix 0 _∋_
_∋_ : (A : Set) → A → A
A ∋ x = x

binderName : Term → String
binderName (pi _ (abs x _)) = x
binderName _                = "(no binder)"

f₁ : Nat₁.Hombre → Nat
f₁ x = x

f₂ : Nat₂.ℕumber → Nat
f₂ x = x

f₃ : Nat₃.n → Nat
f₃ x = x

f₄ : Nat₄.N → Nat
f₄ x = x

_ = binderName (m f₁) ≡ "h" ∋ refl
_ = binderName (m f₂) ≡ "z" ∋ refl  -- Can't toLower ℕ
_ = binderName (m f₃) ≡ "z" ∋ refl  -- Single lower case type name, don't pick same name for binder
_ = binderName (m f₄) ≡ "n" ∋ refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Base.Free.Properties where

open import Relation.Binary.PropositionalEquality using (_≢_)

open import Base.Free                             using (Free; pure; impure)

discriminate : ∀ {S P A} {s : S} {pf : P s → Free S P A} {a : A} → impure s pf ≢ pure a
discriminate = λ ()

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
{-# OPTIONS --cubical --safe #-}
module Algebra where

open import Prelude

module _ {a} {A : Type a} (_∙_ : A → A → A) where
  Associative : Type a
  Associative = ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

  Commutative : Type _
  Commutative = ∀ x y → x ∙ y ≡ y ∙ x

  Idempotent : Type _
  Idempotent = ∀ x → x ∙ x ≡ x

Identityˡ : (A → B → B) → A → Type _
Identityˡ _∙_ x = ∀ y → x ∙ y ≡ y

Zeroˡ : (A → B → A) → A → Type _
Zeroˡ _∙_ x = ∀ y → x ∙ y ≡ x

Zeroʳ : (A → B → B) → B → Type _
Zeroʳ _∙_ x = ∀ y → y ∙ x ≡ x

Identityʳ : (A → B → A) → B → Type _
Identityʳ _∙_ x = ∀ y → y ∙ x ≡ y

_Distributesʳ_ : (A → B → B) → (B → B → B) → Type _
_⊗_ Distributesʳ _⊕_ = ∀ x y z → x ⊗ (y ⊕ z) ≡ (x ⊗ y) ⊕ (x ⊗ z)

_Distributesˡ_ : (B → A → B) → (B → B → B) → Type _
_⊗_ Distributesˡ _⊕_ = ∀ x y z → (x ⊕ y) ⊗ z ≡ (x ⊗ z) ⊕ (y ⊗ z)

Cancellableˡ : (A → B → C) → A → Type _
Cancellableˡ _⊗_ c = ∀ x y → c ⊗ x ≡ c ⊗ y → x ≡ y

Cancellableʳ : (A → B → C) → B → Type _
Cancellableʳ _⊗_ c = ∀ x y → x ⊗ c ≡ y ⊗ c → x ≡ y

Cancellativeˡ : (A → B → C) → Type _
Cancellativeˡ _⊗_ = ∀ c → Cancellableˡ _⊗_ c

Cancellativeʳ : (A → B → C) → Type _
Cancellativeʳ _⊗_ = ∀ c → Cancellableʳ _⊗_ c

record  Semigroup ℓ : Type (ℓsuc ℓ) where
  infixl 6 _∙_
  field
    𝑆      : Type ℓ
    _∙_    : 𝑆 → 𝑆 → 𝑆
    assoc  : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

record  Monoid ℓ : Type (ℓsuc ℓ) where
  infixl 6 _∙_
  field
    𝑆      : Type ℓ
    _∙_    : 𝑆 → 𝑆 → 𝑆
    ε      : 𝑆
    assoc  : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
    ε∙     : ∀ x → ε ∙ x ≡ x
    ∙ε     : ∀ x → x ∙ ε ≡ x

  semigroup : Semigroup ℓ
  semigroup = record
    { 𝑆 = 𝑆; _∙_ = _∙_; assoc = assoc }

record MonoidHomomorphism_⟶_
         {ℓ₁ ℓ₂}
         (from : Monoid ℓ₁)
         (to : Monoid ℓ₂)
       : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  open Monoid from
  open Monoid to
    renaming ( 𝑆 to 𝑅
             ; _∙_ to _⊙_
             ; ε to ⓔ
             )
  field
    f : 𝑆 → 𝑅
    ∙-homo : ∀ x y → f (x ∙ y) ≡ f x ⊙ f y
    ε-homo : f ε ≡ ⓔ

record Group ℓ : Type (ℓsuc ℓ) where
  field
    monoid : Monoid ℓ
  open Monoid monoid public
  field
    -_ : 𝑆 → 𝑆
    ∙⁻ : ∀ x → x ∙ - x ≡ ε
    ⁻∙ : ∀ x → - x ∙ x ≡ ε

  open import Path.Reasoning

  cancelˡ : Cancellativeˡ _∙_
  cancelˡ x y z p =
    y ≡˘⟨ ε∙ y ⟩
    ε ∙ y ≡˘⟨ cong (_∙ y) (⁻∙ x) ⟩
    (- x ∙ x) ∙ y ≡⟨ assoc (- x) x y ⟩
    - x ∙ (x ∙ y) ≡⟨ cong (- x ∙_) p ⟩
    - x ∙ (x ∙ z) ≡˘⟨ assoc (- x) x z ⟩
    (- x ∙ x) ∙ z ≡⟨ cong (_∙ z) (⁻∙ x) ⟩
    ε ∙ z ≡⟨ ε∙ z ⟩
    z ∎

  cancelʳ : Cancellativeʳ _∙_
  cancelʳ x y z p =
    y ≡˘⟨ ∙ε y ⟩
    y ∙ ε ≡˘⟨ cong (y ∙_) (∙⁻ x) ⟩
    y ∙ (x ∙ - x) ≡˘⟨ assoc y x (- x) ⟩
    (y ∙ x) ∙ - x ≡⟨ cong (_∙ - x) p ⟩
    (z ∙ x) ∙ - x ≡⟨ assoc z x (- x) ⟩
    z ∙ (x ∙ - x) ≡⟨ cong (z ∙_) (∙⁻ x) ⟩
    z ∙ ε ≡⟨ ∙ε z ⟩
    z ∎

record CommutativeMonoid ℓ : Type (ℓsuc ℓ) where
  field
    monoid : Monoid ℓ
  open Monoid monoid public
  field
    comm : Commutative _∙_

record Semilattice ℓ : Type (ℓsuc ℓ) where
  field
    commutativeMonoid : CommutativeMonoid ℓ
  open CommutativeMonoid commutativeMonoid public
  field
    idem : Idempotent _∙_

record NearSemiring ℓ : Type (ℓsuc ℓ) where
  infixl 6 _+_
  infixl 7 _*_
  field
    𝑅 : Type ℓ
    _+_ : 𝑅 → 𝑅 → 𝑅
    _*_ : 𝑅 → 𝑅 → 𝑅
    1# : 𝑅
    0# : 𝑅
    +-assoc : Associative _+_
    *-assoc : Associative _*_
    0+ : Identityˡ _+_ 0#
    +0 : Identityʳ _+_ 0#
    1* : Identityˡ _*_ 1#
    *1 : Identityʳ _*_ 1#
    0* : Zeroˡ _*_ 0#
    ⟨+⟩* : _*_ Distributesˡ _+_

record Semiring ℓ : Type (ℓsuc ℓ) where
  field
    nearSemiring : NearSemiring ℓ
  open NearSemiring nearSemiring public
  field
    +-comm : Commutative _+_
    *0 : Zeroʳ _*_ 0#
    *⟨+⟩ : _*_ Distributesʳ _+_

record IdempotentSemiring ℓ : Type (ℓsuc ℓ) where
  field
    semiring : Semiring ℓ
  open Semiring semiring public
  field
    +-idem : Idempotent _+_

record CommutativeSemiring ℓ : Type (ℓsuc ℓ) where
  field
    semiring : Semiring ℓ
  open Semiring semiring public
  field
    *-comm : Commutative _*_

record LeftSemimodule {ℓ₁} (semiring : Semiring ℓ₁) ℓ₂ : Type (ℓ₁ ℓ⊔ ℓsuc ℓ₂) where
  open Semiring semiring public
  field
    semimodule : CommutativeMonoid ℓ₂
  open CommutativeMonoid semimodule renaming (_∙_ to _∪_) public
    renaming (𝑆 to 𝑉
             ; assoc to ∪-assoc
             ; ε∙ to ∅∪
             ; ∙ε to ∪∅
             ; ε to ∅
             )
  infixr 7 _⋊_
  field
    _⋊_ : 𝑅 → 𝑉 → 𝑉
    ⟨*⟩⋊ : ∀ x y z → (x * y) ⋊ z ≡ x ⋊ (y ⋊ z)
    ⟨+⟩⋊ : ∀ x y z → (x + y) ⋊ z ≡ (x ⋊ z) ∪ (y ⋊ z)
    ⋊⟨∪⟩ : _⋊_ Distributesʳ _∪_
    1⋊ : Identityˡ _⋊_ 1#
    0⋊ : ∀ x → 0# ⋊ x ≡ ∅
    ⋊∅ : ∀ x → x ⋊ ∅ ≡ ∅

record SemimoduleHomomorphism[_]_⟶_
         {ℓ₁ ℓ₂ ℓ₃}
         (rng : Semiring ℓ₁)
         (from : LeftSemimodule rng ℓ₂)
         (to : LeftSemimodule rng ℓ₃) : Type (ℓ₁ ℓ⊔ ℓsuc (ℓ₂ ℓ⊔ ℓ₃)) where

  open Semiring rng
  open LeftSemimodule from using (_⋊_; monoid)
  open LeftSemimodule to using () renaming (_⋊_ to _⋊′_; monoid to monoid′)

  field mon-homo : MonoidHomomorphism monoid ⟶ monoid′

  open MonoidHomomorphism_⟶_ mon-homo public

  field ⋊-homo : ∀ r x → f (r ⋊ x) ≡ r ⋊′ f x

record StarSemiring ℓ : Type (ℓsuc ℓ) where
  field
    semiring : Semiring ℓ
  open Semiring semiring public
  field
    _⋆ : 𝑅 → 𝑅
    star-iterʳ : ∀ x → x ⋆ ≡ 1# + x * x ⋆
    star-iterˡ : ∀ x → x ⋆ ≡ 1# + x ⋆ * x
  _⁺ : 𝑅 → 𝑅
  x ⁺ = x * x ⋆

record Functor ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    𝐹   : Type ℓ₁ → Type ℓ₂
    map : (A → B) → 𝐹 A → 𝐹 B
    map-id : map (id {ℓ₁} {A}) ≡ id
    map-comp : (f : B → C) → (g : A → B) → map (f ∘ g) ≡ map f ∘ map g

record Applicative ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    functor : Functor ℓ₁ ℓ₂
  open Functor functor public
  infixl 5 _<*>_
  field
    pure : A → 𝐹 A
    _<*>_ : 𝐹 (A → B) → 𝐹 A → 𝐹 B
    map-ap : (f : A → B) → map f ≡ pure f <*>_
    pure-homo : (f : A → B) → (x : A) → map f (pure x) ≡ pure (f x)
    <*>-interchange : (u : 𝐹 (A → B)) → (y : A) → u <*> pure y ≡ map (_$ y) u
    <*>-comp : (u : 𝐹 (B → C)) → (v : 𝐹 (A → B)) → (w : 𝐹 A) → pure _∘′_ <*> u <*> v <*> w ≡ u <*> (v <*> w)

record IsMonad {ℓ₁} {ℓ₂} (𝐹 : Type ℓ₁ → Type ℓ₂) : Type (ℓsuc ℓ₁ ℓ⊔ ℓ₂) where
  infixl 1 _>>=_
  field
    _>>=_ : 𝐹 A → (A → 𝐹 B) → 𝐹 B
    return : A → 𝐹 A

    >>=-idˡ : (f : A → 𝐹 B) → (x : A) → (return x >>= f) ≡ f x
    >>=-idʳ : (x : 𝐹 A) → (x >>= return) ≡ x
    >>=-assoc : (xs : 𝐹 A) (f : A → 𝐹 B) (g : B → 𝐹 C) → ((xs >>= f) >>= g) ≡ (xs >>= (λ x → f x >>= g))

record Monad ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    𝐹 : Type ℓ₁ → Type ℓ₂
    isMonad : IsMonad 𝐹
  open IsMonad isMonad public

record MonadHomomorphism_⟶_
         {ℓ₁ ℓ₂ ℓ₃}
         (from : Monad ℓ₁ ℓ₂)
         (to : Monad ℓ₁ ℓ₃) : Type (ℓsuc ℓ₁ ℓ⊔ ℓ₂ ℓ⊔ ℓ₃) where
  module F = Monad from
  module T = Monad to

  field
    f : F.𝐹 A → T.𝐹 A
    >>=-homo : (xs : F.𝐹 A) (k : A → F.𝐹 B) → (f xs T.>>= (f ∘ k)) ≡ f (xs F.>>= k)
    return-homo : (x : A) → f (F.return x) ≡ T.return x

record IsSetMonad {ℓ₁} {ℓ₂} (𝐹 : Type ℓ₁ → Type ℓ₂) : Type (ℓsuc ℓ₁ ℓ⊔ ℓ₂) where
  infixl 1 _>>=_
  field
    _>>=_ : 𝐹 A → (A → 𝐹 B) → 𝐹 B
    return : A → 𝐹 A

    trunc : isSet A → isSet (𝐹 A)

    >>=-idˡ   : isSet B → (f : A → 𝐹 B) → (x : A) → (return x >>= f) ≡ f x
    >>=-idʳ   : isSet A → (x : 𝐹 A) → (x >>= return) ≡ x
    >>=-assoc : isSet C → (xs : 𝐹 A) (f : A → 𝐹 B) (g : B → 𝐹 C) → ((xs >>= f) >>= g) ≡ (xs >>= (λ x → f x >>= g))

record SetMonad ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    𝐹 : Type ℓ₁ → Type ℓ₂
    isSetMonad : IsSetMonad 𝐹
  open IsSetMonad isSetMonad public

record SetMonadHomomorphism_⟶_
         {ℓ₁ ℓ₂ ℓ₃}
         (from : SetMonad ℓ₁ ℓ₂)
         (to : SetMonad ℓ₁ ℓ₃) : Type (ℓsuc ℓ₁ ℓ⊔ ℓ₂ ℓ⊔ ℓ₃) where
  module F = SetMonad from
  module T = SetMonad to

  field
    f : F.𝐹 A → T.𝐹 A
    >>=-homo : (xs : F.𝐹 A) (k : A → F.𝐹 B) → (f xs T.>>= (f ∘ k)) ≡ f (xs F.>>= k)
    return-homo : (x : A) → f (F.return x) ≡ T.return x

record Alternative ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    applicative : Applicative ℓ₁ ℓ₂
  open Applicative applicative public
  field
    0# : 𝐹 A
    _<|>_ : 𝐹 A → 𝐹 A → 𝐹 A
    <|>-idˡ : (x : 𝐹 A) → 0# <|> x ≡ x
    <|>-idʳ : (x : 𝐹 A) → x <|> 0# ≡ x
    0-annˡ : (x : 𝐹 A) → 0# <*> x ≡ 0# {B}
    <|>-distrib : (x y : 𝐹 (A → B)) → (z : 𝐹 A) → (x <|> y) <*> z ≡ (x <*> z) <|> (y <*> z)

record MonadPlus ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    monad : Monad ℓ₁ ℓ₂
  open Monad monad public
  field
    0# : 𝐹 A
    _<|>_ : 𝐹 A → 𝐹 A → 𝐹 A
    <|>-idˡ : (x : 𝐹 A) → 0# <|> x ≡ x
    <|>-idʳ : (x : 𝐹 A) → x <|> 0# ≡ x
    0-annˡ : (x : A → 𝐹 B) → (0# >>= x) ≡ 0#
    <|>-distrib : (x y : 𝐹 A) → (z : A → 𝐹 B) → ((x <|> y) >>= z) ≡ (x >>= z) <|> (y >>= z)

Endo : Type a → Type a
Endo A = A → A

endoMonoid : ∀ {a} → Type a → Monoid a
endoMonoid A .Monoid.𝑆 = Endo A
endoMonoid A .Monoid.ε x = x
endoMonoid A .Monoid._∙_ f g x = f (g x)
endoMonoid A .Monoid.assoc _ _ _ = refl
endoMonoid A .Monoid.ε∙ _ = refl
endoMonoid A .Monoid.∙ε _ = refl

record Foldable ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    𝐹 : Type ℓ₁ → Type ℓ₂
  open Monoid ⦃ ... ⦄
  field
    foldMap : {A : Type ℓ₁} ⦃ _ : Monoid ℓ₁ ⦄ → (A → 𝑆) → 𝐹 A → 𝑆
  foldr : {A B : Type ℓ₁} → (A → B → B) → B → 𝐹 A → B
  foldr f b xs = foldMap ⦃ endoMonoid _ ⦄ f xs b

record GradedMonad {ℓ₁} (monoid : Monoid ℓ₁) ℓ₂ ℓ₃ : Type (ℓ₁ ℓ⊔ ℓsuc (ℓ₂ ℓ⊔ ℓ₃)) where
  open Monoid monoid
  field
    𝐹 : 𝑆 → Type ℓ₂ → Type ℓ₃
    pure  : A → 𝐹 ε A
    _>>=_ : ∀ {x y} → 𝐹 x A → (A → 𝐹 y B) → 𝐹 (x ∙ y) B

    >>=-idˡ : ∀ {s} (f : A → 𝐹 s B) → (x : A) → (pure x >>= f) ≡[ i ≔ 𝐹 (ε∙ s i) B ]≡ (f x)
    >>=-idʳ : ∀ {s} (x : 𝐹 s A) → (x >>= pure) ≡[ i ≔ 𝐹 (∙ε s i) A ]≡ x
    >>=-assoc : ∀ {x y z} (xs : 𝐹 x A) (f : A → 𝐹 y B) (g : B → 𝐹 z C) → ((xs >>= f) >>= g) ≡[ i ≔ 𝐹 (assoc x y z i) C ]≡ (xs >>= (λ x → f x >>= g))

  infixr 0 proven-bind

  proven-bind : ∀ {x y z} → 𝐹 x A → (A → 𝐹 y B) → (x ∙ y) ≡ z → 𝐹 z B
  proven-bind xs f proof = subst (flip 𝐹 _) proof (xs >>= f)

  syntax proven-bind xs f proof = xs >>=[ proof ] f

  infixr 0 proven-do
  proven-do : ∀ {x y z} → 𝐹 x A → (A → 𝐹 y B) → (x ∙ y) ≡ z → 𝐹 z B
  proven-do = proven-bind

  syntax proven-do xs (λ x → e) proof = x ← xs [ proof ] e

  map : ∀ {x} → (A → B) → 𝐹 x A → 𝐹 x B
  map f xs = xs >>=[ ∙ε _ ] (pure ∘ f)

  _<*>_ : ∀ {x y} → 𝐹 x (A → B) → 𝐹 y A → 𝐹 (x ∙ y) B
  fs <*> xs = fs >>= flip map xs

  _>>=ε_ : ∀ {x} → 𝐹 x A → (A → 𝐹 ε B) → 𝐹 x B
  xs >>=ε f = xs >>=[ ∙ε _ ] f

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Monads where

open import Library
open import Categories

record Monad {a}{b}(C : Cat {a}{b}) : Set (a ⊔ b) where
  constructor monad
  open Cat C
  field T    : Obj → Obj
        η    : ∀ {X} → Hom X (T X)
        bind : ∀{X Y} → Hom X (T Y) → Hom (T X) (T Y)
        law1 : ∀{X} → bind (η {X}) ≅ iden {T X}
        law2 : ∀{X Y}{f : Hom X (T Y)} → comp (bind f) η ≅ f
        law3 : ∀{X Y Z}{f : Hom X (T Y)}{g : Hom Y (T Z)} →
               bind (comp (bind g) f)  ≅ comp (bind g) (bind f)

open import Functors

TFun : ∀{a b}{C : Cat {a}{b}} → Monad C → Fun C C
TFun {C = C} M = let open Monad M; open Cat C in record {
  OMap  = T;
  HMap  = bind ∘ comp η;
  fid   =
    proof
    bind (comp η iden)
    ≅⟨ cong bind idr ⟩
    bind η
    ≅⟨ law1 ⟩
    iden ∎;
  fcomp = λ {_}{_}{_}{f}{g} →
    proof
    bind (comp η (comp f g))
    ≅⟨ cong bind (sym ass) ⟩
    bind (comp (comp η f) g)
    ≅⟨ cong (λ f → bind (comp f g)) (sym law2) ⟩
    bind (comp (comp (bind (comp η f)) η) g)
    ≅⟨ cong bind ass ⟩
    bind (comp (bind (comp η f)) (comp η g))
    ≅⟨ law3 ⟩
    comp (bind (comp η f)) (bind (comp η g))
    ∎}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module CS410-Prelude where

------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- Standard Equipment for use in Exercises
------------------------------------------------------------------------------
------------------------------------------------------------------------------

------------------------------------------------------------------------------
-- functional equipment (types may be generalized later)
------------------------------------------------------------------------------

-- the polymorphic identity function
id : {X : Set} -> X -> X
id x = x

-- standard composition: f << g is "f after g"
_<<_ : {X Y Z : Set} -> (Y -> Z) -> (X -> Y) -> (X -> Z)
(f << g) x = f (g x)

-- diagrammatic composition: f >> g is "f then g"
_>>_ : {X Y Z : Set} -> (X -> Y) -> (Y -> Z) -> (X -> Z)
                     --       ^^^^^^^^          dominoes!
(f >> g) x = g (f x)
infixr 5 _>>_

-- infix application
_$_ : {S : Set}{T : S -> Set}(f : (x : S) -> T x)(s : S) -> T s
f $ s = f s
infixl 2 _$_

------------------------------------------------------------------------------
-- some basic "logical" types
------------------------------------------------------------------------------

data Zero : Set where
  -- to give a value in a data, choose one constructor
  -- there are no constructors
  -- so that's impossible

record One : Set where
  -- to give a value in a record type, fill all its fields
  -- there are no fields
  -- so that's trivial
  --   (can we have a constructor, for convenience?)
  constructor <>

data _+_ (S : Set)(T : Set) : Set where -- "where" wants an indented block
  -- to offer a choice of constructors, list them with their types
  inl : S -> S + T     -- constructors can pack up stuff
  inr : T -> S + T
  -- in Haskell, this was called "Either S T"

record Sg (S : Set)(T : S -> Set) : Set where  -- Sg is short for "Sigma"
  constructor _,_
  field -- introduces a bunch of fields, listed with their types
    fst : S
    snd : T fst
-- make _*_ from Sg ?
open Sg public

_*_ : Set -> Set -> Set
S * T = Sg S \ _ -> T

infixr 4 _,_ _*_

------------------------------------------------------------------------------
-- natural numbers and addition
------------------------------------------------------------------------------

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}
--  ^^^^^^^^^^^^^^^^^^^       this pragma lets us use decimal notation

_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)      -- there are other choices

------------------------------------------------------------------------------
-- equality
------------------------------------------------------------------------------

data _==_ {X : Set} : X -> X -> Set where
  refl : (x : X) -> x == x           -- the relation that's "only reflexive"

{-# BUILTIN EQUALITY _==_ #-}  -- we'll see what that's for, later

_=$=_ : {X Y : Set}{f f' : X -> Y}{x x' : X} ->
        f == f' -> x == x' -> f x == f' x'
refl f =$= refl x = refl (f x)

_=$_ : {S : Set}{T : S -> Set}{f g : (x : S) -> T x} -> (f == g) -> (x : S) -> f x == g x
refl f =$ x = refl (f x)

infixl 2 _=$=_ _=$_

sym : {X : Set}{x y : X} -> x == y -> y == x
sym (refl x) = refl x

_[QED] : {X : Set}(x : X) -> x == x
x [QED] = refl x
_=[_>=_ : {X : Set}(x : X){y z : X} -> x == y -> y == z -> x == z
x =[ refl .x >= q = q
_=<_]=_ : {X : Set}(x : X){y z : X} -> y == x -> y == z -> x == z
x =< refl .x ]= q = q
infixr 1 _=[_>=_ _=<_]=_
infixr 2 _[QED]

------------------------------------------------------------------------------
-- greater-than-or-equals
------------------------------------------------------------------------------

_>=_ : Nat -> Nat -> Set
x     >= zero   = One
zero  >= suc y  = Zero
suc x >= suc y  = x >= y

refl->= : (n : Nat) -> n >= n
refl->= zero    = record {}
refl->= (suc n) = refl->= n

trans->= : (x y z : Nat) -> x >= y -> y >= z -> x >= z
trans->=      x       y  zero    x>=y y>=z = record {}
trans->=      x  zero    (suc z) x>=y ()
trans->= zero    (suc y) (suc z) ()   y>=z
trans->= (suc x) (suc y) (suc z) x>=y y>=z = trans->= x y z x>=y y>=z

suc->= : (x : Nat) -> suc x >= x
suc->= zero    = <>
suc->= (suc x) = suc->= x

----------------------------------------------------------------------------
-- Two -- the type of Boolean values
----------------------------------------------------------------------------

data Two : Set where tt ff : Two
{-# BUILTIN BOOL Two #-}
{-# BUILTIN TRUE tt #-}
{-# BUILTIN FALSE ff #-}

-- nondependent conditional with traditional syntax
if_then_else_ : forall {l}{X : Set l} -> Two -> X -> X -> X
if tt then t else e = t
if ff then t else e = e

-- dependent conditional cooked for partial application
caseTwo : forall {l}{P : Two -> Set l} -> P tt -> P ff -> (b : Two) -> P b
caseTwo t f tt = t
caseTwo t f ff = f

----------------------------------------------------------------------------
-- lists
----------------------------------------------------------------------------

data List (X : Set) : Set where
  []   : List X
  _,-_ : (x : X)(xs : List X) -> List X
infixr 4 _,-_
{-# COMPILE GHC List = data [] ([] | (:)) #-}
{-# BUILTIN LIST List #-}

----------------------------------------------------------------------------
-- chars and strings
----------------------------------------------------------------------------

postulate       -- this means that we just suppose the following things exist...
  Char : Set
  String : Set
{-# BUILTIN CHAR Char #-}
{-# BUILTIN STRING String #-}

primitive       -- these are baked in; they even work!
  primCharEquality    : Char -> Char -> Two
  primStringAppend    : String -> String -> String
  primStringToList    : String -> List Char
  primStringFromList  : List Char -> String