-- Copyright 2020 INP Toulouse. -- Authors : Mathieu Montin. -- This version of CCSLNaturals is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. -- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only -- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. -- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the -- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there- -- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged -- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to -- be ensured and, more generally, to use and operate it in the same conditions as regards security. -- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms. open import Data.Nat hiding (compare) open import Data.Nat.Induction open import Data.Nat.Properties open import Relation.Binary hiding (Decidable) open import Relation.Binary.PropositionalEquality open import Relation.Unary hiding (_⇒_) open import Relation.Nullary open import Data.Product open import Function open import Data.Empty open import Data.Sum renaming (swap to swap⊎) open import Relation.Nullary.Negation open import Induction.WellFounded module CCSLNaturals where precedent : ∀ {ℓ} {P : Pred ℕ ℓ} → Decidable P → (j : ∃ P) → (∀ {x} → x < proj₁ j → ¬ P x) ⊎ ∃ \(i : ∃ P) → proj₁ i < proj₁ j × (∀ {x} → proj₁ i < x → x < proj₁ j → ¬ P x) precedent _ (zero , _) = inj₁ \() precedent dp (suc j , tj) = aux dp j (suc j) tj (n<1+n _) λ j<x → ⊥-elim ∘ (<-irrefl {suc j} refl) ∘ (<-transʳ j<x) where aux : ∀ {ℓ} {P : Pred ℕ ℓ} (dp : Decidable P) (i j : ℕ) (pc : P j) (i<j : i < j) → (∀ {x} → i < x → x < j → ¬ P x) → (∀ {x} → x < j → ¬ P x) ⊎ ∃ \(k : ∃ P) → proj₁ k < j × (∀ {x} → proj₁ k < x → x < j → ¬ P x) aux dp i j pc i≺j p with dp i aux dp zero j pc i≺j p | no ¬p = inj₁ λ { {zero} x<j tx → ⊥-elim (¬p tx) ; {suc _} x<j tx → p (s≤s z≤n) x<j tx} aux dp (suc i) j pc i≺j p | no ¬p = aux dp i j pc (<-trans (n<1+n i) i≺j) λ i<x x<j tx → case m≤n⇒m<n∨m≡n i<x of λ {(inj₁ si<x) → p si<x x<j tx ; (inj₂ refl) → ¬p tx} aux dp i j pc i≺j p | yes p₁ = inj₂ ((i , p₁) , i≺j , p) wf-<P : ∀ {ℓ} {P : Pred ℕ ℓ} → Decidable P → WellFounded {A = ∃ P} (_<_ on proj₁) wf-<P {P = P} dec x = aux x (<-wellFounded (proj₁ x)) where aux : ∀ (i : ∃ P) → Acc _<_ (proj₁ i) → Acc (_<_ on proj₁) i aux i ai with precedent dec i aux i ai | inj₁ p = acc (λ j j≺i → ⊥-elim (p j≺i (proj₂ j))) aux i (acc q) | inj₂ (j , j≺i , p) with aux j (q _ j≺i) aux i ai | inj₂ (j , j≺i , p) | acc rs = acc λ y y≺i → case <-cmp (proj₁ j) (proj₁ y) of λ { (tri< a _ _) → ⊥-elim ((p a y≺i) (proj₂ y)) ; (tri≈ _ refl _) → acc rs ; (tri> _ _ c) → rs y c} initial : ∀ {ℓ} {P : Pred ℕ ℓ} → Decidable P → ∃ P → ∃ λ (x : ∃ P) → ∀ (y : ∃ P) → proj₁ x ≤ proj₁ y initial {P = P} dec p = aux p (<-wellFounded _) where aux : (i : ∃ P) → Acc _<_ (proj₁ i) → ∃ λ (x : ∃ P) → ∀ (y : ∃ P) → proj₁ x ≤ proj₁ y aux i (acc p) with precedent dec i aux i (acc p) | inj₁ x = i , λ y → case <-cmp (proj₁ i) (proj₁ y) of λ { (tri< a _ _) → <⇒≤ a ; (tri≈ _ refl _) → ≤-refl ; (tri> _ _ c) → ⊥-elim (x c (proj₂ y))} aux i (acc p) | inj₂ (y , z , _) = aux y (p _ z) open import CCSL (record { isStrictPartialOrder = <-isStrictPartialOrder }) open Clock record Clock-¬∅-Dec : Set₁ where field clock : Clock non-empty : ∃ (Ticks clock) decidable : Decidable (Ticks clock) wf-≺ : _ wf-≺ = wf-<P decidable birth : _ birth = let (i , p) = initial decidable non-empty in i , swap⊎ ∘ m≤n⇒m<n∨m≡n ∘ p toWf : WFClock toWf = record { clock = clock ; wf-≺ = wf-≺ } toIn : InitialClock toIn = record { clock = clock ; first = birth }