text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Truncation.Base where

open import Cubical.Data.NatMinusOne
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.Sn

data  ∥_∥_ {ℓ} (A : Type ℓ) (n : ℕ₋₁) : Type ℓ where
  ∣_∣ : A  → ∥ A ∥ n
  hub : (f : S (1+ n) → ∥ A ∥ n) → ∥ A ∥ n
  spoke : (f : S (1+ n) → ∥ A ∥ n) (x : S (1+ n)) → hub f ≡ f x

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat renaming (_==_ to _==N_; _<_ to _<N_)

record Eq (A : Set) : Set where
  field
    _==_ : A → A → Bool

open Eq {{...}}

record Ord (A : Set) : Set where
  constructor mkOrd
  field
    _<_ : A → A → Bool
    overlap {{eqA}} : Eq A

open Ord {{...}} hiding (eqA)

record Num (A : Set) : Set where
  constructor mkNum
  field
    fromNat : Nat → A
    overlap {{eqA}} : Eq A

open Num {{...}} hiding (eqA)

instance
  EqNat : Eq Nat
  _==_ {{EqNat}} = _==N_

  OrdNat : Ord Nat
  _<_ {{OrdNat}} = _<N_
  Ord.eqA OrdNat = EqNat

  NumNat : Num Nat
  fromNat {{NumNat}} n = n
  Num.eqA NumNat = EqNat

infixr 3 _||_
_||_ : Bool → Bool → Bool
true  || x = true
false || x = x

-- Here it will pick the eq dictionary from the Ord
leq3 : {A : Set} {{OrdA : Ord A}} {{NumA : Num A}} → A → Bool
leq3 x = x == fromNat 3 || x < fromNat 3

open import Agda.Builtin.Equality

2<3 : true ≡ leq3 2
2<3 = refl

it : ∀ {a} {A : Set a} {{_ : A}} → A
it {{x}} = x

-- Check that you get the first shared dictionary

getShared : {A : Set} {{OrdA : Ord A}} {{NumA : Num A}} → Eq A
getShared = it

itsOrd : {A : Set} {{OrdA : Ord A}} {{NumA : Num A}} → getShared ≡ Ord.eqA OrdA
itsOrd = refl

-- Check that it also works if you pattern match on the dictionaries

leq3' : {A : Set} {{OrdA : Ord A}} {{NumA : Num A}} → A → Bool
leq3' {{mkOrd _<_}} {{mkNum fromNat}} x = x == fromNat 3 || x < fromNat 3

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module GSeTT.GSeTT where
  open import GSeTT.Syntax
  open import GSeTT.Rules
  import GSeTT.CwF-structure
  import GSeTT.Dec-Type-Checking
  import GSeTT.Uniqueness-Derivations
  open import GSeTT.Typed-Syntax

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
------------------------------------------------------------------------
-- Code related to the paper "Isomorphism Is Equality" by Thierry
-- Coquand and Nils Anders Danielsson
--
-- The code is written by Nils Anders Danielsson
------------------------------------------------------------------------

-- Note that the code has been changed after the paper was published.

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

module README.Isomorphism-is-equality where

---=====================================================================
-- 2: Preliminaries

------------------------------------------------------------------------
-- 2.1: Hierarchy of Types

-- The lifting operator ↑. (Note that Agda is universe-polymorphic.)

import Prelude

------------------------------------------------------------------------
-- 2.2: Quantifiers

-- Σ, ∃ and _×_. (The code sometimes uses ∃ instead of Σ.)

import Prelude

------------------------------------------------------------------------
-- 2.3: Equality

-- Axiomatisations of equality, used in order to ensure that the
-- elimination rule (J) does not compute. J is called elim in the
-- code.

import Equality

-- Bijections (_↔_), the key property of equality of Σ-types
-- (Σ-≡,≡↔≡).

import Bijection

-- Extensionality.

import Equality

-- "∀ x. f x ≡ g x is in bijective correspondence with f ≡ g"
-- (extensionality-isomorphism).

import Equivalence

------------------------------------------------------------------------
-- 2.4: More Types

-- ⊤, ⊥, _+_ (called _⊎_ in the code), ℕ.

import Prelude

-- Logical equivalences (_⇔_).

import Logical-equivalence

------------------------------------------------------------------------
-- 2.5: Univalent Foundations

-- Contractible.

import Equality

-- H-level, Is-proposition, Is-set.

import H-level

-- Results that can be used to establish that a type has a certain
-- h-level.

import H-level
import H-level.Closure
import Equality.Decidable-UIP

-- Propositional second components of pairs can be dropped
-- (ignore-propositional-component).

import Function-universe

-- Is-equivalence, subst P eq is an equivalence
-- (subst-is-equivalence), _≃_, _≃_ is logically equivalent to _↔_ and
-- related properties (_≃_.bijection, ↔⇒≃, ↔↔≃, ⇔↔≃), Σ and Π preserve
-- equivalences (Σ-preserves, Π-preserves).

import Equivalence

-- More congruence properties (including _⊎-cong_ and →-cong).

import Function-universe

-- ≡⇒≃, Univalence, ≃⇒≡, the univalence axiom implies extensionality
-- (dependent-extensionality), the transport theorem
-- (transport-theorem), resp eq is an equivalence
-- (resp-is-equivalence), resp eq preserves compositions
-- (resp-preserves-compositions).

import Univalence-axiom

---=====================================================================
-- 3: Isomorphism Is Equality

------------------------------------------------------------------------
-- 3.1: Parameters

-- The parameters are represented using a record type called Universe.

import Univalence-axiom.Isomorphism-is-equality.Simple

------------------------------------------------------------------------
-- 3.2: Codes for Structures

-- Code, Instance, Is-isomorphism, Isomorphic, Carrier, element,
-- equality-pair-lemma.

import Univalence-axiom.Isomorphism-is-equality.Simple

------------------------------------------------------------------------
-- 3.3: Main Theorem

-- The main result (isomorphism-is-equality), isomorphism is equal to
-- equality (isomorphic≡≡), the right-to-left direction of the
-- bijection is equal to a simple function
-- (from-isomorphism-is-equality).

import Univalence-axiom.Isomorphism-is-equality.Simple

------------------------------------------------------------------------
-- 3.4: A Universe

-- U, El, cast, resp, resp-id, Is-isomorphism′,
-- isomorphism-definitions-isomorphic.

import Univalence-axiom.Isomorphism-is-equality.Simple

-- The operators _→-eq_ (→-cong-⇔), _×-eq_ (_×-cong_) and _+-eq_
-- (_⊎-cong_).

import Function-universe

-- The operators _→-rel_, _×-rel_ and _+-rel_ (_⊎-rel_).

import Prelude

------------------------------------------------------------------------
-- 3.5: Examples

-- Monoids, posets, discrete fields, fixpoint operators.

import Univalence-axiom.Isomorphism-is-equality.Simple

---=====================================================================
-- 4: Related Work

-- Aczel's structure identity principle (structure-identity-principle).

import Structure-identity-principle

-- The structure identity principle can be used to prove a slightly
-- restricted variant of our main theorem (isomorphism-is-equality′,
-- from-isomorphism-is-equality′).

import
  Univalence-axiom.Isomorphism-is-equality.Structure-identity-principle

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --copattern --safe --no-sized-types --guardedness #-}
module Copattern where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream public

-- | Bisimulation as equality
record _==_ {A : Set} (x : Stream A) (y : Stream A) : Set where
  coinductive
  field
    refl-head : head x ≡ head y
    refl-tail : tail x == tail y
open _==_ public

module Introduction where

  ones : Stream ℕ
  head ones = suc zero
  tail ones = ones

  repeat : {A : Set} -> A -> Stream A
  repeat {A} a = P
    where
    P : Stream A
    head P = a
    tail P = repeat a

  even : ∀ {A} -> Stream A -> Stream A
  even {A} a = P
    where
    P : Stream A
    head P = head a
    tail P = even (tail (tail a))

  odd : ∀ {A} -> Stream A -> Stream A
  odd {A} a = P
    where
    P : Stream A
    head P = head (tail a)
    tail P = odd (tail (tail a))

module Bisimulation where
  open Introduction

  refl′ : ∀ {A} -> (a : Stream A) -> a == a
  refl′ a = f
    where
    f : a == a
    refl-head f = refl
    refl-tail f = refl′ (tail a)

  oddEven : ∀ {A} -> (a : Stream A) -> odd a == even (tail a)
  oddEven a = f
    where
    f : odd a == even (tail a)
    refl-head f = refl
    refl-tail f = oddEven ((tail (tail a)))

module Merge where
  open Bisimulation
  open Introduction

  merge : ∀ {A} -> Stream A -> Stream A -> Stream A
  merge {A} a b = ma
    where
    ma : Stream A
    head ma = head a
    tail ma = merge b (tail a)

  -- Merge! Even! Odd!
  moe : ∀ {A} -> (a : Stream A) -> (merge (even a) (odd a) == a)
  moe a = f
    where
    f : merge (even a) (odd a) == a
    refl-head f = refl
    refl-head (refl-tail f) = refl
    refl-tail (refl-tail f) = moe (tail (tail a))

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module safe where

-- Note that if every module listed here is safe in isolation, it does
-- not mean that they are using compatible options. As a consequence,
-- importing a combination of some of the modules listed may lead to
-- an unsafe result.


text:
module sv20.assign2.Second where

open import sv20.assign2.SetTheory.Logic   using (_⇔_; ¬_; _∧_; _∨_) renaming (_,_ to ⟨_,_⟩)
open import sv20.assign2.SetTheory.ZAxioms using (𝓢; _⊆_; _∈_; _∉_; _≡_; _⊂_; sym; cong; subs; trans;
                                                  proj₁; proj₂;
                                                  empt; ext; union; pair; pow; sub; pem; sum)
open import sv20.assign2.SetTheory.Algebra using (_∪_; _-_; _∩_)

∪-dist : (A B C : 𝓢) → A ∪ (B ∪ C) ≡ (A ∪ B) ∪ C
∪-dist = ?

-- I could try going this route. This would prove certain things using
-- ZFC and would be really neat but requires too much work.


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

module FiniteTypeEquiv where
open import Level
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function.Equality using (_∘_; _⟶_; _⟨$⟩_)
open ≡-Reasoning
open import Function renaming (_∘_ to _○_)
open import FinVec

------------------------------------------------------------------------------
-- Permutations

record CPerm {ℓ : Level} (values : ℕ) (size : ℕ) : Set ℓ where
  constructor cp
  field
    π  : FinVec values size
    πᵒ : FinVec size values
    αp : π ∘̂ πᵒ ≡ 1C
    βp : πᵒ ∘̂ π ≡ 1C

-- Permutations are compared by ≡

-- The setoid of permutations under ≡

SCPerm : ∀ {ℓ} → ℕ → ℕ → Setoid ℓ ℓ
SCPerm m n = setoid (CPerm m n)

------------------------------------------------------------------------------
-- Equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ○ g) ∼ id
    β : (g ○ f) ∼ id

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) qinv

sym≃ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A ≃ B) → (B ≃ A)
sym≃ (A→B , equiv) = e.g , mkqinv A→B e.β e.α
  where module e = qinv equiv

-- Equivalences are compared by ≋ which reduces to extensional
-- equality of the underlying back and forth functions

_⋆_ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A ≃ B) → (x : A) → B
(f , _) ⋆ x = f x

record _≋_ {ℓ ℓ' : Level} {A : Set ℓ} {B : Set ℓ'} (eq₁ eq₂ : A ≃ B) :
  Set (ℓ ⊔ ℓ') where
  constructor eq
  field
    f≡ : ∀ x → eq₁ ⋆ x ≡ eq₂ ⋆ x
    g≡ : ∀ x → (sym≃ eq₁) ⋆ x ≡ (sym≃ eq₂) ⋆ x

id≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x : A ≃ B} → x ≋ x
id≋ = record { f≡ = λ x → refl ; g≡ = λ x → refl }

sym≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A ≃ B} → x ≋ y → y ≋ x
sym≋ (eq f≡ g≡) = eq (λ a → sym (f≡ a)) (λ b → sym (g≡ b))

trans≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y z : A ≃ B} → x ≋ y → y ≋ z → x ≋ z
trans≋ (eq f≡ g≡) (eq h≡ i≡) =
   eq (λ a → trans (f≡ a) (h≡ a)) (λ b → trans (g≡ b) (i≡ b))

-- The setoid of equivalences under ≋

_S≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Setoid (ℓ ⊔ ℓ') (ℓ ⊔ ℓ')
_S≃_ A B = record
 { Carrier = A ≃ B
 ; _≈_ = _≋_
 ; isEquivalence = record
   { refl = id≋
   ; sym = sym≋
   ; trans = trans≋
   }
 }

------------------------------------------------------------------------------
-- Univalence...

-- On one side we have permutations under ≡
-- On the other we have equivalences under ≋
--
-- The equivalence of these two sides uses a version of ≃ (called ≃S)
-- that relates setoids each with its own equivalence relation

infix 4 _≃S_

record _≃S_ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} (A : Setoid ℓ₁ ℓ₂) (B : Setoid ℓ₃ ℓ₄) :
  Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  constructor equiv
  field
    f : A ⟶ B
    g : B ⟶ A
    α : ∀ {x y} → Setoid._≈_ B x y → Setoid._≈_ B ((f ∘ g) ⟨$⟩ x) y
    β : ∀ {x y} → Setoid._≈_ A x y → Setoid._≈_ A ((g ∘ f) ⟨$⟩ x) y

univalence : {m n : ℕ} →
  _≃S_ {zero} {zero} {zero} {zero} (SCPerm m n) (Fin m S≃ Fin n)
univalence {m} {n} = equiv {!!} {!!} {!!} {!!}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Issue857 where

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

data ⊤ : Set where
  tt : ⊤

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = λ ()

bad : (x : ⊥) → ⊥-elim x ≡ tt
bad x = {!!}  -- Goal type: x ≡ tt, with x : ⊥.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Oscar.Property where

open import Oscar.Builtin.Numbatural
open import Oscar.Builtin.Objectevel

𝑴 : ℕ → ∀ {𝔬} → Ø 𝔬 → ∀ 𝔪 → Ø 𝔬 ∙̂ ↑̂ 𝔪
𝑴 ∅ 𝔒 𝔪 = 𝔒 → Ø 𝔪
𝑴 (↑ n) 𝔒 𝔪 = 𝔒 → 𝑴 n 𝔒 𝔪

𝑴² : ∀ (m : ℕ) n {𝔬} {𝔒 : Ø 𝔬} {𝔪} → 𝑴 n 𝔒 𝔪 → ∀ 𝔮 → Ø 𝔬 ∙̂ 𝔪 ∙̂ ↑̂ 𝔮
𝑴² m ∅ 𝔒 𝔮 = ∀ {o} → 𝑴 m (𝔒 o) 𝔮
𝑴² m (↑ n) 𝔒 𝔮 = ∀ {o} → 𝑴² m n (𝔒 o) 𝔮


text:
-- Andreas, 2015-06-29 fixed handling of projections in positivity checker

