[Agda] pattern match for LessThan'?

[Martin Stone Davis]

We know that if m≢n : m ≡ n → ⊥, then the ≤′-refl case is impossible, but
Agda doesn't know this. However, Agda does know that, in the ≤′-refl case,
m ≡ n. So, if you have m≢n, then on the rhs of a clause containing ≤′-refl,
you can write something like ⊥-elim (m≢n refl).

--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com

On Mon, Feb 1, 2016 at 7:55 PM, Kenichi Asai <asai at is.ocha.ac.jp> wrote:

> In the standard library, we have:
>
> data _≤′_ (m : ℕ) : ℕ → Set where
>   ≤′-refl :                         m ≤′ m
>   ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
>
> Suppose we have a value:
>
> v : m ≤′ n
>
> for some m and n.  From the definition of the type, we see that there
> must be only one choice for v: if m = n, then v must be refl, while if
> m < n, then v must be step.  (And if m > n, v must be ().)
>
> Thus, I want to refine v according to m and n.  Can I do that?  Or in
> more general, can I write an inversion function that deconstructs v?
> If I case split on v, I always obtain the both possibilities and I
> don't see any way to remove the impossible case.
>
> For "less than" without prime:
>
> data _≤_ : Rel ℕ Level.zero where
>   z≤n : ∀ {n}                 → zero  ≤ n
>   s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
>
> we can simply case split on the value of this type, because the type
> uniquely and evidently shows which constructor to take.  I want to do
> the same (or similar) thing for "less than" with prime.
>
> Sincerely,
>
> --
> Kenichi Asai
> _______________________________________________
> 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/20160202/0abacfc7/attachment.html