Unsound and incomplete alecsferra.github.io
![theorem DefEq.inv_aux' : Γ ⊢ t₁ ≡ t₂ ∶ τ
→ PiInv Γ t₁ ∧ IdInv Γ t₁ ∧ PiInv Γ t₂ ∧ IdInv Γ t₂
| .u .. | .var .. | .lam .. | .app .. | .refl .. | .j .. => by
repeat constructor <;> simp [PiInv, IdInv]](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aj2jbvnkyjec77ksuvou5kce/bafkreiacmrailucp6xtoydxwthbjjdmapwawupupkcc42j6dhja6wz3vre)
![src:
data False : 𝟙
=
in data Bool : 𝟙
= true : Bool ⋆
| false : Bool ⋆
in let not = [ λ x . case x as _ in Bool ⋆ of
| Bool.true -> Bool.false
| Bool.false -> Bool.true : Bool ⋆ -> Bool ⋆ ]
in data BoolPair : 𝟙
= mkPair : Bool ⋆ -> Bool ⋆ -> BoolPair ⋆
in data BoolEq : BoolPair ⋆
= refl : (b : Bool ⋆) -> BoolEq (BoolPair.mkPair b b)
in let trueIsNotFalse = [
λ pf . case pf as _ in False ⋆ of
: BoolEq (BoolPair.mkPair Bool.true Bool.false) -> False ⋆ ]
output:
Type checking test.tc
Type checking succeeded!](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aj2jbvnkyjec77ksuvou5kce/bafkreie6xc7el77332izfvy75diiaisedsdjfpwlbxlv4v5qt5pvmbifau)
![{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
module TuringTest where
import Language.Haskell.Liquid.ProofCombinators
{-@ measure length' @-}
{-@ length' :: [a] -> Nat @-}
length' :: [a] -> Int
length' [] = 0
length' (x:xs) = 1 + length' xs
{-@ reflect take' @-}
{-@ take' :: n:Nat -> { xs:[a] | length' xs >= n } -> { xs:[a] | length' xs = n } @-}
take' :: Int -> [a] -> [a]
take' 0 xs = []
take' n (x:xs) = x : take' (n - 1) xs
{-@ reflect drop' @-}
{-@ drop' :: n:Nat -> { xs:[a] | length' xs >= n } -> { ys:[a] | length' ys = length' xs -n } @-}
drop' :: Int -> [a] -> [a]
drop' 0 xs = xs
drop' n (x:xs) = drop' (n - 1) xs
{-@ reflect concat' @-}
concat' :: [a] -> [a] -> [a]
concat' [] ys = ys
concat' (x:xs) ys = x : concat' xs ys
{-@ reflect rotate @-}
{-@ rotate :: n:Nat -> { xs:[a] | length' xs >= n } -> [a] @-}
rotate :: Int -> [a] -> [a]
rotate n xs = concat' (drop' (length' xs - n) xs) (take' (length' xs - n) xs)
{-@ reflect lookup' @-}
{-@ lookup' :: n:Nat -> { xs:[a] | length' xs > n } -> a @-}
lookup' :: Int -> [a] -> a
lookup' 0 (x:xs) = x
lookup' n (x:xs) = lookup' (n - 1) xs
{-@ rotateCorrect :: o:Nat -> i:Nat -> { xs:[a] | i < length' xs && o <= length' xs }
-> { lookup' i xs = lookup' (i + o mod length' xs) (rotate o xs) } @-}
rotateCorrect :: Int -> Int -> [a] -> Proof
rotateCorrect = undefined](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aj2jbvnkyjec77ksuvou5kce/bafkreifemeor5hudb4yq2fwg2gffgbsuxehb5cggyudcx2hv6upccjgcni)
![{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
module TuringTest where
import Language.Haskell.Liquid.ProofCombinators
{-@ measure length' @-}
{-@ length' :: [a] -> Nat @-}
length' :: [a] -> Int
length' [] = 0
length' (x:xs) = 1 + length' xs
{-@ reflect take' @-}
{-@ take' :: n:Nat -> { xs:[a] | length' xs >= n } -> { xs:[a] | length' xs = n } @-}
take' :: Int -> [a] -> [a]
take' 0 xs = []
take' n (x:xs) = x : take' (n - 1) xs
{-@ reflect drop' @-}
{-@ drop' :: n:Nat -> { xs:[a] | length' xs >= n } -> { ys:[a] | length' ys = length' xs -n } @-}
drop' :: Int -> [a] -> [a]
drop' 0 xs = xs
drop' n (x:xs) = drop' (n - 1) xs
{-@ reflect concat' @-}
concat' :: [a] -> [a] -> [a]
concat' [] ys = ys
concat' (x:xs) ys = x : concat' xs ys
{-@ reflect rotate @-}
{-@ rotate :: n:Nat -> { xs:[a] | length' xs >= n } -> [a] @-}
rotate :: Int -> [a] -> [a]
rotate n xs = concat' (drop' (length' xs - n) xs) (take' (length' xs - n) xs)
{-@ reflect lookup' @-}
{-@ lookup' :: n:Nat -> { xs:[a] | length' xs > n } -> a @-}
lookup' :: Int -> [a] -> a
lookup' 0 (x:xs) = x
lookup' n (x:xs) = lookup' (n - 1) xs
{-@ rotateCorrect :: o:Nat -> i:Nat -> { xs:[a] | i < length' xs && o <= length' xs }
-> { lookup' i xs = lookup' (i + o mod length' xs) (rotate o xs) } @-}
rotateCorrect :: Int -> Int -> [a] -> Proof
rotateCorrect = undefined](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aj2jbvnkyjec77ksuvou5kce/bafkreigfpftybs6zuckmed3xpezvm7wycuf5k7swjzdfloior26m24ibzy)
Unsound and incomplete alecsferra.github.io