-- {-# OPTIONS -v tc.polarity:20 -v tc.proj.like:10 -v tc.pos:10  --show-implicit #-}
-- {-# OPTIONS -v tc.pos.occ:70  #-}

open import Common.Prelude
open import Common.Product

dup : (b : Bool) (X : Set) → Set × Set
dup true  X = (X → X) , X
dup false X = (X → X) , X

postulate b : Bool

data D : Set where
  c : proj₁ (dup b D) → D

-- ERROR WAS:
-- D is not strictly positive, because it occurs
-- in the second argument to dup
-- in the type of the constructor c
-- in the definition of D.

-- EXPECTED ERROR:
-- D is not strictly positive, because it occurs
-- in the second argument to dup
-- in the first argument to proj₁
-- in the type of the constructor c
-- in the definition of D.


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Normal Forms.
------------------------------------------------------------------------------

open import Data.Nat
  using (suc; zero; _+_;_*_)
  renaming (_⊔_ to max; ℕ to Nat )

module Data.PropFormula.NormalForms (n : Nat) where

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

open import Data.Bool.Base
  using ( Bool; true; false; if_then_else_; not)
  renaming (_∧_ to _and_; _∨_ to _or_)

open import Data.Fin  using ( Fin; #_ )
open import Data.List using ( List; [_]; [];  _++_; _∷_ ; concatMap; map )

open import Data.PropFormula.Properties n using ( subst )
open import Data.PropFormula.Syntax n
open import Data.PropFormula.Views  n

open import Relation.Nullary using (yes; no)
open import Data.PropFormula.Theorems n

open import Function using ( _∘_; _$_ )
open import Relation.Binary.PropositionalEquality using ( _≡_; sym )

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

------------------------------------------------------------------------------
-- Negation Normal Form (NNF)
------------------------------------------------------------------------------

-- Def.
nnf₁ : Nat → PropFormula → PropFormula
nnf₁ (suc n) φ
  with n-view φ
...  | conj φ₁ φ₂   = nnf₁ n φ₁ ∧ nnf₁ n φ₂
...  | disj φ₁ φ₂   = nnf₁ n φ₁ ∨ nnf₁ n φ₂
...  | impl φ₁ φ₂   = nnf₁ n ((¬ φ₁) ∨ φ₂)
...  | biimpl φ₁ φ₂ = nnf₁ n ((φ₁ ⊃ φ₂) ∧ (φ₂ ⊃ φ₁))
...  | nconj φ₁ φ₂  = nnf₁ n ((¬ φ₁) ∨ (¬ φ₂))
...  | ndisj φ₁ φ₂  = nnf₁ n ((¬ φ₁) ∧ (¬ φ₂))
...  | nneg φ₁      = nnf₁ n φ₁
...  | nimpl φ₁ φ₂  = nnf₁ n (¬ (φ₂ ∨ (¬ φ₁)))
...  | nbiim φ₁ φ₂  = nnf₁ n (¬ ((φ₁ ⊃ φ₂) ∧ (φ₂ ⊃ φ₁)))
...  | ntop         = ⊥
...  | nbot         = ⊤
...  | other .φ     = φ
nnf₁ zero φ         = φ

-- Theorem.
nnf₁-lem
  : ∀ {Γ} {φ}
  → (n : Nat)
  → Γ ⊢ φ
  → Γ ⊢ nnf₁ n φ

-- Proof.
nnf₁-lem {Γ} {φ} (suc n) Γ⊢φ
  with n-view φ
...  | conj φ₁ φ₂ =
  ∧-intro
    (nnf₁-lem n (∧-proj₁ Γ⊢φ))
    (nnf₁-lem n (∧-proj₂ Γ⊢φ))
...  | disj φ₁ φ₂ =
  (⊃-elim
    (⊃-intro
     (∨-elim
       (∨-intro₁
         (nnf₁ n φ₂)
         (nnf₁-lem n (assume φ₁)))
       (∨-intro₂
         (nnf₁ n φ₁)
         (nnf₁-lem n (assume φ₂)))))
      Γ⊢φ)
...  | impl φ₁ φ₂   = nnf₁-lem n (⊃-to-¬∨ Γ⊢φ)
...  | biimpl φ₁ φ₂ = nnf₁-lem n (⇔-equiv₁ Γ⊢φ)
...  | nconj φ₁ φ₂  = nnf₁-lem n (¬∧-to-¬∨¬ Γ⊢φ)
...  | ndisj φ₁ φ₂  = nnf₁-lem n (¬∨-to-¬∧¬ Γ⊢φ)
...  | nneg φ₁      = nnf₁-lem n (¬¬-equiv₁ Γ⊢φ)
...  | nimpl φ₁ φ₂  = nnf₁-lem n (subst⊢¬ helper Γ⊢φ)
  where
    helper : Γ ⊢ φ₂ ∨ ¬ φ₁ ⊃ (φ₁ ⊃ φ₂)
    helper = ⊃-intro (¬∨-to-⊃ (∨-comm (assume (φ₂ ∨ ¬ φ₁))))
...  | nbiim φ₁ φ₂  =
  nnf₁-lem n
    (subst⊢¬
      (⊃-intro
        (⇔-equiv₂
          (assume ((φ₁ ⊃ φ₂) ∧ (φ₂ ⊃ φ₁)))))
          Γ⊢φ)
...  | ntop       = ¬-elim Γ⊢φ ⊤-intro
...  | nbot       = ⊤-intro
...  | other .φ   = Γ⊢φ
nnf₁-lem {Γ} {φ} zero Γ⊢φ = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Complexity measure.
nnf-cm : PropFormula → Nat
nnf-cm φ with n-view φ
... | conj φ₁ φ₂   = nnf-cm φ₁ + nnf-cm φ₂ + 1
... | disj φ₁ φ₂   = nnf-cm φ₁ + nnf-cm φ₂ + 1
... | impl φ₁ φ₂   = 2 * nnf-cm φ₁  + nnf-cm φ₂ + 1
... | biimpl φ₁ φ₂ = 2 * (nnf-cm φ₁ + nnf-cm φ₂) + 3
... | nconj φ₁ φ₂  = nnf-cm (¬ φ₁) + nnf-cm (¬ φ₂) + 1
... | ndisj φ₁ φ₂  = nnf-cm (¬ φ₁) + nnf-cm (¬ φ₂) + 1
... | nneg φ₁      = nnf-cm (¬ φ₁) + 1
... | nimpl φ₁ φ₂  = nnf-cm φ₁ + nnf-cm (¬ φ₂) + 3
... | nbiim φ₁ φ₂  = nnf-cm φ₁ + nnf-cm φ₂ +
                     nnf-cm (¬ φ₁) + nnf-cm (¬ φ₂) + 8
... | ntop         = 1
... | nbot         = 1
... | other .φ     = 1

-- Def.
nnf : PropFormula → PropFormula
nnf φ = nnf₁ (nnf-cm φ) φ

-- Theorem.
nnf-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ nnf φ

-- Proof.
nnf-lem {Γ} {φ} Γ⊢φ = nnf₁-lem (nnf-cm φ) Γ⊢φ
--------------------------------------------------------------------------- ∎

------------------------------------------------------------------------------
-- Disjunctive Normal Form (DNF)
------------------------------------------------------------------------------

-- Def.
dist-∧ : PropFormula → PropFormula
dist-∧ φ with d-view-aux φ
... | case₁ φ₁ φ₂ φ₃ = dist-∧ (φ₁ ∧ φ₃) ∨ dist-∧ (φ₂ ∧ φ₃)
... | case₂ φ₁ φ₂ φ₃ = dist-∧ (φ₁ ∧ φ₂) ∨ dist-∧ (φ₁ ∧ φ₃)
... | other .φ       = φ

-- Theorem.
dist-∧-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ dist-∧ φ

-- Proof.
dist-∧-lem {Γ} {φ} Γ⊢φ with d-view-aux φ
dist-∧-lem {Γ} {.((φ ∨ ψ) ∧ γ)} Γ⊢⟨φ∨ψ⟩∧γ | case₁ φ ψ γ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ (dist-∧ (ψ ∧ γ))
          (dist-∧-lem
            (∧-intro
              (assume φ)
              (weaken φ (∧-proj₂ Γ⊢⟨φ∨ψ⟩∧γ)))))
        (∨-intro₂ (dist-∧ (φ ∧ γ))
          (dist-∧-lem
            (∧-intro
              (assume ψ)
              (weaken ψ (∧-proj₂ Γ⊢⟨φ∨ψ⟩∧γ)))))))
     (∧-proj₁ Γ⊢⟨φ∨ψ⟩∧γ)

dist-∧-lem {Γ} {.(φ ∧ (ψ ∨ γ))} Γ⊢φ∧⟨ψ∨γ⟩ | case₂ φ ψ γ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ (dist-∧ (φ ∧ γ))
          (dist-∧-lem
            (∧-intro
              (weaken ψ (∧-proj₁ Γ⊢φ∧⟨ψ∨γ⟩))
              (assume ψ))))
        (∨-intro₂ (dist-∧ (φ ∧ ψ))
          (dist-∧-lem
            (∧-intro
              (weaken γ (∧-proj₁ Γ⊢φ∧⟨ψ∨γ⟩))
              (assume γ))))))
    (∧-proj₂ Γ⊢φ∧⟨ψ∨γ⟩)
dist-∧-lem {Γ} {.φ} Γ⊢φ             | other φ     = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Theorem.
from-dist-∧-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ dist-∧ φ
  → Γ ⊢ φ

-- Proof.
from-dist-∧-lem {Γ} {φ} Γ⊢φ with d-view-aux φ
from-dist-∧-lem {Γ} {.((φ ∨ ψ) ∧ γ)} Γ⊢⟨φ∨ψ⟩∧γ | case₁ φ ψ γ =
  ∧-comm
    (∧-dist₂
      (⊃-elim
        (⊃-intro
          (∨-elim
            (∨-intro₁ (γ ∧ ψ)
              (∧-comm
                (from-dist-∧-lem
                  (assume (dist-∧ (φ ∧ γ))))))
            (∨-intro₂ (γ ∧ φ)
              (∧-comm
                (from-dist-∧-lem
                  (assume (dist-∧ (ψ ∧ γ))))))))
        Γ⊢⟨φ∨ψ⟩∧γ))
from-dist-∧-lem {Γ} {.(φ ∧ (ψ ∨ γ))} Γ⊢φ∧⟨ψ∨γ⟩ | case₂ φ ψ γ =
  ∧-dist₂
    (⊃-elim
      (⊃-intro
        (∨-elim
          (∨-intro₁ (φ ∧ γ)
            (from-dist-∧-lem (assume (dist-∧ (φ ∧ ψ)))))
          (∨-intro₂ (φ ∧ ψ)
            (from-dist-∧-lem (assume (dist-∧ (φ ∧ γ)))))))
      Γ⊢φ∧⟨ψ∨γ⟩)
from-dist-∧-lem {Γ} {.φ} Γ⊢φ             | other φ     = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Def.
dnf-dist : PropFormula → PropFormula
dnf-dist φ with d-view φ
dnf-dist .(φ ∧ ψ) | conj φ ψ = dist-∧ (dnf-dist φ ∧ dnf-dist ψ)
dnf-dist .(φ ∨ ψ) | disj φ ψ = dnf-dist φ ∨ dnf-dist ψ
dnf-dist φ        | other .φ = φ

-- Theorem.
dnf-dist-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ dnf-dist φ

-- Proof.
dnf-dist-lem {Γ} {φ} Γ⊢φ with d-view φ
dnf-dist-lem {Γ} {φ ∧ ψ} Γ⊢φ∧ψ | conj .φ .ψ =
  dist-∧-lem
    (∧-intro
      (dnf-dist-lem (∧-proj₁ Γ⊢φ∧ψ))
      (dnf-dist-lem (∧-proj₂ Γ⊢φ∧ψ)))
dnf-dist-lem {Γ} {φ ∨ ψ} Γ⊢φ∨ψ | disj .φ .ψ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ (dnf-dist ψ) (dnf-dist-lem (assume φ)))
        (∨-intro₂ (dnf-dist φ) (dnf-dist-lem (assume ψ)))))
    Γ⊢φ∨ψ
dnf-dist-lem {Γ} {φ} Γ⊢φ       | other .φ   = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Theorem.
from-dnf-dist-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ dnf-dist φ
  → Γ ⊢ φ

-- Proof.
from-dnf-dist-lem {_} {φ} Γ⊢φ with d-view φ
from-dnf-dist-lem {_} {φ ∧ ψ} Γ⊢φ∧ψ | conj .φ .ψ =
  ∧-intro
    (from-dnf-dist-lem {φ = φ}
      (∧-proj₁ (from-dist-∧-lem Γ⊢φ∧ψ)))
    (from-dnf-dist-lem {φ = ψ}
      (∧-proj₂ {φ = dnf-dist φ}
        (from-dist-∧-lem Γ⊢φ∧ψ)))
from-dnf-dist-lem {_} {φ ∨ ψ} Γ⊢φ∨ψ | disj .φ .ψ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ ψ
          (from-dnf-dist-lem (assume (dnf-dist φ))))
        (∨-intro₂ φ
          (from-dnf-dist-lem (assume (dnf-dist ψ))))))
    Γ⊢φ∨ψ
from-dnf-dist-lem {_} {φ} Γ⊢φ       | other .φ   = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Def.
dnf : PropFormula → PropFormula
dnf = dnf-dist ∘ nnf

-- Theorem.
dnf-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ dnf φ

-- Proof.
dnf-lem = dnf-dist-lem ∘ nnf-lem
--------------------------------------------------------------------------- ∎

------------------------------------------------------------------------------
-- Conjunctive Normal Forms (CNF)
------------------------------------------------------------------------------

-- Def.
dist-∨ : PropFormula → PropFormula
dist-∨ φ with c-view-aux φ
dist-∨ .((φ₁ ∧ φ₂) ∨ φ₃) | case₁ φ₁ φ₂ φ₃ =
  dist-∨ (φ₁ ∨ φ₃) ∧ dist-∨ (φ₂ ∨ φ₃)
dist-∨ .(φ₁ ∨ (φ₂ ∧ φ₃)) | case₂ φ₁ φ₂ φ₃ =
  dist-∨ (φ₁ ∨ φ₂) ∧ dist-∨ (φ₁ ∨ φ₃)
dist-∨ φ                 | other .φ       = φ

-- Theorem.
dist-∨-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ dist-∨ φ

-- Proof.
dist-∨-lem {Γ} {φ} Γ⊢φ with c-view-aux φ
dist-∨-lem {Γ} {.((φ ∧ ψ) ∨ γ)} Γ⊢φ | case₁ φ ψ γ =
  ∧-intro
   (dist-∨-lem (∧-proj₁ helper))
   (dist-∨-lem (∧-proj₂ helper))
  where
    helper : Γ ⊢ (φ ∨ γ) ∧ (ψ ∨ γ)
    helper =
      ∧-intro
        (∨-comm (∧-proj₁ (∨-dist₁ (∨-comm Γ⊢φ))))
        (∨-comm (∧-proj₂ (∨-dist₁ (∨-comm Γ⊢φ))))
dist-∨-lem {Γ} {.(φ ∨ (ψ ∧ γ))} Γ⊢φ | case₂ φ ψ γ =
  ∧-intro
    (dist-∨-lem (∧-proj₁ (∨-dist₁ Γ⊢φ)))
    (dist-∨-lem (∧-proj₂ (∨-dist₁ Γ⊢φ)))
dist-∨-lem {Γ} {.φ}  Γ⊢φ | other φ = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Theorem.
from-dist-∨-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ dist-∨ φ
  → Γ ⊢ φ

-- Proof.
from-dist-∨-lem {Γ} {φ} Γ⊢φ with c-view-aux φ
from-dist-∨-lem {Γ} {.((φ ∧ ψ) ∨ γ)} Γ⊢φ | case₁ φ ψ γ =
  ∨-comm
    (∨-dist₂
      (∧-intro
        (∨-comm
          (from-dist-∨-lem (∧-proj₁ Γ⊢φ)))
        (∨-comm
          (from-dist-∨-lem (∧-proj₂ Γ⊢φ)))))
from-dist-∨-lem {Γ} {.(φ ∨ (ψ ∧ γ))} Γ⊢φ | case₂ φ ψ γ =
  ∨-dist₂
    (∧-intro (from-dist-∨-lem (∧-proj₁ Γ⊢φ))
    (from-dist-∨-lem (∧-proj₂ Γ⊢φ)))
from-dist-∨-lem {Γ} {.φ}  Γ⊢φ | other φ = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Def.
cnf-dist : PropFormula → PropFormula
cnf-dist φ with d-view φ
cnf-dist .(φ ∧ ψ) | conj φ ψ = cnf-dist φ ∧ cnf-dist ψ
cnf-dist .(φ ∨ ψ) | disj φ ψ = dist-∨ ((cnf-dist φ) ∨ (cnf-dist ψ))
cnf-dist φ        | other .φ = φ

-- Theorem.
cnf-dist-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ cnf-dist φ

-- Proof.
cnf-dist-lem {_} {φ} Γ⊢φ
  with d-view φ
cnf-dist-lem {_} {.(φ ∧ ψ)} Γ⊢φ∧ψ | conj φ ψ =
  ∧-intro (cnf-dist-lem (∧-proj₁ Γ⊢φ∧ψ)) (cnf-dist-lem (∧-proj₂ Γ⊢φ∧ψ))
