text:
module foldr-monoid-foldl where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning

open import lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; foldr; IsMonoid)
open IsMonoid
open import foldl using (foldl)

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- foldr-monoidのfoldl版
-- _⊗_ と e がモノイドをなすとき、任意の値でfoldを再表現できる
foldl-monoid : ∀ {A : Set} → (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e
  → ∀ (xs : List A) (y : A) → foldl _⊗_ y xs ≡ y ⊗ (foldl _⊗_ e xs)
foldl-monoid _⊗_ e ⊗-monoid [] y =
  begin
    foldl _⊗_ y []
  ≡⟨⟩
    y
  ≡⟨ sym (identityʳ ⊗-monoid y) ⟩
    y ⊗ e
  ≡⟨⟩
    y ⊗ (foldl _⊗_ e [])
  ∎
foldl-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
  begin
    foldl _⊗_ y (x ∷ xs)
  ≡⟨⟩
    foldl _⊗_ (y ⊗ x) xs
  ≡⟨ foldl-monoid _⊗_ e ⊗-monoid xs (y ⊗ x) ⟩
    (y ⊗ x) ⊗ (foldl _⊗_ e xs)
  ≡⟨ assoc ⊗-monoid y x (foldl _⊗_ e xs) ⟩
    y ⊗ (x ⊗ (foldl _⊗_ e xs))
  ≡⟨ cong (y ⊗_) (sym (foldl-monoid _⊗_ e ⊗-monoid xs x)) ⟩
    y ⊗ (foldl _⊗_ x xs)
  ≡⟨ cong (λ e⊗x → y ⊗ (foldl _⊗_ e⊗x xs)) (sym (identityˡ ⊗-monoid x)) ⟩
    y ⊗ (foldl _⊗_ (e ⊗ x) xs)
  ≡⟨⟩
    y ⊗ (foldl _⊗_ e (x ∷ xs))
  ∎

-- 外延性の公理を用いた証明のための補題
lemma : ∀ {A : Set} → (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e
  → ∀ (xs : List A) → foldr _⊗_ e xs ≡ foldl _⊗_ e xs
lemma _⊗_ e ⊗-monoid [] =
  begin
    foldr _⊗_ e []
  ≡⟨⟩
    e
  ≡⟨⟩
    foldl _⊗_ e []
  ∎
lemma _⊗_ e ⊗-monoid (x ∷ xs) =
  begin
    foldr _⊗_ e (x ∷ xs)
  ≡⟨⟩
    x ⊗ (foldr _⊗_ e xs)
  ≡⟨ cong (x ⊗_) (lemma _⊗_ e ⊗-monoid xs) ⟩
    x ⊗ (foldl _⊗_ e xs)
  ≡⟨ sym (foldl-monoid _⊗_ e ⊗-monoid xs x) ⟩
    foldl _⊗_ x xs
  ≡⟨ cong (λ e⊗x → foldl _⊗_ e⊗x xs) (sym (identityˡ ⊗-monoid x)) ⟩
    foldl _⊗_ (e ⊗ x) xs
  ≡⟨⟩
    foldl _⊗_ e (x ∷ xs)
  ∎

-- _⊗_ と e がモノイドをなすとき、foldrとfoldlが等しくなることの証明
foldr-monoid-foldl : ∀ {A : Set} → (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e
  → foldr _⊗_ e ≡ foldl _⊗_ e
foldr-monoid-foldl _⊗_ e ⊗-monoid = extensionality (lemma _⊗_ e ⊗-monoid)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module Human.Empty where

data Empty : Set where

void : ∀ {P : Set} → Empty → P
void ()

ext: agda

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
module Data.Maybe.Properties.Extra {a}{A : Set a} where

open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

nothing≢just : ∀ {a : A} → ¬ (_≡_ {A = Maybe A} nothing (just a))
nothing≢just ()


text:
{-# OPTIONS --no-positivity-check #-}
{-# OPTIONS --no-termination-check #-}

module UniDB.Examples.Free where

open import UniDB
open import Function
open import Relation.Binary.PropositionalEquality
import Level

-- Interpret a value of the morphism representation Ξ as
-- a morphism between S and T.
Int : (Ξ : MOR) (S T : STX) → Set
Int Ξ S T = (γ₁ γ₂ : Dom) (ξ : Ξ γ₁ γ₂) → S γ₁ → T γ₂

-- Combine two types and their interpretations to an
-- intepretation of an outer composition.
IntPair : (Ξ Ζ : MOR) (S T U : STX) →
  (intΞ : Int Ξ S T) (intΖ : Int Ζ T U) →
  Int (Pair Ξ Ζ) S U
IntPair Ξ Ζ S T U intΞ intΖ _ _ (ξ ⊗ ζ) = intΖ _ _ ζ ∘ intΞ _ _ ξ

-- Predicate: The interpretation of an identity morphism is
-- indeed an identity.
IntIdm : (Ξ : MOR) (T : STX) {{idmΞ : Idm Ξ}} (intΞ : Int Ξ T T) → Set
IntIdm Ξ T intΞ = (γ : Dom) (t : T γ) → intΞ _ _ (idm {Ξ} γ) t ≡ t

-- Pointwise equality between two differently represented morphisms.
_∣_⊢_≃_ :
  {Ξ Ζ : MOR} {S T : STX} {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  (intΞ : Int Ξ S T) (intΖ : Int Ζ S T)
  {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₁ γ₂) → Set
intΞ ∣ intΖ ⊢ ξ ≃ ζ = ∀ s → intΞ _ _ ξ s ≡ intΖ _ _ ζ s

-- Equality at arbitrary depths
data _∣_⊢_≅_
  {Ξ Ζ : MOR} {S T : STX} {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  (intΞ : Int Ξ S T) (intΖ : Int Ζ S T) :
  {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₁ γ₂) → Set where
  ≃-to-≅ :
    {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₁ γ₂)
    (δ : Dom) (eq≃ : (δ' : Dom) → intΞ ∣ intΖ ⊢ (ξ ↑ δ') ≃ (ζ ↑ δ')) →
    intΞ ∣ intΖ ⊢ (ξ ↑ δ) ≅ (ζ ↑ δ)

-- ≅ can always be pushed under binders
int≅-↑₁ :
  {Ξ Ζ : MOR} {S T : STX} {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  {intΞ : Int Ξ S T} {intΖ : Int Ζ S T}
  {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂} →
  intΞ ∣ intΖ ⊢ ξ ≅ ζ →
  intΞ ∣ intΖ ⊢ (ξ ↑₁) ≅ (ζ ↑₁)
int≅-↑₁ (≃-to-≅ ξ ζ δ eq≃) rewrite sym (↑-suc ξ δ) | sym (↑-suc ζ δ) =
  ≃-to-≅ ξ ζ (suc δ) eq≃

int≅-↑ :
  {Ξ Ζ : MOR} {S T : STX} {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  {intΞ : Int Ξ S T} {intΖ : Int Ζ S T}
  {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂} →
  intΞ ∣ intΖ ⊢ ξ ≅ ζ →
  (δ : Dom) → intΞ ∣ intΖ ⊢ (ξ ↑ δ) ≅ (ζ ↑ δ)
int≅-↑ {ξ = ξ} {ζ} eq zero    rewrite ↑-zero ξ  | ↑-zero ζ  = eq
int≅-↑ {ξ = ξ} {ζ} eq (suc δ) rewrite ↑-suc ξ δ | ↑-suc ζ δ = int≅-↑₁ (int≅-↑ eq δ)

lk≅ :
  {Ξ Ζ : MOR} {S T : STX} {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  {intΞ : Int Ξ S T} {intΖ : Int Ζ S T}
  {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂} →
  intΞ ∣ intΖ ⊢ ξ ≅ ζ →
  ∀ s → intΞ _ _ ξ s ≡ intΖ _ _ ζ s
lk≅ (≃-to-≅ ξ ζ δ eq≃) s = eq≃ δ s

record Functor (F : STX → STX) : Set₁ where
  field
    fmap :
      (Ξ : MOR) (S T : STX) {{up : Up Ξ}} (intΞ : Int Ξ S T) →
      (γ₁ γ₂ : Dom) (ξ : Ξ γ₁ γ₂) → F S γ₁ → F T γ₂
    fmap-idm :
      (Ξ : MOR) (T : STX) {{upΞ : Up Ξ}} {{idmΞ : Idm Ξ}}
      (intΞ : Int Ξ T T) (intIdmΞ : IntIdm Ξ T intΞ)
      (γ : Dom) (ft : F T γ) →
      fmap Ξ T T intΞ _ _ (idm {Ξ} γ) ft ≡ ft
    fmap-⊗ :
      (Ξ Ζ : MOR) (S T U : STX) {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
      (intΞ : Int Ξ S T) (intΖ : Int Ζ T U)
      (γ₁ γ₂ γ₃ : Dom) (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃) (fs : F S γ₁) →
      fmap (Pair Ξ Ζ) S U (IntPair Ξ Ζ S T U intΞ intΖ) _ _ (ξ ⊗ ζ) fs ≡
      fmap Ζ T U intΖ _ _ ζ (fmap Ξ S T intΞ _ _ ξ fs)
    fmap-≅ :
      (Ξ Ζ : MOR) (S T : STX) {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
      (intΞ : Int Ξ S T) (intΖ : Int Ζ S T)
      (γ₁ γ₂ : Dom) (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₁ γ₂) →
      intΞ ∣ intΖ ⊢ ξ ≅ ζ  →
      fmap Ξ S T intΞ ∣ fmap Ζ S T intΖ ⊢ ξ ≅ ζ
open Functor {{...}}

--------------------------------------------------------------------------------
-- Freely generated functor

data Free (F : STX → STX) (V : STX) (γ : Dom) : Set where
  var  : (i : V γ) → Free F V γ
  free : F (Free F V) γ → Free F V γ

bind :
  (F : STX → STX) {{functorF : Functor F}}
  (V W : STX) (Ξ : MOR) {{upΞ : Up Ξ}}
  (intΞ : (γ₁ γ₂ : Dom) → Ξ γ₁ γ₂ → V γ₁ → Free F W γ₂) →
  (γ₁ γ₂ : Dom) → Free F V γ₁ → Ξ γ₁ γ₂ → Free F W γ₂
bind F V W Ξ intΞ γ₁ γ₂ (var v)    ξ = intΞ γ₁ γ₂ ξ v
bind F V W Ξ intΞ γ₁ γ₂ (free ffv) ξ =
  free (fmap {F} Ξ (Free F V) (Free F W)
          (λ γ₃ γ₄ ξ' x' → bind F V W Ξ intΞ γ₃ γ₄ x' ξ' )
          γ₁ γ₂ ξ ffv)

--------------------------------------------------------------------------------
-- Functor instance for Free F

postulate
  ext : Extensionality Level.zero Level.zero

fmap-intpair :
  (F : STX → STX) {{_ : Functor F}}
  (Ξ Ζ : MOR) (S T U : STX) {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  (intΞ : Int Ξ S T) (intΖ : Int Ζ T U) →
  fmap {F} (Pair Ξ Ζ) S U (IntPair Ξ Ζ S T U intΞ intΖ) ≡
  IntPair Ξ Ζ (F S) (F T) (F U) (fmap {F} Ξ S T intΞ) (fmap {F} Ζ T U intΖ)
fmap-intpair F Ξ Ζ S T U intΞ intΖ =
  ext λ γ₁ → ext λ γ₃ → ext λ { (_⊗_ {._} {γ₂} ξ ζ) → ext λ fs →
    fmap-⊗ {F} Ξ Ζ S T U intΞ intΖ γ₁ γ₂ γ₃ ξ ζ fs }

instance
  iFunctorFree : {F : STX → STX} {{functorF : Functor F}} →
    Functor (Free F)
  fmap {{iFunctorFree {F}}} Ξ S T intΞ _ _ ξ (var s) = var (intΞ _ _ ξ s)
  fmap {{iFunctorFree {F}}} Ξ S T intΞ _ _ ξ (free x) =
    free (fmap Ξ (Free F S) (Free F T) (fmap Ξ S T intΞ) _ _ ξ x)
  fmap-idm {{iFunctorFree {F}}} Ξ T intΞ intIdmΞ _ (var t)    = cong var (intIdmΞ _ t)
  fmap-idm {{iFunctorFree {F}}} Ξ T intΞ intIdmΞ _ (free fft) = cong free
    (fmap-idm {F} Ξ (Free F T) (fmap Ξ T T intΞ) (fmap-idm {Free F} Ξ T intΞ intIdmΞ) _ fft)
  fmap-⊗ {{iFunctorFree {F}}} Ξ Ζ S T U intΞ intΖ _ _ _ ξ ζ (var i) = cong var refl
  fmap-⊗ {{iFunctorFree {F}}} Ξ Ζ S T U intΞ intΖ _ _ _ ξ ζ (free x) = cong free (begin
    fmap (Pair Ξ Ζ) (Free F S) (Free F U) (fmap (Pair Ξ Ζ) S U (IntPair Ξ Ζ S T U intΞ intΖ)) _ _ (ξ ⊗ ζ) x
      ≡⟨ cong
           (λ (int : Int (Pair Ξ Ζ) (Free F S) (Free F U)) →
              fmap (Pair Ξ Ζ) (Free F S) (Free F U) int _ _ (ξ ⊗ ζ) x)
           (fmap-intpair (Free F) Ξ Ζ S T U intΞ intΖ)
       ⟩
    fmap (Pair Ξ Ζ) (Free F S) (Free F U) (IntPair Ξ Ζ (Free F S) (Free F T) (Free F U) (fmap Ξ S T intΞ) (fmap Ζ T U intΖ)) _ _ (ξ ⊗ ζ) x
      ≡⟨ fmap-⊗ {F} Ξ Ζ (Free F S) (Free F T) (Free F U) (fmap Ξ S T intΞ) (fmap Ζ T U intΖ) _ _ _ ξ ζ x ⟩
    fmap Ζ (Free F T) (Free F U) (fmap Ζ T U intΖ) _ _ ζ (fmap Ξ (Free F S) (Free F T) (fmap Ξ S T intΞ) _ _ ξ x)
      ∎)
  fmap-≅ {{iFunctorFree {F}}} Ξ Ζ S T intΞ intΖ _ _ _ _ eq = {!!}

--------------------------------------------------------------------------------
-- Specialiation to monads relative on Ix

module _ {F : STX → STX} {{functorF : Functor F}} where
  instance
    iVrFree : Vr (Free F Ix)
    vr     {{iVrFree}}      = var
    vr-inj {{iVrFree}} refl = refl

    iApFree : Ap (Free F Ix) (Free F Ix)
    ap {{iApFree}} {Ξ} ξ x = bind F Ix Ix Ξ (λ _ _ → lk) _ _ x ξ

    iApVrFree : ApVr (Free F Ix)
    ap-vr {{iApVrFree}} ξ i = refl

    -- After proving these three properties the relative monad laws
    -- can be derived from the library.
    iApIdmFree : ApIdm (Free F Ix) (Free F Ix)
    ap-idm {{iApIdmFree}} {Ξ} x = {!!}

    iApPairFree : ApPair (Free F Ix) (Free F Ix)
    ap-pair {{iApPairFree}} ξ ζ x = {!!}

    iApRelFree : ApRel (Free F Ix) (Free F Ix)
    ap-rel≅ {{iApRelFree}} eq x = {!!}

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

open import Function using (_∘_)
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym; cong; cong₂)
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Data.Product using (Σ-syntax; _,_)
open import Data.Unit using (tt)
open import Relation.Nullary using (yes; no)

import Data.Nat as ℕ
import Data.Nat.Properties as ℕₚ
import Data.Fin as Fin
import Data.Fin.Properties as Finₚ

open ℕ using (ℕ; zero; suc)
open Fin using (Fin; zero; suc)

open import PiCalculus.Syntax
open Scoped
open import PiCalculus.Semantics

module PiCalculus.Semantics.Properties where
private
  variable
    n : ℕ
    i j : Fin n
    P : Scoped n

lift-lower : (i : Fin (suc n)) (P : Scoped (suc n)) (uP : Unused i P)
           → lift i (lower i P uP) ≡ P
lift-lower i 𝟘 uP = refl
lift-lower i (ν P) uP
  rewrite lift-lower (suc i) P uP = refl
lift-lower i (P ∥ Q) (uP , uQ)
  rewrite lift-lower i P uP
  | lift-lower i Q uQ = refl
lift-lower i (x ⦅⦆ P) (i≢x , uP)
  rewrite lift-lower (suc i) P uP
  | Finₚ.punchIn-punchOut i≢x = refl
lift-lower i (x ⟨ y ⟩ P) (i≢x , i≢y , uP)
  rewrite lift-lower i P uP
  | Finₚ.punchIn-punchOut i≢x
  | Finₚ.punchIn-punchOut i≢y = refl

substFin-suc : (i j x : Fin n) → (suc x) [ suc i ↦ suc j ]' ≡ suc (x [ i ↦ j ]')
substFin-suc i j x with i Finₚ.≟ x
substFin-suc i j x | yes p = refl
substFin-suc i j x | no ¬p = refl

exchangeFin-suc : (i : Fin n) (x : Fin (suc n)) → suc (exchangeFin i x) ≡ exchangeFin (suc i) (suc x)
exchangeFin-suc i x with Fin.inject₁ i Finₚ.≟ x
exchangeFin-suc i .(Fin.inject₁ i) | yes refl = cong suc (cong suc (Finₚ.lower₁-irrelevant _ _ _))
exchangeFin-suc i x | no ¬p with (suc i) Fin.≟ x
exchangeFin-suc i x | no ¬p | yes q = refl
exchangeFin-suc i x | no ¬p | no ¬q = refl

exchangeFin-injectˡ : (i : Fin n) → exchangeFin i (Fin.inject₁ i) ≡ suc i
exchangeFin-injectˡ zero = refl
exchangeFin-injectˡ (suc i) rewrite sym (exchangeFin-suc i (Fin.inject₁ i)) = cong suc (exchangeFin-injectˡ i)

exchangeFin-injectʳ : (i : Fin n) → exchangeFin i (suc i) ≡ Fin.inject₁ i
exchangeFin-injectʳ zero = refl
exchangeFin-injectʳ (suc i) rewrite sym (exchangeFin-suc i (suc i)) = cong suc (exchangeFin-injectʳ i)

exchangeFin-neq : (i j : Fin n) → i ≢ j → Fin.inject₁ i ≢ suc j → exchangeFin i (suc j) ≡ suc j
exchangeFin-neq zero zero i≢j ii≢sj = ⊥-elim (i≢j refl)
exchangeFin-neq zero (suc zero) i≢j ii≢sj = refl
exchangeFin-neq zero (suc (suc j)) i≢j ii≢sj = refl
exchangeFin-neq (suc zero) zero i≢j ii≢sj = ⊥-elim (ii≢sj refl)
exchangeFin-neq (suc (suc i)) zero i≢j ii≢sj = refl
exchangeFin-neq (suc i) (suc j) i≢j ii≢sj
  rewrite sym (exchangeFin-suc i (suc j))
  = cong suc (exchangeFin-neq i j (i≢j ∘ cong suc) (ii≢sj ∘ cong suc))

exchangeFin-exchangeFin : ∀ (i : Fin n) (x : Fin (suc n)) → exchangeFin i (exchangeFin i x) ≡ x
exchangeFin-exchangeFin i x with Fin.inject₁ i Fin.≟ x
exchangeFin-exchangeFin i x | yes p with Fin.inject₁ i Finₚ.≟ (suc (Fin.lower₁ x (notMax i x p)))
exchangeFin-exchangeFin i .(Fin.inject₁ i) | yes refl | yes q = ⊥-elim (ℕₚ.1+n≢n (begin
  suc (Fin.toℕ i)                              ≡˘⟨ cong (suc ∘ Fin.toℕ) (Finₚ.lower₁-inject₁ i) ⟩
  suc (Fin.toℕ (Fin.lower₁ (Fin.inject₁ i) _)) ≡⟨ cong (suc ∘ Fin.toℕ) (Finₚ.lower₁-irrelevant _ _ _) ⟩
  suc (Fin.toℕ (Fin.lower₁ (Fin.inject₁ i) _)) ≡˘⟨ cong Fin.toℕ q ⟩
  Fin.toℕ (Fin.inject₁ i)                      ≡⟨ Finₚ.toℕ-inject₁ i ⟩
  Fin.toℕ i                                    ∎
  ))
exchangeFin-exchangeFin i x | yes p | no ¬q with i Finₚ.≟ Fin.lower₁ x (notMax i x p)
exchangeFin-exchangeFin i x | yes p | no ¬q | yes r = p
exchangeFin-exchangeFin i x | yes refl | no ¬q | no ¬r = ⊥-elim (¬r (begin
  i                            ≡˘⟨ Finₚ.lower₁-inject₁ i ⟩
  Fin.lower₁ (Fin.inject₁ i) _ ≡⟨ Finₚ.lower₁-irrelevant _ _ _ ⟩
  Fin.lower₁ (Fin.inject₁ i) _ ∎))
exchangeFin-exchangeFin i x | no ¬p with (suc i) Fin.≟ x
exchangeFin-exchangeFin i x | no ¬p | yes q with Fin.inject₁ i Fin.≟ Fin.inject₁ i
exchangeFin-exchangeFin i x | no ¬p | yes refl | yes refl = begin
  suc (Fin.lower₁ (Fin.inject₁ i) _)
    ≡⟨ cong suc (Finₚ.lower₁-irrelevant _ _ _) ⟩
  suc (Fin.lower₁ (Fin.inject₁ i) _)
    ≡⟨ cong suc (Finₚ.lower₁-inject₁ i) ⟩
  suc i
    ∎
exchangeFin-exchangeFin i x | no ¬p | yes q | no ¬r = ⊥-elim (¬r refl)
exchangeFin-exchangeFin i x | no ¬p | no ¬q with Fin.inject₁ i Fin.≟ x
exchangeFin-exchangeFin i x | no ¬p | no ¬q | yes r = ⊥-elim (¬p r)
exchangeFin-exchangeFin i x | no ¬p | no ¬q | no ¬r with (suc i) Fin.≟ x
exchangeFin-exchangeFin i x | no ¬p | no ¬q | no ¬r | yes s = ⊥-elim (¬q s)
exchangeFin-exchangeFin i x | no ¬p | no ¬q | no ¬r | no ¬s = refl

exchange-exchange : ∀ (i : Fin n) (P : Scoped (suc n)) → exchange i (exchange i P) ≡ P
exchange-exchange i 𝟘 = refl
exchange-exchange i (ν P) rewrite exchange-exchange (suc i) P = refl
exchange-exchange i (P ∥ Q) rewrite exchange-exchange i P | exchange-exchange i Q = refl
exchange-exchange i (x ⦅⦆ P) rewrite exchangeFin-exchangeFin i x | exchange-exchange (suc i) P = refl
exchange-exchange i (x ⟨ y ⟩ P) rewrite exchangeFin-exchangeFin i x | exchangeFin-exchangeFin i y | exchange-exchange i P = refl

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


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

module FOT.PA.Inductive.CanonicalTerm where

-- We cannot extract a canonical term from a non-intuitionistic proof.

open import PA.Inductive.Base
open import PA.Inductive.PropertiesI

------------------------------------------------------------------------------
-- The existential projections

∃-proj₁ : ∀ {A} → ∃ A → ℕ
∃-proj₁ (x , _) = x

∃-proj₂ : ∀ {A} → (h : ∃ A) → A (∃-proj₁ h)
∃-proj₂ (_ , Ax) = Ax

------------------------------------------------------------------------------
-- Non-intuitionistic logic theorems

-- The principle of the excluded middle.
postulate pem : ∀ {A} → A ∨ ¬ A

-- The principle of indirect proof (proof by contradiction).
¬-elim : ∀ {A} → (¬ A → ⊥) → A
¬-elim h = case (λ a → a) (λ ¬a → ⊥-elim (h ¬a)) pem

-- ∃ in terms of ∀ and ¬.
¬∃¬→∀ : {A : ℕ → Set} → ¬ (∃[ x ] ¬ A x) → ∀ {x} → A x
¬∃¬→∀ h {x} = ¬-elim (λ h₁ → h (x , h₁))

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

-- Intuitionistic proof.
proof₁ : ∃[ x ] x ≢ succ x
proof₁ = succ zero , x≢Sx

-- Non-intuitionistic proof.
proof₂ : ∃[ x ] x ≢ succ x
proof₂ = ¬-elim (λ h → x≢Sx {succ zero} (¬∃¬→∀ h))

-- We can extract a canonical term from an intuitionistic proof.
canonicalTerm₁ : ∃-proj₁ proof₁ ≡ succ zero
canonicalTerm₁ = refl

-- We cannot extract a canonical term from a non-intuitionistic proof.
-- canonicalTerm₂ : ∃-proj₁ proof₂ ≡ succ zero
-- canonicalTerm₂ = {!refl!}

-- Agda error:
--
-- ∃-proj₁ ([ (λ a → a) , (λ ¬a → ⊥-elim (x≢Sx (¬∃¬→∀ ¬a))) ] pem) !=
-- succ zero of type M
-- when checking that the expression refl has type
-- ∃-proj₁ proof₂ ≡ succ zero

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module CombiningProofs.ForallExistSchema where

open import Common.FOL.FOL-Eq

A : D → Set
A x = x ≡ x ∨ x ≡ x
{-# ATP definition A #-}

postulate ∀→∃₁ : (∀ {x} → A x) → ∃ A
{-# ATP prove ∀→∃₁ #-}

postulate ∀→∃₂ : {A : D → Set} → (∀ {x} → A x) → ∃ A
{-# ATP prove ∀→∃₂ #-}


text:
module prime where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions

open import gcd
open import nat

record Prime (i : ℕ ) : Set where
   field
      p>1 : i > 1
      isPrime : ( j : ℕ ) → j < i → 0 < j → gcd i j ≡ 1

record NonPrime ( n : ℕ ) : Set where
   field
      factor : ℕ
      prime : Prime factor
      dividable : Dividable factor n

PrimeP : ( n : ℕ ) → Dec ( Prime n )
PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>1 p) (s≤s z≤n)))
PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>1 p) (s≤s (≤-refl))))
PrimeP (suc (suc n)) = isPrime1 (suc (suc n)) (suc n) (s≤s (s≤s z≤n)) a<sa (λ i m<i i<n → isp0 (suc n) i (<to≤ m<i) i<n ) where
   isp0 : (n : ℕ) (i : ℕ) ( n<i : n ≤ i) ( i<n : i < suc n ) →  gcd (suc n) i ≡ 1
   isp0  n i n<i i<n with <-cmp i n
   ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> n<i a)
   ... | tri≈ ¬a refl ¬c = gcd203 i
   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<n )
   isPrime1 : ( n m : ℕ ) → n > 1 → m < n → ( (i : ℕ) → m < i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
   isPrime1 n zero n>1 m<n lt = yes record { isPrime = λ j j<i 0<j → lt j 0<j j<i ; p>1 = n>1 }
   isPrime1 n (suc m) n>1 m<n lt with <-cmp (gcd n (suc m)) 1
   ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) n>1) (s≤s z≤n)) a )
   ... | tri≈ ¬a b ¬c = isPrime1 n m n>1 (<-trans a<sa m<n) isp1 where
    --  lt : (i : ℕ) → suc m ≤ i → suc i ≤ n → gcd1 n n i i ≡ 1
        isp1 :  (i : ℕ) → m < i → i < n → gcd n i ≡ 1
        isp1 i m<i i<n with <-cmp (suc m) i
        ... | tri< a ¬b ¬c = lt i a i<n
        ... | tri≈ ¬a m=i  ¬c = subst (λ k → gcd n k ≡ 1) m=i b -- gcd n (suc m) ≡ 1 →  gcd n i ≡ 1
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c) -- suc i ≤ suc m →  i < m
   ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) m<n (s≤s z≤n) )) c )

