在伊德里斯，我如何從一個類型中提取證據？

如果我有一個So的類型，比如So (x < y)，通過創造的東西像在伊德里斯，我如何從一個類型中提取證據？

IsLt : Ord a => (x: a) -> (y: a) -> Type 
IsLt x y = So (x < y)

我怎樣才能提取(x < y)證明了這件事？我無法在標準庫中找到此功能。

So在標準庫中定義爲：

data So : Bool -> Type where 
    Oh : So True

而且我不知道如何從提取的證據，用於在證明這樣的：

ltNeNat : {x: Nat} -> {y: Nat} -> So (x < y) -> Not (x = y)

來源

2017-07-02 LogicChains

您可以通過感應上x證明引理：

ltNeNat : {x: Nat} -> {y: Nat} -> So (lt x y) -> Not (x = y) 
ltNeNat {x = Z} {y = Z} Oh _ impossible 
ltNeNat {x = Z} {y = S _} _ Refl impossible 
ltNeNat {x = S x} {y = Z} so Refl impossible 
ltNeNat {x = S x} {y = S y} so eq = 
    let IH = ltNeNat {x} {y} so in 
    IH $ succInjective _ _ eq

我有lt更換<否則伊德里斯看不出So (S x < S y)和So (x < y)是definitionally相等。

注意到我在第一個和最後一個條款中使用了編碼在So中的信息。

來源

2017-07-03 09:40:07

的確如此。我被證明'S x ~~x Shersh~~

+1

你需要「反映」布爾變成命題。（Coq生態系統）的ssreflect廣泛使用它。這樣你就可以使用邏輯和計算 - 這在處理可決定的命題時非常有用。 –

3

似乎就像你不能從布爾值中提取證據一樣。 So是弱類型。它應該僅用於保證在運行時進行一些檢查的性能。也看到了這個問題：

So: what's the point?

我不知道這是不可能的。但我試圖證明ltNeNat並慘敗。雖然，也許我只是愚蠢的。考慮使用一些證據而不是So，如Refl。 So上的模式匹配不會爲您提供更多幫助證明事物的力量。您可以在this tutorial下找到So的有效用例。即使您能夠從So中提取證據，它也需要您提供大量代碼，處理So不太方便。

來源

2017-07-02 21:50:30 Shersh

在伊德里斯，我如何從一個類型中提取證據？

回答

相關問題