cnf-dist-lem {_} {.(φ ∨ ψ)} Γ⊢φ∨ψ | disj φ ψ =
  dist-∨-lem
    (⊃-elim
      (⊃-intro
        (∨-elim
          (∨-intro₁ (cnf-dist ψ) (cnf-dist-lem (assume φ)))
          (∨-intro₂ (cnf-dist φ) (cnf-dist-lem (assume ψ)))))
      Γ⊢φ∨ψ)
cnf-dist-lem {_} {.φ} Γ⊢φ | other φ  = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Theorem.
from-cnf-dist-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ cnf-dist φ
  → Γ ⊢ φ

-- Proof.
from-cnf-dist-lem {_} {φ} Γ⊢cnfdist
  with d-view φ
from-cnf-dist-lem {_} {.(φ ∧ ψ)} Γ⊢cnfdistφ∧ψ | conj φ ψ =
  ∧-intro
    (from-cnf-dist-lem (∧-proj₁ Γ⊢cnfdistφ∧ψ))
    (from-cnf-dist-lem (∧-proj₂ Γ⊢cnfdistφ∧ψ))
from-cnf-dist-lem {_} {.(φ ∨ ψ)} Γ⊢cnfdistφ∨ψ | disj φ ψ =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₁ ψ (from-cnf-dist-lem (assume (cnf-dist φ))))
        (∨-intro₂ φ (from-cnf-dist-lem (assume (cnf-dist ψ))))))
    (from-dist-∨-lem Γ⊢cnfdistφ∨ψ)
from-cnf-dist-lem {_} {.φ} Γ⊢φ | other φ  = Γ⊢φ
--------------------------------------------------------------------------- ∎

-- Def.
cnf : PropFormula → PropFormula
cnf = cnf-dist ∘ nnf

-- Theorem.
cnf-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ cnf φ

-- Proof.
cnf-lem = cnf-dist-lem ∘ nnf-lem  -- ▪

----------------------------------------------------------------------------
-- Testing for a normal form.

is∨ : PropFormula → Bool
is∨ φ
  with d-view φ
is∨ .(φ₁ ∧ φ₂) | conj φ₁ φ₂ = false
is∨ .(φ₁ ∨ φ₂) | disj φ₁ φ₂ = is∨ φ₁ and is∨ φ₂
is∨ φ          | other .φ   = true

is∧∨ : PropFormula → Bool
is∧∨ φ
  with d-view φ
is∧∨ .(φ₁ ∧ φ₂) | conj φ₁ φ₂ = is∧∨ φ₁ and is∧∨ φ₂
is∧∨ .(φ₁ ∨ φ₂) | disj φ₁ φ₂ = is∨ φ₁ and is∨ φ₂
is∧∨ φ          | other .φ   = true

is∧ : PropFormula → Bool
is∧ φ
  with d-view φ
is∧ .(φ₁ ∧ φ₂) | conj φ₁ φ₂ = is∧ φ₁ and is∧ φ₂
is∧ .(φ₁ ∨ φ₂) | disj φ₁ φ₂ = false
is∧ φ          | other .φ   = true

is∨∧ : PropFormula → Bool
is∨∧ φ
  with d-view φ
is∨∧ .(φ₁ ∧ φ₂) | conj φ₁ φ₂ = is∧ φ₁ and is∧ φ₂
is∨∧ .(φ₁ ∨ φ₂) | disj φ₁ φ₂ = is∨∧ φ₁ and is∨∧ φ₂
is∨∧ φ          | other .φ   = true

isNNF : PropFormula → Bool
isNNF φ
  with push-neg-view φ
isNNF φ          | yes .φ     = false
isNNF .(φ₁ ∧ φ₂) | no-∧ φ₁ φ₂ = isNNF φ₁ and isNNF φ₂
isNNF .(φ₁ ∨ φ₂) | no-∨ φ₁ φ₂ = isNNF φ₁ and isNNF φ₂
isNNF φ          | no .φ      = true

isCNF : PropFormula → Bool
isCNF φ = isNNF φ and is∧∨ φ

isDNF : PropFormula → Bool
isDNF φ = isNNF φ and is∨∧ φ

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
module Tactic.Nat.Simpl.Lemmas where

open import Prelude
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Container.Bag
open import Tactic.Nat.Auto
open import Prelude.Nat.Properties
open import Container.List.Properties
open import Tactic.Nat.Auto.Lemmas

product1-sound : ∀ xs → product1 xs ≡ productR xs
product1-sound [] = refl
product1-sound (x ∷ xs)
  rewrite sym (cong (λ x → foldl _*_ x xs) (mul-one-r x))
        | foldl-assoc _*_ mul-assoc x 1 xs
        | foldl-foldr _*_ 1 mul-assoc add-zero-r mul-one-r xs
        = refl

map-eq : ∀ {c b} {A : Set c} {B : Set b} (f g : A → B) →
           (∀ x → f x ≡ g x) → ∀ xs → map f xs ≡ map g xs
map-eq f g f=g [] = refl
map-eq f g f=g (x ∷ xs) rewrite f=g x | map-eq f g f=g xs = refl

fst-*** : ∀ {a b} {A₁ A₂ : Set a} {B₁ B₂ : Set b}
            (f : A₁ → B₁) (g : A₂ → B₂) (p : A₁ × A₂) →
            fst ((f *** g) p) ≡ f (fst p)
fst-*** f g (x , y) = refl

snd-*** : ∀ {a b} {A₁ A₂ : Set a} {B₁ B₂ : Set b}
            (f : A₁ → B₁) (g : A₂ → B₂) (p : A₁ × A₂) →
            snd ((f *** g) p) ≡ g (snd p)
snd-*** f g (x , y) = refl

eta : ∀ {a b} {A : Set a} {B : Set b} (p : A × B) → p ≡ (fst p , snd p)
eta (x , y) = refl

private
  shuffle₁ : (a b c : Nat) → a + (b + c) ≡ b + (a + c)
  shuffle₁ a b c = auto

module _ {Atom : Set} {{_ : Ord Atom}} where

  NFEqS : NF Atom × NF Atom → Env Atom → Set
  NFEqS (nf₁ , nf₂) ρ = ⟦ nf₁ ⟧ns ρ ≡ ⟦ nf₂ ⟧ns ρ

  NFEq : NF Atom × NF Atom → Env Atom → Set
  NFEq (nf₁ , nf₂) ρ = ⟦ nf₁ ⟧n ρ ≡ ⟦ nf₂ ⟧n ρ

  ts-sound : ∀ x (ρ : Env Atom) → ⟦ x ⟧ts ρ ≡ ⟦ x ⟧t ρ
  ts-sound (0 , x) ρ = mul-zero-r (product1 (map ρ x))
  ts-sound (1 , x) ρ = product1-sound (map ρ x) ⟨≡⟩ʳ add-zero-r _
  ts-sound (suc (suc i) , x) ρ
    rewrite sym (product1-sound (map ρ x))
          = auto

  private
    et : Env Atom → Nat × Tm Atom → Nat
    et  = flip ⟦_⟧t

    ets : Env Atom → Nat × Tm Atom → Nat
    ets = flip ⟦_⟧ts

    plus-nf : Nat → Env Atom → NF Atom → Nat
    plus-nf = λ a ρ xs → a + ⟦ xs ⟧n ρ

  ns-sound : ∀ nf (ρ : Env Atom) → ⟦ nf ⟧ns ρ ≡ ⟦ nf ⟧n ρ
  ns-sound [] ρ = refl
  ns-sound (x ∷ nf) ρ
    rewrite sym (foldl-map-fusion _+_ (ets ρ) (ets ρ x) nf)
          | ts-sound x ρ
          | map-eq (ets ρ) (et ρ) (flip ts-sound ρ) nf
          | sym (foldl-foldr _+_ 0 add-assoc (λ _ → refl) add-zero-r (map (et ρ) nf))
          | sym (foldl-assoc _+_ add-assoc (et ρ x) 0 (map (et ρ) nf))
          | add-zero-r (et ρ x)
          = refl

  private
    lem-sound : ∀ a b ρ f g (xs : NF Atom × NF Atom) →
            a + ⟦ fst ((f *** g) xs) ⟧n ρ ≡ b + ⟦ snd ((f *** g) xs) ⟧n ρ →
            a + ⟦ f (fst xs) ⟧n ρ         ≡ b + ⟦ g (snd xs) ⟧n ρ
    lem-sound a b ρ f g xs H =
      cong (plus-nf a ρ) (fst-*** f g xs)
      ʳ⟨≡⟩ H
       ⟨≡⟩ cong (plus-nf b ρ) (snd-*** f g xs)

  cancel-sound′ : ∀ a b nf₁ nf₂ (ρ : Env Atom) →
                    a + ⟦ fst (cancel nf₁ nf₂) ⟧n ρ ≡ b + ⟦ snd (cancel nf₁ nf₂) ⟧n ρ →
                    a + ⟦ nf₁ ⟧n ρ ≡ b + ⟦ nf₂ ⟧n ρ
  cancel-sound′ a b [] []        ρ H = H
  cancel-sound′ a b [] (x ∷ nf₂) ρ H = H
  cancel-sound′ a b (x ∷ nf₁) [] ρ H = H
  cancel-sound′ a b ((i , x) ∷ nf₁) ((j , y) ∷ nf₂) ρ H
    with compare x y
  ... | less _ = add-assoc a _ _ ⟨≡⟩ cancel-sound′ (a + et ρ (i , x)) b nf₁ ((j , y) ∷ nf₂) ρ
                   (add-assoc a _ _ ʳ⟨≡⟩ lem-sound a b ρ (_∷_ (i , x)) id (cancel nf₁ ((j , y) ∷ nf₂)) H)
  ... | greater _ =
          cancel-sound′ a (b + et ρ (j , y)) ((i , x) ∷ nf₁) nf₂ ρ
            (lem-sound a b ρ id (_∷_ (j , y)) (cancel ((i , x) ∷ nf₁) nf₂) H ⟨≡⟩ add-assoc b _ _)
          ⟨≡⟩ʳ add-assoc b _ _
  cancel-sound′ a b ((i , x) ∷ nf₁) ((j , .x) ∷ nf₂) ρ H | equal refl
    with compare i j
  cancel-sound′ a b ((i , x) ∷ nf₁) ((.(suc k + i) , .x) ∷ nf₂) ρ H | equal refl | less (diff! k) =
    shuffle₁ a (et ρ (i , x)) _
    ⟨≡⟩ cong (et ρ (i , x) +_) (cancel-sound′ a (b + et ρ (suc k , x)) nf₁ nf₂ ρ
          (lem-sound a b ρ id (_∷_ (suc k , x)) (cancel nf₁ nf₂) H ⟨≡⟩ add-assoc b _ _))
    ⟨≡⟩ auto
  cancel-sound′ a b ((.(suc k + j) , x) ∷ nf₁) ((j , .x) ∷ nf₂) ρ H | equal refl | greater (diff! k) =
    sym (shuffle₁ b (et ρ (j , x)) _
         ⟨≡⟩ cong (et ρ (j , x) +_) (sym (cancel-sound′ (a + et ρ (suc k , x)) b nf₁ nf₂ ρ
               (add-assoc a _ _ ʳ⟨≡⟩ lem-sound a b ρ (_∷_ (suc k , x)) id (cancel nf₁ nf₂) H)))
         ⟨≡⟩ auto)
  cancel-sound′ a b ((i , x) ∷ nf₁) ((.i , .x) ∷ nf₂) ρ H | equal refl | equal refl =
    shuffle₁ a (et ρ (i , x)) _
    ⟨≡⟩ cong (et ρ (i , x) +_) (cancel-sound′ a b nf₁ nf₂ ρ H)
    ⟨≡⟩ shuffle₁ (et ρ (i , x)) b _

  cancel-sound-s′ : ∀ a b nf₁ nf₂ (ρ : Env Atom) →
                         a + ⟦ fst (cancel nf₁ nf₂) ⟧ns ρ ≡ b + ⟦ snd (cancel nf₁ nf₂) ⟧ns ρ →
                         a + ⟦ nf₁ ⟧ns ρ ≡ b + ⟦ nf₂ ⟧ns ρ
  cancel-sound-s′ a b nf₁ nf₂ ρ eq =
    (a +_) $≡ ns-sound nf₁ ρ ⟨≡⟩
    cancel-sound′ a b nf₁ nf₂ ρ
      ((a +_) $≡ ns-sound (fst (cancel nf₁ nf₂)) ρ ʳ⟨≡⟩
       eq ⟨≡⟩ (b +_) $≡ ns-sound (snd (cancel nf₁ nf₂)) ρ) ⟨≡⟩ʳ
    (b +_) $≡ ns-sound nf₂ ρ

  cancel-sound : ∀ nf₁ nf₂ ρ → NFEqS (cancel nf₁ nf₂) ρ → NFEq (nf₁ , nf₂) ρ
  cancel-sound nf₁ nf₂ ρ H rewrite cong (λ p → NFEqS p ρ) (eta (cancel nf₁ nf₂)) =
    (cancel-sound′ 0 0 nf₁ nf₂ ρ
      (ns-sound (fst (cancel nf₁ nf₂)) ρ
         ʳ⟨≡⟩ H ⟨≡⟩
       ns-sound (snd (cancel nf₁ nf₂)) ρ))

  private
    prod : Env Atom → List Atom → Nat
    prod ρ x = productR (map ρ x)

  private
    lem-complete : ∀ a b ρ f g (xs : NF Atom × NF Atom) →
            a + ⟦ f (fst xs) ⟧n ρ         ≡ b + ⟦ g (snd xs) ⟧n ρ →
            a + ⟦ fst ((f *** g) xs) ⟧n ρ ≡ b + ⟦ snd ((f *** g) xs) ⟧n ρ
    lem-complete a b ρ f g xs H =
      cong (plus-nf a ρ) (fst-*** f g xs)
       ⟨≡⟩  H
       ⟨≡⟩ʳ cong (plus-nf b ρ) (snd-*** f g xs)

  cancel-complete′ : ∀ a b nf₁ nf₂ (ρ : Env Atom) →
                       a + ⟦ nf₁ ⟧n ρ ≡ b + ⟦ nf₂ ⟧n ρ →
                       a + ⟦ fst (cancel nf₁ nf₂) ⟧n ρ ≡ b + ⟦ snd (cancel nf₁ nf₂) ⟧n ρ
  cancel-complete′ a b [] [] ρ H = H
  cancel-complete′ a b [] (x ∷ nf₂) ρ H = H
  cancel-complete′ a b (x ∷ nf₁) [] ρ H = H
  cancel-complete′ a b ((i , x) ∷ nf₁) ((j , y) ∷ nf₂) ρ H with compare x y
  ... | less lt =
    lem-complete a b ρ (_∷_ (i , x)) id (cancel nf₁ ((j , y) ∷ nf₂))
      (add-assoc a _ _
       ⟨≡⟩ cancel-complete′ (a + et ρ (i , x)) b nf₁ ((j , y) ∷ nf₂) ρ
             (add-assoc a _ _ ʳ⟨≡⟩ H))
  ... | greater _ =
    lem-complete a b ρ id (_∷_ (j , y)) (cancel ((i , x) ∷ nf₁) nf₂)
      (cancel-complete′ a (b + et ρ (j , y)) ((i , x) ∷ nf₁) nf₂ ρ
        (H ⟨≡⟩ add-assoc b _ _)
       ⟨≡⟩ʳ add-assoc b _ _)
  cancel-complete′ a b ((i , x) ∷ nf₁) ((j , .x) ∷ nf₂) ρ H | equal refl with compare i j
  cancel-complete′ a b ((i , x) ∷ nf₁) ((.(suc (k + i)) , .x) ∷ nf₂) ρ H | equal refl | less (diff! k) =
    lem-complete a b ρ id (_∷_ (suc k , x)) (cancel nf₁ nf₂)
      (cancel-complete′ a (b + suc k * prod ρ x) nf₁ nf₂ ρ
        (add-inj₂ (i * prod ρ x) _ _
          (shuffle₁ (i * prod ρ x) a _
            ⟨≡⟩ H ⟨≡⟩ auto))
      ⟨≡⟩ʳ add-assoc b _ _)
  cancel-complete′ a b ((.(suc (k + j)) , x) ∷ nf₁) ((j , .x) ∷ nf₂) ρ H | equal refl | greater (diff! k) =
    lem-complete a b ρ (_∷_ (suc k , x)) id (cancel nf₁ nf₂)
      (add-assoc a _ _ ⟨≡⟩
       cancel-complete′ (a + suc k * prod ρ x) b nf₁ nf₂ ρ
         (add-inj₂ (j * prod ρ x) _ _
           (sym (shuffle₁ (j * prod ρ x) b _ ⟨≡⟩ʳ
                 auto ʳ⟨≡⟩ H))))
  cancel-complete′ a b ((i , x) ∷ nf₁) ((.i , .x) ∷ nf₂) ρ H | equal refl | equal refl =
    cancel-complete′ a b nf₁ nf₂ ρ
      (add-inj₂ (i * prod ρ x) _ _
        (shuffle₁ a (i * prod ρ x) _ ʳ⟨≡⟩ H ⟨≡⟩ shuffle₁ b (i * prod ρ x) _))

  cancel-complete-s′ : ∀ a b nf₁ nf₂ (ρ : Env Atom) →
                         a + ⟦ nf₁ ⟧ns ρ ≡ b + ⟦ nf₂ ⟧ns ρ →
                         a + ⟦ fst (cancel nf₁ nf₂) ⟧ns ρ ≡ b + ⟦ snd (cancel nf₁ nf₂) ⟧ns ρ
  cancel-complete-s′ a b nf₁ nf₂ ρ eq =
    (a +_) $≡ ns-sound (fst (cancel nf₁ nf₂)) ρ ⟨≡⟩
    cancel-complete′ a b nf₁ nf₂ ρ
      ((a +_) $≡ ns-sound nf₁ ρ ʳ⟨≡⟩
       eq ⟨≡⟩ (b +_) $≡ ns-sound nf₂ ρ) ⟨≡⟩ʳ
    (b +_) $≡ ns-sound (snd (cancel nf₁ nf₂)) ρ

  cancel-complete : ∀ nf₁ nf₂ ρ → NFEq (nf₁ , nf₂) ρ → NFEqS (cancel nf₁ nf₂) ρ
  cancel-complete nf₁ nf₂ ρ H rewrite cong (λ p → NFEqS p ρ) (eta (cancel nf₁ nf₂)) =
         ns-sound (fst (cancel nf₁ nf₂)) ρ
    ⟨≡⟩  cancel-complete′ 0 0 nf₁ nf₂ ρ H
    ⟨≡⟩ʳ ns-sound (snd (cancel nf₁ nf₂)) ρ

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Extension Theorems of the Syntax definitions.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Weakening ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Properties n using ( substΓ )

