[Agda] --without-K option too restrictive?

[Dmytro Starosud]

Hello Andrés/Everybody

What does the K-rule mean?
I cannot find any articles related to it in the internet.

Thanks,
Dmytro

2013/5/29 Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>:
> Hi,
>
> As far as I understand, the --without-K option rejects the K-rule which
> cannot be proved using subst. Given
>
> open import Data.List
> open import Data.Nat
> open import Data.Product
> open import Relation.Binary.PropositionalEquality
>
> open import Relation.Binary
> module NDTO = DecTotalOrder decTotalOrder
>
> P : {A : Set} → List A → List A → Set
> P xs ys = ∃ (λ x → ys ≡ x ∷ xs)
>
> Q : {A : Set} → List A → List A → Set
> Q xs ys = (length xs) < (length ys)
>
> helper : {A : Set}(y : A)(xs : List A) → (length xs) < (length (y ∷ xs))
> helper y []       = s≤s z≤n
> helper y (x ∷ xs) = s≤s NDTO.refl
>
> Why the --without-K option rejects the following proof
>
> foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
> foo xs .(x ∷ xs) (x , refl) = helper x xs
>
> if I can prove foo using only subst
>
> foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
> foo' xs ys (x , h) =
>   subst (λ ys' → length xs < length ys') (sym h) (helper x xs)
>
> ?
>
> Thanks,
>
> --
> Andrés
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda