<div dir="ltr">The K-rule is Streicher's axiom K. A brief google search for "axiom K" gives me <a href="http://ncatlab.org/nlab/show/axiom+K">http://ncatlab.org/nlab/show/axiom+K</a> and <a href="http://adam.chlipala.net/cpdt/html/Equality.html">http://adam.chlipala.net/cpdt/html/Equality.html</a>.<div>
<br></div><div>-Jason</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, May 29, 2013 at 2:20 PM, Dmytro Starosud <span dir="ltr"><<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Andrés/Everybody<br>
<br>
What does the K-rule mean?<br>
I cannot find any articles related to it in the internet.<br>
<br>
Thanks,<br>
Dmytro<br>
<br>
2013/5/29 Andrés Sicard-Ramírez <<a href="mailto:andres.sicard.ramirez@gmail.com">andres.sicard.ramirez@gmail.com</a>>:<br>
<div class="HOEnZb"><div class="h5">> Hi,<br>
><br>
> As far as I understand, the --without-K option rejects the K-rule which<br>
> cannot be proved using subst. Given<br>
><br>
> open import Data.List<br>
> open import Data.Nat<br>
> open import Data.Product<br>
> open import Relation.Binary.PropositionalEquality<br>
><br>
> open import Relation.Binary<br>
> module NDTO = DecTotalOrder decTotalOrder<br>
><br>
> P : {A : Set} → List A → List A → Set<br>
> P xs ys = ∃ (λ x → ys ≡ x ∷ xs)<br>
><br>
> Q : {A : Set} → List A → List A → Set<br>
> Q xs ys = (length xs) < (length ys)<br>
><br>
> helper : {A : Set}(y : A)(xs : List A) → (length xs) < (length (y ∷ xs))<br>
> helper y [] = s≤s z≤n<br>
> helper y (x ∷ xs) = s≤s NDTO.refl<br>
><br>
> Why the --without-K option rejects the following proof<br>
><br>
> foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys<br>
> foo xs .(x ∷ xs) (x , refl) = helper x xs<br>
><br>
> if I can prove foo using only subst<br>
><br>
> foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys<br>
> foo' xs ys (x , h) =<br>
> subst (λ ys' → length xs < length ys') (sym h) (helper x xs)<br>
><br>
> ?<br>
><br>
> Thanks,<br>
><br>
> --<br>
> Andrés<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>