open import Data.List using ( List ; [] ; _∷_ ; _++_ ; [_] )

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

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

-- Theorem.
weaken-Δ₁
  : ∀ {Γ} {φ}
  → (Δ : Ctxt)
  → Γ ⊢ φ
  → Γ ⨆ Δ ⊢ φ

-- Proof.
weaken-Δ₁ {[]}    {φ} [] Γ⊢φ = Γ⊢φ
weaken-Δ₁ {x ∷ Γ} {φ} [] Γ⊢φ = substΓ (sym helper) Γ⊢φ
  where
    helper : ∀ {Γ} → Γ ⨆ [] ≡ Γ
    helper {[]} = refl
    helper {x ∷ Γ} rewrite helper {Γ = Γ} = refl
weaken-Δ₁ {Γ} {φ} (x ∷ []) Γ⊢φ = weaken x Γ⊢φ
weaken-Δ₁ {Γ} {φ} (x₁ ∷ Δ) Γ⊢φ =
  substΓ
    helper
    (weaken-Δ₁ Δ
      (weaken x₁ Γ⊢φ))
  where
    helper : ∀ {Γ Δ} {x} → (Γ , x ) ⨆  Δ ≡ Γ ⨆ (x ∷ Δ)
    helper {[]} {Δ} = refl
    helper {y ∷ Γ} {Δ} {x} rewrite helper {Γ = Γ} {Δ = Δ} {x = x} = refl
-------------------------------------------------------------------------- ∎

-- Theorem.
weaken-Δ₂
  :  ∀ {Γ} {φ}
  → (Δ : Ctxt)
  → Γ ⊢ φ
  → Δ ⨆ Γ ⊢ φ

-- Proof.
weaken-Δ₂ {_}  []           Γ⊢φ = Γ⊢φ
weaken-Δ₂ {[]} (hyp ∷ [])   Γ⊢φ = weaken₂ hyp Γ⊢φ
weaken-Δ₂ {_}  (hyp ∷ [])   Γ⊢φ = weaken₂ hyp Γ⊢φ
weaken-Δ₂ {_}  (hyp ∷ hyps) Γ⊢φ = weaken₂ hyp (weaken-Δ₂ hyps Γ⊢φ)
-------------------------------------------------------------------------- ∎


text:
-- Andreas, 2016-07-08, issue reported by Nisse

module Issue2081 where

module M where

  private

    Private : Set₁
    Private = Set
      -- The local module should be private as well!
      module Public where
        -- The definitions inside this module should not be private
        -- unless declared so explicitly!
        Public : Set₁
        Public = Set

  private
    Bla = Public -- should work!
      -- This `where` should not give a 'useless private' error:
      where open Public

module Pu = M.Public -- should fail!


text:
{-

Macros (autoDesc, AutoStructure, AutoEquivStr, autoUnivalentStr) for automatically generating structure definitions.

For example:

  autoDesc (λ (X : Type₀) → X → X × ℕ)   ↦   function+ var (var , constant ℕ)

We prefer to use the constant structure whenever possible, e.g., [autoDesc (λ (X : Type₀) → ℕ → ℕ)]
is [constant (ℕ → ℕ)] rather than [function (constant ℕ) (constant ℕ)].

Writing [auto* (λ X → ⋯)] doesn't seem to work, but [auto* (λ (X : Type ℓ) → ⋯)] does.

-}
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Structures.Relational.Auto where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.List
open import Cubical.Data.Bool
open import Cubical.Data.Maybe

open import Cubical.Structures.Relational.Macro as Macro

import Agda.Builtin.Reflection as R

-- Magic number
private
  FUEL = 10000

-- Mark a constant type with a proof it is a set
abstract
  Const[_] : ∀ {ℓ} → hSet ℓ → Type ℓ
  Const[ A ] = A .fst

-- Some reflection utilities
private
  _>>=_ = R.bindTC
  _<|>_ = R.catchTC

  _>>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → R.TC A → R.TC B → R.TC B
  f >> g = f >>= λ _ → g

  infixl 4 _>>=_ _>>_ _<|>_

  varg : ∀ {ℓ} {A : Type ℓ} → A → R.Arg A
  varg = R.arg (R.arg-info R.visible R.relevant)

  tLevel = R.def (quote Level) []

  tType : R.Term → R.Term
  tType ℓ = R.def (quote Type) [ varg ℓ ]

  thSet : R.Term → R.Term
  thSet ℓ = R.def (quote hSet) [ varg ℓ ]

  tPosRelDesc : R.Term → R.Term
  tPosRelDesc ℓ = R.def (quote PosRelDesc) [ varg ℓ ]

  tRelDesc : R.Term → R.Term
  tRelDesc ℓ = R.def (quote RelDesc) [ varg ℓ ]

  func : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
  func ℓ ℓ' = Type ℓ → Type ℓ'

  tStruct : R.Term → R.Term → R.Term
  tStruct ℓ ℓ' = R.def (quote func) (varg ℓ ∷ varg ℓ' ∷ [])

  newMeta = R.checkType R.unknown

-- We try to build a descriptor by unifying the provided structure with combinators we're aware of. We
-- redefine the structure combinators as the *Shape terms below so that we don't depend on the specific way
-- these are defined in other files (order of implicit arguments and so on); the syntactic analysis that goes
-- on here means that we would get mysterious errors if those changed.
private
  constantShape : ∀ {ℓ'} (ℓ : Level) (A : hSet ℓ') → (Type ℓ → Type ℓ')
  constantShape _ A _ = Const[ A ]

  pointedShape : (ℓ : Level) → Type ℓ → Type ℓ
  pointedShape _ X = X

  productShape : ∀ {ℓ₀ ℓ₁} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → (Type ℓ → Type ℓ₁) → Type ℓ → Type (ℓ-max ℓ₀ ℓ₁)
  productShape _ A₀ A₁ X = A₀ X × A₁ X

  paramShape : ∀ {ℓ₀ ℓ'} (ℓ : Level)
    → Type ℓ' → (Type ℓ → Type ℓ₀) → Type ℓ → Type (ℓ-max ℓ' ℓ₀)
  paramShape _ A A₀ X = A → A₀ X

  functionShape :  ∀ {ℓ₀ ℓ₁} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → (Type ℓ → Type ℓ₁) → Type ℓ → Type (ℓ-max ℓ₀ ℓ₁)
  functionShape _ A₀ A₁ X = A₀ X → A₁ X

  maybeShape : ∀ {ℓ₀} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → Type ℓ → Type ℓ₀
  maybeShape _ A₀ X = Maybe (A₀ X)

private
  -- Build transport structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildPosRelDesc : ℕ → R.Term → R.Term → R.Term → R.TC R.Term
  buildPosRelDesc zero ℓ ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n" ∷ R.termErr t ∷ [])
  buildPosRelDesc (suc fuel) ℓ ℓ' t =
    tryConstant t <|> tryPointed t <|> tryProduct t <|> tryMaybe t <|>
    R.typeError (R.strErr "Can't automatically generate a positive structure for\n" ∷ R.termErr t ∷ [])
    where
    tryConstant : R.Term → R.TC R.Term
    tryConstant t =
      newMeta (thSet ℓ') >>= λ A →
      R.unify t (R.def (quote constantShape) (varg ℓ ∷ varg A ∷ [])) >>
      R.returnTC (R.con (quote PosRelDesc.constant) (varg A ∷ []))

    tryPointed : R.Term → R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) (varg ℓ ∷ [])) >>
      R.returnTC (R.con (quote PosRelDesc.var) [])

    tryProduct : R.Term → R.TC R.Term
    tryProduct t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote productShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildPosRelDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildPosRelDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote PosRelDesc._,_) (varg d₀ ∷ varg d₁ ∷ []))

    tryMaybe : R.Term → R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote maybeShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildPosRelDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote PosRelDesc.maybe) (varg d₀ ∷ []))

  autoPosRelDesc' : R.Term → R.Term → R.TC Unit
  autoPosRelDesc' t hole =
    R.inferType hole >>= λ H →
    newMeta tLevel >>= λ ℓ →
    newMeta tLevel >>= λ ℓ' →
    R.unify (tPosRelDesc ℓ) H >>
    R.checkType t (tStruct ℓ ℓ') >>
    buildPosRelDesc FUEL ℓ ℓ' t >>= R.unify hole

  -- Build structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildRelDesc : ℕ → R.Term → R.Term → R.Term → R.TC R.Term
  buildRelDesc zero ℓ ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n" ∷ R.termErr t ∷ [])
  buildRelDesc (suc fuel) ℓ ℓ' t =
    tryConstant t <|> tryPointed t <|> tryProduct t <|> tryParam t <|> tryFunction t <|>
    tryMaybe t <|>
    R.typeError (R.strErr "Can't automatically generate a structure for\n" ∷ R.termErr t ∷ [])
    where
    tryConstant : R.Term → R.TC R.Term
    tryConstant t =
      newMeta (thSet ℓ') >>= λ A →
      R.unify t (R.def (quote constantShape) (varg ℓ ∷ varg A ∷ [])) >>
      R.returnTC (R.con (quote RelDesc.constant) (varg A ∷ []))

    tryPointed : R.Term → R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) (varg ℓ ∷ [])) >>
      R.returnTC (R.con (quote RelDesc.var) [])

    tryProduct : R.Term → R.TC R.Term
    tryProduct t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote productShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildRelDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildRelDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote RelDesc._,_) (varg d₀ ∷ varg d₁ ∷ []))

    tryParam : R.Term → R.TC R.Term
    tryParam t =
      newMeta (tType R.unknown) >>= λ A →
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote paramShape) (varg ℓ ∷ varg A ∷ varg A₀ ∷ [])) >>
      buildRelDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote RelDesc.param) (varg A ∷ varg d₀ ∷ []))

    tryFunction : R.Term → R.TC R.Term
    tryFunction t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote functionShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildPosRelDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildRelDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote RelDesc.function+) (varg d₀ ∷ varg d₁ ∷ []))

    tryMaybe : R.Term → R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote maybeShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildRelDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote RelDesc.maybe) (varg d₀ ∷ []))

  autoRelDesc' : R.Term → R.Term → R.TC Unit
  autoRelDesc' t hole =
    R.inferType hole >>= λ H →
    newMeta tLevel >>= λ ℓ →
    newMeta tLevel >>= λ ℓ' →
    R.unify (tRelDesc ℓ) H >>
    R.checkType t (tStruct ℓ ℓ') >>
    buildRelDesc FUEL ℓ ℓ' t >>= R.unify hole

macro
  -- (Type ℓ → Type ℓ₁) → PosRelDesc ℓ
  autoPosRelDesc : R.Term → R.Term → R.TC Unit
  autoPosRelDesc = autoPosRelDesc'

  -- (S : Type ℓ → Type ℓ₁) → RelDesc ℓ
  autoRelDesc : R.Term → R.Term → R.TC Unit
  autoRelDesc = autoRelDesc'

  -- (S : Type ℓ → Type ℓ₁) → (Type ℓ → Type ℓ₁)
  -- Sanity check: should be the identity
  AutoStructure : R.Term → R.Term → R.TC Unit
  AutoStructure t hole =
    newMeta (tRelDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote RelMacroStructure) [ varg d ]) >>
    autoRelDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → StrRel S _
  AutoRelStr : R.Term → R.Term → R.TC Unit
  AutoRelStr t hole =
    newMeta (tRelDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote RelMacroRelStr) [ varg d ]) >>
    autoRelDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → SuitableStrRel S (AutoStrRel S)
  autoSuitableRel : R.Term → R.Term → R.TC Unit
  autoSuitableRel t hole =
    newMeta (tRelDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote relMacroSuitableRel) [ varg d ]) >>
    autoRelDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → StrRelMatchesEquiv (AutoRelStr S) (AutoEquivStr S)
  autoMatchesEquiv : R.Term → R.Term → R.TC Unit
  autoMatchesEquiv t hole =
    newMeta (tRelDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote relMacroMatchesEquiv) [ varg d ]) >>
    autoRelDesc' t d

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module LogicalFormulae where

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