open import logic
open _∧_

-- find prime factor

data Factoring (m : ℕ ) : (n : ℕ) → Set where
     findFactor : (n : ℕ) → m ≤ n → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → Factoring m n
     skipFactor : (n : ℕ) → n < m →  Factoring m n

nonPrime : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
nonPrime {n} 1<n np = np1 n n np 1<n (findFactor n ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) )) where
    mg1 :  (n m : ℕ )→ ( (j : ℕ ) → m < j → j < n → gcd n j ≡ 1  ) →  gcd n m ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1
    mg1 n m mg gcd j m<j j<n with <-cmp m j
    ... | tri< a ¬b ¬c = mg j a j<n
    ... | tri≈ ¬a refl ¬c = gcd
    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<j c)
    np1 : ( n m : ℕ ) → ¬ Prime n → 1 < n → Factoring m n → NonPrime n
    np1 n zero np 1<n (findFactor n m≤n mg ) = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n
    np1 n (suc m) np 1<n (findFactor n m≤n mg) with <-cmp ( gcd n m ) 1
    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n m (<-trans (s≤s z≤n) 1<n) 0<m ) a ) where
         0<m : 0 < m
         0<m with <-cmp 0 m
         ... | tri< a ¬b ¬c = a
         ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<> a (subst (λ k → 1 < k) (sym (gcd20 n)) 1<n ))
    ... | tri≈ ¬a b ¬c = np1 n m np 1<n (findFactor n (≤-trans refl-≤s m≤n) (mg1 n m mg b ) )
    ... | tri> ¬a ¬b c with PrimeP ( gcd n m )
    ... | yes y = record { factor = gcd n m ; prime = y ;  dividable = proj1 (gcd-dividable n m ) }
    ... | no ngcd = np2 where
         skip-case : NonPrime (gcd n m) → NonPrime n
         skip-case  cc = record { factor = NonPrime.factor cc ; prime = NonPrime.prime cc ; dividable =
                          record { factor = (Dividable.factor (proj1 (gcd-dividable n m))) * (Dividable.factor (NonPrime.dividable cc))
                              ; is-factor = begin
             Dividable.factor (proj1 (gcd-dividable n m)) * Dividable.factor (NonPrime.dividable cc) * NonPrime.factor cc + 0 ≡⟨ refl ⟩
             g * d * p + 0 ≡⟨ +-comm _ 0 ⟩
             g * d * p  ≡⟨ *-assoc g d p  ⟩
             g * (d * p)  ≡⟨ cong (λ k → g * k ) (+-comm 0 _) ⟩
             g * (d * p + 0)  ≡⟨ cong (λ k → g * k ) (Dividable.is-factor (NonPrime.dividable cc) ) ⟩
             g * gcd n m  ≡⟨ +-comm 0 _ ⟩
             g * gcd n m + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable n m)) ⟩
             n ∎  }} where
                open ≡-Reasoning
                g =  Dividable.factor (proj1 (gcd-dividable n m))
                d =  Dividable.factor (NonPrime.dividable cc)
                p = NonPrime.factor cc
         np2 :  NonPrime n
         np2 with <-cmp (gcd n m) m
         ... | tri< a ¬b ¬c = skip-case (np1 (gcd n m) m ngcd c (skipFactor (gcd n m) a ))
         ... | tri≈ ¬a b ¬c = skip-case (np1 (gcd n m) m ngcd c
              (subst (λ k → Factoring m k) (sym b) (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))))
         ... | tri> ¬a ¬b' c with <-cmp 0 m
         ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (subst (λ k → k ≤ m) (gcdsym {m} {n}) (gcd-≤ a (<-trans a m≤n))) c )
         ... | tri≈ ¬a' b' ¬c = ⊥-elim ( np record { isPrime = λ j lt 0<j → mg j (subst (λ k → k < j) b' 0<j) lt ; p>1 = 1<n } ) -- suc m ≤ j
    np1 n zero np 1<n (skipFactor n ())
    np1 n (suc m) np 1<n  (skipFactor n n<m) with <-cmp m n
    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a n<m)
    ... | tri> ¬a ¬b c    = np1 n m np 1<n (skipFactor n c)
    ... | tri≈ ¬a refl ¬c = np1 n m np 1<n (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))

factorial : (n : ℕ) → ℕ
factorial zero = 1
factorial (suc n) = (suc n) * (factorial n)
factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n)
factorial-mono n = begin
     factorial n  ≤⟨ x≤x+y ⟩
     factorial n + n * factorial n ≡⟨ refl ⟩
     (suc n) * factorial n  ≡⟨ refl ⟩
     factorial (suc n)  ∎  where open ≤-Reasoning
