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

[Jason Gross]

The K-rule is Streicher's axiom K.  A brief google search for "axiom K"
gives me http://ncatlab.org/nlab/show/axiom+K and
http://adam.chlipala.net/cpdt/html/Equality.html.

-Jason


On Wed, May 29, 2013 at 2:20 PM, Dmytro Starosud <d.starosud at gmail.com>wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130529/0c080722/attachment.html