{-# BUILTIN EQUALITY _≡_ #-}

data False : Set where
data False' {a : _} : Set a where

record True : Set where
{-# BUILTIN UNIT True #-}
record True' {a : _} : Set a where

infix 10 _||_
data _||_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : A → A || B
  inr : B → A || B

infix 15 _&&_
record _&&_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,,_
  field
    fst : A
    snd : B

equalityLeft : {a b : _} {A : Set a} {B : Set b} {x1 x2 : A && B} → (x1 ≡ x2) → _&&_.fst x1 ≡ _&&_.fst x2
equalityLeft {x1 = a ,, _} {.a ,, _} refl = refl

equalityRight : {a b : _} {A : Set a} {B : Set b} {x1 x2 : A && B} → (x1 ≡ x2) → _&&_.snd x1 ≡ _&&_.snd x2
equalityRight {x1 = _ ,, a} {_ ,, .a} refl = refl

infix 15 _&_&_
record _&_&_ {a b c} (A : Set a) (B : Set b) (C : Set c) : Set (a ⊔ b ⊔ c) where
  field
    one : A
    two : B
    three : C

data Sg {n : _} {m : _} (A : Set m) (B : A → Set n) : Set (m ⊔ n) where
  _,_ : (a : A) → (b : B a) → Sg A B

underlying : {n m : _} {A : _} {prop : _} → Sg {n} {m} A prop -> A
underlying (a , b) = a

underlyingRefl : {n m : _} {A : _} {prop : _} → {r s : Sg {n} {m} A prop} → r ≡ s → underlying r ≡ underlying s
underlyingRefl {r = (a , b)} {(.a , .b)} refl = refl

transitivity : {a : _} {A : Set a} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
transitivity refl refl = refl

liftEquality : {a : _} {A B : Set a} (f g : A → B) → (x y : A) → (f ≡ g) → (x ≡ y) → ((f x) ≡ (g y))
liftEquality f .f x .x refl refl = refl

applyEquality : {a : _} {b : _} {A : Set a} {B : Set b} (f : A → B) → {x y : A} → (x ≡ y) → ((f x) ≡ (f y))
applyEquality {A} {B} f {x} {.x} refl = refl

applyEquality2 : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) → {x y : A} → (x ≡ y) → {m n : B} → (m ≡ n) → f x m ≡ f y n
applyEquality2 f x=y m=n rewrite x=y | m=n = refl

identityOfIndiscernablesLeft : {m n o : _} {A : Set m} {B : Set n} {a : A} {b : B} {c : A} → (prop : A → B → Set o) → (prop a b) → (a ≡ c) → (prop c b)
identityOfIndiscernablesLeft {a = a} {b} {.a} prop pAB refl = pAB

identityOfIndiscernablesRight : {m n o : _} {A : Set m} {B : Set n} {a : A} {b c : B} → (prop : A → B → Set o) → (prop a b) → (b ≡ c) → (prop a c)
identityOfIndiscernablesRight {a = a} {b} {.b} prop prAB refl = prAB

equalityCommutative : {a : _} {A : Set a} {x y : A} → (x ≡ y) → (y ≡ x)
equalityCommutative refl = refl

exFalso : {n : _} {A : Set n} → .(x : False) → A
exFalso {a} = λ ()

exFalso' : {r n : _} {A : Set n} → .(x : False' {r}) → A
exFalso' ()

orIsAssociative : {n : _} {a b c : Set n} → ((a || b) || c) → (a || (b || c))
orIsAssociative (inl (inl x)) = inl x
orIsAssociative (inl (inr x)) = inr (inl x)
orIsAssociative (inr x) = inr (inr x)

lemConstructive : {n : _} → {p : Set n} → (p || (p → False)) → (((p → False) → False) → p)
lemConstructive (inl p) = λ _ → p
lemConstructive (inr notP) = λ negnegP → exFalso (negnegP notP)

lemConverse : {n : _} → {p : Set n} → p → ((p → False) → False)
lemConverse p = λ notP → notP p

typeCast : {a : _} {A : Set a} {B : Set a} (el : A) (pr : A ≡ B) → B
typeCast {a} {A} {.A} elt refl = elt

data Singleton {a} {A : Set a} (x : A) : Set a where
  _with≡_ : (y : A) → x ≡ y → Singleton x

inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
inspect x = x with≡ refl

curry : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) → ((Sg A (λ _ → B)) → C)
curry f (a , b) = f a b

uncurry : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : (Sg A (λ _ → B)) → C) → (A → B → C)
uncurry f a b = f (a , b)

decidableOr : {a b : _} → (A : Set a) → (B : Set b) → (A || (A → False)) → (A || B) → (A || ((A → False) && B))
decidableOr {a} {b} A B decidable (inl x) = inl x
decidableOr {a} {b} A B (inl y) (inr x) = inl y
decidableOr {a} {b} A B (inr y) (inr x) = inr (record { fst = y ; snd = x})

embedLevel : {a b : _} → Set a → Set (a ⊔ b)
embedLevel {a} {b} A = A && (True' {b})


text:
------------------------------------------------------------------------
-- A variant of set quotients with erased higher constructors
------------------------------------------------------------------------

-- This module contains some basic definitions with few dependencies
-- (in particular, not Quotient). See Quotient.Erased for more
-- definitions. The definitions below are reexported from
-- Quotient.Erased.

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

-- Partly following the HoTT book, but adapted for erasure.
--
-- Unlike the HoTT book, but following the cubical library (in which
-- set quotients were implemented by Zesen Qian and Anders Mörtberg),
-- the quotienting relations are not (always) required to be
-- propositional.

-- The module is parametrised by a notion of equality. The higher
-- constructors of the HIT defining quotients use path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Quotient.Erased.Basics
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
import H-level P.equality-with-J as PH
open import H-level.Closure equality-with-J

private
  variable
    a b p r : Level
    A B     : Type a
    R       : A → A → Type r
    x y     : A

------------------------------------------------------------------------
-- Quotients

-- The quotient type constructor.

infix 5 _/ᴱ_

data _/ᴱ_ (A : Type a) (@0 R : A → A → Type r) : Type (a ⊔ r) where
  [_]                      : A → A /ᴱ R
  @0 []-respects-relationᴾ : {x y : A} → R x y → [ x ] P.≡ [ y ]
  @0 /ᴱ-is-setᴾ            : P.Is-set (A /ᴱ R)

-- [_] respects the quotient relation (in erased contexts).

@0 []-respects-relation : R x y → _≡_ {A = A /ᴱ R} [ x ] [ y ]
[]-respects-relation = _↔_.from ≡↔≡ ∘ []-respects-relationᴾ

-- Quotients are sets (in erased contexts).

@0 /ᴱ-is-set : Is-set (A /ᴱ R)
/ᴱ-is-set = _↔_.from (H-level↔H-level 2) /ᴱ-is-setᴾ

------------------------------------------------------------------------
-- Eliminators

-- An eliminator, expressed using paths.

record Elimᴾ′ {A : Type a} {@0 R : A → A → Type r}
              (P : A /ᴱ R → Type p) :
              Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    @0 []-respects-relationʳ :
      (r : R x y) →
      P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y

    @0 is-setʳ :
      {eq₁ eq₂ : x P.≡ y} {p : P x} {q : P y}
      (eq₃ : P.[ (λ i → P (eq₁ i)) ] p ≡ q)
      (eq₄ : P.[ (λ i → P (eq₂ i)) ] p ≡ q) →
      P.[ (λ i → P.[ (λ j → P (/ᴱ-is-setᴾ eq₁ eq₂ i j)) ] p ≡ q) ]
        eq₃ ≡ eq₄

open Elimᴾ′ public

elimᴾ′ :
  {@0 R : A → A → Type r}
  {P : A /ᴱ R → Type p} →
  Elimᴾ′ P → (x : A /ᴱ R) → P x
elimᴾ′ {A = A} {R = R} {P = P} e = helper
  where
  module E = Elimᴾ′ e

  helper : (x : A /ᴱ R) → P x
  helper [ x ]                       = E.[]ʳ x
  helper ([]-respects-relationᴾ r i) = E.[]-respects-relationʳ r i
  helper (/ᴱ-is-setᴾ p q i j)        =
    E.is-setʳ (λ i → helper (p i)) (λ i → helper (q i)) i j

-- A possibly more useful eliminator, expressed using paths.

record Elimᴾ {A : Type a} {@0 R : A → A → Type r}
             (P : A /ᴱ R → Type p) :
             Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    @0 []-respects-relationʳ :
      (r : R x y) →
      P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y

    @0 is-setʳ : ∀ x → P.Is-set (P x)

open Elimᴾ public

elimᴾ :
  {@0 R : A → A → Type r}
  {P : A /ᴱ R → Type p} →
  Elimᴾ P → (x : A /ᴱ R) → P x
elimᴾ e = elimᴾ′ λ where
    .[]ʳ                   → E.[]ʳ
    .[]-respects-relationʳ → E.[]-respects-relationʳ
    .is-setʳ               → P.heterogeneous-UIP E.is-setʳ _
  where
  module E = Elimᴾ e

private

  -- One can define elimᴾ′ using elimᴾ.

  elimᴾ′₂ :
    {@0 R : A → A → Type r}
    {P : A /ᴱ R → Type p} →
    Elimᴾ′ P → (x : A /ᴱ R) → P x
  elimᴾ′₂ {P = P} e = elimᴾ λ where
      .[]ʳ                   → E.[]ʳ
      .[]-respects-relationʳ → E.[]-respects-relationʳ
      .is-setʳ x {y} {z} p q →                                          $⟨ E.is-setʳ p q ⟩
        P.[ (λ i →
               P.[ (λ j → P (/ᴱ-is-setᴾ P.refl P.refl i j)) ] y ≡ z) ]
          p ≡ q                                                         ↝⟨ P.subst (λ eq → P.[ (λ i → P.[ (λ j → P (eq i j)) ] y ≡ z) ] p ≡ q)
                                                                                (PH.mono₁ 2 /ᴱ-is-setᴾ _ _) ⟩
        P.[ (λ _ → P.[ (λ _ → P x) ] y ≡ z) ] p ≡ q                     ↔⟨⟩

        p P.≡ q                                                         □
    where
    module E = Elimᴾ′ e

-- A non-dependent eliminator, expressed using paths.

record Recᴾ {A : Type a} (@0 R : A → A → Type r) (B : Type b) :
            Type (a ⊔ r ⊔ b) where
  no-eta-equality
  field
    []ʳ                      : A → B
    @0 []-respects-relationʳ : (r : R x y) → []ʳ x P.≡ []ʳ y
    @0 is-setʳ               : P.Is-set B

open Recᴾ public

recᴾ :
  {@0 R : A → A → Type r} →
  Recᴾ R B → A /ᴱ R → B
recᴾ r = elimᴾ λ where
    .[]ʳ                   → R.[]ʳ
    .[]-respects-relationʳ → R.[]-respects-relationʳ
    .is-setʳ _             → R.is-setʳ
  where
  module R = Recᴾ r

-- An eliminator.

record Elim {A : Type a} {@0 R : A → A → Type r}
            (P : A /ᴱ R → Type p) :
            Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ : ∀ x → P [ x ]

    @0 []-respects-relationʳ :
      (r : R x y) →
      subst P ([]-respects-relation r) ([]ʳ x) ≡ []ʳ y

    @0 is-setʳ : ∀ x → Is-set (P x)

open Elim public

elim :
  {@0 R : A → A → Type r}
  {P : A /ᴱ R → Type p} →
  Elim P → (x : A /ᴱ R) → P x
elim e = elimᴾ λ where
    .[]ʳ                   → E.[]ʳ
    .[]-respects-relationʳ → subst≡→[]≡ ∘ E.[]-respects-relationʳ
    .is-setʳ               → _↔_.to (H-level↔H-level 2) ∘ E.is-setʳ
  where
  module E = Elim e

-- A non-dependent eliminator.

record Rec {A : Type a} (@0 R : A → A → Type r) (B : Type b) :
           Type (a ⊔ r ⊔ b) where
  no-eta-equality
  field
    []ʳ                      : A → B
    @0 []-respects-relationʳ : (r : R x y) → []ʳ x ≡ []ʳ y
    @0 is-setʳ               : Is-set B

open Rec public

rec :
  {@0 R : A → A → Type r} →
  Rec R B → A /ᴱ R → B
rec r = recᴾ λ where
    .[]ʳ                   → R.[]ʳ
    .[]-respects-relationʳ → _↔_.to ≡↔≡ ∘ R.[]-respects-relationʳ
    .is-setʳ               → _↔_.to (H-level↔H-level 2) R.is-setʳ
  where
  module R = Rec r

-- A variant of elim that can be used if the motive composed with [_]
-- is a family of propositions.
--
-- I took the idea for this eliminator from Nicolai Kraus.

record Elim-prop
         {A : Type a} {@0 R : A → A → Type r}
         (P : A /ᴱ R → Type p) :
         Type (a ⊔ r ⊔ p) where
  no-eta-equality
  field
    []ʳ                : ∀ x → P [ x ]
    @0 is-propositionʳ : ∀ x → Is-proposition (P [ x ])

open Elim-prop public

elim-prop :
  {@0 R : A → A → Type r}
  {P : A /ᴱ R → Type p} →
  Elim-prop P → (x : A /ᴱ R) → P x
elim-prop e = elim λ where
    .[]ʳ                     → E.[]ʳ
    .[]-respects-relationʳ _ → E.is-propositionʳ _ _ _
    .is-setʳ                 → elim λ @0 where
      .[]ʳ                     → mono₁ 1 ∘ E.is-propositionʳ
      .[]-respects-relationʳ _ → H-level-propositional ext 2 _ _
      .is-setʳ _               → mono₁ 1 (H-level-propositional ext 2)
  where
  module E = Elim-prop e

-- A variant of rec that can be used if the motive is a proposition.

record Rec-prop (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    []ʳ                : A → B
    @0 is-propositionʳ : Is-proposition B

open Rec-prop public

rec-prop :
  {@0 R : A → A → Type r} →
  Rec-prop A B → A /ᴱ R → B
rec-prop r = elim-prop λ where
    .[]ʳ               → R.[]ʳ
    .is-propositionʳ _ → R.is-propositionʳ
  where
  module R = Rec-prop r


text:
module conversion where

open import lib

open import cedille-types
open import ctxt
open import is-free
open import lift
open import rename
open import subst
open import syntax-util
open import general-util
open import erase

{- Some notes:

   -- hnf{TERM} implements erasure as well as normalization.

   -- hnf{TYPE} does not descend into terms.

   -- definitions are assumed to be in hnf
-}

data unfolding : Set where
  no-unfolding : unfolding
  unfold : (unfold-all : 𝔹) {- if ff we unfold just the head -}
           → (unfold-lift : 𝔹) {- if tt we unfold lifting types -}
           → (dampen-after-head-beta : 𝔹) {- if tt we will not unfold definitions after a head beta reduction -}
           → (erase : 𝔹) -- if tt erase the term as we unfold
           → unfolding

unfolding-get-erased : unfolding → 𝔹
unfolding-get-erased no-unfolding = ff
unfolding-get-erased (unfold _ _ _ e) = e

unfolding-set-erased : unfolding → 𝔹 → unfolding
unfolding-set-erased no-unfolding e = no-unfolding
unfolding-set-erased (unfold b1 b2 b3 _) e = unfold b1 b2 b3 e

unfold-all : unfolding
unfold-all = unfold tt tt ff tt

unfold-head : unfolding
unfold-head = unfold ff tt ff tt

unfold-head-no-lift : unfolding
unfold-head-no-lift = unfold ff ff ff ff

unfold-head-one : unfolding
unfold-head-one = unfold ff tt tt tt

unfold-dampen : (after-head-beta : 𝔹) → unfolding → unfolding
unfold-dampen _ no-unfolding = no-unfolding
unfold-dampen _ (unfold tt b b' e) = unfold tt b b e -- we do not dampen unfolding when unfolding everywhere
unfold-dampen tt (unfold ff b tt e) = no-unfolding
unfold-dampen tt (unfold ff b ff e) = (unfold ff b ff e)
unfold-dampen ff _ = no-unfolding

unfolding-elab : unfolding → unfolding
unfolding-elab no-unfolding = no-unfolding
unfolding-elab (unfold b b' b'' _) = unfold b b' b'' ff

conv-t : Set → Set
conv-t T = ctxt → T → T → 𝔹

{-# TERMINATING #-}

-- main entry point
-- does not assume erased
conv-term : conv-t term
conv-type : conv-t type
conv-kind : conv-t kind

-- assume erased
conv-terme : conv-t term
conv-argse : conv-t (𝕃 term)
conv-typee : conv-t type
conv-kinde : conv-t kind

-- call hnf, then the conv-X-norm functions
conv-term' : conv-t term
conv-type' : conv-t type

hnf : {ed : exprd} → ctxt → (u : unfolding) → ⟦ ed ⟧ → (is-head : 𝔹) → ⟦ ed ⟧

-- assume head normalized inputs
conv-term-norm : conv-t term
conv-type-norm : conv-t type
conv-kind-norm : conv-t kind

hnf-optClass : ctxt → unfolding → optClass → optClass
-- hnf-tk : ctxt → unfolding → tk → tk

-- does not assume erased
conv-tk : conv-t tk
conv-liftingType : conv-t liftingType
conv-optClass : conv-t optClass
-- conv-optType : conv-t optType
conv-tty* : conv-t (𝕃 tty)

-- assume erased
conv-tke : conv-t tk
conv-liftingTypee : conv-t liftingType
conv-optClasse : conv-t optClass
-- -- conv-optTypee : conv-t optType
conv-ttye* : conv-t (𝕃 tty)

conv-ctr-ps : ctxt → var → var → maybe (𝕃 (var × type) × 𝕃 (var × type))
conv-ctr-args : conv-t (var × args)
conv-ctr : conv-t var

conv-term Γ t t' = conv-terme Γ (erase t) (erase t')

conv-terme Γ t t' with decompose-apps t | decompose-apps t'
conv-terme Γ t t' | Var _ x , args | Var _ x' , args' =
     ctxt-eq-rep Γ x x' && conv-argse Γ (erase-args args) (erase-args args')
  || conv-ctr-args Γ (x , args) (x' , args')
  || conv-term' Γ t t'
conv-terme Γ t t' | _ | _ = conv-term' Γ t t'

conv-argse Γ [] [] = tt
conv-argse Γ (a :: args) (a' :: args') = conv-terme Γ a a' && conv-argse Γ args args'
conv-argse Γ _ _ = ff

conv-type Γ t t' = conv-typee Γ (erase t) (erase t')

conv-typee Γ t t' with decompose-tpapps t | decompose-tpapps t'
conv-typee Γ t t' | TpVar _ x , args | TpVar _ x' , args' =
     ctxt-eq-rep Γ x x' && conv-tty* Γ args args'
  || conv-type' Γ t t'
conv-typee Γ t t' | _ | _ = conv-type' Γ t t'

conv-kind Γ k k' = conv-kinde Γ (erase k) (erase k')
conv-kinde Γ k k' = conv-kind-norm Γ (hnf Γ unfold-head k tt) (hnf Γ unfold-head k' tt)