factorial≥1 : {m : ℕ} → 1 ≤ factorial m
factorial≥1 {zero} = ≤-refl
factorial≥1 {suc m} = begin
     1 ≤⟨ s≤s z≤n ⟩
     (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
     (suc m) * factorial m ≡⟨ refl ⟩
     factorial (suc m)  ∎  where open ≤-Reasoning
m<factorial : (m : ℕ) → m ≤ factorial m
m<factorial zero = z≤n
m<factorial (suc m) = begin
     suc m ≡⟨ cong suc (+-comm 0 _) ⟩
     1 * suc m ≡⟨ *-comm 1 _ ⟩
     (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
     (suc m) * factorial m  ≡⟨ refl ⟩
     factorial (suc m)  ∎  where open ≤-Reasoning
-- *-monoˡ-≤ (suc m) {!!}
fact< : (m n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
fact< zero 1 0<n (s≤s (s≤s z≤n)) = record { factor = 1 ; is-factor = refl }
fact< (suc m) (suc zero) 0<n n<m = record { factor = factorial (suc (suc m)) ; is-factor = begin
     factorial (suc (suc m)) * 1 + 0  ≡⟨ +-comm _ 0 ⟩
     factorial (suc (suc m)) * 1   ≡⟨ m*1=m  ⟩
     (suc (suc m)) * factorial (suc m)  ≡⟨ refl ⟩
     factorial (suc (suc m))  ∎  } where open ≡-Reasoning
fact< (suc m) (suc (suc n)) 0<n n<m with <-cmp (suc (suc n)) (suc (suc m))
... | tri< a ¬b ¬c = record { factor = suc (suc m) * Dividable.factor fact1 ; is-factor = fact2 } where
      fact1 : Dividable (suc (suc n))  (factorial (suc m ))
      fact1 = fact< m (suc (suc n)) 0<n a
      d =  (fact< m (suc (suc n)) 0<n a)
      fact2 : suc (suc m) * Dividable.factor d * suc (suc n) + 0 ≡ factorial (suc (suc m))
      fact2 = begin
        suc (suc m) * Dividable.factor d * suc (suc n) + 0  ≡⟨ +-comm _ 0 ⟩
        suc (suc m) * Dividable.factor d * suc (suc n)   ≡⟨ *-assoc (suc (suc m)) (Dividable.factor d) ( suc (suc n)) ⟩
        suc (suc m) * (Dividable.factor d * suc (suc n))   ≡⟨ cong (λ k →  suc (suc m) * k ) ( +-comm 0 (Dividable.factor d * suc (suc n)) ) ⟩
        suc (suc m) * (Dividable.factor d * suc (suc n) + 0)   ≡⟨ cong (λ k → suc (suc m) * k ) (Dividable.is-factor d)  ⟩
        suc (suc m) * factorial (suc m)  ≡⟨ refl ⟩
        factorial (suc (suc m))  ∎   where open ≡-Reasoning
... | tri≈ ¬a b ¬c = record { factor = factorial (suc m)  ; is-factor = begin
     factorial (suc m) * suc (suc n) + 0 ≡⟨ +-comm _ 0 ⟩
     factorial (suc m) * suc (suc n)  ≡⟨ *-comm (factorial (suc m)) (suc (suc n))  ⟩
     (suc (suc n)) * factorial (suc m)  ≡⟨ cong (λ k → k * factorial (suc m) ) b ⟩
     (suc (suc m)) * factorial (suc m)  ≡⟨ refl ⟩
     factorial (suc (suc m))  ∎  } where open ≡-Reasoning
... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n<m)

f>m :  {m : ℕ} → suc m < suc (factorial (suc m))
f>m {m} = begin
     suc (suc m)  ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩
     suc (1 + 1 * m)  ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m)  ⟩
     suc (1 + m * 1)  ≤⟨ s≤s (s≤s (*-monoʳ-≤ m  (factorial≥1 {m}) )) ⟩
     suc (1 + m * factorial m) ≤⟨ s≤s  (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩
     suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
     suc (factorial (suc m)) ∎  where open ≤-Reasoning

prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j )
prime-is-infinite zero pmax = pmax 3 (s≤s z≤n) record { isPrime = λ n lt 0<j → pif3 n lt 0<j  ; p>1 = s≤s (s≤s z≤n) } where
  pif3 : (n : ℕ) →  n < 3 →  0 < n → gcd 3 n ≡ 1
  pif3 .1 (s≤s (s≤s z≤n)) _ = refl
  pif3 .2 (s≤s (s≤s (s≤s z≤n))) _ = refl
prime-is-infinite (suc m) pmax = newPrime where
  prime<max : (n : ℕ ) → Prime n → n < suc (suc m)
  prime<max n p with <-cmp n (suc m)
  ... | tri< a ¬b ¬c = ≤-trans a refl-≤s
  ... | tri≈ ¬a refl ¬c = ≤-refl
  ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p )
  fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
  fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>1 p)) ( prime<max n p )
  -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)
  newPrime : ⊥
  newPrime with PrimeP ( suc (factorial (suc m)) )
  ... | yes p = pmax _ f>m p   -- yes, we found a prime not in list
  ... | no np = div+1 (Prime.p>1 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
      -- n!+1 cannot be dividable, because n! is dividable
      -- the factor need not be a prime, but anyway we prove that there is a prime factor in NonPrime
      p1 : NonPrime  ( suc (factorial (suc m)) )
      p1 = nonPrime (begin
       2 ≤⟨ s≤s ( s≤s z≤n) ⟩
       suc (suc m) ≤⟨ s≤s (m<factorial (suc m))  ⟩
       suc (factorial (suc m)) ∎ ) np where open ≤-Reasoning

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