conv-term' Γ t t' = conv-term-norm Γ (hnf Γ unfold-head t tt) (hnf Γ unfold-head t' tt)
conv-type' Γ t t' = conv-type-norm Γ (hnf Γ unfold-head t tt) (hnf Γ unfold-head t' tt)

-- is-head is only used in hnf{TYPE}
hnf{TERM} Γ no-unfolding e hd = erase-term e
hnf{TERM} Γ u (Parens _ t _) hd = hnf Γ u t hd
hnf{TERM} Γ u (App t1 Erased t2) hd = hnf Γ u t1 hd
hnf{TERM} Γ u (App t1 NotErased t2) hd with hnf Γ u t1 hd
hnf{TERM} Γ u (App _ NotErased t2) hd | Lam _ _ _ x _ t1 = hnf Γ (unfold-dampen tt u) (subst Γ t2 x t1) hd
hnf{TERM} Γ u (App _ NotErased t2) hd | t1 = App t1 NotErased (hnf Γ (unfold-dampen ff u) t2 ff)
hnf{TERM} Γ u (Lam _ Erased _ _ _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd with hnf (ctxt-var-decl x Γ) u t hd
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | (App t' NotErased (Var _ x')) with x =string x' && ~ (is-free-in skip-erased x t')
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | (App t' NotErased (Var _ x')) | tt = t' -- eta-contraction
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | (App t' NotErased (Var _ x')) | ff =
  Lam posinfo-gen NotErased posinfo-gen x NoClass (App t' NotErased (Var posinfo-gen x'))
hnf{TERM} Γ u (Lam _ NotErased _ x oc t) hd | t' = Lam posinfo-gen NotErased posinfo-gen x NoClass t'
hnf{TERM} Γ u (Let _ ff (DefTerm _ x _ t) t') hd = hnf Γ u (subst Γ t x t') hd
hnf{TERM} Γ u (Let _ tt (DefTerm _ x _ t) t') hd = hnf Γ u t' hd
hnf{TERM} Γ u (Let _ fe (DefType _ x _ _) t') hd = hnf (ctxt-var-decl x Γ) u t' hd
hnf{TERM} Γ (unfold _ _ _ _) (Var _ x) hd with ctxt-lookup-term-var-def Γ x
hnf{TERM} Γ (unfold _ _ _ _) (Var _ x) hd | nothing = Var posinfo-gen x
hnf{TERM} Γ (unfold ff _ _ e) (Var _ x) hd | just t = erase-if e t -- definitions should be stored in hnf
hnf{TERM} Γ (unfold tt b b' e) (Var _ x) hd | just t = hnf Γ (unfold tt b b' e) t hd -- this might not be fully normalized, only head-normalized
hnf{TERM} Γ u (AppTp t tp) hd = hnf Γ u t hd
hnf{TERM} Γ u (Sigma _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (Epsilon _ _ _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (IotaPair _ t1 t2 _ _) hd = hnf Γ u t1 hd
hnf{TERM} Γ u (IotaProj t _ _) hd = hnf Γ u t hd
hnf{TERM} Γ u (Phi _ eq t₁ t₂ _) hd = hnf Γ u t₂ hd
hnf{TERM} Γ u (Rho _ _ _ t _ t') hd = hnf Γ u t' hd
hnf{TERM} Γ u (Chi _ T t') hd = hnf Γ u t' hd
hnf{TERM} Γ u (Delta _ T t') hd = id-term
hnf{TERM} Γ u (Theta _ u' t ls) hd = hnf Γ u (lterms-to-term u' t ls) hd
hnf{TERM} Γ u (Beta _ _ (SomeTerm t _)) hd = hnf Γ u t hd
hnf{TERM} Γ u (Beta _ _ NoTerm) hd = id-term
hnf{TERM} Γ u (Open _ _ _ _ t) hd = hnf Γ u t hd
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd with decompose-apps (hnf Γ u t hd)
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | tₕ , as with Mu' pi-gen NoTerm (recompose-apps as tₕ) NoType pi-gen (map (λ {(Case _ x as' t) → Case pi-gen x as' (hnf (foldr (λ {(CaseTermArg _ NotErased x) → ctxt-var-decl x; _ → id}) Γ as') (unfold-dampen ff u) t hd)}) (erase-cases cs)) pi-gen | tₕ
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as |  tₒ | Var _ x with foldl (λ {(Case _ xₘ cas tₘ) m? → m? maybe-or (conv-ctr-ps Γ xₘ x ≫=maybe uncurry λ psₘ ps → just (caseArgs-to-lams cas tₘ , length (erase-caseArgs cas) , length ps))}) nothing (erase-cases cs)
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as | tₒ | Var _ x | just (tₓ , nas , nps) with drop nps (erase-args as)
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as | tₒ | Var _ x | just (tₓ , nas , nps) | as' with nas =ℕ length as'
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as | tₒ | Var _ x | just (tₓ , nas , nps) | as' | tt = hnf Γ (unfold-dampen tt u) (recompose-apps (map (TermArg NotErased) as') tₓ) hd
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as | tₒ | Var _ x | just (tₓ , nas , nps) | as' | ff = tₒ
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as | tₒ | Var _ x | nothing = tₒ
hnf{TERM} Γ u (Mu' _ _ t _ _ cs _) hd | _ , as | tₒ | _ = tₒ
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd with decompose-apps (hnf Γ u t hd)
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as with (λ t → Mu pi-gen pi-gen x t NoType pi-gen (map (λ {(Case _ x as' t) → Case pi-gen x as' (hnf (foldr (λ {(CaseTermArg _ NotErased x) → ctxt-var-decl x; _ → id}) Γ as') (unfold-dampen ff u) t hd)}) (erase-cases cs)) pi-gen) | tₕ
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | Var _ x' with foldl (λ {(Case _ xₘ cas tₘ) m? → m? maybe-or (conv-ctr-ps Γ xₘ x' ≫=maybe uncurry λ psₘ ps → just (caseArgs-to-lams cas tₘ , length (erase-caseArgs cas) , length ps))}) nothing (erase-cases cs) | fresh-var "x" (ctxt-binds-var Γ) empty-renamectxt
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | Var _ x' | just (tₓ , nas , nps) | fₓ with drop nps (erase-args as)
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | Var _ x' | just (tₓ , nas , nps) | fₓ | as' with nas =ℕ length as'
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | Var _ x' | just (tₓ , nas , nps) | fₓ | as' | tt = hnf Γ (unfold-dampen tt u) (recompose-apps (map (TermArg NotErased) as') (subst Γ (mlam fₓ $ tₒ $ mvar fₓ) x tₓ)) hd
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | Var _ x' | just (tₓ , nas , nps) | fₓ | as' | ff = tₒ $ recompose-apps (map (TermArg NotErased) as') tₕ
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | Var _ x' | nothing | fₓ = tₒ $ recompose-apps as tₕ
hnf{TERM} Γ u (Mu _ _ x t _ _ cs _) hd | tₕ , as | tₒ | _ = tₒ $ recompose-apps as tₕ
hnf{TERM} Γ u x hd = x

hnf{TYPE} Γ no-unfolding e _ = e
hnf{TYPE} Γ u (TpParens _ t _) hd = hnf Γ u t hd
hnf{TYPE} Γ u (NoSpans t _)  hd = hnf Γ u t hd
hnf{TYPE} Γ (unfold ff b' _ _) (TpVar _ x) ff  = TpVar posinfo-gen x
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) _ with ctxt-lookup-type-var-def Γ x
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) _ | just tp = tp
hnf{TYPE} Γ (unfold b b' _ _) (TpVar _ x) _ | nothing = TpVar posinfo-gen x
hnf{TYPE} Γ u (TpAppt tp t) hd with hnf Γ u tp hd
hnf{TYPE} Γ u (TpAppt _ t) hd  | TpLambda _ _ x _ tp = hnf Γ u (subst Γ t x tp) hd
hnf{TYPE} Γ u (TpAppt _ t) hd | tp = TpAppt tp (erase-if (unfolding-get-erased u) t)
hnf{TYPE} Γ u (TpApp tp tp') hd with hnf Γ u tp hd
hnf{TYPE} Γ u (TpApp _ tp') hd | TpLambda _ _ x _ tp = hnf Γ u (subst Γ tp' x tp) hd
hnf{TYPE} Γ u (TpApp _ tp') hd | tp with hnf Γ u tp' hd
hnf{TYPE} Γ u (TpApp _ _) hd | tp | tp' = try-pull-lift-types tp tp'

  {- given (T1 T2), with T1 and T2 types, see if we can pull a lifting operation from the heads of T1 and T2 to
     surround the entire application.  If not, just return (T1 T2). -}
  where try-pull-lift-types : type → type → type
        try-pull-lift-types tp1 tp2 with decompose-tpapps tp1 | decompose-tpapps (hnf Γ u tp2 tt)
        try-pull-lift-types tp1 tp2 | Lft _ _ X t l , args1 | Lft _ _ X' t' l' , args2 =
          if conv-tty* Γ args1 args2 then
            try-pull-term-in Γ t l (length args1) [] []
          else
            TpApp tp1 tp2

          where try-pull-term-in : ctxt → term → liftingType → ℕ → 𝕃 var → 𝕃 liftingType → type
                try-pull-term-in Γ t (LiftParens _ l _) n vars ltps = try-pull-term-in Γ t l n vars ltps
                try-pull-term-in Γ t (LiftArrow _ l) 0 vars ltps =
                  recompose-tpapps args1
                    (Lft posinfo-gen posinfo-gen X
                      (Lam* vars (hnf Γ no-unfolding (App t NotErased (App* t' (map (λ v → NotErased , mvar v) vars))) tt))
                      (LiftArrow* ltps l))
                try-pull-term-in Γ (Lam _ _ _ x _ t) (LiftArrow l1 l2) (suc n) vars ltps =
                  try-pull-term-in (ctxt-var-decl x Γ) t l2 n (x :: vars) (l1 :: ltps)
                try-pull-term-in Γ t (LiftArrow l1 l2) (suc n) vars ltps =
                  let x = fresh-var "x" (ctxt-binds-var Γ) empty-renamectxt in
                    try-pull-term-in (ctxt-var-decl x Γ) (App t NotErased (mvar x)) l2 n (x :: vars) (l1 :: ltps)
                try-pull-term-in Γ t l n vars ltps = TpApp tp1 tp2

        try-pull-lift-types tp1 tp2 | _ | _ = TpApp tp1 tp2

hnf{TYPE} Γ u@(unfold all? _ _ _) (Abs _ b _ x atk tp) _
  with Abs posinfo-gen b posinfo-gen x (hnf Γ u atk ff) (hnf (ctxt-var-decl x Γ) u tp ff)
hnf{TYPE} Γ u (Abs _ b _ x atk tp) _ | tp' with to-abs tp'
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | just (mk-abs b x atk tt {- x is free in tp -} tp) = Abs posinfo-gen b posinfo-gen x atk tp
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | just (mk-abs b x (Tkk k) ff tp) = Abs posinfo-gen b posinfo-gen x (Tkk k) tp
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | just (mk-abs b x (Tkt tp') ff tp) = TpArrow tp' b tp
hnf{TYPE} Γ u (Abs _ _ _ _ _ _) _ | tp'' | nothing = tp''
hnf{TYPE} Γ u (TpArrow tp1 arrowtype tp2) _ = TpArrow (hnf Γ u tp1 ff) arrowtype (hnf Γ u tp2 ff)
hnf{TYPE} Γ u (TpEq _ t1 t2 _) _
  = TpEq posinfo-gen (erase t1) (erase t2) posinfo-gen
hnf{TYPE} Γ u (TpLambda _ _ x atk tp) _ =
  TpLambda posinfo-gen posinfo-gen x (hnf Γ u atk ff) (hnf (ctxt-var-decl x Γ) u tp ff)
hnf{TYPE} Γ u @ (unfold b tt b'' b''') (Lft _ _ y t l) _ =
 let t = hnf (ctxt-var-decl y Γ) u t tt in
   do-lift Γ (Lft posinfo-gen posinfo-gen y t l) y l (λ t → hnf{TERM} Γ unfold-head t ff) t
-- We need hnf{TYPE} to preserve types' well-kindedness, so we must check if
-- the defined term is being checked against a type and use chi to make sure
-- that wherever it is substituted, the term will have the same directionality.
-- For example, "[e ◂ {a ≃ b} = ρ e' - β] - A (ρ e - a)", would otherwise
-- head-normalize to A (ρ (ρ e' - β) - a), which wouldn't check because it
-- synthesizes the type of "ρ e' - β" (which in turn fails to synthesize the type
-- of "β"). Similar issues could happen if the term is synthesized and it uses a ρ,
-- and then substitutes into a place where it would be checked against a type.
hnf{TYPE} Γ u (TpLet _ (DefTerm _ x ot t) T) hd =
  hnf Γ u (subst Γ (Chi posinfo-gen ot t) x T) hd
-- Note that if we ever remove the requirement that type-lambdas have a classifier,
-- we would need to introduce a type-level chi to do the same thing as above.
-- Currently, synthesizing or checking a type should not make a difference.
hnf{TYPE} Γ u (TpLet _ (DefType _ x k T) T') hd = hnf Γ u (subst Γ T x T') hd
hnf{TYPE} Γ u x _ = x

hnf{KIND} Γ no-unfolding e hd = e
hnf{KIND} Γ u (KndParens _ k _) hd = hnf Γ u k hd
hnf{KIND} Γ u@(unfold a _ _ _) (KndVar _ x ys) hd with ctxt-lookup-kind-var-def Γ x
... | nothing = KndVar posinfo-gen x ys
... | just (zs , k) with a | subst-params-args Γ zs ys k
... | tt | (kᵢ , [] , []) = hnf Γ u kᵢ hd
... | ff | (kᵢ , [] , []) = kᵢ
... | tf | (kᵢ , ps , as) = KndVar pi-gen x ys

hnf{KIND} Γ u@(unfold a _ _ _) (KndPi _ _ x atk k) hd =
  if is-free-in check-erased x k then
    KndPi posinfo-gen posinfo-gen x atk (if a then hnf (ctxt-var-decl x Γ) u k ff else k)
  else
    tk-arrow-kind atk (if a then hnf Γ u k ff else k)
hnf{KIND} Γ u@(unfold tt _ _ _) (KndArrow k k') hd =
  KndArrow (hnf Γ u k ff) (hnf Γ u k' ff)
hnf{KIND} Γ u@(unfold tt _ _ _) (KndTpArrow T k) hd =
  KndTpArrow (hnf Γ u T ff) (hnf Γ u k ff)
hnf{KIND} Γ u x hd = x

hnf{LIFTINGTYPE} Γ u x hd = x
hnf{TK} Γ u (Tkk k) _ = Tkk (hnf Γ u k tt)
hnf{TK} Γ u (Tkt tp) _ = Tkt (hnf Γ u tp ff)
hnf{QUALIF} Γ u x hd = x
hnf{ARG} Γ u x hd = x

hnf-optClass Γ u NoClass = NoClass
hnf-optClass Γ u (SomeClass atk) = SomeClass (hnf Γ u atk ff)

{- this function reduces a term to "head-applicative" normal form,
   which avoids unfolding definitions if they would lead to a top-level
   lambda-abstraction or top-level application headed by a variable for which we
   do not have a (global) definition. -}
{-# TERMINATING #-}
hanf : ctxt → (e : 𝔹) → term → term
hanf Γ e t with hnf Γ (unfolding-set-erased unfold-head-one e) t tt
hanf Γ e t | t' with decompose-apps t'
hanf Γ e t | t' | (Var _ x) , [] = t'
hanf Γ e t | t' | (Var _ x) , args with ctxt-lookup-term-var-def Γ x
hanf Γ e t | t' | (Var _ x) , args | nothing = t'
hanf Γ e t | t' | (Var _ x) , args | just _ = hanf Γ e t'
hanf Γ e t | t' | h , args {- h could be a Lambda if args is [] -} = t

-- unfold across the term-type barrier
hnf-term-type : ctxt → (e : 𝔹) → type → type
hnf-term-type Γ e (TpEq _ t1 t2 _) = TpEq posinfo-gen (hanf Γ e t1) (hanf Γ e t2) posinfo-gen
hnf-term-type Γ e (TpAppt tp t) = hnf Γ (unfolding-set-erased unfold-head e) (TpAppt tp (hanf Γ e t)) tt
hnf-term-type Γ e tp = hnf Γ unfold-head tp tt

conv-cases : conv-t cases
conv-cases Γ cs₁ cs₂ = isJust $ foldl (λ c₂ x → x ≫=maybe λ cs₁ → conv-cases' Γ cs₁ c₂) (just cs₁) cs₂ where
  conv-cases' : ctxt → cases → case → maybe cases
  conv-cases' Γ [] (Case _ x₂ as₂ t₂) = nothing
  conv-cases' Γ (c₁ @ (Case _ x₁ as₁ t₁) :: cs₁) c₂ @ (Case _ x₂ as₂ t₂) with conv-ctr Γ x₁ x₂
  ...| ff = conv-cases' Γ cs₁ c₂ ≫=maybe λ cs₁ → just (c₁ :: cs₁)
  ...| tt = maybe-if (length as₂ =ℕ length as₁ && conv-term Γ (snd (expand-case c₁)) (snd (expand-case (Case pi-gen x₂ as₂ t₂)))) ≫maybe just cs₁

ctxt-term-udef : posinfo → defScope → opacity → var → term → ctxt → ctxt

conv-term-norm Γ (Var _ x) (Var _ x') = ctxt-eq-rep Γ x x' || conv-ctr Γ x x'
-- hnf implements erasure for terms, so we can ignore some subterms for App and Lam cases below
conv-term-norm Γ (App t1 m t2) (App t1' m' t2') = conv-term-norm Γ t1 t1' && conv-term Γ t2 t2'
conv-term-norm Γ (Lam _ l _ x oc t) (Lam _ l' _ x' oc' t') = conv-term (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) t t'
conv-term-norm Γ (Hole _) _ = tt
conv-term-norm Γ _ (Hole _) = tt
conv-term-norm Γ (Mu _ _ x₁ t₁ _ _ cs₁ _) (Mu _ _ x₂ t₂ _ _ cs₂ _) =
  let --fₓ = fresh-var x₂ (ctxt-binds-var Γ) empty-renamectxt
      --μ = mlam fₓ $ Mu pi-gen pi-gen x₂ (mvar fₓ) NoType pi-gen cs₂ pi-gen
      Γ' = ctxt-rename x₁ x₂ $ ctxt-var-decl x₂ Γ in --ctxt-term-udef pi-gen localScope OpacTrans x₂ μ Γ in
  conv-term Γ t₁ t₂ && conv-cases Γ' cs₁ cs₂ -- (subst-cases Γ' id-term (mu-name-cast x₁) cs₁) (subst-cases Γ' id-term (mu-name-cast x₂) cs₂)
conv-term-norm Γ (Mu' _ _ t₁ _ _ cs₁ _) (Mu' _ _ t₂ _ _ cs₂ _) = conv-term Γ t₁ t₂ && conv-cases Γ cs₁ cs₂
{- it can happen that a term is equal to a lambda abstraction in head-normal form,
   if that lambda-abstraction would eta-contract following some further beta-reductions.
   We implement this here by implicitly eta-expanding the variable and continuing
   the comparison.

   A simple example is

       λ v . t ((λ a . a) v) ≃ t
 -}
conv-term-norm Γ (Lam _ l _ x oc t) t' =
  let x' = fresh-var x (ctxt-binds-var Γ) empty-renamectxt in
  conv-term (ctxt-rename x x' Γ) t (App t' NotErased (Var posinfo-gen x'))
conv-term-norm Γ t' (Lam _ l _ x oc t) =
  let x' = fresh-var x (ctxt-binds-var Γ) empty-renamectxt in
  conv-term (ctxt-rename x x' Γ) (App t' NotErased (Var posinfo-gen x')) t
conv-term-norm Γ _ _ = ff

conv-type-norm Γ (TpVar _ x) (TpVar _ x') = ctxt-eq-rep Γ x x'
conv-type-norm Γ (TpApp t1 t2) (TpApp t1' t2') = conv-type-norm Γ t1 t1' && conv-type Γ t2 t2'
conv-type-norm Γ (TpAppt t1 t2) (TpAppt t1' t2') = conv-type-norm Γ t1 t1' && conv-term Γ t2 t2'
conv-type-norm Γ (Abs _ b _ x atk tp) (Abs _ b' _ x' atk' tp') =
  eq-maybeErased b b' && conv-tk Γ atk atk' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ (TpArrow tp1 a1 tp2) (TpArrow tp1' a2  tp2') = eq-maybeErased a1 a2 && conv-type Γ tp1 tp1' && conv-type Γ tp2 tp2'
conv-type-norm Γ (TpArrow tp1 a tp2) (Abs _ b _ _ (Tkt tp1') tp2') = eq-maybeErased a b && conv-type Γ tp1 tp1' && conv-type Γ tp2 tp2'
conv-type-norm Γ (Abs _ b _ _ (Tkt tp1) tp2) (TpArrow tp1' a tp2') = eq-maybeErased a b && conv-type Γ tp1 tp1' && conv-type Γ tp2 tp2'
conv-type-norm Γ (Iota _ _ x m tp) (Iota _ _ x' m' tp') =
  conv-type Γ m m' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
conv-type-norm Γ (TpEq _ t1 t2 _) (TpEq _ t1' t2' _) = conv-term Γ t1 t1' && conv-term Γ t2 t2'
conv-type-norm Γ (Lft _ _ x t l) (Lft _ _ x' t' l') =
  conv-liftingType Γ l l' && conv-term (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) t t'
conv-type-norm Γ (TpLambda _ _ x atk tp) (TpLambda _ _ x' atk' tp') =
  conv-tk Γ atk atk' && conv-type (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) tp tp'
{-conv-type-norm Γ (TpLambda _ _ x atk tp) tp' =
  let x' = fresh-var x (ctxt-binds-var Γ) empty-renamectxt
      tp'' = if tk-is-type atk then TpAppt tp' (mvar x') else TpApp tp' (mtpvar x') in
  conv-type-norm (ctxt-rename x x' Γ) tp tp''
conv-type-norm Γ tp' (TpLambda _ _ x atk tp) =
  let x' = fresh-var x (ctxt-binds-var Γ) empty-renamectxt
      tp'' = if tk-is-type atk then TpAppt tp' (mvar x') else TpApp tp' (mtpvar x') in
  conv-type-norm (ctxt-rename x x' Γ) tp'' tp-}
conv-type-norm Γ _ _ = ff

{- even though hnf turns Pi-kinds where the variable is not free in the body into arrow kinds,
   we still need to check off-cases, because normalizing the body of a kind could cause the
   bound variable to be erased (hence allowing it to match an arrow kind). -}
conv-kind-norm Γ (KndArrow k k₁) (KndArrow k' k'') = conv-kind Γ k k' && conv-kind Γ k₁ k''
conv-kind-norm Γ (KndArrow k k₁) (KndPi _ _ x (Tkk k') k'') = conv-kind Γ k k' && conv-kind Γ k₁ k''
conv-kind-norm Γ (KndArrow k k₁) _ = ff
conv-kind-norm Γ (KndPi _ _ x (Tkk k₁) k) (KndArrow k' k'') = conv-kind Γ k₁ k' && conv-kind Γ k k''
conv-kind-norm Γ (KndPi _ _ x atk k) (KndPi _ _ x' atk' k'') =
    conv-tk Γ atk atk' && conv-kind (ctxt-rename x x' (ctxt-var-decl-if x' Γ)) k k''
conv-kind-norm Γ (KndPi _ _ x (Tkt t) k) (KndTpArrow t' k'') = conv-type Γ t t' && conv-kind Γ k k''
conv-kind-norm Γ (KndPi _ _ x (Tkt t) k) _ = ff
conv-kind-norm Γ (KndPi _ _ x (Tkk k') k) _ = ff
conv-kind-norm Γ (KndTpArrow t k) (KndTpArrow t' k') = conv-type Γ t t' && conv-kind Γ k k'
conv-kind-norm Γ (KndTpArrow t k) (KndPi _ _ x (Tkt t') k') = conv-type Γ t t' && conv-kind Γ k k'
conv-kind-norm Γ (KndTpArrow t k) _ = ff
conv-kind-norm Γ (Star x) (Star x') = tt
conv-kind-norm Γ (Star x) _ = ff
conv-kind-norm Γ _ _ = ff -- should not happen, since the kinds are in hnf

conv-tk Γ tk tk' = conv-tke Γ (erase-tk tk) (erase-tk tk')

conv-tke Γ (Tkk k) (Tkk k') = conv-kind Γ k k'
conv-tke Γ (Tkt t) (Tkt t') = conv-type Γ t t'
conv-tke Γ _ _ = ff

conv-liftingType Γ l l' = conv-liftingTypee Γ (erase l) (erase l')
conv-liftingTypee Γ l l' = conv-kind Γ (liftingType-to-kind l) (liftingType-to-kind l')

conv-optClass Γ NoClass NoClass = tt
conv-optClass Γ (SomeClass x) (SomeClass x') = conv-tk Γ (erase-tk x) (erase-tk x')
conv-optClass Γ _ _ = ff

conv-optClasse Γ NoClass NoClass = tt
conv-optClasse Γ (SomeClass x) (SomeClass x') = conv-tk Γ x x'
conv-optClasse Γ _ _ = ff

conv-tty* Γ [] [] = tt
conv-tty* Γ (tterm t :: args) (tterm t' :: args')
  = conv-term Γ (erase t) (erase t') && conv-tty* Γ args args'
conv-tty* Γ (ttype t :: args) (ttype t' :: args')
  = conv-type Γ (erase t) (erase t') && conv-tty* Γ args args'
conv-tty* Γ _ _ = ff

conv-ttye* Γ [] [] = tt
conv-ttye* Γ (tterm t :: args) (tterm t' :: args') = conv-term Γ t t' && conv-ttye* Γ args args'
conv-ttye* Γ (ttype t :: args) (ttype t' :: args') = conv-type Γ t t' && conv-ttye* Γ args args'
conv-ttye* Γ _ _ = ff

conv-ctr Γ x₁ x₂ = conv-ctr-args Γ (x₁ , []) (x₂ , [])

conv-ctr-ps Γ x₁ x₂ with env-lookup Γ x₁ | env-lookup Γ x₂
...| just (ctr-def ps₁ T₁ n₁ i₁ a₁ , _) | just (ctr-def ps₂ T₂ n₂ i₂ a₂ , _) =
  maybe-if (n₁ =ℕ n₂ && i₁ =ℕ i₂ && a₁ =ℕ a₂) ≫maybe
  just (erase-params ps₁ , erase-params ps₂)
...| _ | _ = nothing

conv-ctr-args Γ (x₁ , as₁) (x₂ , as₂) =
  maybe-else' (conv-ctr-ps Γ x₁ x₂) ff $ uncurry λ ps₁ ps₂ →
  conv-argse Γ (drop (length ps₁) $ erase-args as₁) (drop (length ps₂) $ erase-args as₂)

hnf-qualif-term : ctxt → term → term
hnf-qualif-term Γ t = hnf Γ unfold-head (qualif-term Γ t) tt

hnf-qualif-type : ctxt → type → type
hnf-qualif-type Γ t = hnf Γ unfold-head (qualif-type Γ t) tt

hnf-qualif-kind : ctxt → kind → kind
hnf-qualif-kind Γ t = hnf Γ unfold-head (qualif-kind Γ t) tt

{-# TERMINATING #-}
inconv : ctxt → term → term → 𝔹
inconv Γ t₁ t₂ = inconv-lams empty-renamectxt empty-renamectxt
                   (hnf Γ unfold-all t₁ tt) (hnf Γ unfold-all t₂ tt)
  where
  fresh : var → renamectxt → renamectxt → var
  fresh x ρ₁ = fresh-var x (λ x → ctxt-binds-var Γ x || renamectxt-in-field ρ₁ x)

  make-subst : renamectxt → renamectxt → 𝕃 var → 𝕃 var → term → term → (renamectxt × renamectxt × term × term)
  make-subst ρ₁ ρ₂ [] [] t₁ t₂ = ρ₁ , ρ₂ , t₁ , t₂ -- subst-renamectxt Γ ρ₁ t₁ , subst-renamectxt Γ ρ₂ t₂
  make-subst ρ₁ ρ₂ (x₁ :: xs₁) [] t₁ t₂ =
    let x = fresh x₁ ρ₁ ρ₂ in
    make-subst (renamectxt-insert ρ₁ x₁ x) (renamectxt-insert ρ₂ x x) xs₁ [] t₁ (mapp t₂ $ mvar x)
  make-subst ρ₁ ρ₂ [] (x₂ :: xs₂) t₁ t₂ =
    let x = fresh x₂ ρ₁ ρ₂ in
    make-subst (renamectxt-insert ρ₁ x x) (renamectxt-insert ρ₂ x₂ x) [] xs₂ (mapp t₁ $ mvar x) t₂
  make-subst ρ₁ ρ₂ (x₁ :: xs₁) (x₂ :: xs₂) t₁ t₂ =
    let x = fresh x₁ ρ₁ ρ₂ in
    make-subst (renamectxt-insert ρ₁ x₁ x) (renamectxt-insert ρ₂ x₂ x) xs₁ xs₂ t₁ t₂

  inconv-lams : renamectxt → renamectxt → term → term → 𝔹
  inconv-apps : renamectxt → renamectxt → var → var → args → args → 𝔹
  inconv-ctrs : renamectxt → renamectxt → var → var → args → args → 𝔹
  inconv-mu : renamectxt → renamectxt → maybe (var × var) → cases → cases → 𝔹
  inconv-args : renamectxt → renamectxt → args → args → 𝔹

  inconv-args ρ₁ ρ₂ a₁ a₂ =
    let a₁ = erase-args a₁; a₂ = erase-args a₂ in
    ~  length a₁ =ℕ length a₂
    || list-any (uncurry $ inconv-lams ρ₁ ρ₂) (zip a₁ a₂)

  inconv-lams ρ₁ ρ₂ t₁ t₂ =
    elim-pair (decompose-lams t₁) λ l₁ b₁ →
    elim-pair (decompose-lams t₂) λ l₂ b₂ →
    elim-pair (make-subst ρ₁ ρ₂ l₁ l₂ b₁ b₂) λ ρ₁ ρ₂b₁₂ →
    elim-pair ρ₂b₁₂ λ ρ₂ b₁₂ →
    elim-pair b₁₂ λ b₁ b₂ →
    case (decompose-apps b₁ , decompose-apps b₂) of uncurry λ where
      (Var _ x₁ , a₁) (Var _ x₂ , a₂) →
        inconv-apps ρ₁ ρ₂ x₁ x₂ a₁ a₂ || inconv-ctrs ρ₁ ρ₂ x₁ x₂ a₁ a₂
      (Mu _ _ x₁ t₁ _ _ ms₁ _ , a₁) (Mu _ _ x₂ t₂ _ _ ms₂ _ , a₂) →
        inconv-mu ρ₁ ρ₂ (just $ x₁ , x₂) ms₁ ms₂ ||
        inconv-lams ρ₁ ρ₂ t₁ t₂ || inconv-args ρ₁ ρ₂ a₁ a₂
      (Mu' _ _ t₁ _ _ ms₁ _ , a₁) (Mu' _ _ t₂ _ _ ms₂ _ , a₂) →
        inconv-mu ρ₁ ρ₂ nothing ms₁ ms₂ ||
        inconv-lams ρ₁ ρ₂ t₁ t₂ || inconv-args ρ₁ ρ₂ a₁ a₂
      _ _ → ff

  inconv-apps ρ₁ ρ₂ x₁ x₂ a₁ a₂ =
    maybe-else' (renamectxt-lookup ρ₁ x₁) ff λ x₁ →
    maybe-else' (renamectxt-lookup ρ₂ x₂) ff λ x₂ →
    ~ x₁ =string x₂
    || inconv-args ρ₁ ρ₂ a₁ a₂

  inconv-ctrs ρ₁ ρ₂ x₁ x₂ as₁ as₂ with env-lookup Γ x₁ | env-lookup Γ x₂
  ...| just (ctr-def ps₁ _ n₁ i₁ a₁ , _) | just (ctr-def ps₂ _ n₂ i₂ a₂ , _) =
    let ps₁ = erase-params ps₁; ps₂ = erase-params ps₂
        as₁ = erase-args   as₁; as₂ = erase-args   as₂ in
    length as₁ ≤ length ps₁ + a₁ && -- Could use of "≤" here conflict with η-equality?
    length as₂ ≤ length ps₂ + a₂ &&
    (~ n₁ =ℕ n₂ ||
    ~ i₁ =ℕ i₂ ||
    ~ a₁ =ℕ a₂ ||
    ~ length as₁ + length ps₂ =ℕ length as₂ + length ps₁ ||
    -- ^ as₁ ∸ ps₁ ≠ as₂ ∸ ps₂, + ps₁ + ps₂ to both sides ^
    list-any (uncurry $ inconv-lams ρ₁ ρ₂)
      (zip (drop (length ps₁) as₁) (drop (length ps₂) as₂)))
  ...| _ | _ = ff

  inconv-mu ρ₁ ρ₂ xs? ms₁ ms₂ =
    ~ length ms₁ =ℕ length ms₂ ||
    maybe-else ff id
      (foldr {B = maybe 𝔹} (λ c b? → b? ≫=maybe λ b → inconv-case c ≫=maybe λ b' → just (b || b')) (just ff) ms₁)
    where
    matching-case : case → maybe (term × ℕ × ℕ)
    matching-case (Case _ x _ _) = foldl (λ where
      (Case _ xₘ cas tₘ) m? → m? maybe-or
        (conv-ctr-ps Γ xₘ x ≫=maybe uncurry λ psₘ ps →
         just (caseArgs-to-lams cas tₘ , length cas , length ps)))
      nothing ms₂

    inconv-case : case → maybe 𝔹
    inconv-case c₁ @ (Case _ x cas₁ t₁) =
      matching-case c₁ ≫=maybe λ c₂ →
      just (inconv-lams ρ₁ ρ₂ (caseArgs-to-lams cas₁ t₁) (fst c₂))

ctxt-params-def : params → ctxt → ctxt
ctxt-params-def ps Γ@(mk-ctxt (fn , mn , _ , q) syms i symb-occs Δ) =
  mk-ctxt (fn , mn , ps' , q) syms i symb-occs Δ
  where ps' = qualif-params Γ ps

ctxt-kind-def : posinfo → var → params → kind → ctxt → ctxt
ctxt-kind-def pi v ps2 k Γ@(mk-ctxt (fn , mn , ps1 , q) (syms , mn-fn) i symb-occs Δ) = mk-ctxt
  (fn , mn , ps1 , qualif-insert-params q (mn # v) v ps1)
  (trie-insert-append2 syms fn mn v , mn-fn)
  (trie-insert i (mn # v) (kind-def (ps1 ++ qualif-params Γ ps2) k' , fn , pi))
  symb-occs Δ
  where
  k' = hnf Γ unfold-head (qualif-kind Γ k) tt

ctxt-datatype-decl : var → var → args → ctxt → ctxt
ctxt-datatype-decl vₒ vᵣ as Γ@(mk-ctxt mod ss is os (Δ , μ' , μ)) =
  mk-ctxt mod ss is os $ Δ , trie-insert μ' (mu-Type/ vᵣ) (vₒ , mu-isType/ vₒ , as) , μ

-- assumption: classifier (i.e. kind) already qualified
ctxt-datatype-def : posinfo → var → params → kind → kind → ctrs → ctxt → ctxt
ctxt-datatype-def pi v psᵢ kᵢ k cs Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i os (Δ , μ' , μ)) =
  let v' = mn # v
      q' = qualif-insert-params q v' v ps in
  mk-ctxt (fn , mn , ps , q')
    (trie-insert-append2 syms fn mn v , mn-fn)
    (trie-insert i v' (type-def (just ps) OpacTrans nothing (abs-expand-kind psᵢ k) , fn , pi)) os
    (trie-insert Δ v' (ps ++ psᵢ , kᵢ , k , cs) , μ' , trie-insert μ (data-Is/ v') v')

-- assumption: classifier (i.e. kind) already qualified
ctxt-type-def : posinfo → defScope → opacity → var → maybe type → kind → ctxt → ctxt
ctxt-type-def pi s op v t k Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs Δ) = mk-ctxt
  (fn , mn , ps , q')
  ((if (s iff localScope) then syms else trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (type-def (def-params s ps) op t' k , fn , pi))
  symb-occs Δ
  where
  t' = maybe-map (λ t → hnf Γ unfold-head (qualif-type Γ t) tt) t
  v' = if s iff localScope then pi % v else mn # v
  q' = qualif-insert-params q v' v (if s iff localScope then [] else ps)

ctxt-ctr-def : posinfo → var → type → params → (ctrs-length ctr-index : ℕ) → ctxt → ctxt
ctxt-ctr-def pi c t ps' n i Γ@(mk-ctxt mod@(fn , mn , ps , q) (syms , mn-fn) is symb-occs Δ) = mk-ctxt
  (fn , mn , ps , q')
  ((trie-insert-append2 syms fn mn c) , mn-fn)
  (trie-insert is c' (ctr-def (ps ++ ps') t n i (unerased-arrows t) , fn , pi))
  symb-occs Δ
  where
  c' = mn # c
  q' = qualif-insert-params q c' c ps

-- assumption: classifier (i.e. type) already qualified
ctxt-term-def : posinfo → defScope → opacity → var → maybe term → type → ctxt → ctxt
ctxt-term-def pi s op v t tp Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs Δ) = mk-ctxt
  (fn , mn , ps , q')
  ((if (s iff localScope) then syms else trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (term-def (def-params s ps) op t' tp , fn , pi))
  symb-occs Δ
  where
  t' = maybe-map (λ t → hnf Γ unfold-head (qualif-term Γ t) tt) t
  v' = if s iff localScope then pi % v else mn # v
  q' = qualif-insert-params q v' v (if s iff localScope then [] else ps)

ctxt-term-udef pi s op v t Γ@(mk-ctxt (fn , mn , ps , q) (syms , mn-fn) i symb-occs Δ) = mk-ctxt
  (fn , mn , ps , qualif-insert-params q v' v (if s iff localScope then [] else ps))
  ((if (s iff localScope) then syms else trie-insert-append2 syms fn mn v) , mn-fn)
  (trie-insert i v' (term-udef (def-params s ps) op t' , fn , pi))
  symb-occs Δ
  where
  t' = hnf Γ unfold-head (qualif-term Γ t) tt
  v' = if s iff localScope then pi % v else mn # v

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
-- | In this module we show that the substream relation is transitive.

open import Streams
open import Relation.Binary.PropositionalEquality as P
open import Data.Product
open import Function.Equivalence

mutual
  record F : Set where
    coinductive
    field out : Fμ

  data Fμ : Set where
    pres : F → Fμ
    drop : Fμ → Fμ

open F public

μfilter : ∀{A} → Fμ → Stream A → Stream A
filter : ∀{A} → F → Stream A → Stream A

filter x = μfilter (out x)

hd (μfilter (pres x) s) = hd s
tl (μfilter (pres x) s) = filter x (tl s)
μfilter (drop u) s = μfilter u (tl s)

comp : F → F → F
μcomp : Fμ → Fμ → Fμ

out (comp x y) = μcomp (out x) (out y)

μcomp (pres x) (pres y) = pres (comp x y)
μcomp (pres x) (drop v) = drop (μcomp (out x) v)
μcomp (drop u) v        = drop (μcomp u v)

_•_ : F → F → F
y • x = comp x y

_•μ_ : Fμ → Fμ → Fμ
v •μ u = μcomp u v

filter-comp : ∀{A} → ∀ x y (s : Stream A) →
              filter (y • x) s ~ filter y (filter x s)
μfilter-comp : ∀{A} → ∀ u v (s : Stream A) →
               μfilter (v •μ u) s ~ μfilter v (μfilter u s)

filter-comp x y s = μfilter-comp (out x) (out y) s

hd~(μfilter-comp (pres x) (pres y) s) = refl
tl~(μfilter-comp (pres x) (pres y) s) = filter-comp x y (tl s)
μfilter-comp (pres x) (drop v) s = μfilter-comp (out x) v (tl s)
-- The following cases are just the same, they need to be there for Agda to
-- reduce the definition of μcomp
μfilter-comp (drop u) (pres x) s = μfilter-comp u (pres x) (tl s)
μfilter-comp (drop u) (drop v) s = μfilter-comp u (drop v) (tl s)

_≤[_]_ : ∀{A} → Stream A → F → Stream A → Set
s ≤[ x ] t = s ~ filter x t

_≤μ[_]_ : ∀{A} → Stream A → Fμ → Stream A → Set
s ≤μ[ x ] t = s ~ μfilter x t

mutual
  record _≤_ {A : Set} (s t : Stream A) : Set where
    coinductive
    field out≤ : s ≤μ t

  data _≤μ_ {A : Set} (s t : Stream A) : Set where
    ma : hd s ≡ hd t → (tl s) ≤ (tl t) → s ≤μ t
    sk : s ≤μ (tl t) → s ≤μ t

open _≤_ public

witness : ∀{A} {s t : Stream A} → s ≤ t → F
xwitness : ∀{A} {s t : Stream A} → s ≤μ t → Fμ

out (witness p) = xwitness (out≤ p)

xwitness (ma _ t≤) = pres (witness t≤)
xwitness (sk u)    = drop (xwitness u)

impl₁ : ∀{A} {s t : Stream A} → (p : s ≤ t) → s ≤[ witness p ] t
ximpl₁ : ∀{A} {s t : Stream A} → (p : s ≤μ t) → s ≤μ[ xwitness p ] t

impl₁ {A} {s} {t} p = ximpl₁ (out≤ p)

hd~ (ximpl₁ (ma h≡ t≤)) = h≡
tl~ (ximpl₁ (ma h≡ t≤)) = impl₁ t≤
ximpl₁ (sk q) = ximpl₁ q

impl₂ : ∀{A} {s t : Stream A} (x : F) → s ≤[ x ] t → s ≤ t
ximpl₂ : ∀{A} {s t : Stream A} (u : Fμ) → s ≤μ[ u ] t → s ≤μ t

out≤ (impl₂ x p) = ximpl₂ (out x) p

ximpl₂ (pres x) p = ma (hd~ p) (impl₂ x (tl~ p))
ximpl₂ (drop u) p = sk (ximpl₂ u p)

≤⇔filter-≤ : ∀{A} (s t : Stream A) →
             s ≤ t ⇔ ∃ λ p → s ≤[ p ] t
≤⇔filter-≤ s t = equivalence (λ x → witness x , impl₁ x)
                             (λ {(x , p) → impl₂ x p})

filter-resp~ : ∀{A} {s t : Stream A} (x : F) →
               s ~ t → filter x s ~ filter x t
μfilter-resp~ : ∀{A} {s t : Stream A} (u : Fμ) →
                s ~ t → μfilter u s ~ μfilter u t

filter-resp~ x p = μfilter-resp~ (out x) p
hd~ (μfilter-resp~ (pres x) p) = hd~ p
tl~ (μfilter-resp~ (pres x) p) = filter-resp~ x (tl~ p)
μfilter-resp~ (drop u) p = μfilter-resp~ u (tl~ p)

{-
We prove transitivity of the witnessed substream relation by
r ~ filter x s
  ~ filter x (filter y t)
  ~ filter (comp x y) t

-}
≤-filter-trans : ∀{A} {r s t : Stream A} {x y} →
                 r ≤[ x ] s → s ≤[ y ] t → r ≤[ x • y ] t
≤-filter-trans {x = x} {y} p q =
  ~trans p (
    ~trans (filter-resp~ x q)
           (~sym (filter-comp y x _)))

≤-trans : ∀{A} {r s t : Stream A} →
          r ≤ s → s ≤ t → r ≤ t
≤-trans p q = impl₂ (witness p • witness q)
                    (≤-filter-trans {x = witness p}
                                    {y = witness q}
                                    (impl₁ p)
                                    (impl₁ q)
                    )

-- lem : ∀{A} {s t : Stream A} → hd s ≡ hd t → tl s ≤ tl t → t ≤μ tl s → tl t ≤μ tl s
-- lem s0≡t0 t'≤s' (ma t0≡s1 t'≤s'') with out≤ t'≤s'
-- lem s0≡t0 t'≤s' (ma t0≡s1 t'≤s'') | ma s1≡t1 s''≤t'' = ma (P.sym s1≡t1) {!!}
-- lem s0≡t0 t'≤s' (ma t0≡s1 t'≤s'') | sk p = {!!}
-- lem {s = s} s0≡t0 s'≤t' (sk p) = {!!}

-- ≤-antisym : ∀{A} {s t : Stream A} →
--             s ≤ t → t ≤ s → s ~ t
-- ≤μ-antisym : ∀{A} {s t : Stream A} →
--             s ≤μ t → t ≤μ s → s ~ t
-- ≤-antisym p q = ≤μ-antisym (out≤ p) (out≤ q)
-- hd~ (≤μ-antisym (ma hs≡ht ts≤tt) _) = hs≡ht
-- tl~ (≤μ-antisym (ma hs≡ht ts≤tt) (ma ht≡hs tt≤ts)) = ≤-antisym ts≤tt tt≤ts
-- tl~ (≤μ-antisym (ma hs≡ht ts≤tt) (sk q)) = ≤μ-antisym (out≤ ts≤tt) {!!}
-- ≤μ-antisym (sk p) q = {!!}

{-
------------------
--- Try to convince Agda that x = zip(ev(x), odd(x)) is well-defined.

even : ∀{A} → Stream A → Stream A
hd (even s) = hd s
tl (even s) = even (tl (tl s))

odd : ∀{A} → Stream A → Stream A
odd s = even (tl s)

zips : ∀{A} → Stream A → Stream A → Stream A
hd (zips s t) = hd s
tl (zips s t) = zips t (tl s)

open import Data.Nat

foo : Stream ℕ
hd foo = 0
tl foo = zips (even foo) (odd foo)

-- H : Stream ℕ → Stream ℕ → Stream ℕ
-- f : ℕ → Stream ℕ → Stream ℕ → Stream ℕ

-- H s t = f (hd t) s t

-- hd (f zero s t) = hd s
-- tl (f zero s t) = H s (tl t)
-- f (suc n) s t = f n (tl s) t
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox